------------------------------------------------------------------------
-- 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  _·ⁿ_
infix   ƛⁿ_

mutual

  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  _[_]ⁿ _[_]ⁿ'

mutual

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

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

-- Structure-preserving conversion to terms.

mutual

  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