------------------------------------------------------------------------
-- Evaluating terms
------------------------------------------------------------------------

open import Data.Nat

module SimplyTyped.Evaluation
         -- Semantic domains of all the base types.
         (Base : ℕ → Set)
         where

open import SimplyTyped.TypeSystem
import SimplyTyped.Environment
open import SimplyTyped.ApplicativeStructure

-- Semantic domains for types.

⟦_⟧⋆ : Ty → Set
⟦ base n ⟧⋆ = Base n
⟦ σ ⟶ τ  ⟧⋆ = ⟦ σ ⟧⋆ → ⟦ τ ⟧⋆

open SimplyTyped.Environment ⟦_⟧⋆

-- Applicative structure.

appStr : ApplicativeStructure
appStr = record
  { Dom = λ Γ τ → Env Γ → ⟦ τ ⟧⋆
  ; Var = lookup
  ; Lam = λ f ρ v → f (ρ ▷ v)
  ; App = λ f x ρ → f ρ (x ρ)
  }

module ForIllustrationOnly where

  -- The applicative structure above may be hard to grasp at first. If
  -- the interpretation function is written out explicitly we get the
  -- following:

  ⟦_⟧ : ∀ {Γ τ} → Γ ⊢ τ → Env Γ → ⟦ τ ⟧⋆
  ⟦ var x   ⟧ ρ = lookup x ρ
  ⟦ ƛ t     ⟧ ρ = λ v → ⟦ t ⟧ (ρ ▷ v)
  ⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ (⟦ t₂ ⟧ ρ)