{-# OPTIONS --safe #-}
module CtxTyp.Substitution where

open import Function.Base using (id)

open import Data.Nat.Base using (ℕ; suc; zero)

open import CtxTyp.Context
open import CtxTyp.Term
open import CtxTyp.Depth

substᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Term n Γ A → Term n Γ′ A
substSubstᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Subst Δ Γ → Subst Δ Γ′

substᵈ {σ = σ} σᵈ (` x `with σ′) with lookup σ x | lookupᵈ σᵈ x | substSubstᵈ σᵈ σ′
substᵈ {σ = σ} σᵈ (` x `with σ′)             | var y  | _        | σσ′ = ` y `with σσ′
substᵈ {d = suc _} {σ = σ} σᵈ (` x `with σ′) | term e | term-Δ<d | σσ′ = substᵈ (liftᵈ id ++ˢᵈ σσ′ᵈ) e
  where σσ′ᵈ = ≤ᵈ-dom σσ′ (untermᵈ term-Δ<d)
substᵈ σᵈ `true = `true
substᵈ σᵈ `false = `false
substᵈ σᵈ (`if e₁ `then e₂ `else e₃) = `if substᵈ σᵈ e₁ `then substᵈ σᵈ e₂ `else substᵈ σᵈ e₃
substᵈ σᵈ (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ substᵈ (extsᵈ σᵈ) e
substᵈ σᵈ (e₁ · e₂) = substᵈ σᵈ e₁ · substᵈ (exts++ᵈ _ σᵈ) e₂
substᵈ σᵈ ⟨ e ⟩ = ⟨ substᵈ (exts↾ᵈ σᵈ) e ⟩
substᵈ σᵈ (`let⟨ Δ ⟩ e₁ e₂) = `let⟨ Δ ⟩ (substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) e₁) (substᵈ (extsᵈ σᵈ) e₂)
substᵈ σᵈ (`wrap Δ e) = `wrap Δ (substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) e)
substᵈ σᵈ (`letwrap Δ e₁ e₂) = `letwrap Δ (substᵈ σᵈ e₁) (substᵈ (extsᵈ σᵈ) e₂)
 
substSubstᵈ σᵈ ∅ = ∅
substSubstᵈ {Δ = Δ ,[ Δ′ ⊢ A ^ m≥n ]} σᵈ (σ′ , term e) = substSubstᵈ σᵈ σ′ , term (substᵈ (exts++ᵈ Δ′ (exts↾≥ᵈ m≥n σᵈ)) e)
substSubstᵈ {σ = σ} σᵈ (σ′ , var x) = substSubstᵈ σᵈ σ′ , lookup σ x

substᵈ[_] : ∀ {d} (σ : Subst Γ Γ′) → σ ≤ᵈ′ d → Term n Γ A → Term n Γ′ A
substᵈ[ σ ] = substᵈ {σ = σ}

{-# DISPLAY substᵈ {σ = σ} = substᵈ[ σ ] #-}

subst : Subst Γ Γ′ → Term n Γ A → Term n Γ′ A
subst σ = substᵈ (≤ᵈ′-refl σ)

substSubst : Subst Γ Γ′ → Subst Δ Γ → Subst Δ Γ′
substSubst σ = substSubstᵈ (≤ᵈ′-refl σ)