blob: d269eb65921463db071df4ad4dc2107d703f843f (
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
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
|
module Level1
import Data.DPair
import Data.SnocList.Elem
import NormalForm
import Term
import Thinning
%hide NormalForm.Normal
data IsNormSubst : Subst ctx ctx' -> Type where
Base : IsNormSubst (Base thin)
(:<) : IsNormSubst sub -> IsNormal t -> IsNormSubst (sub :< t)
%name IsNormSubst prf
Normal : SnocList Ty -> Ty -> Type
Normal ctx ty = Subset (Term ctx ty) IsNormal
NormSubst : SnocList Ty -> SnocList Ty -> Type
NormSubst ctx ctx' = Subset (Subst ctx ctx') IsNormSubst
indexNormal : IsNormSubst sub -> (i : Elem ty ctx) -> IsNormal (index sub i)
indexNormal Base i = Ntrl Var
indexNormal (sub :< t) Here = t
indexNormal (sub :< t) (There i) = indexNormal sub i
index : NormSubst ctx' ctx -> Elem ty ctx -> Normal ctx' ty
index sub i = Element (index (fst sub) i) (indexNormal (snd sub) i)
restrictNormal : IsNormSubst sub -> (thin : ctx3 `Thins` ctx2) -> IsNormSubst (restrict sub thin)
restrictNormal Base thin = Base
restrictNormal (sub :< t) Id = sub :< t
restrictNormal (sub :< t) (Drop thin) = restrictNormal sub thin
restrictNormal (sub :< t) (Keep thin) = restrictNormal sub thin :< t
restrict : NormSubst ctx1 ctx2 -> ctx3 `Thins` ctx2 -> NormSubst ctx1 ctx3
restrict sub thin = Element (restrict (fst sub) thin) (restrictNormal (snd sub) thin)
data Value : Type where
V : (ctx : SnocList Ty) -> (ty : Ty) -> Value
S : (ctx, ctx' : SnocList Ty) -> Value
Raw : Value -> Type
Raw (V ctx ty) = Term ctx ty
Raw (S ctx ctx') = Subst ctx ctx'
Norm : (a : Value) -> Raw a -> Type
Norm (V _ _) = IsNormal
Norm (S _ _) = IsNormSubst
data Cont : Value -> Value -> Type where
EvalAbs1 : Term (ctx :< ty) ty' -> Cont (S (ctx' :< ty) ctx) (V ctx' (ty ~> ty'))
EvalAbs2 : Cont (V (ctx :< ty) ty') (V ctx (ty ~> ty'))
EvalApp1 : Term ctx ty -> NormSubst ctx' ctx -> Cont (V ctx' (ty ~> ty')) (V ctx' ty')
EvalApp2 : Normal ctx (ty ~> ty') -> Cont (V ctx ty) (V ctx ty')
EvalSucc1 : Cont (V ctx N) (V ctx N)
EvalRec1 :
Term ctx ty ->
Term (ctx :< ty) ty ->
NormSubst ctx' ctx ->
Cont (V ctx' N) (V ctx' ty)
EvalRec2 :
Normal ctx' N ->
Term (ctx :< ty) ty ->
NormSubst ctx' ctx ->
Cont (V ctx' ty) (V ctx' ty)
EvalRec3 :
Normal ctx' N ->
Normal ctx' ty ->
Term (ctx :< ty) ty ->
Cont (S (ctx' :< ty) ctx) (V ctx' ty)
EvalRec4 :
Normal ctx N ->
Normal ctx ty ->
Cont (V (ctx :< ty) ty) (V ctx ty)
EvalSub1 : Term ctx ty -> Cont (S ctx' ctx) (V ctx' ty)
EvalSnoc1 :
Term ctx ty ->
NormSubst ctx' ctx ->
Cont (S ctx' ctx'') (S ctx' (ctx'' :< ty))
EvalSnoc2 : NormSubst ctx' ctx -> Cont (V ctx' ty) (S ctx' (ctx :< ty))
RecSucc1 : Normal (ctx :< ty) ty -> Cont (V ctx ty) (V ctx ty)
data Stack : Value -> Value -> Type where
Nil : Stack a a
(::) : Cont a b -> Stack b c -> Stack a c
%name Cont k
%name Stack stack
data Case : Value -> Type where
Eval : Term ctx ty -> NormSubst ctx' ctx -> Case (V ctx' ty)
EvalSub : Subst ctx' ctx -> NormSubst ctx'' ctx' -> Case (S ctx'' ctx)
App : Normal ctx (ty ~> ty') -> Normal ctx ty -> Case (V ctx ty')
Rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Case (V ctx ty)
Run : Subset (Raw a) (Norm a) -> Case a
%name Case c
%prefix_record_projections off
record Config (ret : Value) where
constructor On
{0 a : Value}
c : Case a
stack : Stack a ret
data NotDone : Config ret -> Type where
EvalNotDone : NotDone (Eval t sub `On` stack)
EvalSubNotDone : NotDone (EvalSub sub sub' `On` stack)
AppNotDone : NotDone (App t u `On` stack)
RecNotDone : NotDone (Rec t u v `On` stack)
RunSomeNotDone : NotDone (Run x `On` step :: stack)
step : (config : Config ret) -> {auto 0 _ : NotDone config} -> Config ret
step (Eval (Var i) sub `On` stack) =
Run (index sub i) `On`
stack
step (Eval (Abs t) sub `On` stack) =
EvalSub (fst sub) (Element (Base $ Drop Id) Base) `On`
EvalAbs1 t :: stack
step (Eval (App t u) sub `On` stack) =
Eval t sub `On`
EvalApp1 u sub :: stack
step (Eval Zero sub `On` stack) =
Run (Element Zero Zero) `On`
stack
step (Eval (Succ t) sub `On` stack) =
Eval t sub `On`
EvalSucc1 :: stack
step (Eval (Rec t u v) sub `On` stack) =
Eval t sub `On`
EvalRec1 u v sub :: stack
step (Eval (Sub t sub') sub `On` stack) =
EvalSub sub' sub `On`
EvalSub1 t :: stack
step (EvalSub (Base thin) sub' `On` stack) =
Run (restrict sub' thin) `On`
stack
step (EvalSub (sub :< t) sub' `On` stack) =
EvalSub sub sub' `On`
EvalSnoc1 t sub' :: stack
step (App (Element (Abs t) prf) u `On` stack) =
Eval t (Element (Base Id :< fst u) (Base :< snd u)) `On`
stack
step (App (Element t@(Var _) prf) u `On` stack) =
Run (Element (App t (fst u)) (Ntrl $ App Var (snd u))) `On`
stack
step (App (Element t@(App _ _) prf) u `On` stack) =
Run (Element (App t (fst u)) (Ntrl $ App (appNtrl prf) (snd u))) `On`
stack
step (App (Element t@(Rec _ _ _) prf) u `On` stack) =
Run (Element (App t (fst u)) (Ntrl $ App (recNtrl prf) (snd u))) `On`
stack
step (App (Element t@(Sub _ _) prf) u `On` stack) = void $ absurd prf
step (Rec (Element Zero prf) u v `On` stack) =
Run u `On`
stack
step (Rec (Element (Succ t) prf) u v `On` stack) =
Rec (Element t (predNorm prf)) u v `On`
RecSucc1 v :: stack
step (Rec (Element t@(Var _) prf) u v `On` stack) =
Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec Var (snd u) (snd v))) `On`
stack
step (Rec (Element t@(App _ _) prf) u v `On` stack) =
Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec (appNtrl prf) (snd u) (snd v))) `On`
stack
step (Rec (Element t@(Rec _ _ _) prf) u v `On` stack) =
Run (Element (Rec t (fst u) (fst v)) (Ntrl $ Rec (recNtrl prf) (snd u) (snd v))) `On`
stack
step (Rec (Element t@(Sub _ _) prf) u v `On` stack) = void $ absurd prf
step (Run sub `On` EvalAbs1 t :: stack) =
Eval t (Element (fst sub :< Var Here) (snd sub :< Ntrl Var)) `On`
EvalAbs2 :: stack
step (Run t `On` EvalAbs2 :: stack) =
Run (Element (Abs $ fst t) (Abs $ snd t)) `On`
stack
step (Run t `On` EvalApp1 u sub :: stack) =
Eval u sub `On`
EvalApp2 t :: stack
step (Run u `On` EvalApp2 t :: stack) =
App t u `On`
stack
step (Run t `On` EvalSucc1 :: stack) =
Run (Element (Succ $ fst t) (Succ $ snd t)) `On`
stack
step (Run t `On` EvalRec1 u v sub :: stack) =
Eval u sub `On`
EvalRec2 t v sub :: stack
step (Run u `On` EvalRec2 t v sub :: stack) =
EvalSub (fst sub) (Element (Base $ Drop Id) Base) `On`
EvalRec3 t u v :: stack
step (Run sub `On` EvalRec3 t u v :: stack) =
Eval v (Element (fst sub :< Var Here) (snd sub :< Ntrl Var)) `On`
EvalRec4 t u :: stack
step (Run v `On` EvalRec4 t u :: stack) =
Rec t u v `On`
stack
step (Run sub `On` EvalSub1 t :: stack) =
Eval t sub `On`
stack
step (Run sub `On` EvalSnoc1 t sub' :: stack) =
Eval t sub' `On`
EvalSnoc2 sub :: stack
step (Run t `On` EvalSnoc2 sub :: stack) =
Run (Element (fst sub :< fst t) (snd sub :< snd t)) `On`
stack
step (Run val `On` RecSucc1 v :: stack) =
Eval (fst v) (Element (Base Id :< fst val) (Base :< snd val)) `On`
stack
unwindStack : Raw a -> (stack : Stack a b) -> Raw b
unwindStack x [] = x
unwindStack sub (EvalAbs1 t :: stack) = unwindStack (Abs (Sub t (sub :< Var Here))) stack
unwindStack t (EvalAbs2 :: stack) = unwindStack (Abs t) stack
unwindStack t (EvalApp1 u sub :: stack) = unwindStack (App t (Sub u (fst sub))) stack
unwindStack u (EvalApp2 t :: stack) = unwindStack (App (fst t) u) stack
unwindStack t (EvalSucc1 :: stack) = unwindStack (Succ t) stack
unwindStack t (EvalRec1 u v sub :: stack) =
unwindStack (Rec t (Sub u (fst sub)) (Sub v (Base (Drop Id) . fst sub :< Var Here))) stack
unwindStack u (EvalRec2 t v sub :: stack) =
unwindStack (Rec (fst t) u (Sub v (Base (Drop Id) . fst sub :< Var Here))) stack
unwindStack sub (EvalRec3 t u v :: stack) =
unwindStack (Rec (fst t) (fst u) (Sub v (sub :< Var Here))) stack
unwindStack v (EvalRec4 t u :: stack) =
unwindStack (Rec (fst t) (fst u) v) stack
unwindStack sub (EvalSub1 t :: stack) = unwindStack (Sub t sub) stack
unwindStack sub (EvalSnoc1 t sub' :: stack) = unwindStack (sub :< Sub t (fst sub')) stack
unwindStack t (EvalSnoc2 sub :: stack) = unwindStack (fst sub :< t) stack
unwindStack val (RecSucc1 v :: stack) = unwindStack (Sub (fst v) (Base Id :< val)) stack
unwind : Config a -> Raw a
unwind (Eval t sub `On` stack) = unwindStack (Sub t $ fst sub) stack
unwind (EvalSub sub sub' `On` stack) = unwindStack (fst sub' . sub) stack
unwind (App t u `On` stack) = unwindStack (App (fst t) (fst u)) stack
unwind (Rec t u v `On` stack) = unwindStack (Rec (fst t) (fst u) (fst v)) stack
unwind (Run x `On` stack) = unwindStack (fst x) stack
eval : Nat -> Config ret -> Raw ret
eval 0 config = unwind config
eval (S n) (Run x `On` []) = fst x
eval (S n) config@(Run _ `On` _ :: _) = eval n (step config)
eval (S n) config@(Eval _ _ `On` _) = eval n (step config)
eval (S n) config@(EvalSub _ _ `On` _) = eval n (step config)
eval (S n) config@(App _ _ `On` _) = eval n (step config)
eval (S n) config@(Rec _ _ _ `On` _) = eval n (step config)
|
