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

module NonDeterministic.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 Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import NonDeterministic.Expr

------------------------------------------------------------------------
-- Partial lists

-- A partial list can end in ⊥.

infixr  _∷_

data PartialList (A : Set) : Set where
  ⊥   : PartialList A
  []  : PartialList A
  _∷_ : (x : A) (xs : PartialList A) → PartialList A

-- xs ⊑ ys means that xs is an approximation of ys.

infix  _⊑_

data _⊑_ {A} : PartialList A → Colist A → Set where
  ⊥   : ∀ {ys}                          → ⊥      ⊑ ys
  []  :                                   []     ⊑ []
  _∷_ : ∀ x {xs ys} (xs⊑ys : xs ⊑ ♭ ys) → x ∷ xs ⊑ x ∷ ys

------------------------------------------------------------------------
-- Semantics

-- []⊑Trace[ e ] means that [] is an approximation of the trace of e.
--
-- The use of coinduction here is unsatisfactory to me. It would
-- perhaps be more natural to use ⊥ as the semantics/trace of a
-- non-terminating, non-productive computation (an infinite sequence
-- of nops which does not emit any messages). In that case I believe
-- that it would be correct to say that ms (a partial stream) is one
-- of the traces of e if
--   ⑴ all /finite/ approximations of ms are approximations of the
--     trace of e, and also
--   ⑵ ms is not an approximation of some other partial stream ms′
--     satisfying ⑴, ignoring streams ms′ that differ from ms just by
--     the addition of trailing external messages.
-- However, the second part of ⑵ (ignoring…) seems a bit ugly, so I
-- have not pursued this definition.

data []⊑Trace[_] : Expr → Set where
  nop : ∀ {e} (x : ∞ []⊑Trace[ ♭ e ]) → []⊑Trace[ nop e ]

-- ms ⊑Trace[ e ] means that ms is an approximation of the trace of e.

infix  _⊑Trace[_]

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

-- A colist of messages is a trace of e if all its approximations are
-- approximations of /some/ trace of e.

infix  _HasTrace_

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

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

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

possible : nops HasTrace []
possible ⊥  = ⊥
possible [] = [] []⊑Trace[nops]

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

impossible : ∀ {m ms} → ¬ nops HasTrace (user m ∷ ms)
impossible {m} ht = no-msgs (ht (user m ∷ ⊥))

ok : ticks HasTrace scissors
ok ⊥                   = ⊥
ok (.(user ✂) ∷ xs⊑ys) = tick (ok xs⊑ys)