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

module Deterministic.Expr where

open import Coinduction
open import Data.Colist

-- Messages.

data Msg : Set where
  ✂ : Msg
  ✈ : Msg
  ✆ : 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 : Msg) (e : ∞ Expr) → Expr

-- Traces.

Trace : Set
Trace = Colist Msg

-- Semantics.

Semantics : Set1
Semantics = Expr → Trace → Set

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

scissors : Trace
scissors = ✂ ∷ (♯ scissors)

nops : Expr
nops = nop (♯ nops)

ticks : Expr
ticks = tick ✂ (♯ ticks)