------------------------------------------------------------------------
-- This approach is (hopefully) easy to work with, but may be harder
-- to understand
------------------------------------------------------------------------

module Deterministic.EasyToWorkWith where

open import Data.Colist
open import Function
open import Coinduction
open import Relation.Nullary

open import Deterministic.Expr

-- Invokes coinduction only when the trace is empty.

∞? : Trace → Set → Set
∞? [] = ∞
∞? ms = id

infix 4 _HasTrace_

data _HasTrace_ : Semantics where
  nop  : ∀ {e   ms} (s : ∞? ms (♭ e HasTrace   ms)) → nop    e HasTrace     ms
  tick : ∀ {e m ms} (s : ∞     (♭ e HasTrace ♭ ms)) → tick m e HasTrace m ∷ ms

-- Helper function.

♭? : ∀ {ms e} → ∞? ms (e HasTrace ms) → e HasTrace ms
♭? {[]}    s = ♭ s
♭? {_ ∷ _} s = s

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

possible : nops HasTrace []
possible = nop (♯ possible)

impossible : ∀ {m ms} → ¬ nops HasTrace (m ∷ ms)
impossible (nop s) = impossible s

ok : ticks HasTrace scissors
ok = tick (♯ ok)