{-|
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.
-}

{-# OPTIONS --safe #-}
module CtxTyp.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 CtxTyp.Context
open import CtxTyp.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)