------------------------------------------------------------------------
-- Expressions and other shared code
------------------------------------------------------------------------

module NonDeterministic.Expr where

open import Coinduction
open import Data.Colist

-- Messages.

data UserMsg : Set where
  ✂ : UserMsg
  ✈ : UserMsg
  ✆ : UserMsg

data ExternalMsg : Set where
  ↯ : ExternalMsg

data Msg : Set where
  user : (m : UserMsg) → Msg
  ext  : (m : ExternalMsg) → Msg

-- Unannotated expressions.

data Expr : Set where
  -- Does not emit a message and continues with e.
  nop  : (e : ∞ Expr) → Expr
  -- Emits the message m and continues with e.
  tick : (m : UserMsg) (e : ∞ Expr) → Expr

-- Traces.

Trace : Set
Trace = Colist Msg

-- Semantics.

Semantics : Set1
Semantics = Expr → Trace → Set

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

scissors : Trace
scissors = user ✂ ∷ (♯ scissors)

nops : Expr
nops = nop (♯ nops)

ticks : Expr
ticks = tick ✂ (♯ ticks)