Instantly share code, notes, and snippets.

Embed
What would you like to do?
Type-safe printf in Idris including a practical run-time validation example -- https://zgcoder.net/ramblings/typesafe-printf.html
%default total
Prefix : Type
Prefix = String
data Format = Number Prefix Format | Str Prefix Format | End Prefix
parse : List Char -> String -> Format
parse [] prefix_acc = End prefix_acc
parse ('%' :: 'd' :: xs) prefix_acc = Number prefix_acc (parse xs "")
parse ('%' :: 's' :: xs) prefix_acc = Str prefix_acc (parse xs "")
parse (x :: xs) prefix_acc = parse xs (prefix_acc ++ strCons x "")
parseFormat : String -> Format
parseFormat xs = parse (unpack xs) ""
PrintfType : Format -> Type
PrintfType (Number _ format) = Int -> PrintfType format
PrintfType (Str _ format) = String -> PrintfType format
PrintfType (End _) = String
printfFormat : (format : Format) -> String -> PrintfType format
printfFormat (Number prefix' format) acc =
\num => printfFormat format (acc ++ prefix' ++ show num)
printfFormat (Str prefix' format) acc =
\str => printfFormat format (acc ++ prefix' ++ str)
printfFormat (End prefix') acc = acc ++ prefix'
printfFormatter : (format : Format) -> PrintfType format
printfFormatter format = printfFormat format ""
printf : (str : String) -> PrintfType (parseFormat str)
printf str = printfFormatter (parseFormat str)
formatSingleNumber : String -> Maybe String
formatSingleNumber str =
let format = parseFormat str in
case format of
numberFormat@(Number _ (End _)) =>
Just (printfFormatter numberFormat 999)
_ => Nothing
main : IO ()
main = do
putStrLn "Translate in your language of choice:"
putStrLn "I have %d ponies"
translation <- getLine
case formatSingleNumber translation of
Nothing => putStrLn "Invalid response!"
(Just result) => putStrLn result
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment