------------------------------------------------------------------------
-- Normal forms
------------------------------------------------------------------------

module HOAS.SimplyTyped.NormalForm where

open import HOAS.SimplyTyped.TypeSystem

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

infixl 70 _·_
infix  50 ƛ_

mutual

  data Ne (V : Ty  Set) : Ty  Set where
    var :  {τ} (x : V τ)  Ne V τ
    _·_ :  {σ τ} (t₁ : Ne V (σ  τ)) (t₂ : NF' V σ)  Ne V τ

  data NF' (V : Ty  Set) : Ty  Set where
    ne :  {n} (t : Ne V (base n))  NF' V (base n)
    ƛ_ :  {σ τ} (t : V σ  NF' V τ)  NF' V (σ  τ)

NF : Ty  Set1
NF σ =  {V}  NF' V σ

-- Structure-preserving conversion to terms.

mutual

  neToTm :  {V τ}  Ne V τ  Tm' V τ
  neToTm (var x)   = var x
  neToTm (t₁ · t₂) = neToTm t₁ · nfToTm' t₂

  nfToTm' :  {V τ}  NF' V τ  Tm' V τ
  nfToTm' (ne t) = neToTm t
  nfToTm' (ƛ t)  = ƛ  x  nfToTm' (t x))

nfToTm :  {τ}  NF τ  Tm τ
nfToTm t = nfToTm' t