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. OK, I Understand
 
Top