printf.idr

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