-
Notifications
You must be signed in to change notification settings - Fork 0
/
2020-03-21-stlc.agda
533 lines (410 loc) · 25.2 KB
/
2020-03-21-stlc.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
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
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
module _ where
module _ where
record ⊤ : Set where
constructor tt
infixr 5 _,_
record _×_ (A B : Set) : Set where
constructor _,_
field
fst : A
snd : B
infixr 5 _,,_
record Σ (A : Set) (B : A → Set) : Set where
constructor _,,_
field
first : A
second : B first
data ℕ : Set where
zero : ℕ
succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
_€_ : {A B : Set} → A → (A → B) → B
x € f = f x
data _+_ (A B : Set) : Set where
inl : A → A + B
inr : B → A + B
data _≡_ {A : Set} (a : A) : A → Set where
refl : a ≡ a
transport : {A : Set} {a b : A} → (P : A → Set) → a ≡ b → P a → P b
transport P refl Pa = Pa
cong : {A B : Set} {a a' : A} → (f : A → B) → a ≡ a' → f a ≡ f a'
cong f refl = refl
infixr 15 _∷_
data List (A : Set) : Set where
ε : List A
_∷_ : A → List A → List A
single : ∀ {A} → A → List A
single a = a ∷ ε
_++_ : {A : Set} → List A → List A → List A
ε ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
data Has {A : Set} : List A → A → Set where
here : ∀ {a as} → Has (a ∷ as) a
there : ∀ {a b as} → Has as a → Has (b ∷ as) a
$0 : ∀ {A a0 as} → Has {A} (a0 ∷ as) a0
$1 : ∀ {A a0 a1 as} → Has {A} (a0 ∷ a1 ∷ as) a1
$2 : ∀ {A a0 a1 a2 as} → Has {A} (a0 ∷ a1 ∷ a2 ∷ as) a2
$3 : ∀ {A a0 a1 a2 a3 as} → Has {A} (a0 ∷ a1 ∷ a2 ∷ a3 ∷ as) a3
$0 = here
$1 = there here
$2 = there (there here)
$3 = there (there (there here))
data All {A : Set} (P : A → Set) : List A → Set where
ε : All P ε
_∷_ : ∀ {a as} → P a → All P as → All P (a ∷ as)
_++'_ : {A : Set} {P : A → Set} {xs ys : List A} → All P xs → All P ys → All P (xs ++ ys)
ε ++' Pys = Pys
(Px ∷ Pxs) ++' Pys = Px ∷ (Pxs ++' Pys)
get : ∀ {A P a as} → All {A} P as → Has as a → P a
get (x ∷ env) here = x
get (x ∷ env) (there var) = get env var
mapAll : {A : Set} {P Q : A → Set} {as : List A} → ({a : A} → P a → Q a) → All P as → All Q as
mapAll f ε = ε
mapAll f (Pa ∷ Pas) = f Pa ∷ mapAll f Pas
data All2 {A : Set} {P : A → Set} (P2 : {a : A} → P a → Set) : {as : List A} → All P as → Set where
ε : All2 P2 ε
_∷_ : ∀ {a as Pa Pas} → P2 Pa → All2 P2 {as} Pas → All2 P2 {a ∷ as} (Pa ∷ Pas)
_++2_ : ∀ {A P xs ys Pxs Pys} {P2 : {a : A} → P a → Set} → All2 P2 {xs} Pxs → All2 P2 {ys} Pys → All2 {A} {P} P2 {xs ++ ys} (Pxs ++' Pys)
ε ++2 Pys = Pys
(Px ∷ Pxs) ++2 Pys = Px ∷ (Pxs ++2 Pys)
get2 : ∀ {A P a as Pas} → {P2 : {a : A} → P a → Set} → All2 {A} {P} P2 {as} Pas → (i : Has as a) → P2 (get Pas i)
get2 (x ∷ x₁) here = x
get2 (x ∷ x₁) (there i) = get2 x₁ i
mapAll2 : {A : Set} {P : A → Set} {P2 Q2 : {a : A} → P a → Set} {as : List A} {Pas : All P as} → ({a : A} → {Pa : P a} → P2 Pa → Q2 Pa) → All2 P2 Pas → All2 Q2 Pas
mapAll2 f ε = ε
mapAll2 f (P2Pa ∷ P2Pas) = f P2Pa ∷ mapAll2 f P2Pas
data Type : Set where
σ π : List Type → Type
_⇒_ : List Type → Type → Type
nat : Type
-- list : Type → Type
-- stream : Type → Type
Context : Set
Context = List Type
Var : List Type → Type → Set
Var Γ τ = Has Γ τ
mutual
data Expr (Γ : List Type) : Type → Set where
lambda : (ρs : List Type) (τ : Type) → Term (ρs ++ Γ) τ → Expr Γ (ρs ⇒ τ)
call : (ρs : List Type) (τ : Type) → Var Γ (ρs ⇒ τ) → All (\ρ → Var Γ ρ) ρs → Expr Γ τ
inj : (τs : List Type) (τ : Type) → Has τs τ → Var Γ τ → Expr Γ (σ τs)
case : (τs : List Type) (ρ : Type) → Var Γ (σ τs) → All (\τ → Term (τ ∷ Γ) ρ) τs → Expr Γ ρ
tuple : (τs : List Type) → All (\τ → Var Γ τ) τs → Expr Γ (π τs)
untuple : (τs : List Type) (ρ : Type) → Var Γ (π τs) → Term (τs ++ Γ) ρ → Expr Γ ρ
zero : Expr Γ nat
succ : Var Γ nat → Expr Γ nat
foldNat : (ρ : Type) → Var Γ nat → Term Γ ρ → Term (ρ ∷ Γ) ρ → Expr Γ ρ
data Term (Γ : List Type) : Type → Set where
ret : ∀ {τ} → Var Γ τ → Term Γ τ
set : ∀ {ρ τ} → Expr Γ ρ → Term (ρ ∷ Γ) τ → Term Γ τ
mutual
data Value : Type → Set where
#closure : ∀ {ρs τ} → Closure ρs τ → Value (ρs ⇒ τ)
#tuple : ∀ {τs} → All Value τs → Value (π τs)
#inj : ∀ {τs τ} → (i : Has τs τ) → Value τ → Value (σ τs)
#zero : Value nat
#succ : Value nat → Value nat
-- #nat : ℕ → Value nat
-- #list : List (Value τ) → Value (list τ)
-- #conat : ∀ {ρ} → Value ρ → Closure ρ σ[π[],ρ] → Value conat
-- #stream : ∀ {ρ} → Value ρ → Closure ρ π[τ,ρ] → Value (stream τ)
Env : List Type → Set
Env Γ = All Value Γ
data Closure (ρs : List Type) (τ : Type) : Set where
_&_ : ∀ {Γ} → Env Γ → Term (ρs ++ Γ) τ → Closure ρs τ
data Cont : List Type → Type → Set where
ε : ∀ {ρ} → Cont (single ρ) ρ
_∷_ : ∀ {ρs ϕ τ} → Closure ρs ϕ → Cont (single ϕ) τ → Cont ρs τ
VS : Type → Set
VS τ = Value τ + Cont ε τ
applyFunction : ∀ {ρs τ} → Value (ρs ⇒ τ) → All Value ρs → Cont ε τ
applyFunction (#closure (envf & termf)) vs = (vs ++' envf) & termf ∷ ε
applyCase : ∀ {Γ τs ρ} → Env Γ → Value (σ τs) → All (\τ → Term (τ ∷ Γ) ρ) τs → Cont ε ρ
applyCase env (#inj i v) terms = ((v ∷ env) & get terms i) ∷ ε
applyTuple : ∀ {Γ τs ρ} → Env Γ → Value (π τs) → Term (τs ++ Γ) ρ → Cont ε ρ
applyTuple env (#tuple vs) term = ((vs ++' env) & term) ∷ ε
getContFoldNat : ∀ {ρ Γ} → Env Γ → Value nat → Term (ρ ∷ Γ) ρ → Cont (single ρ) ρ
getContFoldNat env #zero terms = ε
getContFoldNat env (#succ v) terms = (env & terms) ∷ getContFoldNat env v terms
applyFoldNat : ∀ {ρ Γ} → Env Γ → Value nat → Term Γ ρ → Term (ρ ∷ Γ) ρ → Cont ε ρ
applyFoldNat env n termz terms = (env & termz) ∷ getContFoldNat env n terms
stepExpr : ∀ {Γ τ} → Env Γ → Expr Γ τ → Value τ + Cont ε τ
stepExpr env (lambda ρs τ term) = inl (#closure (env & term))
stepExpr env (call ρs τ f xs) = inr (applyFunction (get env f) (mapAll (get env) xs))
stepExpr env (inj τs τ i x) = inl (#inj i (get env x))
stepExpr env (case τs ρ x terms) = inr (applyCase env (get env x) terms)
stepExpr env (tuple τs xs) = inl (#tuple (mapAll (get env) xs))
stepExpr env (untuple τs ρ x term) = inr (applyTuple env (get env x) term)
stepExpr env zero = inl #zero
stepExpr env (succ x) = inl (#succ (get env x))
stepExpr env (foldNat ρ x termz terms) = inr (applyFoldNat env (get env x) termz terms)
composeCont : ∀ {ρs τ ϕ} → Cont ρs τ → Cont (single τ) ϕ → Cont ρs ϕ
composeCont ε cont2 = cont2
composeCont (cl1 ∷ cont1) cont2 = cl1 ∷ composeCont cont1 cont2
applyEnvClosure : ∀ {τs ϕ} → Env τs → Closure τs ϕ → Closure ε ϕ
applyEnvClosure env (env' & term) = (env ++' env') & term
applyEnvCont : ∀ {τs ϕ} → Env τs → Cont τs ϕ → Value ϕ + Cont ε ϕ
applyEnvCont vs (cl ∷ cont) = inr (applyEnvClosure vs cl ∷ cont)
applyEnvCont (v ∷ ε) ε = inl v
applyVCont : ∀ {τ ϕ} → Value τ → Cont (single τ) ϕ → Value ϕ + Cont ε ϕ
applyVCont v cont = applyEnvCont (v ∷ ε) cont
applyVSCont : ∀ {τ ϕ} → Value τ + Cont ε τ → Cont (single τ) ϕ → Value ϕ + Cont ε ϕ
applyVSCont (inl v) cont = applyVCont v cont
applyVSCont (inr cont') cont = inr (composeCont cont' cont)
stepExprCont : ∀ {Γ τ ϕ} → Env Γ → Expr Γ τ → Cont (single τ) ϕ → Value ϕ + Cont ε ϕ
stepExprCont env expr cont = applyVSCont (stepExpr env expr) cont
stepTermCont : ∀ {Γ τ ϕ} → Env Γ → Term Γ τ → Cont (single τ) ϕ → Value ϕ + Cont ε ϕ
stepTermCont env (ret x) cont = applyVCont (get env x) cont
stepTermCont env (set expr term) cont = stepExprCont env expr ((env & term) ∷ cont)
step : ∀ {ϕ} → Cont ε ϕ → Value ϕ + Cont ε ϕ
step ((env & term) ∷ cont) = stepTermCont env term cont
composeApplyEnvContIsCompose : ∀ {τs ϕ ϕ'} → (env : Env τs) → (cont1 : Cont τs ϕ) → (cont2 : Cont (single ϕ) ϕ') → applyVSCont (applyEnvCont env cont1) cont2 ≡ applyEnvCont env (composeCont cont1 cont2)
composeApplyEnvContIsCompose env (cl ∷ cont1) cont2 = refl
composeApplyEnvContIsCompose (v ∷ ε) ε cont2 = refl
composeContIsCompose : ∀ {ρs τ ϕ ϕ'} → (cont0 : Cont ρs τ) → (cont1 : Cont (single τ) ϕ) → (cont2 : Cont (single ϕ) ϕ') → composeCont (composeCont cont0 cont1) cont2 ≡ composeCont cont0 (composeCont cont1 cont2)
composeContIsCompose ε cont1 cont2 = refl
composeContIsCompose (closure ∷ cont0) cont1 cont2 = cong (\x → closure ∷ x) (composeContIsCompose cont0 cont1 cont2)
composeApplyVSContIsCompose : ∀ {τ ϕ ϕ'} → (vs : VS τ) → (cont1 : Cont (single τ) ϕ) → (cont2 : Cont (single ϕ) ϕ') → applyVSCont (applyVSCont vs cont1) cont2 ≡ applyVSCont vs (composeCont cont1 cont2)
composeApplyVSContIsCompose (inl value) cont1 cont2 = composeApplyEnvContIsCompose (value ∷ ε) cont1 cont2
composeApplyVSContIsCompose (inr cont') cont1 cont2 = cong inr (composeContIsCompose cont' cont1 cont2)
composeStepExprContIsCompose : ∀ {Γ τ ϕ ϕ'} → (env : Env Γ) → (expr : Expr Γ τ) → (cont1 : Cont (single τ) ϕ) → (cont2 : Cont (single ϕ) ϕ') → applyVSCont (stepExprCont env expr cont1) cont2 ≡ stepExprCont env expr (composeCont cont1 cont2)
composeStepExprContIsCompose env expr cont1 cont2 = composeApplyVSContIsCompose (stepExpr env expr) cont1 cont2
composeStepTermContIsCompose : ∀ {ρs τ ϕ ϕ'} → (env : Env ρs) → (term : Term ρs τ) → (cont1 : Cont (single τ) ϕ) → (cont2 : Cont (single ϕ) ϕ') → applyVSCont (stepTermCont env term cont1) cont2 ≡ stepTermCont env term (composeCont cont1 cont2)
composeStepTermContIsCompose env (ret x) ε cont2 = refl
composeStepTermContIsCompose env (ret x) (x₁ ∷ cont1) cont2 = refl
composeStepTermContIsCompose env (set expr term) cont1 cont2 = composeStepExprContIsCompose env expr ((env & term) ∷ cont1) cont2
composeStepIsStepCompose : ∀ {τ ϕ} → (cont1 : Cont ε τ) → (cont2 : Cont (single τ) ϕ) → applyVSCont (step cont1) cont2 ≡ step (composeCont cont1 cont2)
composeStepIsStepCompose ((env & term) ∷ cont1) cont2 = composeStepTermContIsCompose env term cont1 cont2
record PredVS (τ : Type) : Set₁ where
constructor mkPredVS
field
applyPredVS : VS τ → Set
applyPredV : Value τ → Set
open PredVS public
data All₁ {A : Set} (P : A → Set₁) : List A → Set₁ where
ε : All₁ P ε
_∷_ : ∀ {a as} → P a → All₁ P as → All₁ P (a ∷ as)
data All2₁ {A : Set} {P : A → Set} (P2 : {a : A} → P a → Set₁) : {as : List A} → All P as → Set₁ where
ε : All2₁ P2 ε
_∷_ : ∀ {a as Pa Pas} → P2 Pa → All2₁ P2 {as} Pas → All2₁ P2 {a ∷ as} (Pa ∷ Pas)
get₁ : ∀ {A P a as} → All₁ {A} P as → Has as a → P a
get₁ (x ∷ env) here = x
get₁ (x ∷ env) (there var) = get₁ env var
AllPredVS : List Type → Set₁
AllPredVS τs = All₁ PredVS τs
AllPredVS' : List Type → Set₁
AllPredVS' τs = (τ : Type) → Has τs τ → PredVS τ
getAllPredVS : ∀ {τs τ} → AllPredVS τs → Has τs τ → Value τ → Set
getAllPredVS (Fin-τ ∷ Fin-τs) here value = applyPredV Fin-τ value
getAllPredVS (Fin-τ ∷ Fin-τs) (there i) value = getAllPredVS Fin-τs i value
NormValueF : ∀ {τ} → PredVS τ → Value τ → Set
NormValueF Fin-τ value = applyPredV Fin-τ value
NormEnvF : ∀ {τs} → AllPredVS τs → Env τs → Set
NormEnvF ε ε = ⊤
NormEnvF (Fin-τ ∷ Fin-τs) (value ∷ values) = NormValueF Fin-τ value × NormEnvF Fin-τs values
GoodClosureF : ∀ {ρs τ} → AllPredVS ρs → PredVS τ → Closure ρs τ → Set
GoodClosureF {ρs} {τ} Fin-ρs Fin-τ closure = ∀ {values} → NormEnvF {ρs} Fin-ρs values → applyPredVS Fin-τ (inr (applyEnvClosure values closure ∷ ε))
NormValue-⇒F : ∀ {ρs τ} → (Fin-ρs : AllPredVS ρs) (Fin-τ : PredVS τ) → Value (ρs ⇒ τ) → Set
NormValue-⇒F Fin-ρs Fin-τ (#closure cl) = GoodClosureF Fin-ρs Fin-τ cl
NormValue-πF : ∀ {τs} → (Fin-τs : AllPredVS τs) → Value (π τs) → Set
NormValue-πF Fin-τs (#tuple vs) = NormEnvF Fin-τs vs
--NormValue-σF : ∀ {τs} → (Fin-τs : AllPredVS τs) → Value (σ τs) → Set
--NormValue-σF Fin-τs (#inj i v) = getAllPredVS Fin-τs i v
data NormValue-σF {τs} (Fin-τs : AllPredVS τs) : Value (σ τs) → Set where
normInj : ∀ {τ} → (i : Has τs τ) → {v : Value τ} → applyPredV (get₁ Fin-τs i) v → NormValue-σF Fin-τs (#inj i v)
NormValue-natF : Value nat → Set
NormValue-natF value = ⊤
data GoodVSF {τ} (Norm-τ : Value τ → Set) : VS τ → Set where
fin : ∀ {v} → Norm-τ v → GoodVSF Norm-τ (inl v)
nex : ∀ {s} → GoodVSF Norm-τ (step s) → GoodVSF Norm-τ (inr s)
mutual
GoodVSPred : (τ : Type) → PredVS τ
GoodVSPred τ = mkPredVS (GoodVSF (NormValue' τ)) (NormValue' τ)
NormValue' : (τ : Type) → Value τ → Set
NormValue' (ρs ⇒ τ) = NormValue-⇒F (AllGoodVSPred ρs) (GoodVSPred τ)
NormValue' (σ τs) = NormValue-σF (AllGoodVSPred τs)
NormValue' (π τs) = NormValue-πF (AllGoodVSPred τs)
NormValue' nat = NormValue-natF
AllGoodVSPred : (τs : List Type) → AllPredVS τs
AllGoodVSPred ε = ε
AllGoodVSPred (τ ∷ τs) = GoodVSPred τ ∷ AllGoodVSPred τs
GoodVS : ∀ {τ} → VS τ → Set
GoodVS {τ} = applyPredVS (GoodVSPred τ)
GoodClosure : ∀ {ρs τ} → Closure ρs τ → Set
GoodClosure {ρs} {τ} = GoodClosureF (AllGoodVSPred ρs) (GoodVSPred τ)
NormValue : ∀ {τ} → Value τ → Set
NormValue {τ} = NormValue' τ
NormEnv : ∀ {τs} → Env τs → Set
NormEnv {τs} = NormEnvF (AllGoodVSPred τs)
GoodTerm : ∀ {Γ τ} → Term Γ τ → Set
GoodTerm {Γ} {τ} term = ∀ {env} → NormEnv {Γ} env → GoodVS (inr ((env & term) ∷ ε))
data NormClosure {ρs τ} : Closure ρs τ → Set where
_&_ : ∀ {Γ env term} → NormEnv {Γ} env → GoodTerm term → NormClosure (env & term)
GoodCont : ∀ {ρs τ} → Cont ρs τ → Set
GoodCont cont = ∀ {vs} → NormEnv vs → GoodVS (applyEnvCont vs cont)
data NormExpr {Γ} : ∀ {τ} → Expr Γ τ → Set where
normLambda : ∀ {ρs τ term} → GoodTerm term → NormExpr (lambda ρs τ term)
normCall : ∀ {ρs τ} f xs → NormExpr (call ρs τ f xs)
normInj : ∀ {τs τ i} x → NormExpr (inj τs τ i x)
normCase : ∀ {τs ρ} x {terms} → All2 GoodTerm terms → NormExpr (case τs ρ x terms)
normTuple : ∀ {τs} xs → NormExpr (tuple τs xs)
normUntuple : ∀ {τs ρ} x {term} → GoodTerm term → NormExpr (untuple τs ρ x term)
normZero : NormExpr zero
normSucc : ∀ x → NormExpr (succ x)
normFoldNat : ∀ {ρ} x {termz terms} → GoodTerm termz → GoodTerm terms → NormExpr (foldNat ρ x termz terms)
data NormCont : ∀ {ρs τ} → Cont ρs τ → Set where
ε : ∀ {τ} → NormCont {single τ} {τ} ε
_∷_ : ∀ {ρs ϕ τ cl cont} → GoodClosure {ρs} {ϕ} cl → NormCont {single ϕ} {τ} cont → NormCont (cl ∷ cont)
data NormVS {τ} : VS τ → Set where
normInl : ∀ {v} → NormValue v → NormVS (inl v)
normInr : ∀ {c} → NormCont c → NormVS (inr c)
goodGoodApplyVSCont : ∀ {τ ϕ vs cont} → GoodVS {τ} vs → GoodCont {single τ} {ϕ} cont → GoodVS (applyVSCont vs cont)
goodGoodApplyVSCont {vs = inl value} (fin norm-value) good-cont = good-cont (norm-value , tt)
goodGoodApplyVSCont {vs = inr cont1} {cont = cont2} (nex good-vs) good-cont2 = nex (transport GoodVS (composeStepIsStepCompose cont1 cont2) (goodGoodApplyVSCont good-vs good-cont2))
goodNormCont : ∀ {ρs τ cont} → NormCont {ρs} {τ} cont → GoodCont {ρs} {τ} cont
goodNormCont {cont = (env & term) ∷ cont} (good-closure ∷ norm-cont) {values} norm-values = goodGoodApplyVSCont {cont = cont} good-vs good-cont
where
good-vs : GoodVS (inr (((values ++' env) & term) ∷ ε))
good-vs = good-closure norm-values
good-cont1 : GoodCont ((env & term) ∷ ε)
good-cont1 norm-vs = good-closure norm-vs
good-cont : GoodCont cont
good-cont = goodNormCont norm-cont
goodNormCont ε {v ∷ ε} (norm-value , tt) = fin norm-value
goodNormVS : ∀ {τ vs} → NormVS {τ} vs → GoodVS vs
goodNormVS (normInl norm-value) = fin norm-value
goodNormVS (normInr norm-cont@(_∷_ {cl = _ & _} _ _)) = goodNormCont norm-cont tt
appendNormEnv : ∀ {ρs τs values1 values2} → NormEnv {ρs} values1 → NormEnv {τs} values2 → NormEnv {ρs ++ τs} (values1 ++' values2)
appendNormEnv {values1 = ε} norm-values1 norm-values2 = norm-values2
appendNormEnv {values1 = value ∷ values1} (norm-value , norm-values1) norm-values2 = norm-value , appendNormEnv norm-values1 norm-values2
getNormEnv : ∀ {τs τ env} → NormEnv {τs} env → (x : Var τs τ) → NormValue (get env x)
getNormEnv {env = v ∷ env} (norm-v , norm-env) here = norm-v
getNormEnv {env = v ∷ env} (norm-v , norm-env) (there x) = getNormEnv norm-env x
goodNormClosure : ∀ {ρs τ closure} → NormClosure {ρs} {τ} closure → GoodClosure closure
goodNormClosure (norm-env & good-term) norm-values = good-term (appendNormEnv norm-values norm-env)
normMapGet : ∀ {Γ τs env} → NormEnv {Γ} env → (xs : All (Var Γ) τs) → NormEnv {τs} (mapAll (get env) xs)
normMapGet norm-env ε = tt
normMapGet norm-env (x ∷ xs) = getNormEnv norm-env x , normMapGet norm-env xs
normApplyFunction : ∀ {ρs τ vf vs} → NormValue {ρs ⇒ τ} vf → NormEnv vs → NormCont (applyFunction vf vs)
normApplyFunction {vf = #closure (envf & termf)} {vs} good-closure norm-vs = good-closure' ∷ ε
where
good-closure' : GoodClosure ((vs ++' envf) & termf)
good-closure' {ε} norm-ε = good-closure norm-vs
lem : ∀ {τ} τs (i : Has τs τ) (v : Value τ) → applyPredV (get₁ (AllGoodVSPred τs) i) v → applyPredV (GoodVSPred τ) v
lem τs here v norm-v = norm-v
lem (τ ∷ τs) (there i) v = lem τs i v
lem' : ∀ {τ} τs (i : Has τs τ) (v : Value τ) → applyPredV (GoodVSPred τ) v → applyPredV (get₁ (AllGoodVSPred τs) i) v
lem' τs here v norm-v = norm-v
lem' (τ ∷ τs) (there i) v = lem' τs i v
normApplyCase : ∀ {Γ τs ρ env v terms} → NormEnv {Γ} env → NormValue {σ τs} v → All2 (GoodTerm {_ ∷ Γ} {ρ}) terms → NormCont (applyCase env v terms)
normApplyCase {v = #inj {τs} {τ} i v} norm-env (normInj _ norm-v) good-terms = goodNormClosure ((lem τs i v norm-v , norm-env) & get2 good-terms i) ∷ ε
normApplyTuple : ∀ {Γ τs ρ env v term} → NormEnv {Γ} env → NormValue {π τs} v → GoodTerm {τs ++ Γ} {ρ} term → NormCont (applyTuple env v term)
normApplyTuple {v = #tuple values} norm-env norm-values good-term = goodNormClosure (appendNormEnv norm-values norm-env & good-term) ∷ ε
normGetContFoldNat : ∀ {ρ Γ env v term} → NormEnv {Γ} env → NormValue {nat} v → GoodTerm {ρ ∷ Γ} {ρ} term → NormCont (getContFoldNat env v term)
normGetContFoldNat {v = #zero} norm-env norm-value good-term = ε
normGetContFoldNat {v = #succ v} norm-env norm-value good-term = goodNormClosure (norm-env & good-term) ∷ normGetContFoldNat norm-env tt good-term
normApplyFoldNat : ∀ {ρ Γ env v termZ termS} → NormEnv {Γ} env → NormValue {nat} v → GoodTerm {Γ} {ρ} termZ → GoodTerm {ρ ∷ Γ} {ρ} termS → NormCont (applyFoldNat env v termZ termS)
normApplyFoldNat norm-env norm-value good-termZ good-termS = goodNormClosure (norm-env & good-termZ) ∷ normGetContFoldNat norm-env norm-value good-termS
normStepExpr : ∀ {Γ τ expr env} → NormEnv {Γ} env → NormExpr {Γ} {τ} expr → NormVS (stepExpr env expr)
normStepExpr norm-env (normLambda good-term) = normInl \norm-values → good-term (appendNormEnv norm-values norm-env)
normStepExpr norm-env (normCall f xs) = normInr (normApplyFunction (getNormEnv norm-env f) (normMapGet norm-env xs))
normStepExpr norm-env (normInj {τs} {τ} {i} x) = normInl (normInj _ (lem' τs i _ (getNormEnv norm-env x)))
normStepExpr norm-env (normCase x good-terms) = normInr (normApplyCase norm-env (getNormEnv norm-env x) good-terms)
normStepExpr norm-env (normTuple xs) = normInl (normMapGet norm-env xs)
normStepExpr norm-env (normUntuple x good-term) = normInr (normApplyTuple norm-env (getNormEnv norm-env x) good-term)
normStepExpr norm-env normZero = normInl tt
normStepExpr norm-env (normSucc x) = normInl (getNormEnv norm-env x)
normStepExpr norm-env (normFoldNat x good-termz good-terms) = normInr (normApplyFoldNat norm-env (getNormEnv norm-env x) good-termz good-terms)
normComposeCont : ∀ {ρs τ ϕ cont1 cont2} → NormCont {ρs} {τ} cont1 → NormCont {single τ} {ϕ} cont2 → NormCont (composeCont cont1 cont2)
normComposeCont ε norm-cont2 = norm-cont2
normComposeCont (norm-closure ∷ norm-cont1) norm-cont2 = norm-closure ∷ normComposeCont norm-cont1 norm-cont2
normApplyVSCont : ∀ {τ ϕ vs cont} → NormVS {τ} vs → NormCont {single τ} {ϕ} cont → NormVS (applyVSCont vs cont)
normApplyVSCont (normInl norm-value) ε = normInl norm-value
normApplyVSCont {cont = closure@(_ & _) ∷ _} (normInl {value} norm-value) (good-closure ∷ norm-cont) = normInr (good-closure' ∷ norm-cont)
where
good-closure' : GoodClosure (applyEnvClosure (value ∷ ε) closure)
good-closure' {ε} tt = good-closure (norm-value , tt)
normApplyVSCont (normInr norm-cont') norm-cont = normInr (normComposeCont norm-cont' norm-cont)
goodApplyVSCont : ∀ {τ ϕ vs cont} → NormVS {τ} vs → NormCont {single τ} {ϕ} cont → GoodVS (applyVSCont vs cont)
goodApplyVSCont norm-vs norm-cont = goodNormVS (normApplyVSCont norm-vs norm-cont)
goodStepExprCont : ∀ {Γ τ ρ expr env cont} → NormEnv {Γ} env → NormExpr {Γ} {τ} expr → NormCont {single τ} {ρ} cont → GoodVS (stepExprCont env expr cont)
goodStepExprCont norm-env norm-expr norm-cont = goodApplyVSCont (normStepExpr norm-env norm-expr) norm-cont
mutual
normExpr : ∀ {Γ τ} → (expr : Expr Γ τ) → NormExpr expr
normExpr (lambda ρs τ term) = normLambda (goodTerm term)
normExpr (call ρs τ f xs) = normCall f xs
normExpr (inj τs τ i x) = normInj x
normExpr (case τs ρ x terms) = normCase x (goodAllTerms terms)
normExpr (tuple τs x) = normTuple x
normExpr (untuple τs ρ xs term) = normUntuple xs (goodTerm term)
normExpr zero = normZero
normExpr (succ x) = normSucc x
normExpr (foldNat ρ x termZ termS) = normFoldNat x (goodTerm termZ) (goodTerm termS)
goodAllTerms : ∀ {Γ τs ρ} → (terms : All (\τ → Term (τ ∷ Γ) ρ) τs) → All2 GoodTerm terms
goodAllTerms ε = ε
goodAllTerms (term ∷ terms) = goodTerm term ∷ goodAllTerms terms
goodTerm : ∀ {Γ τ} → (term : Term Γ τ) → GoodTerm term
goodTerm (ret x) {env} norm-env = nex {s = (env & ret x) ∷ ε} (fin {v = get env x} (getNormEnv norm-env x))
goodTerm (set expr term) {env} norm-env = nex {s = (env & set expr term) ∷ ε} (goodStepExprCont {cont = (env & term) ∷ ε} norm-env (normExpr expr) (good-closure ∷ ε))
where
good-term : GoodTerm term
good-term = goodTerm term
good-closure : GoodClosure (env & term)
good-closure norm-values = good-term (appendNormEnv norm-values norm-env)
result : ∀ {τ vc} → GoodVS {τ} vc → Value τ
result (fin {v} _norm) = v
result (nex c) = result c
eval : ∀ {τ} → Term ε τ → Value τ
eval term = result (goodTerm term tt)
module Test where
infixr 5 _▸_
_▸_ : ∀ {Γ ρ τ} → Expr Γ ρ → Term (ρ ∷ Γ) τ → Term Γ τ
_▸_ = set
num : ∀ Γ → ℕ → Term Γ nat
num Γ n = set zero (go n) where
go : {Γ : Context} → ℕ → Term (nat ∷ Γ) nat
go zero = ret here
go (succ n) = succ here ▸ go n
add : ∀ Γ → Term (nat ∷ nat ∷ Γ) nat
add _ =
foldNat nat $1
(ret $0)
( succ $0 ▸
ret $0
)
▸ ret here
test : ℕ → ℕ → Term ε nat
test n m =
lambda _ _ (num _ n) ▸
call _ _ $0 ε ▸
lambda _ _ (num _ m) ▸
call _ _ $0 ε ▸
lambda (nat ∷ nat ∷ ε) _ (add _) ▸
call _ _ $0 ($1 ∷ $3 ∷ ε) ▸
ret $0
_ : Set
_ = {!eval (test 1 1)!}
{-
module Extra where
mutual
normValue : ∀ {τ} → (value : Value τ) → NormValue value
--normValue (#closure (env & term)) = normEnv env & goodTerm term
normValue _ = {!!}
--normValue (#closure closure) = goodClosure closure
--normValue (#tuple values) = normAllValues values
--normValue (#inj i value) = normValue value
--normValue #zero = tt
--normValue (#succ value) = normValue value
normAllValues : ∀ {τs} → (values : All Value τs) → All2 NormValue values
normAllValues ε = ε
normAllValues (value ∷ values) = normValue value ∷ normAllValues values
normEnv : ∀ {Γ} → (env : Env Γ) → NormEnv env
normEnv = {!!}
--normEnv ε = ε
--normEnv (value ∷ env) = normValue value ∷ normEnv env
goodClosure : ∀ {ρs τ} → (closure : Closure ρs τ) → GoodClosure closure
--goodClosure (env & term) norm-values = goodTerm term (norm-values ++2 normEnv env)
goodClosure (env & term) = {!!}
apply : ∀ {Γ τ} → Term Γ τ → Env Γ → Value τ
apply term env = result (goodTerm term (normEnv env))
-}