{-# OPTIONS --safe #-}

module CCS.Syntax where

open import Prelude hiding (P; ⊥)

open import CCS.Act

infixr  _·_ ν_-_
infixl  _⊕_
infixl  _⌊_ _∥_
data P (A : Type b) : Type b where
  𝟘 : P A
  _⊕_  : (p : P A) (q : P A) → P A
  _⌊_  : (p : P A) (q : P A) → P A
  _∥_  : (p : P A) (q : P A) → P A
  _·_  : (a : Act A) (p : P A) → P A
  ν_-_ : (n : A) (p : P A) → P A
  ! : (p : P A) → P A

module _ {A : Type a} where
  open import Data.Empty.UniversePolymorphic {a}
  infix  _∈ₚ_ _∉ₚ_
  _∈ₚ_ : A → P A → Type a
  n ∈ₚ 𝟘 = ⊥
  n ∈ₚ p ⊕ q = (n ∈ₚ p) ⊎ (n ∈ₚ q)
  n ∈ₚ p ⌊ q = (n ∈ₚ p) ⊎ (n ∈ₚ q)
  n ∈ₚ p ∥ q = (n ∈ₚ p) ⊎ (n ∈ₚ q)
  n ∈ₚ a · p = (n ∈ₐ a) ⊎ (n ∈ₚ p)
  n ∈ₚ ν x - p = (n ≡ x) ⊎ (n ∈ₚ p)
  n ∈ₚ ! p = n ∈ₚ p

  _∉ₚ_ : A → P A → Type a
  n ∉ₚ p = ¬ (n ∈ₚ p)

ρ : (A → B) → P A → P B
ρ f 𝟘 = 𝟘
ρ f (x ⊕ y) = ρ f x ⊕ ρ f y
ρ f (x ⌊ y) = ρ f x ⌊ ρ f y
ρ f (x ∥ y) = ρ f x ∥ ρ f y
ρ f (x · y) = map-act f x · ρ f y
ρ f (ν n - x) = ν f n - ρ f x
ρ f (! x) = ! (ρ f x)

ρᵢ : (p : P A) → (∀ x → x ∈ₚ p → B) → P B
ρᵢ 𝟘 f = 𝟘
ρᵢ (p ⊕ q) f = ρᵢ p (λ x → f x ∘ inl) ⊕ ρᵢ q (λ x → f x ∘ inr)
ρᵢ (p ⌊ q) f = ρᵢ p (λ x → f x ∘ inl) ⌊ ρᵢ q (λ x → f x ∘ inr)
ρᵢ (p ∥ q) f = ρᵢ p (λ x → f x ∘ inl) ∥ ρᵢ q (λ x → f x ∘ inr)
ρᵢ (inp x · p) f = inp (f x (inl refl)) · ρᵢ p (λ x → f x ∘ inr)
ρᵢ (out x · p) f = out (f x (inl refl)) · ρᵢ p (λ x → f x ∘ inr)
ρᵢ (τ · p) f = τ · ρᵢ p (λ x → f x ∘ inr)
ρᵢ (ν n - p) f = ν (f n (inl refl)) - ρᵢ p (λ x → f x ∘ inr)
ρᵢ (! p) f = ! (ρᵢ p f)

ρ≡ρᵢ : (p : P A) (f : A → B) → ρ f p ≡ ρᵢ p (const ∘′ f)
ρ≡ρᵢ 𝟘 f = refl
ρ≡ρᵢ (p ⊕ q) f = cong₂ _⊕_ (ρ≡ρᵢ p f) (ρ≡ρᵢ q f)
ρ≡ρᵢ (p ⌊ q) f = cong₂ _⌊_ (ρ≡ρᵢ p f) (ρ≡ρᵢ q f)
ρ≡ρᵢ (p ∥ q) f = cong₂ _∥_ (ρ≡ρᵢ p f) (ρ≡ρᵢ q f)
ρ≡ρᵢ (inp x · p) f = cong (inp (f x) ·_) (ρ≡ρᵢ p f)
ρ≡ρᵢ (out x · p) f = cong (out (f x) ·_) (ρ≡ρᵢ p f)
ρ≡ρᵢ (τ · p) f = cong (τ ·_) (ρ≡ρᵢ p f)
ρ≡ρᵢ (ν n - p) f = cong (ν f n -_) (ρ≡ρᵢ p f)
ρ≡ρᵢ (! p) f = cong ! (ρ≡ρᵢ p f)

fold-P : (A → A → A) → A → P A → A
fold-P f b 𝟘            = b
fold-P f b (xs ⊕ ys)    = f (fold-P f b xs) (fold-P f b ys)
fold-P f b (xs ⌊ ys)    = f (fold-P f b xs) (fold-P f b ys)
fold-P f b (xs ∥ ys)    = f (fold-P f b xs) (fold-P f b ys)
fold-P f b (inp x · xs) = f x (fold-P f b xs)
fold-P f b (out x · xs) = f x (fold-P f b xs)
fold-P f b (τ · xs)     = fold-P f b xs
fold-P f b (ν x - xs)   = f x (fold-P f b xs)
fold-P f b (! xs)       = fold-P f b xs

foldr-P : (A → B → B) → B → P A → B
foldr-P f b 𝟘            = b
foldr-P f b (xs ⊕ ys)    = foldr-P f (foldr-P f b ys) xs
foldr-P f b (xs ⌊ ys)    = foldr-P f (foldr-P f b ys) xs
foldr-P f b (xs ∥ ys)    = foldr-P f (foldr-P f b ys) xs
foldr-P f b (inp x · xs) = f x (foldr-P f b xs)
foldr-P f b (out x · xs) = f x (foldr-P f b xs)
foldr-P f b (τ · xs)     = foldr-P f b xs
foldr-P f b (ν x - xs)   = f x (foldr-P f b xs)
foldr-P f b (! xs)       = foldr-P f b xs

map-∈ₐ : ∀ (f : A → B) x a → x ∈ₐ a → f x ∈ₐ map-act f a
map-∈ₐ f x (inp y) = cong f
map-∈ₐ f x (out y) = cong f

ρ-∈ₚ : ∀ (f : A → B) x p → x ∈ₚ p → f x ∈ₚ ρ f p
ρ-∈ₚ f x (p ⊕ q) = map-⊎ (ρ-∈ₚ f x p) (ρ-∈ₚ f x q)
ρ-∈ₚ f x (p ⌊ q) = map-⊎ (ρ-∈ₚ f x p) (ρ-∈ₚ f x q)
ρ-∈ₚ f x (p ∥ q) = map-⊎ (ρ-∈ₚ f x p) (ρ-∈ₚ f x q)
ρ-∈ₚ f x (a · p) = map-⊎ (map-∈ₐ f x a) (ρ-∈ₚ f x p)
ρ-∈ₚ f x (ν n - p) = map-⊎ (cong f) (ρ-∈ₚ f x p)
ρ-∈ₚ f x (! p) x∈p = ρ-∈ₚ f x p x∈p

ρ-∉ₚ : ∀ (f : A ↣ B) x p → x ∉ₚ p → fst f x ∉ₚ ρ (fst f) p
ρ-∉ₚ f x (p ⊕ q) x∉p = ρ-∉ₚ f x p (x∉p ∘ inl) ▿ ρ-∉ₚ f x q (x∉p ∘ inr)
ρ-∉ₚ f x (p ⌊ q) x∉p = ρ-∉ₚ f x p (x∉p ∘ inl) ▿ ρ-∉ₚ f x q (x∉p ∘ inr)
ρ-∉ₚ f x (p ∥ q) x∉p = ρ-∉ₚ f x p (x∉p ∘ inl) ▿ ρ-∉ₚ f x q (x∉p ∘ inr)
ρ-∉ₚ f x (inp n · p) x∉p (inl fx∈fa) = x∉p (inl (snd f fx∈fa))
ρ-∉ₚ f x (out n · p) x∉p (inl fx∈fa) = x∉p (inl (snd f fx∈fa))
ρ-∉ₚ f x (a · p) x∉p (inr fx∈p) = ρ-∉ₚ f x p (x∉p ∘ inr) fx∈p
ρ-∉ₚ f x (ν n - p) x∉p (inl fx≡n) = x∉p (inl (snd f fx≡n))
ρ-∉ₚ f x (ν n - p) x∉p (inr fx∈p) = ρ-∉ₚ f x p (x∉p ∘ inr) fx∈p
ρ-∉ₚ f x (! p) x∉p x∈p = ρ-∉ₚ f x p x∉p x∈p

module _ {A : Type a} ⦃ _ : IsDiscrete A ⦄ where
  open import Swaps {A = A} ⦃ it ⦄

  ρ→∉ : ∀ x y p → x ∉ₚ p → ρ (x /→ y) p ≡ p
  ρ→∉ x y 𝟘 x∉p = refl
  ρ→∉ x y (p ⊕ q) x∉p = cong₂ _⊕_ (ρ→∉ x y p (λ z → x∉p (inl z))) (ρ→∉ x y q (λ z → x∉p (inr z)))
  ρ→∉ x y (p ⌊ q) x∉p = cong₂ _⌊_ (ρ→∉ x y p (λ z → x∉p (inl z))) (ρ→∉ x y q (λ z → x∉p (inr z)))
  ρ→∉ x y (p ∥ q) x∉p = cong₂ _∥_ (ρ→∉ x y p (λ z → x∉p (inl z))) (ρ→∉ x y q (λ z → x∉p (inr z)))
  ρ→∉ x y (inp z · p) x∉p = cong₂ _·_ (cong inp (cong (bool′ _ _) (it-doesn't (z ≟ x) (x∉p ∘ inl ∘ sym)))) (ρ→∉ x y p (λ z → x∉p (inr z)))
  ρ→∉ x y (out z · p) x∉p = cong₂ _·_ (cong out (cong (bool′ _ _) (it-doesn't (z ≟ x) (x∉p ∘ inl ∘ sym)))) (ρ→∉ x y p (λ z → x∉p (inr z)))
  ρ→∉ x y (τ · p) x∉p = cong (τ ·_) (ρ→∉ x y p (λ z → x∉p (inr z)))
  ρ→∉ x y (ν z - p) x∉p with z ≟ x
  ... | yes z≡x = absurd (x∉p (inl (sym z≡x)))
  ... | no  z≢x = cong (ν z -_) (ρ→∉ x y p λ z → x∉p (inr z))
  ρ→∉ x y (! p) x∉p = cong ! (ρ→∉ x y p x∉p)

  ρ-∉-↔ : ∀ (n m : A) (p : P A) → m ∉ₚ p → ρ (n /→ m) p ≡ ρ (n /↔ m) p
  ρ-∉-↔ n m p m∉p =
    ρ (n /→ m) p ≡⟨ ρ≡ρᵢ p (n /→ m) ⟩
    ρᵢ p (const ∘′ (n /→ m)) ≡⟨ cong (ρᵢ p) (funExt (funExt ∘′ lemma))  ⟩
    ρᵢ p (const ∘′ (n /↔ m)) ≡˘⟨ ρ≡ρᵢ p (n /↔ m) ⟩
    ρ (n /↔ m) p ∎
    where
    lemma : ∀ x → x ∈ₚ p → (n /→ m) x ≡ (n /↔ m) x
    lemma x x∈p with x ≟ n
    ... | yes _ = refl
    ... | no x≢n with x ≟ m
    ... | no _ = refl
    ... | yes x≡m = absurd (m∉p (subst (_∈ₚ p) x≡m x∈p))