{-# OPTIONS --safe #-}

module Problem17 (Act : Set) where

open import Data.Empty
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product hiding (map)
open import Data.Sum using (inj₁; inj₂)
open import Data.Unit
open import Function.Base using (id)
open import Relation.Binary.PropositionalEquality hiding ([_])

data Process : Set where
  ⟨_⟩   : Act → Process
  skip  : Process
  abort : Process
  -- not the normal semicolon, use \; and choose the correct option..
  _;_   : Process → Process → Process
  _+_   : Process → Process → Process
  _∥_   : Process → Process → Process

infixr 60 _;_
infixr 70 _+_
infixr 80 _∥_
variable P P′ Q Q′ : Process
variable a b c x : Act
variable xs : List Act

NoPar : Process → Set
NoPar (P ; Q) = NoPar P × NoPar Q
NoPar (P + Q) = NoPar P × NoPar Q
NoPar (P ∥ Q) = ⊥
NoPar ⟨ _ ⟩   = ⊤
NoPar skip    = ⊤
NoPar abort   = ⊤

interleave : List Act → List Act → List (List Act)
interleave [] ys = [ ys ]
interleave xs [] = [ xs ]
interleave (x ∷ xs) (y ∷ ys) = map (x ∷_) (interleave xs (y ∷ ys)) ++ map (y ∷_) (interleave (x ∷ xs) ys)

⟦_⟧ : Process → List (List Act)
⟦ ⟨ a ⟩ ⟧ = [ [ a ] ]
⟦ skip  ⟧ = [ [] ]
⟦ abort ⟧ = []
⟦ P + Q ⟧ = ⟦ P ⟧ ++ ⟦ Q ⟧
⟦ P ; Q ⟧ = concatMap (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧
⟦ P ∥ Q ⟧ = concatMap (λ p → concatMap (interleave p) ⟦ Q ⟧) ⟦ P ⟧

_≈_ : Process → Process → Set
P ≈ Q = ∀ xs → (xs ∈ ⟦ P ⟧ → xs ∈ ⟦ Q ⟧) × (xs ∈ ⟦ Q ⟧ → xs ∈ ⟦ P ⟧)

-- Helpers for dealing with sequential traces

;-trace : ∀ (P Q : Process) {xs ys} → xs ∈ ⟦ P ⟧ → ys ∈ ⟦ Q ⟧ → xs ++ ys ∈ ⟦ P ; Q ⟧
;-trace P Q {xs} xs∈⟦P⟧ ys∈⟦Q⟧ =
  ∈-concat⁺′ (∈-map⁺ (xs ++_) ys∈⟦Q⟧) (∈-map⁺ (λ p → map (p ++_) ⟦ Q ⟧) xs∈⟦P⟧)

;-trace⁻¹ :
  ∀ (P Q : Process) {xs} →
  xs ∈ ⟦ P ; Q ⟧ → ∃₂ λ ys zs → xs ≡ ys ++ zs × ys ∈ ⟦ P ⟧ × zs ∈ ⟦ Q ⟧
;-trace⁻¹ P Q {xs} xs∈⟦P;Q⟧ with ∈-concat⁻′ (map (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧) xs∈⟦P;Q⟧
... | xss , xs∈xss , xss∈⟦P⟧++⟦Q⟧ with ∈-map⁻ (λ p → map (p ++_) ⟦ Q ⟧) xss∈⟦P⟧++⟦Q⟧
... | ys , ys∈⟦P⟧ , refl with ∈-map⁻ (ys ++_) xs∈xss
... | zs , zs∈⟦Q⟧ , refl = ys , zs , refl , ys∈⟦P⟧ , zs∈⟦Q⟧

-- Idea
-- Each trace has a canonical process---the list of actions. We can map a list
-- of possible traces to a canonical process by taking the sum of all individual
-- traces.
--
-- We show the canonical process for list of traces is correct (contains all
-- traces) and unique (contains only the desired traces).

canonical₁ : List Act → Process
canonical₁ []       = skip
canonical₁ (a ∷ as) = ⟨ a ⟩ ; canonical₁ as

canonical : List (List Act) → Process
canonical []         = abort
canonical (as ∷ ass) = canonical₁ as + canonical ass

canonical₁-correct : ∀ as → as ∈ ⟦ canonical₁ as ⟧
canonical₁-correct []       = here refl
canonical₁-correct (a ∷ as) = ;-trace ⟨ a ⟩ (canonical₁ as) (here refl) (canonical₁-correct as)

canonical₁-unique : ∀ as {xs} → xs ∈ ⟦ canonical₁ as ⟧ → xs ≡ as
canonical₁-unique []       (here prf) = prf
canonical₁-unique (a ∷ as) prf with ;-trace⁻¹ ⟨ a ⟩ (canonical₁ as) prf
... | .([ a ]) , xs , refl , here refl , prf = cong (a ∷_) (canonical₁-unique as prf)

canonical₁-NoPar : ∀ as → NoPar (canonical₁ as)
canonical₁-NoPar []       = _
canonical₁-NoPar (a ∷ as) = _ , canonical₁-NoPar as

canonical-correct : ∀ ass {as} → as ∈ ass → as ∈ ⟦ canonical ass ⟧
canonical-correct (as ∷ ass) (here refl) = ∈-++⁺ˡ (canonical₁-correct as)
canonical-correct (as ∷ ass) (there prf) = ∈-++⁺ʳ ⟦ canonical₁ as ⟧ (canonical-correct ass prf)

canonical-unique : ∀ ass {as} → as ∈ ⟦ canonical ass ⟧ → as ∈ ass
canonical-unique (as ∷ ass) prf with ∈-++⁻ ⟦ canonical₁ as ⟧ prf
... | inj₁ prf with refl ← canonical₁-unique as prf = here refl
... | inj₂ prf = there (canonical-unique ass prf)

canonical-NoPar : ∀ ass → NoPar (canonical ass)
canonical-NoPar []         = _
canonical-NoPar (as ∷ ass) = canonical₁-NoPar as , canonical-NoPar ass

goal : ∀ (P : Process) → ∃[ P′ ] (P′ ≈ P) × NoPar P′
goal P =
    canonical ⟦ P ⟧
  , (λ as → canonical-unique ⟦ P ⟧ , canonical-correct ⟦ P ⟧)
  , canonical-NoPar ⟦ P ⟧