------------------------------------------------------------------------
-- This approach appears to be both awkward to use and non-trivial to
-- understand
------------------------------------------------------------------------

module Deterministic.LongestPrefix where

open import Data.Nat
open import Data.List
open import Data.Colist hiding ([_])
open import Coinduction
open import Data.Maybe
open import Data.Product
open import Data.Empty
open import Function.Equality
open import Function.Equivalence
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Deterministic.Expr

-- ms ⊑Trace[ e ] means that ms is a prefix of the trace of e.

infix 4 _⊑Trace[_]

data _⊑Trace[_] : List Msg → Expr → Set where
  []   : ∀ {e}                             → []     ⊑Trace[ e        ]
  nop  : ∀ {e ms}   (x : ms ⊑Trace[ ♭ e ]) → ms     ⊑Trace[ nop    e ]
  tick : ∀ {e m ms} (x : ms ⊑Trace[ ♭ e ]) → m ∷ ms ⊑Trace[ tick m e ]

-- Note that the trace is the longest colist which is a prefix of the
-- trace.

infix 4 _HasTrace_

_HasTrace_ : Semantics
e HasTrace ms = ∀ {p} → p ⊑Trace[ e ]  ⇔  fromList p ⊑ ms

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

possible : nops HasTrace []
possible = equivalent longest (prefix _)
  where
  longest : ∀ {ms} → ms ⊑Trace[ nops ] → fromList ms ⊑ []
  longest []      = []
  longest (nop x) = longest x

  prefix : ∀ ms → fromList ms ⊑ [] → ms ⊑Trace[ nops ]
  prefix []       _  = []
  prefix (m ∷ ms) ()

no-msgs : ∀ {m p} → ¬ m ∷ p ⊑Trace[ nops ]
no-msgs (nop x) = no-msgs x

impossible : ∀ {m ms} → ¬ nops HasTrace (m ∷ ms)
impossible {m} ht = no-msgs (Equivalent.from ht ⟨$⟩ m ∷ ♯ [])

ok : ticks HasTrace scissors
ok = equivalent longest (prefix _)
  where
  longest : ∀ {ms} → ms ⊑Trace[ ticks ] → fromList ms ⊑ scissors
  longest []       = []
  longest (tick x) = ✂ ∷ ♯ longest x

  prefix : ∀ ms → fromList ms ⊑ scissors → ms ⊑Trace[ ticks ]
  prefix []        _        = []
  prefix (.✂ ∷ ms) (.✂ ∷ p) = tick (prefix ms (♭ p))