{-|
This module defines the depth of contexts and substitutions as described in
Section 4.1.1, and proves that depth is preserved by several operations on substitutions.
The definitions are exactly the same as the ones in the CtxTyp.Depth module.
-}

{-# OPTIONS --safe #-}
module Pat.Depth where

open import Data.Nat using (ℕ; suc; zero; _≥‴_; ≤‴-refl; ≤‴-step; _≤_; s≤s; z≤n; _⊔_)
import Data.Nat.Properties as ℕ
open import Function using (id; _∘_)

open import Pat.Context
open import Pat.Term

private variable
  d d′ : ℕ
  σ σ′ : Subst Γ Γ′

-- | Context depth
depth : Context n → ℕ
depth ∅ = zero
depth (Γ ,[ Δ ⊢ _ ^ _ ]) = depth Γ ⊔ suc (depth Δ)
depth (Γ ++ Δ) = depth Γ ⊔ depth Δ

-- | Substitution depth
depthSubstItem : Γ ⊩[ Δ ⊢ A ^ m≥n ] → ℕ
depthSubstItem (var _) = zero
depthSubstItem {Δ = Δ} (term e) = suc (depth Δ)

depthSubst : Subst Γ Γ′ → ℕ
depthSubst ∅ = zero
depthSubst (σ , item) = depthSubst σ ⊔ depthSubstItem item
depthSubst (σ₁ ++ˢ σ₂) = depthSubst σ₁ ⊔ depthSubst σ₂


-- Inductively defined depth upper bound relations

infix  _≤ᵈ_  _≤ᵈ′_
infixl  _++ᵈ_ _++ˢᵈ_

-- | Γ ≤ᵈ d means that the depth of Γ is at most d.
data _≤ᵈ_ {n} : Context n → ℕ → Prop where
  ∅ : ∅ ≤ᵈ d
  _,_ : Γ ≤ᵈ suc d → Δ ≤ᵈ d → Γ ,[ Δ ⊢ A ^ m≥n ] ≤ᵈ suc d
  _++ᵈ_ : Γ ≤ᵈ d → Δ ≤ᵈ d → Γ ++ Δ ≤ᵈ d

module _ {Γ′ Δ A} {m≥n : m ≥‴ n} where
  infix  _≤ᵈ″_
  -- | item ≤ᵈ″ d means that the depth of the substitution entry is at most d.
  data _≤ᵈ″_ : Γ′ ⊩[ Δ ⊢ A ^ m≥n ] → ℕ → Prop where
    term : ∀ {e} → Δ ≤ᵈ d → term e ≤ᵈ″ suc d
    var : ∀ {x} → var x ≤ᵈ″ d

  untermᵈ : ∀ {e} → term e ≤ᵈ″ suc d → Δ ≤ᵈ d
  untermᵈ (term e) = e

-- | σ ≤ᵈ′ d means that the depth of the substitution σ is at most d.
data _≤ᵈ′_ {Γ′ : Context n} : Subst Γ Γ′ → ℕ → Prop where
  ∅ : ∅ ≤ᵈ′ d
  _,_ : ∀ {item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]} → σ ≤ᵈ′ d → item ≤ᵈ″ d → σ , item ≤ᵈ′ d
  _++ˢᵈ_ : ∀ {σ : Γ′ ⊩ Γ} {σ′ : Γ′ ⊩ Δ} → σ ≤ᵈ′ d → σ′ ≤ᵈ′ d → σ ++ˢ σ′ ≤ᵈ′ d

-- | Weaken a context depth upper bound.
≤ᵈ-≤-trans : Γ ≤ᵈ d → d ≤ d′ → Γ ≤ᵈ d′
≤ᵈ-≤-trans ∅ z≤n = ∅
≤ᵈ-≤-trans ∅ (s≤s d≤d′) = ∅
≤ᵈ-≤-trans (Γ≤ , Γ≤₁) (s≤s d≤d′) = ≤ᵈ-≤-trans Γ≤ (s≤s d≤d′) , ≤ᵈ-≤-trans Γ≤₁ d≤d′
≤ᵈ-≤-trans (Γ≤ ++ᵈ Δ≤) d≤d′ = ≤ᵈ-≤-trans Γ≤ d≤d′ ++ᵈ ≤ᵈ-≤-trans Δ≤ d≤d′

