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

open import Data.Nat

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

open import HOAS.SimplyTyped.TypeSystem

-- Semantic domains for types.

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

-- Evaluation.

⟦_⟧' : ∀ {τ} → Tm' ⟦_⟧⋆ τ → ⟦ τ ⟧⋆
⟦ var x   ⟧' = x
⟦ ƛ t     ⟧' = λ x → ⟦ t x ⟧'
⟦ t₁ · t₂ ⟧' = ⟦ t₁ ⟧' ⟦ t₂ ⟧'

⟦_⟧ : ∀ {τ} → Tm τ → ⟦ τ ⟧⋆
⟦ t ⟧ = ⟦ t ⟧'