module Syntax where
open import Data.Nat
infixl 7 _⊕_
infixl 6 _catch_
infixr 6 _finally_
infixl 5 _>>_
data Totality : Set where
total : Totality
partial : Totality
data Value : Set where
nat : (n : ℕ) → Value
throw : Value
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)
data Status : Set where
U : Status
B : Status