------------------------------------------------------------------------
-- 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.
    _⇓[_]_ : forall {t} -> Expr t -> Status -> Value -> Set

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