------------------------------------------------------------------------
-- The language is deterministic
------------------------------------------------------------------------

module Deterministic.Deterministic where

open import Coinduction
open import Data.Colist
open import Data.Empty

-- I can choose any semantics (since they are all equivalent), so I
-- choose EasyToWorkWith.

open import Deterministic.Expr
open import Deterministic.EasyToWorkWith

[]∷-lemma : ∀ {e m ms} → e HasTrace [] → e HasTrace m ∷ ms → ⊥
[]∷-lemma (nop s₁) (nop s₂) = []∷-lemma (♭ s₁) s₂

deterministic : ∀ {e} ms₁ ms₂ →
                e HasTrace ms₁ → e HasTrace ms₂ → ms₁ ≈ ms₂
deterministic []         []         s₁        s₂        = []
deterministic []         (m  ∷ ms)  s₁        s₂        = ⊥-elim ([]∷-lemma s₁ s₂)
deterministic (m  ∷ ms)  []         s₁        s₂        = ⊥-elim ([]∷-lemma s₂ s₁)
deterministic (m₁ ∷ ms₁) (m₂ ∷ ms₂) (nop  s₁) (nop  s₂) = deterministic _ _ s₁ s₂
deterministic (m  ∷ ms₁) (.m ∷ ms₂) (tick s₁) (tick s₂) = m ∷ ♯ deterministic _ _ (♭ s₁) (♭ s₂)