------------------------------------------------------------------------ -- 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.