------------------------------------------------------------------------
-- The various approaches are equivalent
------------------------------------------------------------------------

module NonDeterministic.Equivalence where

open import Coinduction
open import Data.Colist

open import NonDeterministic.Expr
open import NonDeterministic.EasyToWorkWith
  renaming (_HasTrace_ to _HasTraceW_)
open import NonDeterministic.LongestPrefix
  renaming (_HasTrace_ to _HasTraceL_)

------------------------------------------------------------------------
-- EasyToWorkWith to LongestPrefix

WtoL[] : ∀ {e} → e HasTraceW [] → []⊑Trace[ e ]
WtoL[] (nop s) = nop (♯ WtoL[] (♭ s))

WtoL : ∀ {e ms} → e HasTraceW ms → e HasTraceL ms
WtoL s        ⊥                  = ⊥
WtoL s        []                 = []   (WtoL[] s)
WtoL (nop  s) (m ∷ p⊑ms)         = nop  (WtoL s (m ∷ p⊑ms))
WtoL (tick s) (.(user _) ∷ p⊑ms) = tick (WtoL (♭ s) p⊑ms)
WtoL (tock s) (.(ext  _) ∷ p⊑ms) = tock (WtoL (♭ s) p⊑ms)

------------------------------------------------------------------------
-- LongestPrefix to EasyToWorkWith

nop-lemmaL : ∀ {e ms} → nop e HasTraceL ms → ♭ e HasTraceL ms
nop-lemmaL s x = drop-nop (s x)
  where
  drop-nop : ∀ {ms e} → ms ⊑Trace[ nop e ] → ms ⊑Trace[ ♭ e ]
  drop-nop ⊥             = ⊥
  drop-nop ([] (nop x′)) = [] (♭ x′)
  drop-nop (nop  x′)     = x′
  drop-nop (tock x′)     = tock (drop-nop x′)

tick-lemmaL : ∀ {m e ms} →
              tick m e HasTraceL user m ∷ ms → ♭ e HasTraceL ♭ ms
tick-lemmaL {m} s x with s (user m ∷ x)
... | tick x′ = x′

tock-lemmaL : ∀ {m e ms} → e HasTraceL ext m ∷ ms → e HasTraceL ♭ ms
tock-lemmaL {m} s x = drop-tock (s (ext m ∷ x))
  where
  drop-tock : ∀ {ms e} → ext m ∷ ms ⊑Trace[ e ] → ms ⊑Trace[ e ]
  drop-tock (nop  x′) = nop (drop-tock x′)
  drop-tock (tock x′) = x′

mutual

  LtoW : ∀ e ms → e HasTraceL ms → e HasTraceW ms
  LtoW (nop e)    []             s = nop (♯ LtoW (♭ e) [] (nop-lemmaL s))
  LtoW (nop e)    (m ∷ ms)       s = LtoW′ s (s (m ∷ ⊥))
  LtoW (tick m e) []             s with s []
  LtoW (tick m e) []             s | [] ()
  LtoW (tick m e) (m′      ∷ ms) s with s (m′ ∷ ⊥)
  LtoW (tick m e) (user .m ∷ ms) s | tick x = tick (♯ LtoW (♭ e) (♭ ms) (tick-lemmaL s))
  LtoW (tick m e) (ext  m′ ∷ ms) s | tock x = tock (♯ LtoW (tick m e) (♭ ms) (tock-lemmaL s))

  LtoW′ : ∀ {e m ms} →
          e HasTraceL m ∷ ms → m ∷ ⊥ ⊑Trace[ e ] → e HasTraceW m ∷ ms
  LtoW′ s (nop  x) = nop (LtoW′ (nop-lemmaL s) x)
  LtoW′ s (tick x) = tick (♯ LtoW _ _ (tick-lemmaL s))
  LtoW′ s (tock x) = tock (♯ LtoW _ _ (tock-lemmaL s))