• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Jul 12th, 2019 66 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. open import Function
2. open import Data.Nat
3. open import Data.Fin renaming (_+_ to _f+_)
4. open import Data.Unit
5. open import Relation.Binary.PropositionalEquality
6. open import Data.Product
7. open import Data.Sum
8. open import Data.Vec
9. open import Data.Vec.Properties
10. import Level as L
11.
12. --------------------------------- Helpers --------------------------------------------
13.
14. fromℕ' : ∀ n → Fin (n + 1)
15. fromℕ' zero    = zero
16. fromℕ' (suc n) = suc (fromℕ' n)
17.
18. veclast :
19.   ∀ {a}{A : Set a} n x (xs : Vec A n)
20.   → lookup (xs ++ x ∷ []) (fromℕ' n) ≡ x
21. veclast zero x [] = refl
22. veclast (suc n) x (y ∷ ys) = veclast n x ys
23.
24. tighten : ∀ {n}(i : Fin (n + 1)) → (i ≡ fromℕ' n) ⊎ (∃ λ (i' : Fin n) → i ≡ inject+ 1 i')
25. tighten {zero} zero = inj₁ refl
26. tighten {zero} (suc ())
27. tighten {suc n} zero = inj₂ (zero , refl)
28. tighten {suc n} (suc i) with tighten {n} i
29. tighten {suc n} (suc .(fromℕ' n)) | inj₁ refl = inj₁ refl
30. tighten {suc n} (suc .(inject+ 1 proj₁)) | inj₂ (proj₁ , refl) = inj₂ (suc proj₁ , refl)
31.
32. ------------------------------------- Types -------------------------------------------
33.
34. infixr 5 _⇒_
35. data Type (f b : ℕ) : (level : ℕ) → Set  where
36.   free   : Fin f → Type f b zero
37.   bound  : Fin b → Type f b zero
38.   unit   : Type f b zero
39.   _⇒_    : ∀ {l1 l2} → Type f b l1 → Type f b l2 → Type f b (l1 ⊔ l2)
40.   ∀'     : ∀ {l} → Type f (suc b) l → Type f b (suc zero ⊔ l)
41.
42. relaxBound : ∀ {f b l} n → Type f b l → Type f (b + n) l
43. relaxBound n (free x)   = free x
44. relaxBound n (bound x)  = bound  (inject+ n x)
45. relaxBound n unit       = unit
46. relaxBound n (a ⇒ b)    = relaxBound n a ⇒ relaxBound n b
47. relaxBound n (∀' t)     = ∀' (relaxBound n t)
48.
49. raiseFree : ∀ {f b l} n → Type f b l → Type (n + f) b l
50. raiseFree n (free x)   = free (raise n x)
51. raiseFree n (bound x)  = bound x
52. raiseFree n unit       = unit
53. raiseFree n (a ⇒ b)    = raiseFree n a ⇒ raiseFree n b
54. raiseFree n (∀' x)     = ∀' (raiseFree n x)
55.
56. inst : ∀ {f b l} → Type f 0 zero → Type f (b + 1) l → Type f b l
57. inst t' (free x)         = free x
58. inst {_}{b} t' (bound x) = [ const (relaxBound b t') , bound ∘ proj₁ ]′ (tighten x)
59. inst t' unit             = unit
60. inst t' (a ⇒ b)          = inst t' a ⇒ inst t' b
61. inst t' (∀' x)           = ∀' (inst t' x)
62.
63. abst : ∀ {f b l} → Type (suc f) b l → Type f (b + 1) l
64. abst {_}{b}(free zero) = bound (fromℕ' b)
65. abst (free (suc x))    = free x
66. abst (bound x)         = bound (inject+ 1 x)
67. abst unit              = unit
68. abst (a ⇒ b)           = abst a ⇒ abst b
69. abst (∀' x)            = ∀' (abst x)
70.
71. -- ----------------------------------- Language -----------------------------------------------
72.
73. data Context : ℕ → Set where
74.   []   : Context 0
75.   term : ∀ {f l} → Type f 0 l → Context f → Context f
76.   type : ∀ {f}   → Context f → Context (suc f)
77.
78. data Var {l : ℕ} : ∀ {f} → Context f → Type f 0 l → Set where
79.   here : ∀ {f cxt t}       → Var {f = f}(term t cxt) t
80.   term : ∀ {f cxt t l' t'} → Var {l} cxt t → Var {f = f} (term {l = l'} t' cxt) t
81.   type : ∀ {f cxt t}       → Var cxt t → Var {f = suc f} (type cxt) (raiseFree 1 t)
82.
83. infixl 5 _\$'_
84.
85. data Term {f : ℕ} (cxt : Context f) : ∀ {l} → Type f 0 l → Set where
86.   unit  :                  Term cxt unit
87.   var   : ∀ {l t}        → Var {l} cxt t → Term cxt {l} t
88.   λ'    : ∀ {l1 l2 b} a  → Term (term {l = l1} a cxt) {l2} b → Term cxt {l1 ⊔ l2} (a ⇒ b)
89.   _\$'_  : ∀ {l1 l2 a b}  → Term cxt {l1 ⊔ l2} (a ⇒ b) → Term cxt {l1} a → Term cxt {l2} b
90.   Λ     : ∀ {l t}        → Term (type cxt) {l} t → Term cxt {suc zero ⊔ l}(∀' (abst t))
91.   _\$*_  : ∀ {l t}        → Term cxt (∀' {l = l} t) → (t' : Type f 0 zero) → Term cxt (inst t' t)
92.
93. -- ------------------------------------ Levels -----------------------------------------------
94.
95. getLevel : ∀ {f b l} → Type f b l → L.Level
96. getLevel (free x)  = L.zero
97. getLevel (bound x) = L.zero
98. getLevel unit      = L.zero
99. getLevel (a ⇒ b)   = getLevel a L.⊔ getLevel b
100. getLevel (∀' t)    = L.suc L.zero L.⊔ getLevel t
101.
102. level : ℕ → L.Level
103. level zero    = L.zero
104. level (suc n) = L.suc (level n)
105.
106. level-⊔ : ∀ l1 l2 → level l1 L.⊔ level l2 ≡ level (l1 ⊔ l2)
107. level-⊔ zero zero         = refl
108. level-⊔ zero (suc r2)     = refl
109. level-⊔ (suc r1) zero     = refl
110. level-⊔ (suc r1) (suc r2) = cong L.suc (level-⊔ r1 r2)
111.
112. level-subst : ∀ {l l'} → l ≡ l' → Set l → Set l'
113. level-subst refl x = x
114.
115. level-subst-remove : ∀ {l l' x} p  → level-subst{l}{l'} p x → x
116. level-subst-remove refl x₁ = x₁
117.
118. level-subst-add : ∀ {l l' x} p → x → level-subst{l}{l'} p x
119. level-subst-add refl x₁ = x₁
120.
121. level-cong : ∀ {f b l} → (t : Type f b l) → getLevel t ≡ level l
122. level-cong (free x) = refl
123. level-cong (bound x) = refl
124. level-cong unit = refl
125. level-cong (_⇒_ {la}{lb} a b) rewrite level-cong a | level-cong b = level-⊔ la lb
126. level-cong (∀' {l} t) rewrite level-cong t = level-⊔ (suc zero) l
127.
128. -- ----------------------------------- Interpretation ------------------------------------------
129.
130. interp : ∀ {f b l} → Vec Set f → Vec Set b → (t : Type f b l) → Set (getLevel t)
131. interp fs bs (free x)   = lookup fs x
132. interp fs bs (bound x)  = lookup bs x
133. interp fs bs unit       = ⊤
134. interp fs bs (a ⇒ b)    = interp fs bs a → interp fs bs b
135. interp fs bs (∀' t)     = ∀ (A : Set) → interp fs (A ∷ bs) t
136.
137. _⟦_⟧ : ∀ {f} fs → Type f 0 zero → Set
138. _⟦_⟧ fs t = level-subst (level-cong t) (interp fs [] t)
139.
140. iRaiseFree :
141.   ∀ {f b l bs fs x} t
142.   → interp{f}{b}{l} fs bs t
143.   → interp (x ∷ fs) bs (raiseFree 1 t)
144.
145. iRaiseFree' :
146.   ∀ {f b l bs fs x} t
147.   → interp (x ∷ fs) bs (raiseFree 1 t)
148.   → interp{f}{b}{l} fs bs t
149.
150. iRaiseFree (free x₁) y = y
151. iRaiseFree (bound x₁) y = y
152. iRaiseFree unit y = tt
153. iRaiseFree (a ⇒ b) f y = iRaiseFree b \$ f \$ iRaiseFree' a y
154. iRaiseFree (∀' t) g A = iRaiseFree t \$ g A
155.
156. iRaiseFree' (free x₁) y = y
157. iRaiseFree' (bound x₁) y = y
158. iRaiseFree' unit y = tt
159. iRaiseFree' (a ⇒ b) f y = iRaiseFree' b \$ f \$ iRaiseFree a y
160. iRaiseFree' (∀' t) g A = iRaiseFree' t \$ g A
161.
162. iRelaxBound :
163.   ∀ {b b' bs bs' f fs l} t
164.   → interp {f}{b}{l} fs bs t
165.   → interp fs (bs ++ bs') (relaxBound b' t)
166.
167. iRelaxBound' :
168.   ∀ {b b' bs bs' f fs l} t
169.   → interp fs (bs ++ bs') (relaxBound b' t)
170.   → interp {f}{b}{l} fs bs t
171.
172. iRelaxBound (free x) y = y
173. iRelaxBound {bs = bs}{bs' = bs'}(bound x) y rewrite lookup-++ˡ bs bs' x = y
174. iRelaxBound unit y = y
175. iRelaxBound (a ⇒ b) f y = iRelaxBound b \$ f \$ iRelaxBound' a y
176. iRelaxBound (∀' t) g A = iRelaxBound t \$ g A
177.
178. iRelaxBound' (free x) y = y
179. iRelaxBound' {bs = bs}{bs' = bs'}(bound x) y rewrite lookup-++ˡ bs bs' x = y
180. iRelaxBound' unit y = y
181. iRelaxBound' (a ⇒ b) f y = iRelaxBound' b \$ f \$ iRelaxBound a y
182. iRelaxBound' (∀' t) g A = iRelaxBound' t \$ g A
183.
184. iAbst :
185.   ∀ {f b l bs fs A} t
186.   → interp{suc f}{b}{l} (A ∷ fs) bs t
187.   → interp{f}{b + 1}{l} fs (bs ++ A ∷ []) (abst t)
188.
189. iAbst' :
190.   ∀ {f b l bs fs A} t
191.   → interp{f}{b + 1}{l} fs (bs ++ A ∷ []) (abst t)
192.   → interp{suc f}{b}{l} (A ∷ fs) bs t
193.
194. iAbst {f}{b}{bs = bs}{A = A}(free zero) y rewrite veclast b A bs = y
195. iAbst (free (suc x)) y = y
196. iAbst {bs = bs}{fs = fs}{A = A}(bound x) y rewrite lookup-++ˡ bs (A ∷ []) x = y
197. iAbst unit y = y
198. iAbst (a ⇒ b) f y = iAbst b \$ f \$ iAbst' a y
199. iAbst (∀' t) g A = iAbst t \$ g A
200.
201. iAbst' {f}{b}{bs = bs}{A = A}(free zero) y rewrite veclast b A bs = y
202. iAbst' (free (suc x)) y = y
203. iAbst' {bs = bs}{fs = fs}{A = A}(bound x) y rewrite lookup-++ˡ bs (A ∷ []) x = y
204. iAbst' unit y = y
205. iAbst' (a ⇒ b) f y = iAbst' b \$ f \$ iAbst a y
206. iAbst' (∀' t) g A = iAbst' t \$ g A
207.
208. iInst :
209.   ∀ {f b l fs bs t'} t
210.   → interp fs (bs ++ (fs ⟦ t' ⟧) ∷ []) t
211.   → interp {f}{b}{l} fs bs (inst t' t)
212.
213. iInst' :
214.   ∀ {f b l fs bs t'} t
215.   → interp {f}{b}{l} fs bs (inst t' t)
216.   → interp fs (bs ++ (fs ⟦ t' ⟧) ∷ []) t
217.
218. iInst (free x) y = y
219. iInst {b = b}(bound x) y with tighten{b} x
220. iInst {fs = fs}{bs = bs}{t' = t'}(bound ._) y | inj₁ refl
221.   rewrite veclast _ (fs ⟦ t' ⟧) bs = iRelaxBound t' (level-subst-remove (level-cong t') y)
222. iInst {fs = fs}{bs = bs}{t' = t'}(bound .(inject+ 1 i)) y | inj₂ (i , refl)
223.   rewrite lookup-++ˡ bs (fs ⟦ t' ⟧ ∷ []) i = y
224. iInst unit y = y
225. iInst {f}{b'}(a ⇒ b) g y = iInst{f}{b'} b \$ g \$ iInst'{f}{b'} a y
226. iInst {f}{b}(∀' t) g A = iInst {f} {suc b} t (g A)
227.
228. iInst' (free x) y = y
229. iInst' {b = b}(bound x) y with tighten {b} x
230. iInst' {fs = fs}{bs = bs}{t' = t'}(bound ._) y | inj₁ refl
231.   rewrite veclast _ (fs ⟦ t' ⟧) bs = level-subst-add (level-cong t') \$ iRelaxBound' t' y
232. iInst' {fs = fs}{bs = bs}{t' = t'}(bound .(inject+ 1 i)) y | inj₂ (i , refl)
233.   rewrite lookup-++ˡ bs (fs ⟦ t' ⟧ ∷ []) i = y
234. iInst' unit y = y
235. iInst' {f}{b'}(a ⇒ b) g y = iInst'{f}{b'} b \$ g \$ iInst{f}{b'} a y
236. iInst' {f}{b}(∀' t) g A = iInst' {f} {suc b} t (g A)
237.
238. -- ------------------------------------- Evaluation -----------------------------------------------
239.
240. data Env : ∀ {f} → Vec Set f → Context f → Set₁ where
241.   []   : Env [] []
242.   term : ∀ {f l ts cxt t} → interp {f}{0}{l} ts [] t → Env ts cxt → Env ts (term t cxt)
243.   type : ∀ {f ts cxt t} → Env {f} ts cxt → Env (t ∷ ts) (type cxt)
244.
245. lookupTerm : ∀ {l f fs cxt t} → Var {l} {f} cxt t → Env fs cxt → interp fs [] t
246. lookupTerm here             (term x env) = x
247. lookupTerm (term v)         (term x env) = lookupTerm v env
248. lookupTerm (type {t = t} v) (type env)   = iRaiseFree t \$ lookupTerm v env
249.
250. eval : ∀ {f l cxt fs t} → Env fs cxt → Term {f} cxt {l} t → interp fs [] t
251. eval env unit       = tt
252. eval env (var x)    = lookupTerm x env
253. eval env (λ' _ e) x = eval (term x env) e
254. eval env (f \$' x)   = eval env f (eval env x)
255. eval env (Λ {t = t} e) A = iAbst t \$ eval (type env) e
256. eval {fs = fs} env (_\$*_ {t = t} f t') = iInst {b = 0} t \$ eval env f (fs ⟦ t' ⟧)
257.
258. -- examples
259.
260. levelof : ∀ {l}{t : Type 0 0 l} → Term [] t → ℕ
261. levelof {l} _ = l
262.
263. -- Λ a. λ (x : a). x
264. ID : Term [] _
265. ID = Λ (λ' (free zero) (var here))
266.
267. -- Λ a b. λ (x : a) (y : b). x
268. CONST : Term [] _
269. CONST = Λ (Λ (λ' (free (suc zero)) (λ' (free zero) (var (term here)))))
270.
271. -- Λ a. λ (x : a). Λ b. λ (y : b). x
272. CONST' : Term [] _
273. CONST' = Λ (λ' (free zero) (Λ (λ' (free zero) (var (term (type here))))))
274.
275. -- Λ a. λ (id : Λ a. a → a) (x : a). id [a] x
276. IDAPP : Term [] _
277. IDAPP = Λ (λ' (∀' (bound zero ⇒ bound zero)) (λ' (free zero) (var (term here) \$* free zero  \$' var here)))
278.
279. evaltest : eval [] IDAPP ℕ (eval [] ID) 10 ≡ 10
280. evaltest = refl
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top