-
Notifications
You must be signed in to change notification settings - Fork 463
/
Algorithmic.lagda
203 lines (162 loc) · 4.97 KB
/
Algorithmic.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
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
\begin{code}
module Algorithmic where
\end{code}
## Imports
\begin{code}
open import Function hiding (_∋_)
open import Type
open import Type.BetaNormal
open import Type.BetaNBE
open import Type.BetaNBE.RenamingSubstitution renaming (_[_]Nf to _[_])
open import Builtin
open import Builtin.Signature
Ctx⋆ Kind ∅ _,⋆_ * _∋⋆_ Z S _⊢Nf⋆_ (ne ∘ `) con booleanNf
open import Builtin.Constant.Term Ctx⋆ Kind * _⊢Nf⋆_ con
open import Data.Product renaming (_,_ to _,,_)
open import Data.List hiding ([_])
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Unit
\end{code}
## Fixity declarations
To begin, we get all our infix declarations out of the way.
We list separately operators for judgements, types, and terms.
\begin{code}
infix 4 _∋_
infix 4 _⊢_
infixl 5 _,_
\end{code}
## Contexts and erasure
We need to mutually define contexts and their
erasure to type contexts.
\begin{code}
--data Ctx : Set
--∥_∥ : Ctx → Ctx⋆
\end{code}
A context is either empty, or extends a context by
a type variable of a given kind, or extends a context
by a variable of a given type.
\begin{code}
data Ctx : Ctx⋆ → Set where
∅ : Ctx ∅
_,⋆_ : ∀{Φ} → Ctx Φ → (J : Kind) → Ctx (Φ ,⋆ J)
_,_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Ctx Φ
\end{code}
Let `Γ` range over contexts. In the last rule,
the type is indexed by the erasure of the previous
context to a type context and a kind.
The erasure of a context is a type context.
\begin{code}
--∥ ∅ ∥ = ∅
--∥ Γ ,⋆ J ∥ = ∥ Γ ∥ ,⋆ J
--∥ Γ , A ∥ = ∥ Γ ∥
\end{code}
## Variables
A variable is indexed by its context and type.
\begin{code}
open import Type.BetaNormal.Equality
data _∋_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
Z : ∀ {Φ Γ} {A : Φ ⊢Nf⋆ *}
----------
→ Γ , A ∋ A
S : ∀ {Φ Γ} {A : Φ ⊢Nf⋆ *} {B : Φ ⊢Nf⋆ *}
→ Γ ∋ A
----------
→ Γ , B ∋ A
T : ∀ {Φ Γ K}{A : Φ ⊢Nf⋆ *}
→ Γ ∋ A
-------------------
→ Γ ,⋆ K ∋ weakenNf A
\end{code}
Let `x`, `y` range over variables.
## Terms
A term is indexed over by its context and type. A term is a variable,
an abstraction, an application, a type abstraction, or a type
application.
\begin{code}
open import Data.String
Tel : ∀ {Φ} Γ Δ → (∀ {J} → Δ ∋⋆ J → Φ ⊢Nf⋆ J) → List (Δ ⊢Nf⋆ *) → Set
data _⊢_ : ∀ {Φ} (Γ : Ctx Φ) → Φ ⊢Nf⋆ * → Set where
` : ∀ {Φ Γ} {A : Φ ⊢Nf⋆ *}
→ Γ ∋ A
------
→ Γ ⊢ A
ƛ : ∀ {Φ Γ}{A B : Φ ⊢Nf⋆ *}
→ Γ , A ⊢ B
-----------
→ Γ ⊢ A ⇒ B
_·_ : ∀ {Φ Γ}{A B : Φ ⊢Nf⋆ *}
→ Γ ⊢ A ⇒ B
→ Γ ⊢ A
-----------
→ Γ ⊢ B
Λ : ∀ {Φ Γ K}
→ {B : Φ ,⋆ K ⊢Nf⋆ *}
→ Γ ,⋆ K ⊢ B
----------
→ Γ ⊢ Π B
_·⋆_ : ∀ {Φ Γ K}
→ {B : Φ ,⋆ K ⊢Nf⋆ *}
→ Γ ⊢ Π B
→ (A : Φ ⊢Nf⋆ K)
---------------
→ Γ ⊢ B [ A ]
wrap1 : ∀{Φ Γ K}
→ (pat : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *)
→ (arg : Φ ⊢Nf⋆ K)
→ (term : Γ ⊢ nf (embNf pat · (μ1 · embNf pat) · embNf arg))
→ Γ ⊢ ne (μ1 · pat · arg)
unwrap1 : ∀{Φ Γ K}
→ {pat : Φ ⊢Nf⋆ (K ⇒ *) ⇒ K ⇒ *}
→ {arg : Φ ⊢Nf⋆ K}
→ (term : Γ ⊢ ne (μ1 · pat · arg))
→ Γ ⊢ nf (embNf pat · (μ1 · embNf pat) · embNf arg)
con : ∀{Φ}{Γ : Ctx Φ}{tcn}
→ TermCon {Φ} (con tcn)
-------------------
→ Γ ⊢ con tcn
builtin : ∀{Φ Γ}
→ (bn : Builtin)
→ let Δ ,, As ,, C = SIG bn in
(σ : ∀ {J} → Δ ∋⋆ J → Φ ⊢Nf⋆ J)
→ Tel Γ Δ σ As
-------------------------------
→ Γ ⊢ substNf σ C
error : ∀{Φ Γ} → (A : Φ ⊢Nf⋆ *) → Γ ⊢ A
Tel Γ Δ σ [] = ⊤
Tel Γ Δ σ (A ∷ As) = Γ ⊢ substNf σ A × Tel Γ Δ σ As
\end{code}
# Term Abbreviations
\begin{code}
--void : ∀{Γ} → Γ ⊢ unitNf
--void = Λ (ƛ (` Z))
true : ∀{Φ}{Γ : Ctx Φ} → Γ ⊢ booleanNf
true = Λ (ƛ (ƛ (` (S Z))))
false : ∀{Φ}{Γ : Ctx Φ} → Γ ⊢ booleanNf
false = Λ (ƛ (ƛ (` Z)))
\end{code}
Utility functions
\begin{code}
open import Type.BetaNormal.Equality
conv∋ : ∀ {Φ Γ Γ'}{A A' : Φ ⊢Nf⋆ *}
→ Γ ≡ Γ'
→ A ≡ A'
→ Γ ∋ A
→ Γ' ∋ A'
conv∋ refl refl x = x
open import Type.BetaNBE.Completeness
open import Type.Equality
open import Type.BetaNBE.RenamingSubstitution
conv⊢ : ∀ {Φ Γ Γ'}{A A' : Φ ⊢Nf⋆ *}
→ Γ ≡ Γ'
→ A ≡ A'
→ Γ ⊢ A
→ Γ' ⊢ A'
conv⊢ refl refl t = t
convTel : ∀ {Φ Ψ}{Γ Γ' : Ctx Φ}
→ Γ ≡ Γ'
→ (σ : ∀{J} → Ψ ∋⋆ J → Φ ⊢Nf⋆ J)
→ (As : List (Ψ ⊢Nf⋆ *))
→ Tel Γ Ψ σ As → Tel Γ' Ψ σ As
convTel p σ [] tt = tt
convTel p σ (A ∷ As) (t ,, ts) = conv⊢ p refl t ,, convTel p σ As ts
\end{code}