------------------------------------------------------------------------
-- A small language with exceptions and interrupts
------------------------------------------------------------------------

module Syntax where

open import Data.Nat

------------------------------------------------------------------------
-- Syntax

infixl 7 _⊕_
infixl 6 _catch_
infixr 6 _finally_
infixl 5 _>>_

-- Is the language total?

data Totality : Set where
  total   : Totality
  partial : Totality

-- Values.

data Value : Set where
  nat   : (n : ℕ) -> Value
  throw : Value

-- Expressions.

data Expr : Totality -> Set where
  ⌜_⌝     : forall {t} (v : Value) -> Expr t
  loop    : (x : Expr partial) -> Expr partial
  _⊕_     : forall {t} (x y : Expr t) -> Expr t
  _>>_    : forall {t} (x y : Expr t) -> Expr t
  _catch_ : forall {t} (x y : Expr t) -> Expr t
  block   : forall {t} (x   : Expr t) -> Expr t
  unblock : forall {t} (x   : Expr t) -> Expr t

_finally_ : forall {t} -> Expr t -> Expr t -> Expr t
x finally y = block (unblock x catch (y >> ⌜ throw ⌝) >> y)

------------------------------------------------------------------------
-- Some other syntactic bits and pieces

-- Are interrupts blocked (B) or not (U)?

data Status : Set where
  U : Status
  B : Status