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
53
54
55
56
57
58
59
60
61
62
63
|
module Total.Encoded.Test
import Total.NormalForm
import Total.Pretty
import Total.Encoded.Util
namespace List
ListC : Container
ListC = (Unit, 0) ::: [(N, 1)]
export
List : Ty
List = fix ListC
export
nil : FullTerm List [<]
nil = app (intro {c = ListC} Here) (app' pair [<arb, Pair.nil])
export
cons : FullTerm (N ~> List ~> List) [<]
cons = abs' (S $ S Z)
(\t, ts =>
app (lift $ intro {c = ListC} $ There Here)
(app' (lift pair)
[<t
, app' (lift Pair.cons) [<ts, lift Pair.nil]
]))
export
fold : {ty : Ty} -> FullTerm ((N ~> ty ~> ty) ~> ty ~> List ~> ty) [<]
fold = abs' (S $ S Z)
(\f, z => elim
[ abs (drop z)
, abs' (S Z) (\p =>
app' (drop f)
[<app (lift $ fst {u = Vect 1 ty}) p
, app (lift (index {n = 1} FZ . snd {t = N})) p
])
])
MkList : List Nat -> FullTerm List [<]
MkList = foldr (\n, ts => app' cons [<lit n, ts]) nil
sum : FullTerm (List ~> N) [<]
sum = app' fold [<add, zero]
ten : FullTerm N [<]
ten = (app sum (MkList [1,2,3,4]))
tenNf : Term [<] N
tenNf = toTerm (normalize ten).term
main : IO Builtin.Unit
main = do
let
cases =
[(lit 1, id)
,(lit 3, abs' (S Z) (\n => app' (lift add) [<n, n]))
,(lit 2, abs' (S Z) (\n => app (lift pred) n))]
let t : FullTerm (N ~> N) [<] = cond cases
-- let t : FullTerm N [<] = app sum (MkList [1,2,3,4])
putDoc (group $ Doc.pretty "Input:" <+> line <+> pretty (toTerm t))
putDoc (group $ Doc.pretty "Normal Form:" <+> line <+> pretty (toTerm (normalize t).term))
|
