------------------------------------------------------------------------
-- This approach is easy to understand, but probably more awkward to
-- work with
------------------------------------------------------------------------

module Deterministic.EasyToUnderstand 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 Function.Equality
open import Function.Equivalence
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Deterministic.Expr

infix 4 _[_]=_ _⟨_⟩=_ _HasTrace_

-- e [ i ]= m means that the i-th message in e is m.

data _[_]=_ : Expr → ℕ → Msg → Set where
  nop       : ∀ {e i m}    (x : ♭ e [ i ]= m) → nop     e [ i     ]= m
  tick-zero : ∀ {e m}                         → tick m  e [ zero  ]= m
  tick-suc  : ∀ {e i m m′} (x : ♭ e [ i ]= m) → tick m′ e [ suc i ]= m

_⟨_⟩=_ : ∀ {A} → Colist A → ℕ → A → Set
ms ⟨ i ⟩= m = lookup i ms ≡ just m

_HasTrace_ : Semantics
e HasTrace ms = ∀ i m → ms ⟨ i ⟩= m  ⇔  e [ i ]= m

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

no-msgs : ∀ {i m} → ¬ nops [ i ]= m
no-msgs (nop x) = no-msgs x

possible : nops HasTrace []
possible i m = equivalent (λ()) (λ eq → ⊥-elim (no-msgs eq))

impossible : ∀ m ms → ¬ nops HasTrace (m ∷ ms)
impossible m ms ht = no-msgs (Equivalent.to (ht zero m) ⟨$⟩ refl)

ok : ticks HasTrace scissors
ok i m = equivalent (⇒ i m) (⇐ i m)
  where
  ⇒ : ∀ i m → scissors ⟨ i ⟩= m → ticks [ i ]= m
  ⇒ zero    .✂ refl = tick-zero
  ⇒ (suc n) m  eq   = tick-suc (⇒ n m eq)

  ⇐ : ∀ i m → ticks [ i ]= m → scissors ⟨ i ⟩= m
  ⇐ zero    .✂ tick-zero    = refl
  ⇐ (suc n) m  (tick-suc x) = ⇐ n m x