backing up before changes to TypedDB

src/Typed.lagda

@@ -12,11 +12,11 @@ module Typed where
 
 \begin{code}
 import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_; refl; sym; trans; cong; _≢_)
+open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≟_)
+open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_)
-open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n)
--- open import Data.String using (String; _≟_)
+open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
 open import Data.Unit using (⊤; tt)
 open import Function using (_∘_)
 open import Function.Equivalence using (_⇔_; equivalence)
@@ -31,14 +31,15 @@ open import Relation.Nullary.Product using (_×-dec_)
 
 \begin{code}
 infixr 6 _⇒_
-infixl 5 _,_∈_
+infixl 5 _,_⦂_
-infix  4 _⊧_∈_
+infix  4 _∋_⦂_
-infix  4 _⊢_∈_
+infix  4 _⊢_⦂_
-infix  5 ƛ_∈_⇒_
+infix  5 ƛ_⦂_⇒_
+infix  5 ƛ_
 infixl 6 _·_
 
-data Id : Set where
+Id : Set
-  id : ℕ → Id
+Id = ℕ
 
 data Type : Set where
   o   : Type
@@ -46,54 +47,59 @@ data Type : Set where
 
 data Env : Set where
   ε     : Env
-  _,_∈_ : Env → Id → Type → Env
+  _,_⦂_ : Env → Id → Type → Env
 
 data Term : Set where
   ⌊_⌋      : Id → Term
-  ƛ_∈_⇒_  : Id → Type → Term → Term
+  ƛ_⦂_⇒_  : Id → Type → Term → Term
   _·_     : Term → Term → Term  
 
-data _⊧_∈_ : Env → Id → Type → Set where
+data _∋_⦂_ : Env → Id → Type → Set where
 
   Z : ∀ {Γ A x} →
     -----------------
-    Γ , x ∈ A ⊧ x ∈ A
+    Γ , x ⦂ A ∋ x ⦂ A
 
   S : ∀ {Γ A B x y} →
     x ≢ y →
-    Γ ⊧ x ∈ A →
+    Γ ∋ y ⦂ B →
     -----------------
-    Γ , y ∈ B ⊧ x ∈ A
+    Γ , x ⦂ A ∋ y ⦂ B
 
-data _⊢_∈_ : Env → Term → Type → Set where
+data _⊢_⦂_ : Env → Term → Type → Set where
 
-  Ax : ∀ {Γ A x} →
+  ⌊_⌋ : ∀ {Γ A x} →
-    Γ ⊧ x ∈ A →
+    Γ ∋ x ⦂ A →
     ---------------------
-    Γ ⊢ ⌊ x ⌋ ∈ A
+    Γ ⊢ ⌊ x ⌋ ⦂ A
 
-  ⇒-I  :  ∀ {Γ A B x N} →
+  ƛ_ :  ∀ {Γ x A N B} →
-    Γ , x ∈ A ⊢ N ∈ B →
+    Γ , x ⦂ A ⊢ N ⦂ B →
     --------------------------
-    Γ ⊢ (ƛ x ∈ A ⇒ N) ∈ A ⇒ B
+    Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ A ⇒ B
 
-  ⇒-E : ∀ {Γ A B L M} →
+  _·_ : ∀ {Γ L M A B} →
-    Γ ⊢ L ∈ A ⇒ B →
+    Γ ⊢ L ⦂ A ⇒ B →
-    Γ ⊢ M ∈ A →
+    Γ ⊢ M ⦂ A →
     --------------
-    Γ ⊢ L · M ∈ B
+    Γ ⊢ L · M ⦂ B
 \end{code}
 
 ## Decide whether environments and types are equal
 
 \begin{code}
 _≟I_ : ∀ (x y : Id) → Dec (x ≡ y)
-(id s) ≟I (id t) with s ≟ t
+_≟I_ = _≟_
-...                 | yes refl = yes refl
+
-...                 | no s≢t = no (f s≢t)
+{-
+_≟I_ : ∀ (x y : Id) → Dec (x ≡ y)
+(id m) ≟I (id n) with m ≟ n
+...                 | yes refl  =  yes refl
+...                 | no  m≢n   =  no (f m≢n)
   where
-  f : ∀ {s t : ℕ} → s ≢ t → id s ≢ id t
+  f : ∀ {m n : ℕ} → m ≢ n → id m ≢ id n
-  f s≢t refl = s≢t refl
+  f m≢n refl = m≢n refl
+-}
 
 _≟T_ : ∀ (A B : Type) → Dec (A ≡ B)
 o ≟T o = yes refl
@@ -108,13 +114,13 @@ o ≟T (A′ ⇒ B′) = no (λ())
 
 _≟E_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
 ε ≟E ε = yes refl
-ε ≟E (Γ , x ∈ A) = no (λ())
+ε ≟E (Γ , x ⦂ A) = no (λ())
-(Γ , x ∈ A) ≟E ε = no (λ())
+(Γ , x ⦂ A) ≟E ε = no (λ())
-(Γ , x ∈ A) ≟E (Δ , y ∈ B) = map (equivalence obv1 obv2) ((Γ ≟E Δ) ×-dec ((x ≟I y) ×-dec (A ≟T B)))
+(Γ , x ⦂ A) ≟E (Δ , y ⦂ B) = map (equivalence obv1 obv2) ((Γ ≟E Δ) ×-dec ((x ≟I y) ×-dec (A ≟T B)))
   where
-  obv1 : ∀ {Γ Δ A B x y} → (Γ ≡ Δ) × ((x ≡ y) × (A ≡ B)) → (Γ , x ∈ A) ≡ (Δ , y ∈ B)
+  obv1 : ∀ {Γ Δ A B x y} → (Γ ≡ Δ) × ((x ≡ y) × (A ≡ B)) → (Γ , x ⦂ A) ≡ (Δ , y ⦂ B)
   obv1 ⟨ refl , ⟨ refl , refl ⟩ ⟩ = refl
-  obv2 : ∀ {Γ Δ A B} → (Γ , x ∈ A) ≡ (Δ , y ∈ B) → (Γ ≡ Δ) × ((x ≡ y) × (A ≡ B))
+  obv2 : ∀ {Γ Δ A B} → (Γ , x ⦂ A) ≡ (Δ , y ⦂ B) → (Γ ≡ Δ) × ((x ≡ y) × (A ≡ B))
   obv2 refl = ⟨ refl , ⟨ refl , refl ⟩ ⟩
 \end{code}
 
@@ -123,40 +129,40 @@ _≟E_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
 
 \begin{code}
 m n s z : Id
-m = id 0
+m = 0
-n = id 1
+n = 1
-s = id 2
+s = 2
-z = id 3
+z = 3
 
 Ch : Type
 Ch = (o ⇒ o) ⇒ o ⇒ o
 
 two : Term
-two = ƛ s ∈ (o ⇒ o) ⇒ ƛ z ∈ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))
+two = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))
 
-two⊢ : ε ⊢ two ∈ Ch
+⊢two : ε ⊢ two ⦂ Ch
-two⊢ = ⇒-I (⇒-I (⇒-E (Ax (S (λ()) Z)) (⇒-E (Ax (S (λ()) Z)) (Ax Z))))
+⊢two = ƛ ƛ (⌊ S (λ()) Z ⌋ · (⌊ S (λ()) Z ⌋ · ⌊ Z ⌋))
 
 four : Term
-four = ƛ s ∈ (o ⇒ o) ⇒ ƛ z ∈ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))))
+four = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))))
 
-four⊢ : ε ⊢ four ∈ Ch
+⊢four : ε ⊢ four ⦂ Ch
-four⊢ = ⇒-I (⇒-I (⇒-E (Ax (S (λ()) Z)) (⇒-E (Ax (S (λ()) Z))
+⊢four = ƛ ƛ (⌊ S (λ()) Z ⌋ · (⌊ S (λ()) Z ⌋ ·
-          (⇒-E (Ax (S (λ()) Z)) (⇒-E (Ax (S (λ ()) Z)) (Ax Z))))))
+              (⌊ S (λ()) Z ⌋ · (⌊ S (λ()) Z ⌋ · ⌊ Z ⌋))))
 
 plus : Term
-plus = ƛ m ∈ Ch ⇒ ƛ n ∈ Ch ⇒ ƛ s ∈ (o ⇒ o) ⇒ ƛ z ∈ o ⇒ ⌊ m ⌋ · ⌊ s ⌋ · (⌊ n ⌋ · ⌊ s ⌋ · ⌊ z ⌋)
+plus = ƛ m ⦂ Ch ⇒ ƛ n ⦂ Ch ⇒ ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒
+         ⌊ m ⌋ · ⌊ s ⌋ · (⌊ n ⌋ · ⌊ s ⌋ · ⌊ z ⌋)
 
-plus⊢ : ε ⊢ plus ∈ Ch ⇒ Ch ⇒ Ch
+⊢plus : ε ⊢ plus ⦂ Ch ⇒ Ch ⇒ Ch
-plus⊢ = ⇒-I (⇒-I (⇒-I (⇒-I
+⊢plus = ƛ (ƛ (ƛ (ƛ ((⌊ (S (λ ()) (S (λ ()) (S (λ ()) Z))) ⌋ · ⌊ S (λ ()) Z ⌋) ·
-          (⇒-E (⇒-E (Ax (S (λ ()) (S (λ ()) (S (λ ()) Z)))) (Ax (S (λ ()) Z)))
+          (⌊ S (λ ()) (S (λ ()) Z) ⌋ · ⌊ S (λ ()) Z ⌋ · ⌊ Z ⌋)))))
-            (⇒-E (⇒-E (Ax (S (λ ()) (S (λ ()) Z))) (Ax (S (λ ()) Z))) (Ax Z))))))
 
 four′ : Term
 four′ = plus · two · two
 
-four′⊢ : ε ⊢ four′ ∈ Ch
+⊢four′ : ε ⊢ four′ ⦂ Ch
-four′⊢ = ⇒-E (⇒-E plus⊢ two⊢) two⊢
+⊢four′ = ⊢plus · ⊢two · ⊢two
 \end{code}
 
 # Denotational semantics
@@ -168,36 +174,115 @@ four′⊢ = ⇒-E (⇒-E plus⊢ two⊢) two⊢
 
 ⟦_⟧ᴱ : Env → Set
 ⟦ ε ⟧ᴱ          =  ⊤
-⟦ Γ , x ∈ A ⟧ᴱ  =  ⟦ Γ ⟧ᴱ × ⟦ A ⟧ᵀ
+⟦ Γ , x ⦂ A ⟧ᴱ  =  ⟦ Γ ⟧ᴱ × ⟦ A ⟧ᵀ
 
-⟦_⟧ⱽ : ∀ {Γ x A} → Γ ⊧ x ∈ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
+⟦_⟧ⱽ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
 ⟦ Z ⟧ⱽ     ⟨ ρ , v ⟩ = v
-⟦ S _ n ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ n ⟧ⱽ ρ
+⟦ S _ x ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ x ⟧ⱽ ρ
 
-⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ∈ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
+⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
-⟦ Ax n ⟧      ρ  =  ⟦ n ⟧ⱽ ρ
+⟦ ⌊ x ⌋ ⟧   ρ  =  ⟦ x ⟧ⱽ ρ
-⟦ ⇒-I N⊢ ⟧    ρ  =  λ{ v → ⟦ N⊢ ⟧ ⟨ ρ , v ⟩ }
+⟦ ƛ ⊢N ⟧    ρ  =  λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ }
-⟦ ⇒-E L⊢ M⊢ ⟧ ρ  =  (⟦ L⊢ ⟧ ρ) (⟦ M⊢ ⟧ ρ)
+⟦ ⊢L · ⊢M ⟧ ρ  =  (⟦ ⊢L ⟧ ρ) (⟦ ⊢M ⟧ ρ)
 
-_ : ⟦ four⊢ ⟧ tt ≡ ⟦ four′⊢ ⟧ tt
+_ : ⟦ ⊢four′ ⟧ tt ≡ ⟦ ⊢four ⟧ tt
 _ = refl
 
-_ : ⟦ four⊢ ⟧ tt suc zero ≡ 4
+_ : ⟦ ⊢four ⟧ tt suc zero ≡ 4
 _ = refl
 \end{code}
 
 ## Operational semantics - with simultaneous substitution, a la McBride
 
+## Biggest identifier
+
+\begin{code}
+lemma : ∀ {y z} → y ≤ z → y ≢ 1 + z
+lemma {y} {z} y≤z y≡1+z = 1+n≰n (≤-trans 1+z≤y y≤z)
+  where
+  1+z≤y : 1 + z ≤ y
+  1+z≤y rewrite y≡1+z = ≤-refl
+
+emp≤ : ∀ {y B z} → ε ∋ y ⦂ B → y ≤ z
+emp≤ ()
+
+ext≤ : ∀ {Γ x z A} → (∀ {y B} → Γ ∋ y ⦂ B → y ≤ z) → x ≤ z → (∀ {y B} → Γ , x ⦂ A ∋ y ⦂ B → y ≤ z)
+ext≤ ρ x≤z Z        =  x≤z
+ext≤ ρ x≤z (S _ k)  =  ρ k
+
+fresh : ∀ (Γ : Env) → ∃[ z ] (∀ {y B} → Γ ∋ y ⦂ B → y ≤ z)
+fresh ε                           = ⟨ 0 , emp≤ ⟩
+fresh (Γ , x ⦂ A) with fresh Γ
+...                  | ⟨ z , ρ ⟩  = ⟨ w , ext≤ ((λ y≤z → ≤-trans y≤z z≤w) ∘ ρ) x≤w ⟩
+  where
+  w   = x ⊔ z
+  z≤w = n≤m⊔n x z
+  x≤w = m≤m⊔n x z
+\end{code}
+
+## Erasure
+
+\begin{code}
+lookup : ∀ {Γ x A} → Γ ∋ x ⦂ A → Id
+lookup {Γ , x ⦂ A} Z        =  x
+lookup {Γ , x ⦂ A} (S _ k)  =  lookup {Γ} k
+
+erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term
+erase ⌊ k ⌋                     =  ⌊ lookup k ⌋
+erase (ƛ_ {x = x} {A = A} ⊢N)   =  ƛ x ⦂ A ⇒ erase ⊢N
+erase (⊢L · ⊢M)                 =  erase ⊢L · erase ⊢M
+
+lookup-lemma : ∀ {Γ x A} → (k : Γ ∋ x ⦂ A) → lookup k ≡ x
+lookup-lemma Z        =  refl
+lookup-lemma (S _ k)  =  lookup-lemma k
+
+erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M
+erase-lemma ⌊ k ⌋                    =  cong ⌊_⌋ (lookup-lemma k)
+erase-lemma (ƛ_ {x = x} {A = A} ⊢N)  =  cong (ƛ x ⦂ A ⇒_) (erase-lemma ⊢N)
+erase-lemma (⊢L · ⊢M)                =  cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
+\end{code}
+
 ## Renaming
 
 \begin{code}
-ext⊧ : ∀ {Γ Δ x A} → (∀ {y B} → Γ ⊧ y ∈ B → Δ ⊧ y ∈ B) → Δ ⊧ x ∈ A → (∀ {y B} → Γ , x ∈ A ⊧ y ∈ B → Δ ⊧ y ∈ B)
+rename : ∀ {Γ} → (∀ {y B} → Γ ∋ y ⦂ B → Id) → (∀ {M A} → Γ ⊢ M ⦂ A → Term)
-ext⊧ ρ j Z        =  j
+rename ρ (⌊ k ⌋)                       =  ⌊ ρ k ⌋
-ext⊧ ρ j (S _ k)  =  ρ k
+rename ρ (⊢L · ⊢M)                     =  (rename ρ ⊢L) · (rename ρ ⊢M)
+rename {Γ} ρ (ƛ_ {x = x} {A = A} ⊢N)   =  ƛ x′ ⦂ A ⇒ (rename ρ′ ⊢N)
+  where
+  x′    : Id
+  x′    = 1 + proj₁ (fresh Γ)
+  ρ′ : ∀ {y B} → Γ , x ⦂ A ∋ y ⦂ B → Id
+  ρ′ Z        =  x′
+  ρ′ (S _ j)  =  ρ j
 
-rename⊢ : ∀ {Γ Δ} → (∀ {y B} → Γ ⊧ y ∈ B → Δ ⊧ y ∈ B) → (∀ {M A} → Γ ⊢ M ∈ A → Δ ⊢ M ∈ A)
+{-
-rename⊢ ρ (Ax n)       =  Ax (ρ n)
+⊢rename : ∀ {Γ Δ} → (ρ : ∀ {y B} → Γ ∋ y ⦂ B → ∃[ y′ ] (Δ ∋ y′ ⦂ B)) →
-rename⊢ ρ (⇒-I N⊢)     =  ⇒-I (rename⊢ (ext⊧ (S ? ∘ ρ) Z) N⊢)
+                       (∀ {M A} → (⊢M : Γ ⊢ M ⦂ A) → Δ ⊢ rename (proj₁ ∘ ρ) ⊢M ⦂ A)
-rename⊢ ρ (⇒-E L⊢ M⊢)  =  ⇒-E (rename⊢ ρ L⊢) (rename⊢ ρ M⊢)
+⊢rename ρ (⌊ k ⌋)                       =  ⌊ proj₂ (ρ k) ⌋
+⊢rename ρ (⊢L · ⊢M)                     =  (⊢rename ρ ⊢L) · (⊢rename ρ ⊢M)
+⊢rename {Γ} ρ (ƛ_ {x = x} {A = A} ⊢N)
+  with fresh Γ
+  ... | ⟨ w , σ ⟩                       =  ƛ x′ ⦂ A ⇒ (rename ρ′ ⊢N)
+  where
+  x′    : Id
+  x′    = 1 + w
+  ρ′ : ∀ {y B} → Γ , x ⦂ A ∋ y ⦂ B → ∃[ y′ ] (Δ ∋ y′ ⦂ B)
+  ρ′ Z        =  x′
+  ρ′ (S _ j)  =  ρ j
+-}
+
+
+ext∋ : ∀ {Γ Δ x A} → (∀ {y B} → Γ ∋ y ⦂ B → Δ ∋ y ⦂ B) → Δ ∋ x ⦂ A → (∀ {y B} → Γ , x ⦂ A ∋ y ⦂ B → Δ ∋ y ⦂ B)
+ext∋ ρ j Z        =  j
+ext∋ ρ j (S _ k)  =  ρ k
+
+
+{-
+⊢rename : ∀ {Γ Δ} → (ρ : ∀ {y B} → Γ ∋ y ⦂ B → Δ ∋ y ⦂ B) → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ rename ρ M ⦂ A)
+⊢rename ρ (⌊ x ⌋)    =  ⌊ ρ x ⌋
+⊢rename ρ (ƛ ⊢N)     =  ƛ (⊢rename (ext∋ (S {!!} ∘ ρ) Z) ⊢N)
+⊢rename ρ (⊢L · ⊢M)  =  (⊢rename ρ ⊢L) · (⊢rename ρ ⊢M)
+-}
 \end{code}