{-# OPTIONS --without-K --safe #-}
module Source.Size where

open import Util.HoTT.HLevel.Core
open import Util.Prelude


infix   _<_
infixl  _∙_


mutual
  data Ctx : Set where
    [] : Ctx
    _∙_ : (Δ : Ctx) (n : Size Δ) → Ctx


  data Var : (Δ : Ctx) → Set where
    zero : ∀ {Δ n} → Var (Δ ∙ n)
    suc : ∀ {Δ n} (x : Var Δ) → Var (Δ ∙ n)


  data Size : (Δ : Ctx) → Set where
    var : ∀ {Δ} (x : Var Δ) → Size Δ
    ∞ zero : ∀ {Δ} → Size Δ
    suc : ∀ {Δ} (n : Size Δ) → Size Δ


pattern ⋆ = suc ∞


variable
  Δ Ω Δ′ Ω′ Δ″ Ω″ : Ctx
  x y z : Var Δ
  n m o p b n′ m′ o′ p′ b′ : Size Δ


wk : Size Δ → Size (Δ ∙ n)
wk (var x) = var (suc x)
wk ∞ = ∞
wk zero = zero
wk (suc m) = suc (wk m)


bound : Var Δ → Size Δ
bound (zero {Δ} {n}) = wk n
bound (suc x) = wk (bound x)


data _<_ {Δ} : (n m : Size Δ) → Set where
  var : n ≡ bound x → var x < n
  zero<suc : zero < suc n
  zero<∞ : zero < ∞
  suc<suc : (n<m : n < m) → suc n < suc m
  suc<∞ : (n<∞ : n < ∞) → suc n < ∞
  <-trans : n < m → m < o → n < o
  <suc : n < suc n


data _≤_ {Δ} : (n m : Size Δ) → Set where
  reflexive : n ≡ m → n ≤ m
  <→≤ : n < m → n ≤ m


pattern ≤-refl = reflexive refl

pattern v0 = var zero
pattern v1 = var (suc zero)
pattern v2 = var (suc (suc zero))


abstract
  n<m→n<Sm : n < m → n < suc m
  n<m→n<Sm n<m = <-trans n<m <suc


  n≤m→n<Sm : n ≤ m → n < suc m
  n≤m→n<Sm ≤-refl = <suc
  n≤m→n<Sm (<→≤ n<m) = n<m→n<Sm n<m


  var<suc : var x ≤ n → var x < suc n
  var<suc = n≤m→n<Sm


  ∞<suc : ∞ ≤ n → ∞ < suc n
  ∞<suc = n≤m→n<Sm


  Sn<m→n<m : suc n < m → n < m
  Sn<m→n<m (suc<suc n<m) = <-trans n<m <suc
  Sn<m→n<m (suc<∞ n<∞) = n<∞
  Sn<m→n<m (<-trans Sn<o o<m) = <-trans (Sn<m→n<m Sn<o) o<m
  Sn<m→n<m <suc = <-trans <suc (suc<suc <suc)


  suc-inj-Var : Var.suc {n = n} x ≡ suc y → x ≡ y
  suc-inj-Var refl = refl


  suc≡-prop-Var : (p : Var.suc {n = n} x ≡ suc y) → p ≡ cong suc (suc-inj-Var p)
  suc≡-prop-Var refl = refl


  Var-IsSet : (p q : x ≡ y) → p ≡ q
  Var-IsSet {x = zero} {zero} refl refl = refl
  Var-IsSet {x = suc x} {suc .x} p refl
    = trans (suc≡-prop-Var p) (cong (cong suc) (Var-IsSet _ _))


  suc-inj-Size : Size.suc n ≡ suc m → n ≡ m
  suc-inj-Size refl = refl


  suc≡-prop-Size : (p : Size.suc n ≡ suc m) → p ≡ cong suc (suc-inj-Size p)
  suc≡-prop-Size refl = refl


  var-inj-Size : Size.var x ≡ var y → x ≡ y
  var-inj-Size refl = refl


  var≡-prop-Size : (p : Size.var x ≡ var y) → p ≡ cong var (var-inj-Size p)
  var≡-prop-Size refl = refl


  Size-IsSet : (p q : n ≡ m) → p ≡ q
  Size-IsSet {n = var x} {var .x} p refl
    = trans (var≡-prop-Size p) (cong (cong var) (Var-IsSet _ _))
  Size-IsSet {n = ∞} {∞} refl refl = refl
  Size-IsSet {n = zero} {zero} refl refl = refl
  Size-IsSet {n = suc n} {suc .n} p refl
    = trans (suc≡-prop-Size p) (cong (cong suc) (Size-IsSet _ _))


  wk-resp-< : n < m → wk {n = o} n < wk m
  wk-resp-< (var p) = var (cong wk p)
  wk-resp-< zero<suc = zero<suc
  wk-resp-< zero<∞ = zero<∞
  wk-resp-< (suc<suc n<m) = suc<suc (wk-resp-< n<m)
  wk-resp-< (suc<∞ n<∞) = suc<∞ (wk-resp-< n<∞)
  wk-resp-< (<-trans n<o o<m) = <-trans (wk-resp-< n<o) (wk-resp-< o<m)
  wk-resp-< <suc = <suc