PolyWiringDiagrams

tutorial.agda

{-# OPTIONS --guardedness #-}
module tutorial where

open import Poly
open import Data.Product
open import Dynamics
open Systems

postulate A B C D S T : Set
    
box₁ : Poly
box₁ = B ▹ λ _ → A × C

box₂ : Poly
box₂ = (C × D) ▹ λ _ → B

box₃ : Poly
box₃ = D ▹ (λ _ → A)

composeBoxes : Poly[ box₁ ⊗ₚ box₂ , box₃ ]
composeBoxes = 
        (λ{ (b , c , d) → d})              -- map outputs to outputs
         ⇒ₚ 
         λ{(b , c , _) a → (a , c) , b}    -- map inputs to inputs



postulate impl₁ : Sys S box₁
postulate impl₂ : Sys T box₂

impl₃ : Sys (S × T) (box₃)
impl₃ = (impl₁ ⊗ₛ impl₂) ∘ₛ composeBoxes