------------------------------------------------------------------------
-- An abstract specification of a semantics
------------------------------------------------------------------------

module Semantics where

open import Syntax

-- I don't assume any properties of the semantics.

record Sem : Set1 where
  field
    -- x ⇓[ i ] v means that x _can_ terminate with the value (or
    -- exception) v.
    _⇓[_]_ : ∀ {t} → Expr t → Status → Value → Set

    -- x ⇑[ i ] means that x _can_ fail to terminate.
    _⇑[_] : ∀ {t} → Expr t → Status → Set