{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

------------------------------------------------------------------------
-- the composition of two simulations evaluates to the composition of
-- the two corresponding evalutions
-- up to bisimilarity
-------------------------------------------------------------------------

open import prelude
open import Simulations
open import Simulations.composition
open import equality
open import Bisimulation renaming (Φ to bis-Φ)


module Simulations.eval-composition
       {I₁ I₂ I₃ : Set}
       {w₁ : IS I₁}
       {w₂ : IS I₂}
       {w₃ : IS I₃}
       (Sim₁ : w₁ ⊸ w₂)
       (Sim₂ : w₂ ⊸ w₃)
       where

  open IS w₁ renaming (Command to A₁ ; Response to D₁ ; next to n₁)
  open IS w₂ renaming (Command to A₂ ; Response to D₂ ; next to n₂)
  open IS w₃ renaming (Command to A₃ ; Response to D₃ ; next to n₃)

  open Simulation Sim₁ renaming (R to R₁ ; coalg to coalg₁)
  open Simulation Sim₂ renaming (R to R₂ ; coalg to coalg₂)

  --  associativity
  module _ {i₁ : I₁} {i₂ : I₂} {i₃ : I₃}
           (r₁ : R₁ i₁ i₂) (r₂ : R₂ i₂ i₃)
           (T : ν (w₁ ⊥) i₁) where

    private T₁ : ν (w₃ ⊥) i₃
    T₁ = linear-evaluation w₁ w₃ (composition Sim₂ Sim₁) (i₂ , (r₂ , r₁)) T
    private T₂ : ν (w₃ ⊥) i₃
    T₂ = linear-evaluation w₂ w₃ Sim₂ r₂ (linear-evaluation w₁ w₂ Sim₁ r₁ T)

    private X : Pow (states (w₃ ⊥))
    X (i₃ , T₁ , T₂) =
            Σ I₁              λ i₁ →
            Σ I₂              λ i₂ →
            Σ (ν (w₁ ⊥) i₁)   λ T  →
            Σ (R₁ i₁ i₂)      λ r₁  →
            Σ (R₂ i₂ i₃)      λ r₂  →
            T₁ ≡ linear-evaluation w₁ w₃ (composition Sim₂ Sim₁) (i₂ , (r₂ , r₁)) T ×
            T₂ ≡ linear-evaluation w₂ w₃ Sim₂ r₂ (linear-evaluation w₁ w₂ Sim₁ r₁ T)

    private init : X (i₃ , T₁ , T₂)
    init = (i₁ , i₂ , T , r₁ , r₂ , refl , refl)

    private coalg : X ⊂ bis-Φ (w₃ ⊥) X
    coalg {(i₃ , (T₁ , T₂))} (i₁ , (i₂ , (T , (r₁ , (r₂ , (refl , refl)))))) =
      let f₁ : (a : A₃ i₃) → D₃ i₃ a
          f₁ = fst (νElim T₁) in
      let f₂ = (a : A₃ i₃) → D₃ i₃ a
          f₂ = fst (νElim T₂) in
      let p : f₁ ≡ f₂
          p = refl
      in
      p , λ (a₃ : A₃ i₃) →
            let a₂ : A₂ i₂
                a₂ = fst (coalg₂ r₂ a₃) in
            let a₁ : A₁ i₁
                a₁ = fst (coalg₁ r₁ a₂) in
            let d₁ : D₁ i₁ a₁
                d₁ = fst (νElim T) a₁ in
            let d₂ : D₂ i₂ a₂
                d₂ = fst (snd (coalg₁ r₁ a₂) d₁) in
            let d₃ : D₃ i₃ a₃
                d₃ = f₁ a₃ in
            (n₁ a₁ d₁ ,
            (n₂ a₂ d₂ ,
            (snd (νElim T) a₁ ,
            (snd (snd (coalg₁ r₁ a₂) d₁) ,
            (snd (snd (coalg₂ r₂ a₃) d₂) ,
            refl , refl)))))

    lemma : linear-evaluation w₁ w₃ (composition Sim₂ Sim₁) (i₂ , (r₂ , r₁)) T
                       ≈
                       linear-evaluation w₂ w₃ Sim₂ r₂ (linear-evaluation w₁ w₂ Sim₁ r₁ T)
    lemma = record { carrier = X ; coalg = coalg ; init = init }