-- | Weaken a substitution entry depth upper bound.
≤ᵈ″-≤-trans : {item : Γ ⊩[ Δ ⊢ A ^ m≥n ]} → item ≤ᵈ″ d → d ≤ d′ → item ≤ᵈ″ d′
≤ᵈ″-≤-trans var d≤d′ = var
≤ᵈ″-≤-trans {d = suc _} (term Δ<d) (s≤s d≤d′) = term (≤ᵈ-≤-trans Δ<d d≤d′)

-- | Weaken a substitution depth upper bound.
≤ᵈ′-≤-trans : σ ≤ᵈ′ d → d ≤ d′ → σ ≤ᵈ′ d′
≤ᵈ′-≤-trans ∅ _ = ∅
≤ᵈ′-≤-trans (σ≤ , item) d≤d′ = ≤ᵈ′-≤-trans σ≤ d≤d′ , ≤ᵈ″-≤-trans item d≤d′
≤ᵈ′-≤-trans (σ₁≤ ++ˢᵈ σ₂≤) d≤d′ = ≤ᵈ′-≤-trans σ₁≤ d≤d′ ++ˢᵈ ≤ᵈ′-≤-trans σ₂≤ d≤d′

-- | depth Γ is an upper bound for the depth of Γ.
≤ᵈ-refl : ∀ (Γ : Context n) → Γ ≤ᵈ depth Γ
≤ᵈ-refl ∅ = ∅
≤ᵈ-refl (Γ ,[ Δ ⊢ _ ^ _ ]) with depth Γ | ≤ᵈ-refl Γ
... | zero | ∅ = ∅ , ≤ᵈ-refl Δ
... | zero | ≤d ++ᵈ ≤d′ = (≤ᵈ-≤-trans ≤d z≤n ++ᵈ ≤ᵈ-≤-trans ≤d′ z≤n) , ≤ᵈ-refl Δ
... | suc n | ≤d = ≤ᵈ-≤-trans ≤d (s≤s (ℕ.m≤m⊔n n (depth Δ))) , ≤ᵈ-≤-trans (≤ᵈ-refl Δ) (ℕ.m≤n⊔m n (depth Δ))
≤ᵈ-refl (Γ ++ Δ) = ≤ᵈ-≤-trans (≤ᵈ-refl Γ) (ℕ.m≤m⊔n (depth Γ) (depth Δ)) ++ᵈ ≤ᵈ-≤-trans (≤ᵈ-refl Δ) (ℕ.m≤n⊔m (depth Γ) (depth Δ))

-- | depthSubstItem item is an upper bound for the depth of the substitution entry.
≤ᵈ″-refl : (item : Γ ⊩[ Δ ⊢ A ^ m≥n ]) → item ≤ᵈ″ depthSubstItem item
≤ᵈ″-refl {Δ = Δ} (term e) = term (≤ᵈ-refl Δ)
≤ᵈ″-refl (var x) = var

-- | depthSubst σ is an upper bound for the depth of the substitution.
≤ᵈ′-refl : ∀ (σ : Subst Γ Γ′) → σ ≤ᵈ′ depthSubst σ
≤ᵈ′-refl ∅ = ∅
≤ᵈ′-refl (σ , item) = ≤ᵈ′-≤-trans (≤ᵈ′-refl σ) (ℕ.m≤m⊔n _ _) , ≤ᵈ″-≤-trans (≤ᵈ″-refl item) (ℕ.m≤n⊔m _ _)
≤ᵈ′-refl (σ₁ ++ˢ σ₂) = ≤ᵈ′-≤-trans (≤ᵈ′-refl σ₁) (ℕ.m≤m⊔n _ _) ++ˢᵈ ≤ᵈ′-≤-trans (≤ᵈ′-refl σ₂) (ℕ.m≤n⊔m _ _)

