Rework Context one last time.

1 files changed, 44 insertions, 74 deletions

diff --git a/src/Cfe/Context/Base.agda b/src/Cfe/Context/Base.agda
index a428d3c..e152790 100644
--- a/src/Cfe/Context/Base.agda
+++ b/src/Cfe/Context/Base.agda
@@ -6,91 +6,61 @@ module Cfe.Context.Base
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open import Cfe.Type over
-open import Data.Empty
-open import Data.Fin as F hiding (cast)
-open import Data.Fin.Properties hiding (≤-trans)
-open import Data.Nat as ℕ hiding (_⊔_)
-open import Data.Nat.Properties as NP
-open import Data.Product
-open import Data.Vec
+open import Cfe.Fin
+open import Cfe.Type over using (Type) renaming (_≈_ to _≈ᵗ_; _≤_ to _≤ᵗ_)
+open import Data.Fin hiding (_+_) renaming (zero to #0; suc to 1+_; _≤_ to _≤ᶠ_)
+open import Data.Fin.Properties using (toℕ-fromℕ; toℕ-inject₁)
+open import Data.Nat using (ℕ; suc; _∸_; _+_)
+open import Data.Nat.Properties using (+-suc)
+open import Data.Product using (_×_)
+open import Data.Vec using (Vec; []; insert)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (Pointwise)
 open import Level renaming (suc to lsuc)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; module ≡-Reasoning)
+open import Relation.Nullary.Decidable using (True)
 
-drop′ : ∀ {a A n m i} → m ℕ.≤ n → i ℕ.≤ m → Vec {a} A (m ℕ.+ (n ∸ m)) → Vec A (n ∸ i)
-drop′ z≤n z≤n xs = xs
-drop′ (s≤s m≤n) z≤n (x ∷ xs) = x ∷ drop′ m≤n z≤n xs
-drop′ (s≤s m≤n) (s≤s i≤m) (x ∷ xs) = drop′ m≤n i≤m xs
+private
+  variable
+    n : ℕ
 
-take′ : ∀ {a A m i} → i ℕ.≤ m → Vec {a} A m → Vec A i
-take′ z≤n xs = []
-take′ (s≤s i≤m) (x ∷ xs) = x ∷ (take′ i≤m xs)
+------------------------------------------------------------------------
+-- Definitions
 
-reduce≥′ : ∀ {n m i} → m ℕ.≤ n → toℕ {n} i ≥ m → Fin (n ∸ m)
-reduce≥′ {i = i} z≤n i≥m = i
-reduce≥′ {i = suc i} (s≤s m≤n) (s≤s i≥m) = reduce≥′ m≤n i≥m
+infix 4 _⊐_
 
-reduce≥′-mono : ∀ {n m i j} → (m≤n : m ℕ.≤ n) → (i≥m : toℕ i ≥ m) → (i≤j : i F.≤ j) → reduce≥′ m≤n i≥m F.≤ reduce≥′ m≤n (≤-trans i≥m i≤j)
-reduce≥′-mono z≤n i≥m i≤j = i≤j
-reduce≥′-mono {i = suc i} {suc j} (s≤s m≤n) (s≤s i≥m) (s≤s i≤j) = reduce≥′-mono m≤n i≥m i≤j
+record Context n : Set (c ⊔ lsuc ℓ) where
+  constructor _⊐_
+  field
+    Γ,Δ     : Vec (Type ℓ ℓ) n
+    guard   : Fin (suc n)
 
-insert′ : ∀ {a A n m} → Vec {a} A (n ∸ suc m) → suc m ℕ.≤ n → Fin (n ∸ m) → A → Vec A (n ∸ m)
-insert′ xs (s≤s z≤n) i x = insert xs i x
-insert′ xs (s≤s (s≤s m≤n)) i x = insert′ xs (s≤s m≤n) i x
+open Context public
 
-rotate : ∀ {a A n} {i j : Fin n} → Vec {a} A n → i F.≤ j → Vec A n
-rotate {i = F.zero} {j} (x ∷ xs) z≤n = insert xs j x
-rotate {i = suc i} {suc j} (x ∷ xs) (s≤s i≤j) = x ∷ (rotate xs i≤j)
+∙,∙ : Context 0
+∙,∙ = [] ⊐ #0
 
-remove′ : ∀ {a A n} → Vec {a} A n → Fin n → Vec A (ℕ.pred n)
-remove′ (x ∷ xs) F.zero = xs
-remove′ (x ∷ y ∷ xs) (suc i) = x ∷ remove′ (y ∷ xs) i
+------------------------------------------------------------------------
+-- Insertions
 
