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


  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₂  ρ