module CompositionBased.ExceptionsNonDet where
open import Data.List
open import Data.Maybe
open import Data.Nat
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Derivation
open import FailureAndNonDeterminism as FND
using (FND; _<$>_; _⊛_; ↯; _⊕_; _∣_)
open import ReverseComposition as RC
hiding (_↑_⇨_; module Derivation)
renaming (_⊕_ to _⊕M_)
data Expr : Set where
val : (n : ℕ) → Expr
_⊖_ : (e₁ e₂ : Expr) → Expr
throw : Expr
_catch_ : (e₁ e₂ : Expr) → Expr
_amb_ : (e₁ e₂ : Expr) → Expr
⟦_⟧ : Expr → List (Maybe ℕ)
⟦ val n ⟧ = FND.return n
⟦ e₁ ⊖ e₂ ⟧ = _∸_ <$> ⟦ e₁ ⟧ ⊛ ⟦ e₂ ⟧
⟦ throw ⟧ = ↯
⟦ e₁ catch e₂ ⟧ = ⟦ e₁ ⟧ ⊕ ⟦ e₂ ⟧
⟦ e₁ amb e₂ ⟧ = ⟦ e₁ ⟧ ∣ ⟦ e₂ ⟧
e₁ : Expr
e₁ = ((val 2 ⊖ val 1) amb throw) catch val 3
e₂ : Expr
e₂ = (val 2 amb val 1) ⊖ (val 1 amb val 0)
e₃ : Expr
e₃ = (val 2 amb throw) ⊖ (val 1 amb val 0)
e₄ : Expr
e₄ = (val 2 amb val 1) ⊖ (val 1 amb throw)