module HOAS.SimplyTyped.NormalForm where
open import HOAS.SimplyTyped.TypeSystem
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 σ
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