----------------------------------------------------------------------------------------------------

-- β-short normal forms

module A202401.STLC-Base-NF where

open import A202401.STLC-Base public


----------------------------------------------------------------------------------------------------

mutual
  data NF {Γ} :  {A}  Γ  A  Set where
    ⌜λ⌝ :  {A B} {t : Γ , A  B} (p : NF t)  NF (⌜λ⌝ t)
    nnf :  {A} {t : Γ  A} (p : NNF t)  NF t

  data NNF {Γ} :  {A}  Γ  A  Set where
    var-  :  {A} {i : Γ  A}  NNF (var i)
    _⌜$⌝_ :  {A B} {t₁ : Γ  A ⌜⊃⌝ B} {t₂ : Γ  A} (p₁ : NNF t₁) (p₂ : NF t₂)  NNF (t₁ ⌜$⌝ t₂)

mutual
  uniNF :  {Γ A} {t : Γ  A} (p p′ : NF t)  p  p′
  uniNF (⌜λ⌝ p) (⌜λ⌝ p′) = ⌜λ⌝ & uniNF p p′
  uniNF (nnf p) (nnf p′) = nnf & uniNNF p p′

  uniNNF :  {Γ A} {t : Γ  A} (p p′ : NNF t)  p  p′
  uniNNF var-        var-          = refl
  uniNNF (p₁ ⌜$⌝ p₂) (p₁′ ⌜$⌝ p₂′) = _⌜$⌝_ & uniNNF p₁ p₁′  uniNF p₂ p₂′


----------------------------------------------------------------------------------------------------

mutual
  renNF :  {Γ Γ′ A} {t : Γ  A} (ϱ : Γ  Γ′)  NF t  NF (ren ϱ t)
  renNF ϱ (⌜λ⌝ p) = ⌜λ⌝ (renNF (lift⊑ ϱ) p)
  renNF ϱ (nnf p) = nnf (renNNF ϱ p)

  renNNF :  {Γ Γ′ A} {t : Γ  A} (ϱ : Γ  Γ′)  NNF t  NNF (ren ϱ t)
  renNNF ϱ var-        = var-
  renNNF ϱ (p₁ ⌜$⌝ p₂) = renNNF ϱ p₁ ⌜$⌝ renNF ϱ p₂

open RenNNFKit (kit renkit var-  {_} {_} {_} {t}  renNNF {t = t})) public

mutual
  subNF :  {Γ Ξ A} {σ : Ξ ⊢§ Γ} {t : Γ  A}  NNF§ σ  NF t  NF (sub σ t)
  subNF ψ (⌜λ⌝ p) = ⌜λ⌝ (subNF (liftNNF§ ψ) p)
  subNF ψ (nnf p) = nnf (subNNF ψ p)

  subNNF :  {Γ Ξ A} {σ : Ξ ⊢§ Γ} {t : Γ  A}  NNF§ σ  NNF t  NNF (sub σ t)
  subNNF ψ var-        = sub∋NNF ψ
  subNNF ψ (p₁ ⌜$⌝ p₂) = subNNF ψ p₁ ⌜$⌝ subNF ψ p₂


----------------------------------------------------------------------------------------------------