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

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

module CCS.Hyp.Properties {r} {R : Type r} (mod : CCSSemiModel R) ⦃ discName : IsDiscrete (CCSSemiModel.MName mod) ⦄ where

open CCSAlg ⦃ ... ⦄ hiding (Name)
open CCSAlg (CCSSemiModel.ccsAlg mod) using (Name)
open CCSSemiModel ⦃ ... ⦄ hiding (⊕⌊)

module ℝ = CCSSemiModel mod

instance
  _ : CCSSemiModel R
  _ = mod

instance
  _ : CCSAlg R
  _ = ccsAlg

open import CCS.Hyp.Definition Name R

open import CCS.Hyp.SemiModel ⊕-semilattice {Name = Name} public

open import CCS.Hyp.Renaming {R = R} ⊕-magma public

instance
  _ : CCSAlg Communicator
  _ = hypAlg

instance
  _ : CCSSemiModel Communicator
  _ = hypMod

open import CCS.Hyp.Interp {R = R} ccsAlg ⦃ discName ⦄

ι-·-τ : ∀ (a : Act Name) p q → ι (a · p) q (𝕚 τ) ≡ 𝟘
ι-·-τ (inp _) p q = refl
ι-·-τ (out _) p q = refl
ι-·-τ τ p q = refl

