-
Notifications
You must be signed in to change notification settings - Fork 0
/
Sprintf.idr
53 lines (45 loc) · 1.8 KB
/
Sprintf.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
47
48
49
50
51
52
-- https://www.codewars.com/kata/5c7fe5c859036f142eccaabb
module Sprintf
%access public export
%default total
data Printf = PPercent
| PInteger
| PDouble
| PChar
| PReg Char
-- NOTE: other specifiers such as %s are considered
-- normal characters and will be treated as-is
toPrintf : List Char -> List Printf
toPrintf [] = []
toPrintf ('%' :: 'd' :: xs) = PInteger :: toPrintf xs
toPrintf ('%' :: 'f' :: xs) = PDouble :: toPrintf xs
toPrintf ('%' :: 'c' :: xs) = PChar :: toPrintf xs
toPrintf ('%' :: '%' :: xs) = PPercent :: toPrintf xs
toPrintf (x :: xs) = PReg x :: toPrintf xs
-- deduce type of args passed to printf
corresArgs : List Printf -> List Type
corresArgs [] = []
corresArgs (PPercent :: xs) = corresArgs xs
corresArgs (PInteger :: xs) = Integer :: corresArgs xs
corresArgs (PDouble :: xs) = Double :: corresArgs xs
corresArgs (PChar :: xs) = Char :: corresArgs xs
corresArgs (PReg x :: xs) = corresArgs xs
-- convert a list of types to printf function type
-- example: [Int, Double, Char] -> (Int -> Double -> Char -> List Char)
-- [] -> (List Char) -- no args
typeListToFunc : Type -> List Type -> Type
typeListToFunc ending lst = case lst of
[] => ending
(x :: xs) => x -> typeListToFunc ending xs
fmt : (acc: String)
-> (p: List Printf)
-> typeListToFunc String (corresArgs p)
fmt acc [] = acc
fmt acc (PPercent :: ps) = fmt (acc ++ "%") ps
fmt acc (PInteger :: ps) = \i => fmt (acc ++ show i) ps
fmt acc (PDouble :: ps) = \d => fmt (acc ++ show d) ps
fmt acc (PChar :: ps) = \c => fmt (acc ++ pack [c]) ps
fmt acc (PReg x :: ps) = fmt (acc ++ pack [x]) ps
sprintf : (s: String)
-> typeListToFunc String (corresArgs (toPrintf (unpack s)))
sprintf s = fmt "" (toPrintf (unpack s))