-- | The depth of a substitution is at most the depth of its domain.
≤ᵈ-dom : ∀ (σ : Subst Γ Γ′) → Γ ≤ᵈ d → σ ≤ᵈ′ d
≤ᵈ-dom ∅ _ = ∅
≤ᵈ-dom (σ , term _) (Γ≤d , Δ<d) = ≤ᵈ-dom σ Γ≤d , term Δ<d
≤ᵈ-dom (σ , var _) (Γ≤d , _) = ≤ᵈ-dom σ Γ≤d , var
≤ᵈ-dom (σ₁ ++ˢ σ₂) (Γ≤d ++ᵈ Δ≤d) = ≤ᵈ-dom σ₁ Γ≤d ++ˢᵈ ≤ᵈ-dom σ₂ Δ≤d

-- | Relate the depth of a substitution and its lookup results.
lookupᵈ : σ ≤ᵈ′ d → (x : Γ ∋[ Δ ⊢ A ^ m≥n ]) → lookup σ x ≤ᵈ″ d
lookupᵈ (σ , e) Z = e
lookupᵈ (σ , e) (S x) = lookupᵈ σ x
lookupᵈ (σ₁ ++ˢᵈ σ₂) (L x) = lookupᵈ σ₁ x
lookupᵈ (σ₁ ++ˢᵈ σ₂) (R x) = lookupᵈ σ₂ x

-- | If a function f returns a substitution entry with depth at most d for each variable,
-- then lookup⁻¹ f returns a substitution with depth at most d.
lookup⁻¹ᵈ : {f : ∀ {m} {Δ} {A} {m≥n : m ≥‴ n} → Γ ∋[ Δ ⊢ A ^ m≥n ] → Γ′ ⊩[ Δ ⊢ A ^ m≥n ]} →
  (∀ {m} {Δ} {A} {m≥n : m ≥‴ n} → (x : Γ ∋[ Δ ⊢ A ^ m≥n ]) → f x ≤ᵈ″ d) → lookup⁻¹ f ≤ᵈ′ d
lookup⁻¹ᵈ {Γ = ∅} fᵈ = ∅
lookup⁻¹ᵈ {Γ = Γ ,[ _ ⊢ _ ^ _ ]} fᵈ = lookup⁻¹ᵈ (λ x → fᵈ (S x)) , fᵈ Z
lookup⁻¹ᵈ {Γ = Γ₁ ++ Γ₂} fᵈ = lookup⁻¹ᵈ (λ x → fᵈ (L x)) ++ˢᵈ lookup⁻¹ᵈ (λ x → fᵈ (R x))

-- | renameSubstItem preserves depth upper bounds.
renameSubstItemᵈ : {item : Γ ⊩[ Δ ⊢ A ^ m≥n ]} (ρ : Rename Γ Γ′) → item ≤ᵈ″ d → renameSubstItem ρ item ≤ᵈ″ d
renameSubstItemᵈ ρ (term Δ<d) = term Δ<d
renameSubstItemᵈ ρ var = var

-- | renameSubst preserves depth upper bounds.
renameSubstᵈ : (ρ : Rename Γ Γ′) → σ ≤ᵈ′ d → renameSubst ρ σ ≤ᵈ′ d
renameSubstᵈ ρ ∅ = ∅
renameSubstᵈ ρ (σ , item) = renameSubstᵈ ρ σ , renameSubstItemᵈ ρ item
renameSubstᵈ ρ (σ₁ ++ˢᵈ σ₂) = renameSubstᵈ ρ σ₁ ++ˢᵈ renameSubstᵈ ρ σ₂

-- | Lift creates a substitution with depth 0, so any upper bound d is valid.
liftᵈ : (ρ : Rename Γ Γ′) → lift ρ ≤ᵈ′ d
liftᵈ {Γ = ∅} ρ = ∅
liftᵈ {Γ = Γ ,[ _ ⊢ _ ^ _ ]} ρ = liftᵈ (ρ ∘ S) , var
liftᵈ {Γ = Γ ++ Δ} ρ = liftᵈ {Γ = Γ} (ρ ∘ L) ++ˢᵈ liftᵈ {Γ = Δ} (ρ ∘ R)

