module Printf | |
%default total | |
data Format = FInt Format -- %d | |
| FString Format -- %s | |
| FOther Char Format -- [a-zA-Z0-9] | |
| FEnd -- | |
format : List Char -> Format | |
format ('%'::'d'::cs) = FInt (format cs) | |
format ('%'::'s'::cs) = FString (format cs) | |
format (c::cs) = FOther c (format cs) | |
format [] = FEnd | |
interpFormat : Format -> Type | |
interpFormat (FInt f) = Int -> interpFormat f | |
interpFormat (FString f) = String -> interpFormat f | |
interpFormat (FOther _ f) = interpFormat f | |
interpFormat FEnd = String | |
formatString : String -> Format | |
formatString s = format (unpack s) | |
toFunction : (fmt : Format) -> String -> interpFormat fmt | |
toFunction (FInt f) a = \i => toFunction f (a ++ show i) | |
toFunction (FString f) a = \s => toFunction f (a ++ s) | |
toFunction (FOther c f) a = toFunction f (a ++ singleton c) | |
toFunction FEnd a = a | |
printf : (s : String) -> interpFormat (formatString s) | |
printf s = toFunction (formatString s) "" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This comment has been minimized.
See https://gist.github.com/puffnfresh/6e8f551ea61c5c83b409394760186074 for an example on how to use this function with runtime strings.