{-|
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 #-}
{-# OPTIONS --with-K #-}
module Pat.Substitution where

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

open import Pat.Context
open import Pat.Term
open import Pat.Depth
open import Pat.Matching

-- 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.
-- Since λ○▷ has patterns and substitution patterns, we need to define
-- the corresponding substitution functions for them as well.
substᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ⊢ A ^ n → Γ′ ⊢ A ^ n
substSubstᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ⊩ Δ → Γ′ ⊩ Δ
substSubstItemᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ⊩[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]
substPatternᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ∣ Δ ⊢ A ^ n ↝ Π → Γ′ ∣ Δ ⊢ A ^ n ↝ Π
substSubstPatternᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ′ ∣ Δ ⊩ Δ′ ↝ Π
substSubstPatternItemᵈ : ∀ {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₂)
substᵈ σᵈ (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) =
  `iflet⟨ Δ ⟩
    (substPatternᵈ (exts↾ᵈ σᵈ) p) 
    (substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) e₁) 
    (substᵈ (exts++ᵈ (inject₁ _) σᵈ) e₂)
    (substᵈ σᵈ e₃)
substᵈ σᵈ (`rewrite e₁ p e₂) = `rewrite (substᵈ σᵈ e₁) (substPatternᵈ (exts↾ᵈ σᵈ) p) (substᵈ (exts++ᵈ (inject₁ _) σᵈ) 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

substPatternᵈ σᵈ `pat = `pat
substPatternᵈ σᵈ (` x `with₁ σ₁) = toPattern id (useItemᵈ (renameSubstItemᵈ L (lookupᵈ σᵈ x)) (substSubstᵈ (exts++ᵈ _ σᵈ) σ₁))
substPatternᵈ σᵈ (` x `with₂ π) = ` x `with₂ substSubstPatternᵈ σᵈ π
substPatternᵈ σᵈ `true = `true
substPatternᵈ σᵈ `false = `false
substPatternᵈ σᵈ (`if p `then p₁ `else p₂) = `if substPatternᵈ σᵈ p `then substPatternᵈ σᵈ p₁ `else substPatternᵈ σᵈ p₂
substPatternᵈ σᵈ (`λ⟨ Δ′ ⟩ p) = `λ⟨ Δ′ ⟩ substPatternᵈ σᵈ p
substPatternᵈ σᵈ (p₁ · p₂) = substPatternᵈ σᵈ p₁ · substPatternᵈ σᵈ p₂
substPatternᵈ σᵈ (⟨ p ⟩) = ⟨ substPatternᵈ (exts↾ᵈ σᵈ) p ⟩
substPatternᵈ σᵈ (`let⟨ Δ′ ⟩ p₁ p₂) = `let⟨ Δ′ ⟩ (substPatternᵈ σᵈ p₁) (substPatternᵈ σᵈ p₂)
substPatternᵈ σᵈ (`wrap Δ′ p) = `wrap Δ′ (substPatternᵈ σᵈ p)
substPatternᵈ σᵈ (`letwrap Δ′ p₁ p₂) = `letwrap Δ′ (substPatternᵈ σᵈ p₁) (substPatternᵈ σᵈ p₂)
substPatternᵈ σᵈ (`iflet⟨ Δ′ ⟩ p p₁ p₂ p₃) =
  `iflet⟨ Δ′ ⟩
    (substPatternᵈ (exts++ᵈ _ (exts↾ᵈ σᵈ)) p)
    (substPatternᵈ σᵈ p₁)
    (substPatternᵈ σᵈ p₂)
    (substPatternᵈ σᵈ p₃)
substPatternᵈ σᵈ (`rewrite p₁ p p₂) = `rewrite (substPatternᵈ σᵈ p₁) (substPatternᵈ (exts++ᵈ _ (exts↾ᵈ σᵈ)) p) (substPatternᵈ σᵈ p₂)

substSubstPatternᵈ σᵈ ∅ = ∅
substSubstPatternᵈ σᵈ (σ , item) = substSubstPatternᵈ σᵈ σ , substSubstPatternItemᵈ σᵈ item
substSubstPatternᵈ σᵈ (σ₁ ++ˢᵖ σ₂) = substSubstPatternᵈ σᵈ σ₁ ++ˢᵖ substSubstPatternᵈ σᵈ σ₂

substSubstPatternItemᵈ {m≥n = m≥n} σᵈ (term p) = term (substPatternᵈ (exts↾≥ᵈ m≥n σᵈ) p)
substSubstPatternItemᵈ {σ = σ} σᵈ (var (L x)) = toSubstPatternItem L (lookup σ x)
substSubstPatternItemᵈ σᵈ (var (R x)) = var (R 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 σ)

-- | Apply a substitution σ to a pattern p.
substPattern : Subst Γ Γ′ → Pattern n Γ Δ A Π → Pattern n Γ′ Δ A Π
substPattern σ = substPatternᵈ (≤ᵈ′-refl σ)

-- | Apply a substitution σ to a substitution pattern π.
substSubstPattern : Subst Γ Γ′ → Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ′ ∣ Δ ⊩ Δ′ ↝ Π
substSubstPattern σ = substSubstPatternᵈ (≤ᵈ′-refl σ)

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