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

--------------------------------
-- composition of simulations --
--------------------------------

open import prelude
open import equality
open import Simulations
open import Bisimulation renaming (Φ to Φ-bisimulation)


module Simulations.composition
       {I₁ I₂ I₃ : Set}
       {w₁ : IS I₁}
       {w₂ : IS I₂}
       {w₃ : IS I₃}
       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₃)

module _ (Sim₂ : w₂ ⊸ w₃)
         (Sim₁ : w₁ ⊸ w₂) where

  private R₁ : Rel I₁ I₂
  R₁ = Simulation.R Sim₁
  private coalg₁ : {i₁ : I₁} {i₂ : I₂} → R₁ i₁ i₂ → Φ w₁ w₂ R₁ i₁ i₂
  coalg₁ {i₁} {i₂} r a₂ = Simulation.coalg Sim₁ r a₂

  private R₂ : Rel I₂ I₃
  R₂ = Simulation.R Sim₂
  private coalg₂ : {i₂ : I₂} {i₃ : I₃} → R₂ i₂ i₃ → Φ w₂ w₃ R₂ i₂ i₃
  coalg₂ {i₂} {i₃} s a₃ = Simulation.coalg Sim₂ s a₃


  private coalg-comp : {i₁ : I₁} {i₃ : I₃} → (R₂ • R₁) i₁ i₃ → Φ w₁ w₃ (R₂ • R₁) i₁ i₃
  coalg-comp {i₁} {i₃} ( i₂ , ( s , r ) ) a₃ =
    let a₂ = fst (coalg₂ s a₃) in
    let a₁ = fst (coalg₁ r a₂) in
    (a₁ , (λ d₁ →
    let d₂ = fst ((snd (coalg₁ r a₂)) d₁) in
    let d₃ = fst ((snd (coalg₂ s a₃)) d₂) in
    let r' = snd ((snd (coalg₁ r a₂)) d₁) in
    let s' = snd ((snd (coalg₂ s a₃)) d₂) in

    (d₃ , (n₂ a₂ d₂) , (s' , r'))))

  composition : w₁ ⊸ w₃
  composition = record
    { R = R₂ • R₁ ;
      coalg = coalg-comp }