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

open import Function.Base using (id)

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

open import Core.Context
open import Core.Term
open import Core.Depth

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

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ᵈ σᵈ e₂
substᵈ σᵈ ⟨ e ⟩ = ⟨ substᵈ (exts↾ᵈ σᵈ) e ⟩
substᵈ σᵈ (`let⟨ Δ ⟩ e₁ e₂) = `let⟨ Δ ⟩ (substᵈ (exts++ᵈ (inject₁ Δ) σᵈ) 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 : Subst Γ Γ′ → Term n Γ A → Term n Γ′ A
subst σ = substᵈ (≤ᵈ′-refl σ)

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