------------------------------------------------------------------------
-- A simple language with exceptions and non-determinism
------------------------------------------------------------------------

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

------------------------------------------------------------------------
-- Language

-- A simple expression language.

data Expr : Set where
  val     : (n : )  Expr
  _⊖_     : (e₁ e₂ : Expr)  Expr
  throw   : Expr
  _catch_ : (e₁ e₂ : Expr)  Expr
  _amb_   : (e₁ e₂ : Expr)  Expr

-- The semantics of the language.

⟦_⟧ : Expr  List (Maybe )
 val n        = FND.return n
 e₁  e₂      = _∸_ <$>  e₁    e₂ 
 throw        = 
 e₁ catch e₂  =  e₁    e₂ 
 e₁ amb e₂    =  e₁    e₂ 

------------------------------------------------------------------------
-- Examples

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)

-- Note that e₃ yields three results, while e₄ yields four.