{-# OPTIONS --safe #-}

module CCS.Alg where

open import Prelude hiding (P; ⊥)
open import CCS.Act public

open import CCS.Syntax
  renaming
  ( _·_ to _`·_
  ; ν_-_ to `ν_-_
  ; _⊕_ to _`⊕_
  ; _⌊_ to _`⌊_
  ; _∥_ to _`∥_
  ; ! to `!
  ; 𝟘 to `𝟘
  ; ρ to `ρ
  )
  public

record CCSAlg (C : Type c) : Type (ℓsuc c) where
  infixr  _·_
  infixr  ν_-_
  infixl  _⊕_
  infixl  _∥_ _⌊_
  field
    Name : Type c
    𝟘 : C
    _⊕_ _∥_ _⌊_ : C → C → C
    _·_ : Act Name → C → C
    ν_-_ : Name → C → C
    ! : C → C

  ⟦_⟧ : P Name → C
  ⟦ `𝟘 ⟧ = 𝟘
  ⟦ p `⊕ q ⟧ = ⟦ p ⟧ ⊕ ⟦ q ⟧
  ⟦ p `⌊ q ⟧ = ⟦ p ⟧ ⌊ ⟦ q ⟧
  ⟦ p `∥ q ⟧ = ⟦ p ⟧ ∥ ⟦ q ⟧
  ⟦ a `· p ⟧ = a · ⟦ p ⟧
  ⟦ `ν n - p ⟧ = ν n - ⟦ p ⟧
  ⟦ `! p ⟧ = ! ⟦ p ⟧

  infixr  νₛ_-_ νₛᵣ_-_
  νₛ_-_ : List Name → C → C
  νₛ_-_ = flip (foldl (flip ν_-_))
  {-# INLINE νₛ_-_ #-}

  νₛᵣ_-_ : List Name → C → C
  νₛᵣ_-_ = flip (foldr ν_-_)

  νₛ-ident : ∀ n ns p → νₛ n ∷ ns - p ≡ νₛ ns - ν n - p
  νₛ-ident n ns p = refl

  νₛ-++ : ∀ ns ms p → νₛ ns - νₛ ms - p ≡ νₛ ms ++ ns - p
  νₛ-++ ns ms p = sym (foldl-++ (flip ν_-_) p ms ns)
    where open import Data.List.Properties using (foldl-++)

  open import Algebra

  ⊕-magma : UnitalMagma C
  ⊕-magma = record { _∙_ = _⊕_; ε = 𝟘 }

  open UnitalMagma ⊕-magma using (_⊆_) public

  record ⊕-Distributive (f : P Name → P Name) : Type c where
    field
      ⊕-distrib : ∀ p q → ⟦ f (p `⊕ q) ⟧ ≡ ⟦ f p ⟧ ⊕ ⟦ f q ⟧
      𝟘-distrib : ⟦ f `𝟘 ⟧ ≡ ⟦ `𝟘 ⟧

instance
  syntaxAlg : CCSAlg (P A)
  syntaxAlg = record
    { 𝟘 = `𝟘
    ; _⊕_ = _`⊕_
    ; _∥_ = _`∥_
    ; _⌊_ = _`⌊_
    ; _·_ = _`·_
    ; ν_-_ = `ν_-_
    ; ! = `!
    }