{-# OPTIONS --safe #-}

module CCS.Act where

open import Prelude hiding (⊥)

data Act (A : Type a) : Type a where
  emit : Bool → A → Act A
  τ : Act A

pattern inp x = emit false x
pattern out x = emit true x

map-act : (A → B) → Act A → Act B
map-act f (emit e x) = emit e (f x)
map-act f τ = τ

Message : Type a → Type a
Message A = Maybe (Act A)

module _ {A : Type a} where
  emit-inj : ∀ {s₁ s₂} {x y : A} → emit s₁ x ≡ emit s₂ y → x ≡ y
  emit-inj {x = x} = cong un-emit
    where
    un-emit : Act A → A
    un-emit τ = x
    un-emit (emit _ y) = y

emits? : Act A → Bool
emits? τ = false
emits? (emit _ _) = true

τ≢emit : ∀ {s} {a : A} → τ ≢ emit s a
τ≢emit = false≢true ∘ cong emits?
  where
  open import Data.Bool.Properties

pattern 𝕥 = nothing
pattern 𝕚 a = just a

module _ {A : Type a} where
  open import Data.Empty.UniversePolymorphic {a}

  infix  _∈ₐ_ _∉ₐ_ _ₛ∈ₐ_ _ₛ∉ₐ_ _∈ₘ_ _∉ₘ_ _ₛ∈ₘ_ _ₛ∉ₘ_
  _∈ₐ_ : A → Act A → Type a
  x ∈ₐ emit _ y = x ≡ y
  x ∈ₐ τ = ⊥

  _∉ₐ_ : A → Act A → Type a
  x ∉ₐ a = ¬ (x ∈ₐ a)

  _∈ₘ_ : A → Message A → Type a
  x ∈ₘ m = maybe ⊥ (x ∈ₐ_) m

  _∉ₘ_ : A → Message A → Type a
  x ∉ₘ a = ¬ (x ∈ₘ a)

  open import Data.List.Properties

  _ₛ∈ₐ_ : List A → Act A → Type a
  xs ₛ∈ₐ a = Any (_∈ₐ a) xs

  _ₛ∉ₐ_ : List A → Act A → Type a
  x ₛ∉ₐ a = ¬ (x ₛ∈ₐ a)

  _ₛ∈ₘ_ : List A → Message A → Type a
  xs ₛ∈ₘ a = Any (_∈ₘ a) xs

  _ₛ∉ₘ_ : List A → Message A → Type a
  x ₛ∉ₘ a = ¬ (x ₛ∈ₘ a)

  infix  _∣ₗ_ _∤ₗ_

  _∣ₗ_ _∤ₗ_ : Act A → Act A → Type _
  inp x ∣ₗ out y = x ≡ y
  _ ∣ₗ _ = ⊥
  a ∤ₗ b = ¬ (a ∣ₗ b)

  module _ ⦃ _ : IsDiscrete A ⦄ where

    infix  _∈ₐ?_ _∈ₘ?_ _ₛ∈ₐ?_ _ₛ∈ₘ?_
    _∈ₐ?_ : ∀ x a → Dec (x ∈ₐ a)
    x ∈ₐ? τ = no (λ ())
    x ∈ₐ? emit _ y = x ≟ y

    _∈ₘ?_ : ∀ x a → Dec (x ∈ₘ a)
    x ∈ₘ? 𝕥 = no λ ()
    x ∈ₘ? 𝕚 a = x ∈ₐ? a

    _ₛ∈ₐ?_ : ∀ x a → Dec (x ₛ∈ₐ a)
    xs ₛ∈ₐ? m = Any? (_∈ₐ? m) xs

    _ₛ∈ₘ?_ : ∀ x a → Dec (x ₛ∈ₘ a)
    xs ₛ∈ₘ? m = Any? (_∈ₘ? m) xs

module DiscreteActAlg ⦃ _ : IsDiscrete A ⦄ where
  _≡ᴮ_ : Act A → Act A → Bool
  inp x ≡ᴮ inp y = does (x ≟ y)
  out x ≡ᴮ out y = does (x ≟ y)
  τ ≡ᴮ τ = true
  _ ≡ᴮ _ = false

  sound : ∀ x y → T (x ≡ᴮ y) → x ≡ y
  sound (inp x) (inp y) x≡y = cong inp (from-does (x ≟ y) x≡y)
  sound (out x) (out y) x≡y = cong out (from-does (x ≟ y) x≡y)
  sound τ τ x≡y = refl

  complete : ∀ x → T (x ≡ᴮ x)
  complete (inp x) = to-does (x ≟ x) refl
  complete (out x) = to-does (x ≟ x) refl
  complete τ = tt

infix  _≟ᵃ_
_≟ᵃ_ : ⦃ _ : IsDiscrete A ⦄ → Discrete (Act A)
_≟ᵃ_ = from-bool-eq (record { DiscreteActAlg })


-- instance
--   discreteAct : ⦃ _ : IsDiscrete A ⦄ → IsDiscrete (Act A)
--   discreteAct = record { _≟_ = from-bool-eq (record { DiscreteActAlg }) }