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

open import Function.Base using (id; _∘_)

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

open import CtxTyp.Context
open import CtxTyp.Term

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

-- Depth of a context

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

-- Depth of a substitution

depthSubst : Subst Γ Γ′ → ℕ
depthSubst ∅ = zero
depthSubst {Γ = Γ ,[ Δ ⊢ A ^ m≥n ]} (σ , term e) = depthSubst σ ⊔ suc (depth Δ)
depthSubst (σ , var x) = depthSubst σ

-- Context/Substitution with depth upper bound
infix  _≤ᵈ_  _≤ᵈ′_

data _≤ᵈ_ {n} : Context n → ℕ → Prop where
  ∅ : ∅ ≤ᵈ d
  _,_ : Γ ≤ᵈ suc d → Δ ≤ᵈ d → Γ ,[ Δ ⊢ A ^ m≥n ] ≤ᵈ suc d

module _ {Γ′ Δ A} {m≥n : m ≥‴ n} where
  infix  _≤ᵈ″_
  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

data _≤ᵈ′_ {Γ′ : Context n} : Subst Γ Γ′ → ℕ → Prop where
  ∅ : ∅ ≤ᵈ′ d
  _,_ : ∀ {item : Γ′ ⊩[ Δ ⊢ A ^ m≥n ]} → σ ≤ᵈ′ d → item ≤ᵈ″ d → σ , item ≤ᵈ′ d

≤ᵈ-≤-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 ≤ d′ → σ ≤ᵈ′ d′
≤ᵈ′-≤-trans ∅ _ = ∅
≤ᵈ′-≤-trans (σ≤ , term e) (s≤s d≤d′) = ≤ᵈ′-≤-trans σ≤ (s≤s d≤d′) , term (≤ᵈ-≤-trans e d≤d′)
≤ᵈ′-≤-trans (σ≤ , var) d≤d′ = ≤ᵈ′-≤-trans σ≤ d≤d′ , var

≤ᵈ-refl : ∀ (Γ : Context n) → Γ ≤ᵈ depth Γ
≤ᵈ-refl ∅ = ∅
≤ᵈ-refl (Γ ,[ Δ ⊢ _ ^ _ ]) with depth Γ | ≤ᵈ-refl Γ
... | zero | ∅ = ∅ , ≤ᵈ-refl Δ
... | suc n | ≤d = ≤ᵈ-≤-trans ≤d (s≤s (ℕ.m≤m⊔n n (depth Δ))) , ≤ᵈ-≤-trans (≤ᵈ-refl Δ) (ℕ.m≤n⊔m n (depth Δ))

≤ᵈ′-refl : ∀ (σ : Subst Γ Γ′) → σ ≤ᵈ′ depthSubst σ
≤ᵈ′-refl ∅ = ∅
≤ᵈ′-refl (σ , term e) with depthSubst σ | ≤ᵈ′-refl σ
... | zero | ∅ = ∅ , term (≤ᵈ-refl _)
... | zero | ≤d , var = (≤ᵈ′-≤-trans ≤d z≤n , var) , term (≤ᵈ-refl _)
... | suc n | ≤d = ≤ᵈ′-≤-trans ≤d (s≤s (ℕ.m≤m⊔n n _)) , term (≤ᵈ-≤-trans (≤ᵈ-refl _) (ℕ.m≤n⊔m n _))
≤ᵈ′-refl (σ , var x) = ≤ᵈ′-refl σ , var

≤ᵈ-dom : ∀ (σ : Subst Γ Γ′) → Γ ≤ᵈ d → σ ≤ᵈ′ d
≤ᵈ-dom ∅ _ = ∅
≤ᵈ-dom (σ , term _) (Γ≤d , Δ<d) = ≤ᵈ-dom σ Γ≤d , term Δ<d
≤ᵈ-dom (σ , var _) (Γ≤d , _) = ≤ᵈ-dom σ Γ≤d , var

lookupᵈ : σ ≤ᵈ′ d → (x : Γ ∋[ Δ ⊢ A ^ m≥n ]) → lookup σ x ≤ᵈ″ d
lookupᵈ (σ , e) Z = e
lookupᵈ (σ , e) (S x) = lookupᵈ σ x

renameSubstᵈ : (ρ : Rename Γ Γ′) → σ ≤ᵈ′ d → renameSubst ρ σ ≤ᵈ′ d
renameSubstᵈ ρ ∅ = ∅
renameSubstᵈ ρ (σ , term e) = renameSubstᵈ ρ σ , term e
renameSubstᵈ ρ (σ , var) = renameSubstᵈ ρ σ , var

extsᵈ : σ ≤ᵈ′ d → exts {Δ = Δ} {A = A} {m≥n = m≥n} σ ≤ᵈ′ d
extsᵈ σ = renameSubstᵈ S σ , var

exts++ᵈ : ∀ Δ → σ  ≤ᵈ′ d → exts++ Δ σ ≤ᵈ′ d
exts++ᵈ ∅ σ = σ
exts++ᵈ (Δ ,[ _ ⊢ _ ^ _ ]) σ = extsᵈ (exts++ᵈ Δ σ)

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↾≥ᵈ : (m≥n : m ≥‴ n) → σ ≤ᵈ′ d → exts↾≥ m≥n σ ≤ᵈ′ d
exts↾≥ᵈ ≤‴-refl σ = σ
exts↾≥ᵈ (≤‴-step m≥n) σ = exts↾≥ᵈ m≥n (exts↾ᵈ σ)

infixl  _++ˢᵈ_
_++ˢᵈ_ : σ ≤ᵈ′ d → σ′ ≤ᵈ′ d → σ ++ˢ σ′ ≤ᵈ′ d
σ ++ˢᵈ ∅ = σ
σ ++ˢᵈ (σ′ , e) = σ ++ˢᵈ σ′ , e

liftᵈ : (ρ : Rename Γ Γ′) → lift ρ ≤ᵈ′ d
liftᵈ {Γ = ∅} ρ = ∅
liftᵈ {Γ = Γ ,[ _ ⊢ _ ^ _ ]} ρ = liftᵈ (ρ ∘ S) , var