{-# OPTIONS --safe #-}
{-# OPTIONS --with-K #-}
module Pat.Substitution where

open import Function.Base using (id)

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

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

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)


substᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Term n Γ A → Term n Γ′ A
substSubstᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Subst Δ Γ → Subst Δ Γ′
substPatternᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Pattern n Γ Δ A Π → Pattern n Γ′ Δ A Π
substPatternSubstᵈ : ∀ {d} {σ : Subst Γ Γ′} → σ ≤ᵈ′ d → Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ′ ∣ Δ ⊩ Δ′ ↝ Π

substᵈ {d = d} {σ = σ} σᵈ (` x `with σ′) with d | lookup σ x | lookupᵈ σᵈ x | substSubstᵈ σᵈ σ′
... | _     | var y  | _        | σσ′ = ` y `with σσ′
... | suc _ | 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₂)
substᵈ σᵈ (`iflet⟨ Δ ⟩ p e₁ e₂ e₃) =
  `iflet⟨ Δ ⟩
    (substPatternᵈ (exts↾ᵈ σᵈ) p) 
    (substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) e₁) 
    (substᵈ (exts++ᵈ (inject₁ _) σᵈ) e₂)
    (substᵈ σᵈ e₃)
substᵈ σᵈ (`rewritȩ p e₁ e₂) = `rewritȩ (substPatternᵈ (exts↾ᵈ σᵈ) p) (substᵈ (exts++ᵈ (inject₁ _) σᵈ) e₁) (substᵈ σᵈ e₂)

substSubstᵈ σᵈ ∅ = ∅
substSubstᵈ {Δ = Δ ,[ Δ′ ⊢ A ^ m≥n ]} σᵈ (σ′ , term e) = substSubstᵈ σᵈ σ′ , term (substᵈ (exts++ᵈ Δ′ (exts↾≥ᵈ m≥n σᵈ)) e)
substSubstᵈ{σ = σ} σᵈ (σ′ , var x) = substSubstᵈ σᵈ σ′ , lookup σ x

substPatternᵈ σᵈ `pat = `pat
substPatternᵈ {Δ = Δ} {d = d} {σ = σ} σᵈ (`_`with₁_ {Δ′ = Δ′} x σ′) with d | lookup σ x | lookupᵈ σᵈ x | substSubstᵈ (exts++ᵈ Δ σᵈ) σ′
... | _     | var y  | _        | σσ′ = ` y `with₁ σσ′
... | suc _ | term e | term-Δ<d | σσ′ = toPattern σσ′e
  where
  σσ′ᵈ = ≤ᵈ-dom σσ′ (untermᵈ term-Δ<d)
  σσ′e = substᵈ (liftᵈ id ++ˢᵈ σσ′ᵈ) (rename (ext++ Δ′ (∋-++⁺ˡ Δ)) e)
substPatternᵈ σᵈ (` x `with₂ π) = ` x `with₂ substPatternSubstᵈ σᵈ π
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ᵈ σᵈ (`rewritȩ p p₁ p₂) = `rewritȩ (substPatternᵈ (exts++ᵈ _ (exts↾ᵈ σᵈ)) p) (substPatternᵈ σᵈ p₁) (substPatternᵈ σᵈ p₂)

substPatternSubstᵈ σᵈ ∅ = ∅
substPatternSubstᵈ σᵈ (_,_ {m≥n = m≥n} σ′ (term p)) = substPatternSubstᵈ σᵈ σ′ , term (substPatternᵈ (exts↾≥ᵈ m≥n σᵈ) p)
substPatternSubstᵈ {Δ = Δ} {σ = σ} σᵈ (_,_  {m≥n = m≥n} σ′ (var x)) with ∋-++⁻ Δ x
... | inj₂ xΔ = substPatternSubstᵈ σᵈ σ′ , var (∋-++⁺ʳ _ xΔ)
... | inj₁ xΓ with lookup σ xΓ
... | term e = substPatternSubstᵈ σᵈ σ′ , term (toPattern (rename ρ e)) where
  ρ : Rename (Γ′ ↾≥ m≥n ++ Δ′) (Γ′ ↾≥ m≥n ++ (Δ ↾≥ m≥n ++ Δ′)) -- Weaken by thw local context Δ
  ρ {Γ′ = Γ′} {Δ′ = Δ′} x with ∋-++⁻ Δ′ x
  ... | inj₁ xΓ′ = ∋-++⁺ˡ _ xΓ′
  ... | inj₂ xΔ′ = ∋-++⁺ʳ (Γ′ ↾≥ m≥n) (∋-++⁺ʳ _ xΔ′)
... | var x′ = substPatternSubstᵈ σᵈ σ′ , var (∋-++⁺ˡ _ x′)

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

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

substPattern : Subst Γ Γ′ → Pattern n Γ Δ A Π → Pattern n Γ′ Δ A Π
substPattern σ = substPatternᵈ (≤ᵈ′-refl σ)

substPatternSubst : Subst Γ Γ′ → Γ ∣ Δ ⊩ Δ′ ↝ Π → Γ′ ∣ Δ ⊩ Δ′ ↝ Π
substPatternSubst σ = substPatternSubstᵈ (≤ᵈ′-refl σ)