------------------------------------------------------------------------
-- 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