------------------------------------------------------------------------
-- 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
  ⌜_⌝     : ∀ {t} (v : Value) → Expr t
  loop    : (x : Expr partial) → Expr partial
  _⊕_     : ∀ {t} (x y : Expr t) → Expr t
  _>>_    : ∀ {t} (x y : Expr t) → Expr t
  _catch_ : ∀ {t} (x y : Expr t) → Expr t
  block   : ∀ {t} (x   : Expr t) → Expr t
  unblock : ∀ {t} (x   : Expr t) → Expr t

_finally_ : ∀ {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