sync-nomatch : ∀ (a b : Act Name) p q → a ∤ₗ b → syncᵢₒ (a · p) (b · q) ≡ 𝟘
sync-nomatch a b p q a∤b = cong-ι (funExt ∘′ lemma a b p q a∤b)
  where
  lemma : ∀ (a b : Act Name) p q → a ∤ₗ b → ∀ h m → ι (a · p) ((b · q) ⌊ h) m ≡ 𝟘
  lemma (inp x₁) b p q a∤b h (𝕚 τ) = refl
  lemma (out x₁) b p q a∤b h (𝕚 τ) = refl
  lemma τ b p q a∤b h (𝕚 τ) = refl
  lemma τ b p q a∤b h (𝕚 (emit x x₁)) = refl
  lemma (inp a) b p q a∤b h (𝕚 (inp m)) = refl
  lemma (inp a) b p q a∤b h (𝕚 (out m)) = refl
  lemma (out a) b p q a∤b h (𝕚 (out m)) = refl
  lemma (out a) b p q a∤b h (𝕚 (inp m)) with m ≟ a
  ... | no m≢a = cong (bool _ _) (it-doesn't (m ≟ a) m≢a)
  lemma (out a) b p q a∤b h (𝕚 (inp m)) | yes m≡a = cong (bool _ _) (it-does (m ≟ a) m≡a) ⨾ ι-·-τ b _ _
  lemma a τ p q a∤b h 𝕥 = refl
  lemma a (inp _) p q a∤b h 𝕥 = refl
  lemma τ (out b) p q a∤b h 𝕥 = refl
  lemma (out a) (out b) p q a∤b h 𝕥 = refl
  lemma (inp a) (out b) p q a∤b h 𝕥 = cong (bool _ _) (it-doesn't (a ≟ b) a∤b)

sync-match : ∀ (a b : Act Name) (p : P Name) q → a ∣ₗ b → syncᵢₒ (a · ⟦ p ⟧) (b · q) ≡ τ · (⟦ p ⟧ ∥ q)
sync-match (inp _) τ p q ()
sync-match (out _) τ p q ()
sync-match (inp a) (out b) p q a∣b = cong (λ e → syncᵢₒ (inp a · ⟦ p ⟧) (out e · q)) (sym a∣b) ⨾ cong-ι (λ h → funExt (lemma a p q h))
  where
  lemma : ∀ (a : Name) p q → ∀ h m → ι (inp a · ⟦ p ⟧) ((out a · q) ⌊ h) m ≡ ι (τ · (⟦ p ⟧ ∥ q)) h m
  lemma a p q h (𝕚 τ) = refl
  lemma a p q h (𝕚 (inp _)) = refl
  lemma a p q h (𝕚 (out _)) = refl
  lemma a p q h 𝕥 =
    ι (inp a · ⟦ p ⟧) ((out a · q) ⌊ h) 𝕥 ≡⟨⟩
    ι (out a · q) (h ∥ ⟦ p ⟧) (𝕚 (inp a)) ≡⟨ cong (bool _ _) (it-does (a ≟ a) refl) ⟩
    ι (h ∥ ⟦ p ⟧) q (𝕚 τ) ≡⟨⟩
    ι (h ⌊ ⟦ p ⟧ ⊕ ⟦ p ⟧ ⌊ h) q (𝕚 τ) ≡⟨⟩
    ι (h ⌊ ⟦ p ⟧) q (𝕚 τ) ⊕ ι (⟦ p ⟧ ⌊ h) q (𝕚 τ) ≡⟨⟩
    ι h (⟦ p ⟧ ∥ q) (𝕚 τ) ⊕ ι ⟦ p ⟧ (h ∥ q) (𝕚 τ) ≡⟨ cong (ι h (⟦ p ⟧ ∥ q) (𝕚 τ) ⊕_) (ι-𝕚-τ→𝟘 p (h ∥ q)) ⟩
    ι h (⟦ p ⟧ ∥ q) (𝕚 τ) ⊕ 𝟘 ≡⟨ ⊕𝟘 _ ⟩
    ι h (⟦ p ⟧ ∥ q) (𝕚 τ) ≡⟨⟩
    ι (τ · (⟦ p ⟧ ∥ q)) h 𝕥 ∎

sync𝟘ʳ : ∀ (a : Act Name) (p : P Name) → syncᵢₒ ⟦ a · p ⟧ 𝟘 ≡ 𝟘
sync𝟘ʳ (out a) p = sync-out a ⟦ p ⟧ 𝟘
sync𝟘ʳ τ p = sync-τ ⟦ p ⟧ 𝟘
sync𝟘ʳ (inp a) p = cong-ι (funExt ∘′ lemma a p)
  where
  lemma : ∀ (a : Name) (p : P Name) h m → ι (syncᵢₒ ⟦ inp a · p ⟧ 𝟘) h m ≡ ι 𝟘 h m
  lemma a p h 𝕥 = refl
  lemma a p h (𝕚 _) = refl

ι-·-distrib-⊕ : ∀  (a : Act Name) (p : Communicator) q r m
              → ι (a · p) (q ⊕ r) m ≡ ι (a · p) q m ⊕ ι (a · p) r m
ι-·-distrib-⊕ a p q r 𝕥 = refl
ι-·-distrib-⊕ (inp _) p q r (𝕚 τ) = sym (⊕-idem _)
ι-·-distrib-⊕ (out _) p q r (𝕚 τ) = sym (⊕-idem _)
ι-·-distrib-⊕ τ p q r (𝕚 τ) = sym (⊕-idem _)
ι-·-distrib-⊕ (inp x₁) p q r (𝕚 (inp b)) = sym (⊕-idem _)
ι-·-distrib-⊕ τ p q r (𝕚 (inp b)) = sym (⊕-idem _)
ι-·-distrib-⊕ (inp x₁) p q r (𝕚 (out b)) = sym (⊕-idem _)
ι-·-distrib-⊕ (out x₁) p q r (𝕚 (out b)) = sym (⊕-idem _)
ι-·-distrib-⊕ τ p q r (𝕚 (out b)) = sym (⊕-idem _)
ι-·-distrib-⊕ (out a) p q r (𝕚 (inp b)) with b ≟ a
... | yes _ = refl
... | no _ = sym (⊕-idem _)

syncᵢₒ-⊕ʳ : ∀ (a : Act Name) p q r → syncᵢₒ (a · p) (q ⊕ r) ≡ syncᵢₒ (a · p) q ⊕ syncᵢₒ (a · p) r
syncᵢₒ-⊕ʳ a p q r = cong-ι (funExt ∘′ lemma a p q r)
  where
  lemma : ∀ a p q r h m → ι (syncᵢₒ (a · p) (q ⊕ r)) h m ≡ ι (syncᵢₒ (a · p) q ⊕ syncᵢₒ (a · p) r) h m
  lemma a p q r h m =
    ι (syncᵢₒ (a · p) (q ⊕ r)) h m ≡⟨⟩
    ι (a · p) ((q ⊕ r) ⌊ h) m ≡⟨ cong (flip (ι (a · p)) m) (⊕⌊ _ _ _) ⟩
    ι (a · p) (q ⌊ h ⊕ r ⌊ h) m ≡⟨ ι-·-distrib-⊕ a p (q ⌊ h) (r ⌊ h) m ⟩
    ι (a · p) (q ⌊ h) m ⊕ ι (a · p) (r ⌊ h) m ≡⟨⟩
    ι (syncᵢₒ (a · p) q ⊕ syncᵢₒ (a · p) r) h m ∎

syncᵢₒ-assoc : ∀ (a : Act Name) p q r → syncᵢₒ (a · p) (q ⌊ r) ≡ syncᵢₒ (a · (p ∥ r)) q
syncᵢₒ-assoc a p q r = cong-ι (funExt ∘′ lemma a p q r)
  where
  lemma : ∀ (a : Act Name) p q r h m → ι (a · p) ((q ⌊ r) ⌊ h) m ≡ ι (a · (p ∥ r)) (q ⌊ h) m
  lemma a p q r h 𝕥 =
    ι (a · p) ((q ⌊ r) ⌊ h) 𝕥 ≡⟨⟩
    ι q (r ∥ (h ∥ p)) (𝕚 a) ≡⟨ cong (flip (ι q) (𝕚 a)) (∥-comm r (h ∥ p) ⨾ ∥-assoc h p r) ⟩
    ι q (h ∥ (p ∥ r)) (𝕚 a) ≡⟨⟩
    ι (a · (p ∥ r)) (q ⌊ h) 𝕥 ∎
  lemma (inp x₁) p q r h (𝕚 τ) = refl
  lemma (out x₁) p q r h (𝕚 τ) = refl
  lemma τ p q r h (𝕚 τ) = refl
  lemma (inp x₂) p q r h (𝕚 (inp x₁)) = refl
  lemma (inp x₂) p q r h (𝕚 (out x₁)) = refl
  lemma (out x₂) p q r h (𝕚 (out x₁)) = refl
  lemma τ p q r h (𝕚 (inp x₁)) = refl
  lemma τ p q r h (𝕚 (out x₁)) = refl
  lemma (out a) p q r h (𝕚 (inp b)) with b ≟ a
  ... | no  b≢a = cong (bool _ _) (it-doesn't (b ≟ a) b≢a) ⨾ sym (cong (bool _ _) (it-doesn't (b ≟ a) b≢a))
  ... | yes b≡a = cong (bool _ _) (it-does (b ≟ a) b≡a) ⨾ cong (flip (ι q) (𝕚 τ)) (∥-comm r (h ∥ p) ⨾ ∥-assoc h p r) ⨾ sym (cong (bool _ _) (it-does (b ≟ a) b≡a))