------------------------------------------------------------------------
-- Values
------------------------------------------------------------------------

module HOAS.SimplyTyped.Value where

open import HOAS.SimplyTyped.TypeSystem
open import HOAS.SimplyTyped.NormalForm
open import Function

-- Values.

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 σ

-- Reflection and reification.

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))))

-- Semantic application.

infixl 70 _·ˢ_

_·ˢ_ :  {σ τ}  Val (σ  τ)  Val σ  Val τ
f ·ˢ x = f x

-- Conversions.

varToVal :  {V τ}  V τ  Val' V τ
varToVal = reflect _ ∘′ var

valToTm :  {τ}  Val τ  Tm τ
valToTm t = nfToTm (reify _ t)

-- Evaluation.

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

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