{-|
This module defines substitution functions for well-typed terms and substitutions
as described in section 4.1.
Intrinsic typing ensures that substitution preserves typing (Lemma 4.1).
-}

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

open import Data.Nat using (ℕ; suc; zero; ≤‴-refl)
open import Function using (id)

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

-- We first define variants of the substitution functions that accept a depth upper bound d
-- for the substitution being applied. This allows the termination checker
-- to use d as a termination measure.
substᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
substSubstᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ⊩ Δ → Γ′ ⊩ Δ
substSubstItemᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ⊩[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]

-- The variable case of substᵈ, where the depth upper bound d decreases by 1.
-- We define this separately to simplify proofs of substitution properties.
-- Operationally, it takes a substitution item `item` and a delayed substitution σ which provides its dependencies, and returns a term as a result.
useItemᵈ : ∀ {d} {item : Γ ⊩[ Δ ⊢ A ^ ≤‴-refl ]} → item ≤ᵈ″ d → Γ ⊩ Δ → Γ ⊢ A ^ n
useItemᵈ {item = var x} _ σ = ` x `with σ
useItemᵈ {d = suc d} {item = term e} Δ<d σ = substᵈ {d = d} (liftᵈ id ++ˢᵈ ≤ᵈ-dom σ (untermᵈ Δ<d)) e

substᵈ σᵈ (` x `with σ₁) = useItemᵈ (lookupᵈ σᵈ x) (substSubstᵈ σᵈ σ₁)
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ᵈ σᵈ (σ′ , item) = substSubstᵈ σᵈ σ′ , substSubstItemᵈ σᵈ item
substSubstᵈ σᵈ (σ₁ ++ˢ σ₂) = substSubstᵈ σᵈ σ₁ ++ˢ substSubstᵈ σᵈ σ₂

substSubstItemᵈ {Δ = Δ} {m≥n = m≥n} σᵈ (term e) = term (substᵈ (exts++ᵈ Δ (exts↾≥ᵈ m≥n σᵈ)) e)
substSubstItemᵈ {σ = σ} σᵈ (var x) = lookup σ x

-- We then define the substitution functions without a depth upper bound,
-- by precomputing the depth upper bound using the depth function.
-- Intinsic typing ensures that substitution preserves typing (Lemma 4.1).

-- | Apply a substitution σ to a term e.
subst : Subst Γ Γ′ → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
subst σ = substᵈ (≤ᵈ′-refl σ)

-- | Apply a substitution σ to a another substitution σ₁.
substSubst : Subst Γ Γ′ → Γ ⊩ Δ → Γ′ ⊩ Δ
substSubst σ = substSubstᵈ (≤ᵈ′-refl σ)

-- | Apply a substitution σ to a substitution entry.
substSubstItem : Subst Γ Γ′ → Γ ⊩[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
substSubstItem σ = substSubstItemᵈ (≤ᵈ′-refl σ)