Create a gist now

Instantly share code, notes, and snippets.

Embed
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) ""
@puffnfresh

This comment has been minimized.

Show comment
Hide comment
@puffnfresh

puffnfresh Oct 14, 2016

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

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