{-# OPTIONS --no-termination-check #-}

open import Algebra
open import Prelude hiding (P)

module CCS.Hyp.Alg {r} {R : Type r} (mod : UnitalMagma R) {Name : Type r} where

open import CCS.Alg
open import CCS.Hyp.Definition Name R
open import Hyper.Base

open UnitalMagma mod

module ℍ-Alg where
  𝟘 : Communicator
  ι 𝟘 _ _ = ε

  infixl  _⊕_
  _⊕_ : Communicator → Communicator → Communicator
  (p ⊕ q) .ι h m = ι p h m ∙ ι q h m

  infixl  _⌊_ _∥_
  _⌊_ _∥_ : Communicator → Communicator → Communicator

  ι (p ⌊ q) h = ι p (q ∥ h)
  p ∥ q = p ⌊ q ⊕ q ⌊ p

  ! : Communicator → Communicator
  ι (! p) h = ι p (! p ∥ h)

  module _ ⦃ _ : IsDiscrete Name ⦄ where
    infixr  _·_
    _·_ : Act Name → Communicator → Communicator
    ι (a     · p) q 𝕥           = ι q p (𝕚 a)
    ι (out b · p) q (𝕚 (inp a)) = if does (a ≟ b) then ι q p (𝕚 τ) else ε
    ι (_     · _) _ _           = ε

    infixr  ν_-_
    ν_-_ : Name → Communicator → Communicator
    ι (ν n - p) q m = if does (n ∈ₘ? m) then ε else ι p (ν n - q) m

hypAlg : ⦃ _ : IsDiscrete Name ⦄ → CCSAlg Communicator
hypAlg = record { ℍ-Alg }

open ℍ-Alg

⟦_⟧ᶜ : ⦃ _ : IsDiscrete Name ⦄ → P Name → Communicator
⟦_⟧ᶜ = CCSAlg.⟦_⟧ hypAlg

syncᵢₒ : Communicator → Communicator → Communicator
ι (syncᵢₒ p q) o = ι p (q ⌊ o)

stepₗ : Communicator → Communicator → Communicator
ι (stepₗ p q) o = ι p (o ⌊ q)

step-· : ⦃ _ : IsDiscrete Name ⦄ → ∀ a p q → stepₗ (a · p) q ≡ a · (q ∥ p)
step-· a p q = cong-ι (funExt ∘′ lemma a p q)
  where
  lemma : ∀ a p q r m → ι (stepₗ (a · p) q) r m ≡ ι (a · (q ∥ p)) r m
  lemma a p q r 𝕥 = refl
  lemma (inp _) p q r (𝕚 _) = refl
  lemma τ p q r (𝕚 _) = refl
  lemma (out b) p q r (𝕚 (out x)) = refl
  lemma (out b) p q r (𝕚 τ) = refl
  lemma (out b) p q r (𝕚 (inp a)) = refl

⊕⌊ : ∀ x y z → (x ⊕ y) ⌊ z ≡ (x ⌊ z) ⊕ (y ⌊ z)
⊕⌊ x y z = cong-ι λ h → refl

⌊-∥ : ∀ p q → (p ∥ q) ≡ (p ⌊ q) ⊕ (q ⌊ p)
⌊-∥ p q = cong-ι λ h → refl

!-⌊ : ∀ p → ! p ≡ p ⌊ ! p
!-⌊ p = cong-ι λ h → refl

𝟘⌊ : ∀ p → 𝟘 ⌊ p ≡ 𝟘
𝟘⌊ p = cong-ι λ k → refl

sync𝟘ˡ : ∀ p → syncᵢₒ 𝟘 p ≡ 𝟘
sync𝟘ˡ p = cong-ι λ _ → refl

step𝟘ˡ : ∀ p → stepₗ 𝟘 p ≡ 𝟘
step𝟘ˡ p = cong-ι λ _ → refl

module _ ⦃ _ : IsDiscrete Name ⦄ where
  open import Data.Bool.Properties

  ν𝟘 : ∀ n → ν n - 𝟘 ≡ 𝟘
  ν𝟘 n = cong-ι λ h → funExt λ m → if-idem ε (does (n ∈ₘ? m))

  ν-comm : ∀ x y p → ν x - ν y - p ≡ ν y - ν x - p
  ν-comm x y p = cong-ι λ h → funExt (lemma x y p h)
    where
    lemma : ∀ x y p h m → ι (ν x - ν y - p) h m ≡ ι (ν y - ν x - p) h m
    lemma x y p h (𝕚 τ) = cong (flip (ι p) (𝕚 τ)) (ν-comm y x h)
    lemma x y p h 𝕥 = cong (flip (ι p) 𝕥) (ν-comm y x h)
    lemma x y p h (𝕚 (inp z)) with x ≟ z | y ≟ z
    ... | no  _ | no  _ = cong (flip (ι p) (𝕚 (inp z))) (ν-comm y x h)
    ... | no  _ | yes _ = refl
    ... | yes _ | no  _ = refl
    ... | yes _ | yes _ = refl
    lemma x y p h (𝕚 (out z)) with x ≟ z | y ≟ z
    ... | no  _ | no  _ = cong (flip (ι p) (𝕚 (out z))) (ν-comm y x h)
    ... | no  _ | yes _ = refl
    ... | yes _ | no  _ = refl
    ... | yes _ | yes _ = refl