Skip to content

Instantly share code, notes, and snippets.

Created April 23, 2014 04:21
  • Star 28 You must be signed in to star a gist
  • Fork 3 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save puffnfresh/11202637 to your computer and use it in GitHub Desktop.
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) ""
Copy link

See 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