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

---------------------------------------------------------------------------------
-- simulations representing continuous functions from "ν w₁⊥ i₁" to "ν w₂⊥ i₂" --
---------------------------------------------------------------------------------

open import prelude
open import InteractionSystems.properties
open import RTC


module Simulations where

module _ {I₁ I₂ : Set}
         (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₂)

  ---------------------------------------------------------------
  -- The relation transformer corresponding to linear simulations
  Φ : Rel I₁ I₂ → Rel I₁ I₂
  Φ R i₁ i₂ = Π (A₂ i₂)          λ a₂  →
              Σ (A₁ i₁)          λ a₁  →
              Π (D₁ i₁ a₁)       λ d₁ →
                Σ (D₂ i₂ a₂)       λ d₂ →
                R (n₁ a₁ d₁) (n₂ a₂ d₂)

  ------------------------
  -- Linear simulations --
  record Simulation : Set₁
    where
    field
      R : Rel I₁ I₂
      coalg : {i₁ : I₁} → {i₂ : I₂} →
              R i₁ i₂ → Φ R i₁ i₂

  -- a simulation gives rise to a function ν w₁ → ν w₂. To define that, we
  -- need to define a coalgebra X ⊂ ⟦ w₂ ⟧ X from an element of ν w₁
  module Evaluation (Sim : Simulation)
    where

    open Simulation Sim

    X₂ : Pow I₂
    X₂ i₂ = (ν (w₁ ⊥)) ≬ ((R ~) i₂)

    -- X₂ is a coalgebra for (Π a₂:A₂ i₂) (Σ d₂:D₂ i₂ a₂) _
    private coalg₂-aux : {i₂ : I₂} → (X₂ i₂) → (a₂ : A₂ i₂) → Σ (D₂ i₂ a₂) (λ d₂ → X₂ (n₂ a₂ d₂))
    coalg₂-aux {i₂} ( i₁ , ( T , r ) ) a₂ =
               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
               d₂ , (n₁ a₁ d₁) , ((snd (νElim T) a₁) , (snd (snd (coalg r a₂) d₁)))

    -- we get that X₂ is a coalgebra for ⟦ w₂ ⊥⟧
    coalg₂ : X₂ ⊂ ⟦ w₂ ⊥ ⟧ X₂
    coalg₂ {i₂} x₂ = duality.lemma₂ w₂ X₂ (coalg₂-aux x₂)

  linear-evaluation : (Sim : Simulation) → {i₁ : I₁} → {i₂ : I₂}
              → (Simulation.R Sim i₁ i₂) → (ν (w₁ ⊥) i₁) → (ν (w₂ ⊥) i₂)
  linear-evaluation Sim {i₁} {i₂} r input =
    let open Simulation Sim in
    let open Evaluation Sim in
      νIntro X₂ coalg₂ ( i₁ , ( input , r ) )


_⊸_ : {I₁ I₂ : Set} (w₁ : IS I₁) (w₂ : IS I₂) → Set₁
_⊸_ w₁ w₂ = Simulation w₁ w₂