Skip to content

Instantly share code, notes, and snippets.

@puffnfresh
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) ""
@puffnfresh
Copy link
Author

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