-- | exts preserves depth upper bounds.
extsᵈ : σ ≤ᵈ′ d → exts {Δ = Δ} {A = A} {m≥n = m≥n} σ ≤ᵈ′ d
extsᵈ σ = renameSubstᵈ S σ , var

-- | exts++ preserves depth upper bounds.
exts++ᵈ : ∀ Δ → σ  ≤ᵈ′ d → exts++ Δ σ ≤ᵈ′ d
exts++ᵈ Δ σ =  renameSubstᵈ L σ ++ˢᵈ liftᵈ R

-- | exts↾ preserves depth upper bounds.
exts↾ᵈ : σ ≤ᵈ′ d → exts↾ σ ≤ᵈ′ d
exts↾ᵈ ∅ = ∅
exts↾ᵈ (_,_  {m≥n = ≤‴-refl} σ (term e)) = exts↾ᵈ σ
exts↾ᵈ (_,_ {m≥n = ≤‴-step m≥n} σ (term e)) = exts↾ᵈ σ , term e
exts↾ᵈ (_,_ {m≥n = ≤‴-refl} σ var) = exts↾ᵈ σ
exts↾ᵈ (_,_ {m≥n = ≤‴-step m≥n} σ var) = exts↾ᵈ σ , var
exts↾ᵈ (σ₁ ++ˢᵈ σ₂) = exts↾ᵈ σ₁ ++ˢᵈ exts↾ᵈ σ₂

-- | exts↾≥ preserves depth upper bounds.
exts↾≥ᵈ : (m≥n : m ≥‴ n) → σ ≤ᵈ′ d → exts↾≥ m≥n σ ≤ᵈ′ d
exts↾≥ᵈ ≤‴-refl σ = σ
exts↾≥ᵈ (≤‴-step m≥n) σ = exts↾≥ᵈ m≥n (exts↾ᵈ σ)

-- | ⊩[]-inject₁⁻ preserves depth upper bounds.
⊩[]-inject₁⁻ᵈ : {Γ : Context (suc n)} → {item : inject₁ Γ ⊩[ Δ ⊢ A ^ ≤‴-step m≥n ]} → item ≤ᵈ″ d → ⊩[]-inject₁⁻ item ≤ᵈ″ d
⊩[]-inject₁⁻ᵈ (term Δ≤d) = term Δ≤d
⊩[]-inject₁⁻ᵈ var = var

-- | ⊩-inject₁⁻ preserves depth upper bounds.
⊩-inject₁⁻ᵈ : {Γ Δ : Context (suc n)} {σ : inject₁ Γ ⊩ inject₁ Δ} → σ ≤ᵈ′ d → ⊩-inject₁⁻ σ ≤ᵈ′ d
⊩-inject₁⁻ᵈ {Δ = ∅} ∅ = ∅
⊩-inject₁⁻ᵈ {Δ = Δ ,[ Δ′ ⊢ A ^ m≥n ]} (σᵈ , itemᵈ) = ⊩-inject₁⁻ᵈ σᵈ , ⊩[]-inject₁⁻ᵈ itemᵈ
⊩-inject₁⁻ᵈ {Δ = Δ₁ ++ Δ₂} (σ₁ᵈ ++ˢᵈ σ₂ᵈ) = ⊩-inject₁⁻ᵈ σ₁ᵈ ++ˢᵈ ⊩-inject₁⁻ᵈ σ₂ᵈ
 
-- | renameSubstʳ preserves depth upper bounds.
renameSubstʳᵈ : (ρ : Rename Δ′ Δ) → σ ≤ᵈ′ d → renameSubstʳ ρ σ ≤ᵈ′ d
renameSubstʳᵈ ρ σᵈ = lookup⁻¹ᵈ λ x → lookupᵈ σᵈ (ρ x)