-
Notifications
You must be signed in to change notification settings - Fork 0
/
Printf.idr
46 lines (42 loc) · 1.63 KB
/
Printf.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
||| Representing format string as data type
||| "%s=%d" is equal to Str (Lit "=" (Number End))
private
data Format = Number Format
| Str Format
| Chr Format
| Dbl Format
| Lit String Format
| End
%name Format fmt
private
PrintfType : Format -> Type
PrintfType (Number fmt) = (i: Int) -> PrintfType fmt
PrintfType (Str fmt) = (s: String) -> PrintfType fmt
PrintfType (Chr fmt) = (c: Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (d: Double) -> PrintfType fmt
PrintfType (Lit lit fmt) = PrintfType fmt
PrintfType End = String
private
toFormat : (xs: List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number $ toFormat chars
toFormat ('%' :: 's' :: chars) = Str $ toFormat chars
toFormat ('%' :: 'c' :: chars) = Chr $ toFormat chars
toFormat ('%' :: 'f' :: chars) = Dbl $ toFormat chars
toFormat ('%' :: chars) = Lit "%" $ toFormat chars
toFormat (c :: chars) = case toFormat chars of
(Lit lit chars') => Lit (strCons c lit) chars'
fmt => Lit (strCons c "") fmt
private
printFmt : (fmt: Format) -> (acc: String) -> PrintfType fmt
printFmt (Number fmt) acc = \i => printFmt fmt $ acc ++ show i
printFmt (Str fmt) acc = \s => printFmt fmt $ acc ++ s
printFmt (Chr fmt) acc = \c => printFmt fmt $ strCons c acc
printFmt (Dbl fmt) acc = \d => printFmt fmt $ acc ++ show d
printFmt (Lit lit fmt) acc = printFmt fmt $ acc ++ lit
printFmt End acc = acc
||| Type-safe printf function.
||| Numbers and types of arguments depend on format string.
public
printf : (fmt: String) -> PrintfType $ toFormat $ unpack fmt
printf fmt = printFmt _ ""