{-# OPTIONS --safe #-}
module CtxTyp.Term where
open import Relation.Nullary using (¬_)
open import Function.Base using (id; _∘_)
open import Data.Nat.Base using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step)
open import CtxTyp.Context
data Term : (n : ℕ) → Context n → Type n → Set
infix 4 Term
syntax Term n Γ A = Γ ⊢ A ^ n
infix 4 _⊩_
infix 4 _⊩[_⊢_^_]
infixl 5 _,_
infixl 5 _++ˢ_
data _⊩[_⊢_^_] Γ′ {m} (Δ : Context m) (A : Type m) (m≥n : m ≥‴ n) : Set where
term
: (e : Γ′ ↾≥ m≥n ++ Δ ⊢ A ^ m)
→ Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
var
: (x : Γ′ ∋[ Δ ⊢ A ^ m≥n ])
→ Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
data _⊩_ (Γ′ : Context n) : Context n → Set where
∅ : Γ′ ⊩ ∅
_,_ : (σ : Γ′ ⊩ Γ) → (item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]) → Γ′ ⊩ Γ ,[ Δ ⊢ A ^ m≥n ]
lookup : Γ′ ⊩ Γ → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
lookup (σ , e) Z = e
lookup (σ , e) (S x) = lookup σ x
_++ˢ_ : Γ′ ⊩ Γ → Γ′ ⊩ Δ → Γ′ ⊩ Γ ++ Δ
σ ++ˢ ∅ = σ
σ ++ˢ (σ′ , item) = σ ++ˢ σ′ , item
Subst : Context n → Context n → Set
Subst Γ Γ′ = Γ′ ⊩ Γ
infix 5 `λ⟨_⟩_
infixl 7 _·_
infixr 7 `if_`then_`else_
infix 9 `_`with_
data Term where
`_`with_
: (x : Γ ∋[ Δ ⊢ A ^ ≤‴-refl ])
→ (σ : Γ ⊩ Δ)
→ Γ ⊢ A ^ n
`true
: Γ ⊢ `Bool ^ n
`false
: Γ ⊢ `Bool ^ n
`if_`then_`else_
: (e₁ : Γ ⊢ `Bool ^ n)
→ (e₂ : Γ ⊢ A ^ n)
→ (e₃ : Γ ⊢ A ^ n)
→ Γ ⊢ A ^ n
`λ⟨_⟩_
: ∀ Δ
→ (e : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
→ Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n
_·_
: (e₁ : Γ ⊢ [ Δ ⊢ A ]⇒ B ^ n)
→ (e₂ : Γ ++ inject₁ Δ ⊢ A ^ n)
→ Γ ⊢ B ^ n
⟨_⟩
: (e : Γ ↾ ⊢ A ^ suc n)
→ Γ ⊢ ◯ A ^ n
`let⟨_⟩ : ∀ Δ
→ (e₁ : Γ ++ inject₁ Δ ⊢ ◯ A ^ n)
→ (e₂ : Γ ,[ Δ ⊢ A ^ ≤‴-step ≤‴-refl ] ⊢ B ^ n)
→ Γ ⊢ B ^ n
`wrap : ∀ Δ
→ (e : Γ ++ inject₁ Δ ⊢ A ^ n)
→ Γ ⊢ Δ ▷ A ^ n
`letwrap : ∀ Δ
→ (e₁ : Γ ⊢ Δ ▷ A ^ n)
→ (e₂ : Γ ,[ inject₁ Δ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
→ Γ ⊢ B ^ n
rename : Rename Γ Γ′ → Term n Γ A → Term n Γ′ A
renameSubst : Rename Γ Γ′ → Subst Δ Γ → Subst Δ Γ′
rename ρ (` x `with σ) = ` ρ x `with renameSubst ρ σ
rename ρ `true = `true
rename ρ `false = `false
rename ρ (`if e₁ `then e₂ `else e₃) = `if rename ρ e₁ `then rename ρ e₂ `else rename ρ e₃
rename ρ (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ (rename (ext ρ) e)
rename ρ (e₁ · e₂) = rename ρ e₁ · rename (ext++ _ ρ) e₂
rename ρ ⟨ e ⟩ = ⟨ rename (ext↾ ρ) e ⟩
rename ρ (`let⟨ Δ ⟩ e₁ e₂) = `let⟨ Δ ⟩ (rename (ext++ (inject₁ Δ) ρ) e₁) (rename (ext ρ) e₂)
rename ρ (`wrap Δ e) = `wrap Δ (rename (ext++ (inject₁ Δ) ρ) e)
rename ρ (`letwrap Δ e₁ e₂) = `letwrap Δ (rename ρ e₁) (rename (ext ρ) e₂)
renameSubst ρ ∅ = ∅
renameSubst ρ (_,_ {Δ = Δ} {m≥n = m≥n} σ (term e)) = renameSubst ρ σ , term (rename (ext++ Δ (ext↾≥ m≥n ρ)) e)
renameSubst ρ (σ , var x) = renameSubst ρ σ , var (ρ x)
lift : Rename Γ Γ′ → Subst Γ Γ′
lift {Γ = ∅} ρ = ∅
lift {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} ρ = lift (ρ ∘ S) , var (ρ Z)
exts : Subst Γ Γ′ → Subst (Γ ,[ Δ ⊢ A ^ m≥n ]) (Γ′ ,[ Δ ⊢ A ^ m≥n ])
exts {Δ = Δ} {m≥n = m≥n} σ = renameSubst S σ , var Z
exts++ : ∀ Δ → Subst Γ Γ′ → Subst (Γ ++ Δ) (Γ′ ++ Δ)
exts++ ∅ σ = σ
exts++ (Δ ,[ _ ⊢ _ ^ _ ]) σ = exts (exts++ Δ σ)
exts↾ : Subst Γ Γ′ → Subst (Γ ↾) (Γ′ ↾)
exts↾ ∅ = ∅
exts↾ (_,_ {m≥n = ≤‴-refl} σ (term e)) = exts↾ σ
exts↾ (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) = exts↾ σ , term e
exts↾ (_,_ {m≥n = ≤‴-refl} σ (var x)) = exts↾ σ
exts↾ (_,_ {m≥n = ≤‴-step m≥n} σ (var x)) = exts↾ σ , var (∋-↾⁺ x)
exts↾≥ : (m≥n : m ≥‴ n) → Subst Γ Γ′ → Subst (Γ ↾≥ m≥n) (Γ′ ↾≥ m≥n)
exts↾≥ ≤‴-refl σ = σ
exts↾≥ (≤‴-step sm≥n) σ = exts↾≥ sm≥n (exts↾ σ)