Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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) ""
Owner

puffnfresh commented Oct 14, 2016

See https://gist.github.com/puffnfresh/6e8f551ea61c5c83b409394760186074 for an example on how to use this function with runtime strings.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment