module HOAS.SimplyTyped where

infixl  _·_
infix   ƛ_
infixr  _⟶_

data Ty : Set where
  base : Ty
  _⟶_  : (σ τ : Ty) → Ty

data Tm' (V : Ty → Set) : Ty → Set where
  var : ∀ {σ}   (x : V σ) → Tm' V σ
  ƛ_  : ∀ {σ τ} (t : V σ → Tm' V τ) → Tm' V (σ ⟶ τ)
  _·_ : ∀ {σ τ} (t₁ : Tm' V (σ ⟶ τ)) (t₂ : Tm' V σ) → Tm' V τ

Tm : Ty → Set1
Tm σ = ∀ {V} → Tm' V σ

Val' : (Ty → Set) → Ty → Set
Val' B base    = B base
Val' B (σ ⟶ τ) = Val' B σ → Val' B τ

Val : Ty → Set1
Val σ = ∀ {V} → Val' V σ

⟦_⟧' : ∀ {B τ} → Tm' (Val' B) τ → Val' B τ
⟦ var x   ⟧' = x
⟦ ƛ t     ⟧' = λ x → ⟦ t x ⟧'
⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'

⟦_⟧ : ∀ {τ} → Tm τ → Val τ
⟦ t ⟧ = ⟦ t ⟧'

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 : (t : Ne' V base) → NF' V base
    ƛ_ : ∀ {σ τ} (t : V σ → NF' V τ) → NF' V (σ ⟶ τ)

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

mutual

  reflect : ∀ {V} τ → Ne' V τ → Val' (Ne' V) τ
  reflect base    t = t
  reflect (σ ⟶ τ) t = λ v → reflect τ (t · reify σ v)

  reify : ∀ {V} τ → Val' (Ne' V) τ → NF' V τ
  reify base    t = ne t
  reify (σ ⟶ τ) f = ƛ (λ x → reify τ (f (reflect σ (var x))))

nf : ∀ {τ} → Tm τ → NF τ
nf t = reify _ ⟦ t ⟧