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

open import Prelude hiding (P)
open import CCS.Alg
open import CCS.SemiModel

module CCS.Hyp.Interp {r} {R : Type r} (alg : CCSAlg R) ⦃ _ : IsDiscrete (CCSAlg.Name alg) ⦄ where

open import Hyper.Base

open CCSAlg ⦃ ... ⦄ hiding (Name)
open CCSAlg alg using (Name)

open import CCS.Hyp.Definition Name R

instance
  _ : CCSAlg R
  _ = alg

open import CCS.Hyp.Alg {R = R} ⊕-magma {Name = Name}

instance
  _ : CCSAlg Communicator
  _ = hypAlg

prompt : (Maybe (Act Name) → R) → R
prompt k = k 𝕥

receive : R → Maybe (Act Name) → R
receive r (𝕚 a) = a · r
receive r 𝕥  = r

𝟙 : Communicator
⟦_⟧↓ : Communicator → R

ι 𝟙 h 𝕥  = 𝟘
ι 𝟙 h (𝕚 o) = o · ⟦ h ⟧↓

⟦ h ⟧↓ = ι h 𝟙 𝕥

com-ident : (c : Communicator) → ⟦ c ⟧↓ ≡ ι c 𝟙 𝕥
com-ident c = refl

syncₐₒ : Act Name → Communicator → Communicator → R
syncₐₒ a p q = ι q (𝟙 ∥ p) (𝕚 a)

ι-⌊-push : ∀ p q → ι p (q ∥ 𝟙) 𝕥 ≡ ⟦ p ⌊ q ⟧↓
ι-⌊-push p q = refl

act-hom↓ : ∀ (a : Act Name) (p : Communicator) → a · ⟦ p ⟧↓ ≡ ⟦ a · p ⟧↓
act-hom↓ a p = refl

⊕-hom↓ : ∀ (p q : Communicator) → ⟦ p ⟧↓ ⊕ ⟦ q ⟧↓ ≡ ⟦ p ⊕ q ⟧↓
⊕-hom↓ p q = refl