------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Values for standard evaluation (Def. 3.1 and 3.2, Fig. 4c and 4f).
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type

module Parametric.Denotation.Value
    (Base : Type.Structure)
  where

open import Base.Denotation.Notation

open Type.Structure Base

-- Extension point: Values for base types.
Structure : Set₁
Structure = Base → Set

module Structure (⟦_⟧Base : Structure) where
  -- We provide: Values for arbitrary types.
  ⟦_⟧Type : Type -> Set
  ⟦ base ι ⟧Type = ⟦ ι ⟧Base
  ⟦ σ ⇒ τ ⟧Type = ⟦ σ ⟧Type → ⟦ τ ⟧Type

  -- This means: Overload ⟦_⟧ to mean ⟦_⟧Type.
  meaningOfType : Meaning Type
  meaningOfType = meaning ⟦_⟧Type

  -- We also provide: Environments of such values.
  open import Base.Denotation.Environment Type ⟦_⟧Type public