module HOAS.SimplyTyped.Value where
open import HOAS.SimplyTyped.TypeSystem
open import HOAS.SimplyTyped.NormalForm
open import Function
Val' : (Ty → Set) → Ty → Set
Val' V (base n) = Ne V (base n)
Val' V (σ ⟶ τ) = Val' V σ → Val' V τ
Val : Ty → Set1
Val σ = ∀ {V} → Val' V σ
mutual
reflect : ∀ {V} τ → Ne V τ → Val' V τ
reflect (base n) t = t
reflect (σ ⟶ τ) t = λ v → reflect τ (t · reify σ v)
reify : ∀ {V} τ → Val' V τ → NF' V τ
reify (base n) t = ne t
reify (σ ⟶ τ) f = ƛ (λ x → reify τ (f (reflect σ (var x))))
infixl 70 _·ˢ_
_·ˢ_ : ∀ {σ τ} → Val (σ ⟶ τ) → Val σ → Val τ
f ·ˢ x = f x
varToVal : ∀ {V τ} → V τ → Val' V τ
varToVal = reflect _ ∘′ var
valToTm : ∀ {τ} → Val τ → Tm τ
valToTm t = nfToTm (reify _ t)
⟦_⟧' : ∀ {V τ} → Tm' (Val' V) τ → Val' V τ
⟦ var x ⟧' = x
⟦ ƛ t ⟧' = λ v → ⟦ t v ⟧'
⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'
⟦_⟧ : ∀ {τ} → Tm τ → Val τ
⟦ t ⟧ = ⟦ t ⟧'