-- Normal forms

module SimplyTyped.NormalForm where

open import SimplyTyped.TypeSystem
open import SimplyTyped.Substitution
open VarSubst

-- η-long β-normal forms, defined using neutral and normal forms.

infixl 70 _·ⁿ_
infix  50 ƛⁿ_


  data Ne : TmLike where
    varⁿ :  {Γ τ}  Γ  τ  Ne Γ τ
    _·ⁿ_ :  {Γ σ τ}  Ne Γ (σ  τ)  NF Γ σ  Ne Γ τ

  data NF : TmLike where
    ne  :  {Γ n}  Ne Γ (base n)  NF Γ (base n)
    ƛⁿ_ :  {Γ σ τ}  NF (Γ  σ) τ  NF Γ (σ  τ)

-- Applying substitutions to normal forms.

infix 48 _[_]ⁿ _[_]ⁿ'


  _[_]ⁿ' :  {Γ Δ τ}  Ne Γ τ  Γ  Δ  Ne Δ τ
  varⁿ x   [ ρ ]ⁿ' = varⁿ (lookup x ρ)
  t₁ ·ⁿ t₂ [ ρ ]ⁿ' = (t₁ [ ρ ]ⁿ') ·ⁿ (t₂ [ ρ ]ⁿ)

  _[_]ⁿ :  {Γ Δ τ}  NF Γ τ  Γ  Δ  NF Δ τ
  ne t [ ρ ]ⁿ = ne (t [ ρ ]ⁿ')
  ƛⁿ t [ ρ ]ⁿ = ƛⁿ (t [ ρ  ]ⁿ)

-- Structure-preserving conversion to terms.


  neToTm :  {Γ τ}  Ne Γ τ  Γ  τ
  neToTm (varⁿ x)   = var x
  neToTm (t₁ ·ⁿ t₂) = neToTm t₁ · nfToTm t₂

  nfToTm :  {Γ τ}  NF Γ τ  Γ  τ
  nfToTm (ne t) = neToTm t
  nfToTm (ƛⁿ t) = ƛ nfToTm t