Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
data Format = Number Format
| Str Format
| Lit Char Format
| End
%name Format fmt
PrintfType : Format -> Type
PrintfType (Number fmt) = Int -> PrintfType fmt
PrintfType (Str fmt) = String -> PrintfType fmt
PrintfType (Lit x fmt) = PrintfType fmt
PrintfType End = String
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 's' :: xs) = Str (toFormat xs)
toFormat ('%' :: 'd' :: xs) = Number (toFormat xs)
toFormat (x :: xs) = Lit x (toFormat xs)
printf : (str : String) -> PrintfType (toFormat (unpack str))
printf str = printfFmt _ ""
where
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \s => printfFmt fmt (acc ++ s)
printfFmt (Lit x fmt) acc = printfFmt fmt (acc ++ (singleton x))
printfFmt End acc = acc
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.