Skip to content

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) ""

This comment has been minimized.

Copy link
Owner Author

@puffnfresh puffnfresh commented Oct 14, 2016

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
You can’t perform that action at this time.