This repository has been archived by the owner on May 18, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 33
/
Printf.agda
51 lines (42 loc) · 1.83 KB
/
Printf.agda
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
module Printf where
open import Data.List hiding(_++_)
open import Data.String
open import Data.Unit
open import Data.Empty
open import Data.Char
open import Data.Product
open import Data.Nat.Show renaming (show to showNat)
open import Data.Nat
open import Function using (_∘_)
data ValidFormat : Set₁ where
argument : (A : Set) → (A → String) → ValidFormat
literal : Char → ValidFormat
data Format : Set₁ where
valid : List ValidFormat → Format
invalid : Format
parse : String → Format
parse s = parse′ [] (toList s)
where
parse′ : List ValidFormat → List Char → Format
parse′ l ('%' ∷ 's' ∷ fmt) = parse′ (argument String (λ x → x) ∷ l) fmt
parse′ l ('%' ∷ 'c' ∷ fmt) = parse′ (argument Char (λ x → fromList [ x ]) ∷ l) fmt
parse′ l ('%' ∷ 'd' ∷ fmt) = parse′ (argument ℕ showNat ∷ l) fmt
parse′ l ('%' ∷ '%' ∷ fmt) = parse′ (literal '%' ∷ l) fmt
parse′ l ('%' ∷ c ∷ fmt) = invalid
parse′ l (c ∷ fmt) = parse′ (literal c ∷ l) fmt
parse′ l [] = valid (reverse l)
Args : Format → Set
Args invalid = ⊥ → String
Args (valid (argument t _ ∷ r)) = t → (Args (valid r))
Args (valid (literal _ ∷ r)) = Args (valid r)
Args (valid []) = String
FormatArgs : String → Set
FormatArgs f = Args (parse f)
sprintf : (f : String) → FormatArgs f
sprintf = sprintf′ "" ∘ parse
where
sprintf′ : String → (f : Format) → Args f
sprintf′ accum invalid = λ t → ""
sprintf′ accum (valid []) = accum
sprintf′ accum (valid (argument _ s ∷ l)) = λ t → (sprintf′ (accum ++ s t) (valid l))
sprintf′ accum (valid (literal c ∷ l)) = sprintf′ (accum ++ fromList [ c ]) (valid l)