blob: 5a134a210407f77f47d280a00fc76cf2460c5336 (
plain)
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
module Term.Syntax
import public Data.SnocList
import public Term
%prefix_record_projections off
-- Combinators
export
Id : Term (ty ~> ty) ctx
Id = Abs (Var Here)
export
Zero : Term N ctx
Zero = Op (Lit 0)
export
Suc : Term N ctx -> Term N ctx
Suc t = App (Op Suc) t
export
Num (Term N ctx) where
t + u = App (App (Op Plus) t) u
t * u = App (App (Op Mult) t) u
fromInteger = Op . Lit . fromInteger
export
pred : Term N ctx -> Term N ctx
pred t = App (Op Pred) t
export
minus : Term N ctx -> Term N ctx -> Term N ctx
t `minus` u = App (App (Op Minus) t) u
export
div : Term N ctx -> Term N ctx -> Term N ctx
t `div` u = App (App (Op Div) t) u
export
mod : Term N ctx -> Term N ctx -> Term N ctx
t `mod` u = App (App (Op Mod) t) u
export
Arb : {ty : Ty} -> Term ty ctx
Arb {ty = N} = Op (Lit 0)
Arb {ty = ty ~> ty'} = Const Arb
export
inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
inL = Op (Inl ty1 ty2)
export
inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
inR = Op (Inr ty1 ty2)
export
prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
prL = Op (Prl ty1 ty2)
export
prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
prR = Op (Prr ty1 ty2)
-- HOAS
infixr 4 ~>*
public export
(~>*) : SnocList Ty -> Ty -> Ty
sty ~>* ty = foldr (~>) ty sty
export
Abs' : (Term ty (ctx :< ty) -> Term ty' (ctx :< ty)) -> Term (ty ~> ty') ctx
Abs' f = Abs (f $ Var Here)
export
App : {sty : SnocList Ty} -> Term (sty ~>* ty) ctx -> All (flip Term ctx) sty -> Term ty ctx
App t [<] = t
App t (us :< u) = App (App t us) u
export
AbsAll :
(sty : SnocList Ty) ->
(All (flip Term (ctx ++ sty)) sty -> Term ty (ctx ++ sty)) ->
Term (sty ~>* ty) ctx
AbsAll [<] f = f [<]
AbsAll (sty :< ty') f = AbsAll sty (\vars => Abs' (\x => f (mapProperty shift vars :< x)))
export
(.) : {ty, ty' : Ty} -> Term (ty' ~> ty'') ctx -> Term (ty ~> ty') ctx -> Term (ty ~> ty'') ctx
t . u = Abs (App (shift t) [<App (shift u) [<Var Here]])
export
(.:) :
{sty : SnocList Ty} ->
{ty : Ty} ->
Term (ty ~> ty') ctx ->
Term (sty ~>* ty) ctx ->
Term (sty ~>* ty') ctx
(t .: u) {sty = [<]} = App t u
(t .: u) {sty = sty :< ty''} = Abs' (\f => shift t . f) .: u
|
