------------------------------------------------------------------------
-- 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  _·ˢ_

_·ˢ_ : ∀ {Γ σ τ} → 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₂ ⟧ ρ