-
Notifications
You must be signed in to change notification settings - Fork 0
/
Term.hs
142 lines (128 loc) · 4.34 KB
/
Term.hs
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
module Term where
data Level =
LevelN Int
| LevelW
| LevelAfterW
deriving (Show, Eq, Ord)
data Term =
Lam Term
| App Term Term
| Var Int
| Abort IrrelTerm
| Zero
| Succ Term
| NatRec Term Term Term Term
| AddProof Term Term IrrelTerm
| UseProof Term Term Term Term Term
| Pair Term Term
| Proj1 Term
| Proj2 Term
| Squeeze IrrelTerm
| GetProof Term Term
| UseSquash Term Term Term
| Pi Term Term
| Bottom
| Top
| Nat
| Refine Term Term
| Sigma Term Term
| Squash Term
| Sort Level
| Substed Subst Term
deriving (Show, Eq)
newtype IrrelTerm = Irrel Term
deriving Show
instance Eq IrrelTerm where
a == b = True
data Subst =
IdS
| CompS Subst Subst
| WeakenS Int
| ExtendS Subst Term
deriving (Show, Eq)
weaken1 :: Subst
weaken1 = WeakenS 1
sortN :: Int -> Term
sortN = Sort . LevelN
star :: Term
star = sortN 0
box :: Term
box = sortN 1
fun :: Term -> Term -> Term
fun a b = Pi a $ Substed weaken1 b
bindingSubst :: Term -> Subst
bindingSubst = ExtendS IdS
delaySubst :: Subst -> Subst
delaySubst s = ExtendS (CompS weaken1 s) (Var 0)
bubbleSubsts :: Term -> Term
bubbleSubsts (Lam x) = Lam (bubbleSubsts x)
bubbleSubsts (App x y) = App (bubbleSubsts x) (bubbleSubsts y)
bubbleSubsts (Var n) = Var n
bubbleSubsts (Abort (Irrel x)) = Abort $ Irrel $ bubbleSubsts x
bubbleSubsts (Zero) = Zero
bubbleSubsts (Succ x) = Succ (bubbleSubsts x)
bubbleSubsts (NatRec t x y n) =
NatRec (bubbleSubsts t) (bubbleSubsts x) (bubbleSubsts y) (bubbleSubsts n)
bubbleSubsts (AddProof x t (Irrel p)) =
AddProof (bubbleSubsts x) (bubbleSubsts t) (Irrel $ bubbleSubsts p)
bubbleSubsts (UseProof tx tp x ty y) =
UseProof (bubbleSubsts tx) (bubbleSubsts tp) (bubbleSubsts x)
(bubbleSubsts ty) (bubbleSubsts y)
bubbleSubsts (Pair a b) = Pair (bubbleSubsts a) (bubbleSubsts b)
bubbleSubsts (Proj1 p) = Proj1 $ bubbleSubsts p
bubbleSubsts (Proj2 p) = Proj2 $ bubbleSubsts p
bubbleSubsts (Squeeze (Irrel p)) = Squeeze $ Irrel $ bubbleSubsts p
bubbleSubsts (GetProof tp x) = GetProof (bubbleSubsts tp) (bubbleSubsts x)
bubbleSubsts (UseSquash p ty y) =
UseSquash (bubbleSubsts p) (bubbleSubsts ty) (bubbleSubsts y)
bubbleSubsts (Pi x y) = Pi (bubbleSubsts x) (bubbleSubsts y)
bubbleSubsts (Top) = Top
bubbleSubsts (Bottom) = Bottom
bubbleSubsts (Nat) = Nat
bubbleSubsts (Refine x p) = Refine (bubbleSubsts x) (bubbleSubsts p)
bubbleSubsts (Sigma x y) = Sigma (bubbleSubsts x) (bubbleSubsts y)
bubbleSubsts (Squash x) = Squash $ bubbleSubsts x
bubbleSubsts (Sort k) = Sort k
bubbleSubsts (Substed s x) = substTerm s (bubbleSubsts x)
substTerm :: Subst -> Term -> Term
substTerm s (Lam x) = Lam $ substTerm (delaySubst s) x
substTerm s (App x y) = App (substTerm s x) (substTerm s y)
substTerm s (Abort (Irrel x)) = Abort $ Irrel $ substTerm s x
substTerm s (Zero) = Zero
substTerm s (Succ x) = Succ (substTerm s x)
substTerm s (NatRec t x y n) =
NatRec (substTerm s t) (substTerm s x) (substTerm s' y) (substTerm s n)
where s' = delaySubst $ delaySubst s
substTerm s (AddProof x t (Irrel p)) =
AddProof (substTerm s x) (substTerm s t) (Irrel $ substTerm s p)
substTerm s (UseProof tx tp x ty y) =
UseProof (substTerm s tx) (substTerm s tp) (substTerm s x)
(substTerm s' ty) (substTerm s'' y)
where
s' = delaySubst s
s'' = delaySubst s'
substTerm s (Pair a b) = Pair (substTerm s a) (substTerm s b)
substTerm s (Proj1 p) = Proj1 $ substTerm s p
substTerm s (Proj2 p) = Proj2 $ substTerm s p
substTerm s (Squeeze (Irrel p)) = Squeeze $ Irrel $ substTerm s p
substTerm s (GetProof tp x) = GetProof (substTerm s tp) (substTerm s x)
substTerm s (UseSquash p ty y) =
UseSquash (substTerm s p) (substTerm s ty) (substTerm s' y)
where s' = delaySubst s
substTerm s (Pi x y) = Pi (substTerm s x) (substTerm s' y)
where s' = delaySubst s
substTerm s (Top) = Top
substTerm s (Bottom) = Bottom
substTerm s (Nat) = Nat
substTerm s (Refine x p) = Refine (substTerm s x) (substTerm s' p)
where s' = delaySubst s
substTerm s (Sigma x y) = Sigma (substTerm s x) (substTerm s' y)
where s' = delaySubst s
substTerm s (Squash x) = Squash $ substTerm s x
substTerm s (Sort k) = Sort k
substTerm s (Substed s' x) = Substed (CompS s s') x
substTerm (CompS s s') v@(Var _) = substTerm s $ substTerm s' v
substTerm (IdS) v@(Var _) = v
substTerm (WeakenS n) (Var n') = Var $ n' + n
substTerm (ExtendS s x) (Var 0) = x
substTerm (ExtendS s x) (Var n) = substTerm s (Var $ n - 1)