Created
March 14, 2019 12:12
-
-
Save 553224019/21f410c1b9a1ad619ad5998773afb458 to your computer and use it in GitHub Desktop.
A Simple Implementation of Type-Safe Printf in Idris
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module SafePrintf | |
| data Format = | |
| FNum Format | |
| | FStr Format | |
| | Lit String Format | |
| | End | |
| -- String to Format | |
| toFormat : List Char -> Format | |
| toFormat [] = End | |
| toFormat ('%' :: 'd' :: chars) = FNum (toFormat chars) | |
| toFormat ('%' :: 's' :: chars) = FStr (toFormat chars) | |
| toFormat ('%' :: chars) = Lit "%" (toFormat chars) | |
| toFormat ( c :: chars) = case toFormat chars of | |
| Lit lit chars' => Lit (c `strCons` lit) chars' | |
| fmt => Lit (c `strCons` "") fmt | |
| -- Format to Type | |
| PrintfType : Format -> Type | |
| PrintfType (FNum fmt) = Int -> PrintfType fmt | |
| PrintfType (FStr fmt) = String -> PrintfType fmt | |
| PrintfType (Lit str fmt) = PrintfType fmt | |
| PrintfType End = String | |
| -- Raw Printf | |
| printfFmt : (fmt : Format) -> String -> PrintfType fmt | |
| printfFmt (FNum fmt) acc = \i => printfFmt fmt (acc ++ show i) | |
| printfFmt (FStr fmt) acc = \str => printfFmt fmt (acc ++ str) | |
| printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit) | |
| printfFmt End acc = acc | |
| -- True Printf | |
| printf : (fmt : String) -> PrintfType (toFormat (unpack fmt)) | |
| printf fmt = printfFmt _ "" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment