Introduce variable contexts.

1 files changed, 52 insertions, 21 deletions

diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda
index 754d92d..475968c 100644
--- a/src/Cfe/Judgement/Base.agda
+++ b/src/Cfe/Judgement/Base.agda
@@ -6,33 +6,64 @@ module Cfe.Judgement.Base
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open import Cfe.Expression over as E
+open import Cfe.Expression over renaming (shift to shiftₑ)
 open import Cfe.Type over renaming (_∙_ to _∙ₜ_; _∨_ to _∨ₜ_)
 open import Cfe.Type.Construct.Lift over
 open import Data.Fin as F
+open import Data.Fin.Properties
 open import Data.Nat as ℕ hiding (_⊔_)
-open import Data.Vec hiding (_⊛_)
+open import Data.Nat.Properties
+open import Data.Vec hiding (_⊛_) renaming (lookup to lookup′)
 open import Level hiding (Lift) renaming (suc to lsuc)
 open import Relation.Binary.PropositionalEquality
 
-infix 2 _,_⊢_∶_
-infix 4 _≅_
-
-data _,_⊢_∶_ : {m : ℕ} → {n : ℕ} → Vec (Type ℓ ℓ) m → Vec (Type ℓ ℓ) n → Expression (n ℕ.+ m) → Type ℓ ℓ → Set (c ⊔ lsuc ℓ) where
-  Eps : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} → Γ , Δ ⊢ ε ∶ Lift ℓ ℓ τε
-  Char : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} c → Γ , Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ]
-  Bot : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} → Γ , Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥
-  Var : ∀ {m n : ℕ} {Γ : Vec _ m} {Δ : Vec _ n} {i : Fin (n ℕ.+ m)} (i≥n : toℕ i ≥ n) → Γ , Δ ⊢ Var i ∶ lookup Γ (reduce≥ i i≥n)
-  Fix : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e τ} → Γ , τ ∷ Δ ⊢ e ∶ τ → Γ , Δ ⊢ μ e ∶ τ
-  Cat : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Δ ++ Γ , [] ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ , Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂
-  Vee : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Γ , Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ , Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂
-
-vcast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec A n
-vcast {n = ℕ.zero} eq [] = []
-vcast {n = suc n} eq (x ∷ xs) = x ∷ vcast (suc-injective eq) xs
+record Context n : Set (c ⊔ lsuc ℓ) where
+  field
+    m : ℕ
+    m≤n : m ℕ.≤ n
+    Γ : Vec (Type ℓ ℓ) (n ∸ m)
+    Δ : Vec (Type ℓ ℓ) m
+
+-- Fin n → Fin n∸m
+
+  lookup : (i : Fin n) → toℕ i ≥ m → Type ℓ ℓ
+  lookup i i≥m = lookup′ Γ (reduce≥
+      (F.cast (begin-equality
+        n ≡˘⟨ m+n∸m≡n m n ⟩
+        m ℕ.+ n ∸ m ≡⟨ +-∸-assoc m m≤n ⟩
+        m ℕ.+ (n ∸ m) ∎) i)
+      (begin
+        m ≤⟨ i≥m ⟩
+        toℕ i ≡˘⟨ toℕ-cast _ i ⟩
+        toℕ (F.cast _ i) ∎))
+    where
+    open ≤-Reasoning
+
+cons : ∀ {n} → Type ℓ ℓ → Context n → Context (suc n)
+cons {n} τ Γ,Δ = record
+  { m≤n = s≤s m≤n
+  ; Γ = Γ
+  ; Δ = τ ∷ Δ
+  }
   where
-  open import Data.Nat.Properties using (suc-injective)
+  open Context Γ,Δ
+
+shift : ∀ {n} → Context n → Context n
+shift {n} Γ,Δ = record
+  { m≤n = z≤n
+  ; Γ = subst (Vec (Type ℓ ℓ)) (trans (sym (+-∸-assoc m m≤n)) (m+n∸m≡n m n)) (Δ ++ Γ)
+  ; Δ = []
+  }
+  where
+  open Context Γ,Δ
+
+infix 2 _⊢_∶_
 
-data _≅_ {a A} : {m n : ℕ} → Vec {a} A m → Vec A n → Set a where
-  []≅[] : [] ≅ []
-  _∷_ : ∀ {m n x y} {xs : Vec _ m} {ys : Vec _ n} → (x≡y : x ≡ y) → xs ≅ ys → x ∷ xs ≅ y ∷ ys
+data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → Set (c ⊔ lsuc ℓ) where
+  Eps : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ε ∶ Lift ℓ ℓ τε
+  Char : ∀ {n} {Γ,Δ : Context n} c → Γ,Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ]
+  Bot : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥
+  Var : ∀ {n} {Γ,Δ : Context n} {i : Fin n} (i≥m : toℕ i ℕ.≥ Context.m Γ,Δ) → Γ,Δ ⊢ Var i ∶ Context.lookup Γ,Δ i i≥m
+  Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons τ Γ,Δ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ
+  Cat : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → shift Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ,Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂
+  Vee : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ,Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