-record Context n : Set (c ⊔ lsuc ℓ) where
-  field
-    m : ℕ
-    m≤n : m ℕ.≤ n
-    Γ : Vec (Type ℓ ℓ) (n ∸ m)
-    Δ : Vec (Type ℓ ℓ) m
+wkn₂ : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Type ℓ ℓ → Context (suc n)
+wkn₂ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (inject<! i) τ ⊐ 1+ g
 
-∙,∙ : Context 0
-∙,∙ = record { m≤n = z≤n ; Γ = [] ; Δ = [] }
-
-toVec : ∀ {n} → Context n → Vec (Type ℓ ℓ) n
-toVec record { m = .0 ; m≤n = _ ; Γ = Γ ; Δ = [] } = Γ
-toVec {suc n} record { m = .(suc _) ; m≤n = (s≤s m≤n) ; Γ = Γ ; Δ = (x ∷ Δ) } = x ∷ toVec (record { m≤n = m≤n ; Γ = Γ ; Δ = Δ })
-
-wkn₁ : ∀ {n i} → (Γ,Δ : Context n) → toℕ {suc n} i ≥ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n)
-wkn₁ Γ,Δ i≥m τ = record
-  { m≤n = ≤-step m≤n
-  ; Γ = insert′ Γ (s≤s m≤n) (reduce≥′ (≤-step m≤n) i≥m) τ
-  ; Δ = Δ
-  }
-  where
-  open Context Γ,Δ
-
-wkn₂ : ∀ {n i} → (Γ,Δ : Context n) → toℕ {suc n} i ℕ.≤ Context.m Γ,Δ → Type ℓ ℓ → Context (suc n)
-wkn₂ Γ,Δ i≤m τ = record
-  { m≤n = s≤s m≤n
-  ; Γ = Γ
-  ; Δ = insert Δ (fromℕ< (s≤s i≤m)) τ
-  }
-  where
-  open Context Γ,Δ
+wkn₁ : ∀ (ctx : Context n) → Fin> (guard ctx) → Type ℓ ℓ → Context (suc n)
+wkn₁ (Γ,Δ ⊐ g) i τ = insert Γ,Δ (raise> i) τ ⊐ inject₁ g
+
+------------------------------------------------------------------------
+-- Modifications
+
+shift : ∀ (ctx : Context n) → Fin< (1+ guard ctx) → Context n
+shift (Γ,Δ ⊐ _) i = Γ,Δ ⊐ inject<! i
 
-shift≤ : ∀ {n i} (Γ,Δ : Context n) → i ℕ.≤ Context.m Γ,Δ → Context n
-shift≤ {n} {i} record { m = m ; m≤n = m≤n ; Γ = Γ ; Δ = Δ } i≤m = record
-  { m≤n = ≤-trans i≤m m≤n
-  ; Γ = drop′ m≤n i≤m (Δ ++ Γ)
-  ; Δ = take′ i≤m Δ
-  }
+------------------------------------------------------------------------
+-- Relations
 
-cons : ∀ {n} → Context n → Type ℓ ℓ → Context (suc n)
-cons Γ,Δ τ = wkn₂ Γ,Δ z≤n τ
+-- infix 4 _≈_ _≤_
 
-shift : ∀ {n} → Context n → Context n
-shift Γ,Δ = shift≤ Γ,Δ z≤n
+_≈_ : Rel (Context n) _
+(Γ,Δ₁ ⊐ g₁) ≈ (Γ,Δ₂ ⊐ g₂) = g₁ ≡ g₂ × Pointwise _≈ᵗ_ Γ,Δ₁ Γ,Δ₂
 
-_≋_ : ∀ {n} → Rel (Context n) (c ⊔ lsuc ℓ)
-Γ,Δ ≋ Γ,Δ′ = Σ (Context.m Γ,Δ ≡ Context.m Γ,Δ′) λ {refl → Context.Γ Γ,Δ ≡ Context.Γ Γ,Δ′ × Context.Δ Γ,Δ ≡ Context.Δ Γ,Δ′}
+_≤_ : Rel (Context n) _
+(Γ,Δ₁ ⊐ g₁) ≤ (Γ,Δ₂ ⊐ g₂) = g₂ ≤ᶠ g₁ × Pointwise _≤ᵗ_ Γ,Δ₁ Γ,Δ₂