-
Notifications
You must be signed in to change notification settings - Fork 463
/
Completeness.lagda
146 lines (125 loc) · 4.57 KB
/
Completeness.lagda
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
\begin{code}
module Algorithmic.Completeness where
open import Utils
open import Type
open import Type.Equality
open import Type.RenamingSubstitution
import Declarative as Syn
import Algorithmic as Norm
open import Type.BetaNormal
open import Type.BetaNormal.Equality
open import Type.BetaNBE
open import Type.BetaNBE.Completeness
open import Type.BetaNBE.RenamingSubstitution
open import Relation.Binary.PropositionalEquality renaming (subst to substEq) hiding ([_])
open import Function
open import Data.Vec hiding ([_];length)
open import Data.Sum
nfCtx : ∀ {Φ} → Syn.Ctx Φ → Norm.Ctx Φ
nfCtx Syn.∅ = Norm.∅
nfCtx (Γ Syn.,⋆ K) = nfCtx Γ Norm.,⋆ K
nfCtx (Γ Syn., A) = nfCtx Γ Norm., nf A
nfTyVar : ∀{Φ Γ}
→ {A : Φ ⊢⋆ *}
→ Γ Syn.∋ A
→ nfCtx Γ Norm.∋ nf A
nfTyVar Syn.Z = Norm.Z
nfTyVar (Syn.S α) = Norm.S (nfTyVar α)
nfTyVar (Syn.T {A = A} α) = Norm.conv∋ refl (ren-nf S A) (Norm.T (nfTyVar α))
open import Type.BetaNormal.Equality
lemΠ : ∀{Γ K }(B : Γ ,⋆ K ⊢⋆ *) →
nf (Π B) ≡ Π (nf B)
lemΠ B = cong Π (sym (subNf-lemma' B))
open import Type.BetaNBE.Soundness
stability-μ : ∀{Φ K}(A : Φ ⊢⋆ _)(B : Φ ⊢⋆ K) →
nf (A · ƛ (μ (weaken A) (` Z)) · B)
≡
nf (embNf (nf A) · ƛ (μ (embNf (weakenNf (nf A))) (` Z)) · embNf (nf B))
stability-μ A B = completeness
(·≡β
(·≡β
(soundness A)
(ƛ≡β (μ≡β (trans≡β
(soundness (ren S A))
(≡2β (sym (cong embNf (ren-nf S A))))) (refl≡β (` Z)))))
(soundness B))
open import Type.BetaNBE.Completeness
open import Type.BetaNBE.Soundness
open import Type.BetaNBE.Stability
lem[] : ∀{Γ K}(A : Γ ⊢⋆ K)(B : Γ ,⋆ K ⊢⋆ *) →
(nf B [ nf A ]Nf) ≡ nf (B [ A ])
lem[] A B = trans
(sub-eval (embNf (nf B)) idCR (embNf ∘ subNf-cons (ne ∘ `) (nf A)))
(trans
(fund
(λ {Z → symCR (fund idCR (soundness A)) ; (S α) → idCR _})
(sym≡β (soundness B)))
(sym (sub-eval B idCR (sub-cons ` A))))
open import Builtin hiding (length)
import Builtin.Constant.Term Ctx⋆ Kind * _⊢⋆_ con as STermCon
import Builtin.Constant.Term Ctx⋆ Kind * _⊢Nf⋆_ con as NTermCon
nfTypeTC : ∀{φ}{A : φ ⊢⋆ *} → STermCon.TermCon A → NTermCon.TermCon (nf A)
nfTypeTC (STermCon.integer i) = NTermCon.integer i
nfTypeTC (STermCon.bytestring b) = NTermCon.bytestring b
nfTypeTC (STermCon.string s) = NTermCon.string s
nfTypeTC (STermCon.bool b) = NTermCon.bool b
nfTypeTC STermCon.unit = NTermCon.unit
nfTypeTC (STermCon.Data d) = NTermCon.Data d
open import Data.Product renaming (_,_ to _,,_)
open import Data.List
lemσ : ∀{Γ Δ Δ'}
→ (σ : Sub Δ Γ)
→ (C : Δ ⊢⋆ *)
→ (C' : Δ' ⊢Nf⋆ *)
→ (q : Δ' ≡ Δ)
→ nf C ≡ substEq (_⊢Nf⋆ *) q C' →
subNf
(λ {J} α →
nf
(σ (substEq (_∋⋆ J) q α)))
C'
≡
nf (sub σ C)
lemσ σ C _ refl q = trans
(subNf-cong' (nf ∘ σ) (sym q))
(trans
(trans
(sub-eval (embNf (nf C)) idCR (embNf ∘ nf ∘ σ))
(fund (λ α → fund idCR (sym≡β (soundness (σ α)))) (sym≡β (soundness C))))
(sym (sub-eval C idCR σ)))
-- this should be a lemma in NBE/RenSubst
-- subNf (nf ∘ σ) (nf C) ≡ nf (sub σ C)
open import Builtin.Constant.Type Ctx⋆ (_⊢Nf⋆ *)
nfList : ∀{Δ} → List (Δ ⊢⋆ *) → List (Δ ⊢Nf⋆ *)
nfList [] = []
nfList (A ∷ As) = nf A ∷ nfList As
postulate btype-lem : ∀ {Φ} b → Norm.btype {Φ} b ≡ nf (Syn.btype b)
nfType : ∀{Φ Γ}
→ {A : Φ ⊢⋆ *}
→ Γ Syn.⊢ A
→ nfCtx Γ Norm.⊢ nf A
nfType (Syn.` α) = Norm.` (nfTyVar α)
nfType (Syn.ƛ t) = Norm.ƛ (nfType t)
nfType (t Syn.· u) = nfType t Norm.· nfType u
nfType (Syn.Λ {B = B} t) =
Norm.Λ (Norm.conv⊢ refl (subNf-lemma' B) (nfType t))
nfType (Syn._·⋆_ {B = B} t A) = Norm.conv⊢
refl
(lem[] A B)
(Norm._·⋆_ (Norm.conv⊢ refl (lemΠ B) (nfType t)) (nf A))
nfType (Syn.wrap A B t) = Norm.wrap
(nf A)
(nf B)
(Norm.conv⊢ refl (stability-μ A B) (nfType t))
nfType (Syn.unwrap {A = A}{B = B} t) = Norm.conv⊢
refl
(sym (stability-μ A B))
(Norm.unwrap (nfType t))
nfType (Syn.conv p t) = Norm.conv⊢ refl (completeness p) (nfType t)
nfType (Syn.con t) = Norm.con (nfTypeTC t)
nfType (Syn.builtin b) = Norm.conv⊢ refl (btype-lem b) (Norm.builtin b)
nfType (Syn.error A) = Norm.error (nf A)
completenessT : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ Syn.⊢ A
→ nfCtx Γ Norm.⊢ nf A × (A ≡β embNf (nf A))
completenessT {A = A} t = nfType t ,, soundness A
\end{code}