{-# OPTIONS --safe -WnoUnsupportedIndexedMatch #-}

module CCS.Bisimilar where

open import Prelude
  hiding (P; a; b; c; p)
open import CCS.Syntax
open import CCS.Act

open import Data.List

private
  variable
    ℓ ℓ′ : Level
    N : Type ℓ
    M : Type ℓ′
    n : N
    a : Act N
    b : Act M
    p p′ : P N
    q q′ : P M

module _ {N : Type ℓ} where
  infix  _-[_]→_
  data _-[_]→_ : P N → Act N → P N → Type ℓ where

    act :

        -----------------
         a · p -[ a ]→ p

    sumₗ :

            p -[ a ]→ p′
       → ------------------
          p ⊕ q -[ a ]→ p′

        
    sumᵣ :

            q -[ a ]→ q′
       → ------------------
          p ⊕ q -[ a ]→ q′


    stepₗ :

             p -[ a ]→ p′
       → ----------------------
          p ⌊ q -[ a ]→ p′ ⌊ q

    -- stepᵣ :

    --          q -[ a ]→ q′
    --    → ---------------------
    --       p ∥ q -[ a ]→ p ∥ q′

    syncᵢₒ : 

          p -[ inp n ]→ p′
      →   q -[ out n ]→ q′
      → -----------------------
          p ⌊ q -[ τ ]→ p′ ⌊ q′

    -- syncₒᵢ : 

    --         p -[ out n ]→ p′
    --   →     q -[ inp n ]→ q′
    --   → -----------------------
    --       p ∥ q -[ τ ]→ p′ ∥ q′

    res : 

                p -[ a ]→ p′
      →           n ∉ₐ a
      → ---------------------------
          ν n - p -[ a ]→ ν n - p′

    rep :

           p ∥ ! p -[ a ]→ p′
      → -----------------------
             ! p -[ a ]→ p′

    parₗ :

           p ⌊ q -[ a ]→ p′
      → -----------------------
           p ∥ q -[ a ]→ p′

    parᵣ :

           q ⌊ p -[ a ]→ q′
      → -----------------------
           p ∥ q -[ a ]→ q′


  mutual
    infix  _≲_ _≈_

    record Evolve (q p′ : P N) (a : Act N) : Type ℓ where
      inductive
      field
        result : P N
        evolves : q -[ a ]→ result
        bisim : p′ ≈ result

    record _≲_ (p q : P N) : Type ℓ where
      coinductive
      field
        step : ∀ a p′
             → (p-a→p′ : p -[ a ]→ p′)
             → Evolve q p′ a

    _≈_ : P N → P N → Type ℓ
    p ≈ q = p ≲ q × q ≲ p

open _≲_ public
open Evolve public


≈-refl : (p : P N) → p ≈ p
≈-refl p .fst .step a p′ p-a→p′ .result = p′
≈-refl p .fst .step a p′ p-a→p′ .evolves = p-a→p′
≈-refl p .fst .step a p′ p-a→p′ .bisim = ≈-refl p′
≈-refl p .snd .step a p′ p-a→p′ .result = p′
≈-refl p .snd .step a p′ p-a→p′ .evolves = p-a→p′
≈-refl p .snd .step a p′ p-a→p′ .bisim = ≈-refl p′

≈-sym : (p q : P N) → p ≈ q → q ≈ p
≈-sym p q (pq , qp) = qp , pq

≈-trans′ : (p q r : P N) → p ≈ q → q ≈ r → p ≲ r
≈-trans : (p q r : P N) → p ≈ q → q ≈ r → p ≈ r

≈-trans p q r pq qr = ≈-trans′ p q r pq qr , ≈-trans′ r q p (≈-sym _ _ qr) (≈-sym _ _ pq)

≈-trans′ p q r pq qr .step a p′ p-a→p′ =
  let p′q = pq .fst .step a p′ p-a→p′
      q′r = qr .fst .step a (p′q .result) (p′q .evolves)
  in λ where .result → q′r .result
             .evolves → q′r .evolves
             .bisim → ≈-trans p′ _ _ (p′q .bisim) (q′r .bisim)

∥-comm′ : (p q : P N) → p ∥ q ≲ q ∥ p
∥-comm : (p q : P N) → p ∥ q ≈ q ∥ p

∥-comm′ p q .step a p′ (parₗ p-a→p′) .result = _
∥-comm′ p q .step a p′ (parₗ p-a→p′) .evolves = parᵣ p-a→p′
∥-comm′ p q .step a p′ (parₗ p-a→p′) .bisim = ≈-refl _
∥-comm′ p q .step a p′ (parᵣ p-a→p′) .result = _
∥-comm′ p q .step a p′ (parᵣ p-a→p′) .evolves = parₗ p-a→p′
∥-comm′ p q .step a p′ (parᵣ p-a→p′) .bisim = ≈-refl _

∥-comm p q = ∥-comm′ p q , ∥-comm′ q p