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

module Deterministic.ShortestExtension where

open import Data.Nat
open import Data.Colist
open import Coinduction
open import Data.Maybe
open import Data.Product
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Deterministic.Expr

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

open import Deterministic.Incorrect public
  using (nop; tick) renaming (_HasTrace_ to Trace[_]⊑_)

-- Note that the trace is the shortest extension of the trace.

infix 4 _HasTrace_

_HasTrace_ : Semantics
e HasTrace ms = Trace[ e ]⊑ ms × (∀ {ms′} → Trace[ e ]⊑ ms′ → ms ⊑ ms′)

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

Trace[nops]⊑[] : Trace[ nops ]⊑ []
Trace[nops]⊑[] = nop (♯ Trace[nops]⊑[])

possible : nops HasTrace []
possible = (Trace[nops]⊑[] , λ _ → [])

impossible : ∀ {m ms} → ¬ nops HasTrace (m ∷ ms)
impossible ht with proj₂ ht Trace[nops]⊑[]
... | ()

ok : ticks HasTrace scissors
ok = (prefix , λ {_} → shortest)
  where
  prefix : Trace[ ticks ]⊑ scissors
  prefix = tick (♯ prefix)

  shortest : ∀ {ms} → Trace[ ticks ]⊑ ms → scissors ⊑ ms
  shortest (tick x) = ✂ ∷ ♯ shortest (♭ x)