```------------------------------------------------------------------------
-- Values
------------------------------------------------------------------------

module SimplyTyped.Value where

open import SimplyTyped.TypeSystem
open import SimplyTyped.NormalForm
open import SimplyTyped.Substitution
open import SimplyTyped.ContextExtension
open import SimplyTyped.ApplicativeStructure
open import Function hiding (_∋_)
open import Relation.Binary.PropositionalEquality

-- Values.

Val : TmLike
Val Γ (base n) = Ne Γ (base n)
Val Γ (σ ⟶ τ)  = ∀ Γ⁺ → Val (Γ ▻▻ Γ⁺) σ → Val (Γ ▻▻ Γ⁺) τ

-- Semantic application.

infixl 70 _·ˢ_

_·ˢ_ : ∀ {Γ σ τ} → Val Γ (σ ⟶ τ) → Val Γ σ → Val Γ τ
f ·ˢ x = f ε x

-- Reflection and reification.

mutual

reflect : ∀ {Γ} τ → Ne Γ τ → Val Γ τ
reflect (base n) t = t
reflect (σ ⟶ τ)  t = λ Γ⁺ v →
reflect τ ((t [ wk⋆ Γ⁺ ]ⁿ') ·ⁿ reify σ v)
where open VarSubst

reify : ∀ {Γ} τ → Val Γ τ → NF Γ τ
reify (base n) t = ne t
reify (σ ⟶ τ)  f = ƛⁿ (reify τ (f (ε ▻ σ) (reflect σ (varⁿ vz))))

-- Weakening.

wkˢ : ∀ {Γ} τ Γ⁺ → Val Γ τ → Val (Γ ▻▻ Γ⁺) τ
wkˢ     (base n) Γ⁺ t = t [ wk⋆ Γ⁺ ]ⁿ' where open VarSubst
wkˢ {Γ} (σ ⟶ τ)  Γ⁺ f = λ Γ⁺⁺ v →
let cast₁ = subst (λ Γ → Val Γ σ) (sym \$ ▻▻-assoc Γ Γ⁺ Γ⁺⁺)
cast₂ = subst (λ Γ → Val Γ τ) (▻▻-assoc Γ Γ⁺ Γ⁺⁺)
in cast₂ (f (Γ⁺ ▻▻ Γ⁺⁺) (cast₁ v))

-- Value substitutions.

open SubstDef using (SubstKit)

varToVal : ∀ {Γ τ} → Γ ∋ τ → Val Γ τ
varToVal = reflect _ ∘ varⁿ

valToTm : ∀ {Γ τ} → Val Γ τ → Γ ⊢ τ
valToTm = nfToTm ∘ reify _

valKit : SubstKit Val
valKit = record
{ vr     = varToVal
; weaken = wkˢ _ (ε ▻ _)
; tm     = valToTm
}

module ValSubst where
open Subst valKit public

open ValSubst

-- An applicative structure using these values.

appStr : ApplicativeStructure
appStr = record
{ Dom = λ Γ τ → ∀ {Δ} → Γ ⇒ Δ → Val Δ τ
; Var = λ x ρ → lookup x ρ
; Lam = λ f ρ Δ⁺ v → f (wk⇒⋆ Δ⁺ ρ ▷ v)
; App = λ v₁ v₂ ρ → v₁ ρ ·ˢ v₂ ρ
}

module ForIllustrationOnly where

-- The evaluation function that you get from this applicative
-- structure:

⟦_⟧ : ∀ {Γ Δ τ} → Γ ⊢ τ → Γ ⇒ Δ → Val Δ τ
⟦ var x   ⟧ ρ = lookup x ρ
⟦ ƛ t     ⟧ ρ = λ Δ⁺ v → ⟦ t ⟧ (wk⇒⋆ Δ⁺ ρ ▷ v)
⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ ·ˢ ⟦ t₂ ⟧ ρ
```