Integrate PiWare/Semantics/SimulationState/Properties/Sequential*

parent e163593f
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.SimulationState.Properties.Sequential (A : Atomic) where
open import Coinduction using (♯_; ♭)
open import Data.Product using (_,_; proj₁)
open import Data.Vec using (_++_)
open import Data.Vec.Properties.Extra using (,-injective; splitAt′-++-inverse)
open import Data.Stream using (zipWith; _≈_; _∷_)
open import Data.Stream.Properties using (≡-to-≈)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; ≈-to-≈ₚ; reflₚ; transₚ)
open import Data.Product using (_×_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong-app; cong₂)
open import PiWare.Circuit using (ℂ; _∥_; _⟫_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.SimulationState A using (⟦_⟧ₛ[_]; ⟦_⟧ω'[_]; mealy; _∥ₛ_; _⟫ₛ_)
\end{code}
%<*mealy-cong>
\AgdaTarget{mealy-cong}
\begin{code}
mealy-cong : ∀ {ℓ} {𝕊 : Set ℓ} {α β} {f : 𝕊 → α → (𝕊 × β)} {s xs ys} → xs ≈ ys → mealy f s xs ≈ mealy f s ys
mealy-cong {xs = x ∷ xs′} {.x ∷ ys′} (refl ∷ xs′≈ys′) = refl ∷ ♯ mealy-cong (♭ xs′≈ys′)
\end{code}
%</mealy-cong>
%<*⟦⟧ω'[–]-cong>
\AgdaTarget{⟦⟧ω'[–]-cong}
\begin{code}
⟦⟧ω'[–]-cong : ∀ {i o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i o) {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'[–]-cong _ _ = mealy-cong
\end{code}
%</⟦⟧ω'[–]-cong>
%<*mealy⟦⟧ₛ[–]-⟫⇒∘>
\AgdaTarget{mealy⟦⟧ₛ[–]-⟫⇒∘}
\begin{code}
mealy⟦⟧ₛ[–]-⟫⇒∘ : ∀ {i m o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i m) (d : ℂ G m o) {cₛ dₛ xs}
→ mealy ⟦ c ⟫ d ⟧ₛ[ g ] (cₛ ⟫ₛ dₛ) xs ≈ mealy ⟦ d ⟧ₛ[ g ] dₛ (mealy ⟦ c ⟧ₛ[ g ] cₛ xs)
mealy⟦⟧ₛ[–]-⟫⇒∘ g c d {xs = _ ∷ _} = refl ∷ ♯ mealy⟦⟧ₛ[–]-⟫⇒∘ g c d
\end{code}
%</mealy⟦⟧ₛ[–]-⟫⇒∘>
%<*⟦⟧ω'[–]-⟫⇒∘>
\AgdaTarget{⟦⟧ω'[–]-⟫⇒∘}
\begin{code}
⟦⟧ω'[–]-⟫⇒∘ : ∀ {i m o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i m) (d : ℂ G {s} m o) {xs}
→ ⟦ c ⟫ d ⟧ω'[ g ] xs ≈ ⟦ d ⟧ω'[ g ] (⟦ c ⟧ω'[ g ] xs)
⟦⟧ω'[–]-⟫⇒∘ g c d = mealy⟦⟧ₛ[–]-⟫⇒∘ g c d
\end{code}
%</⟦⟧ω'[–]-⟫⇒∘>
%<*mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ>
\AgdaTarget{mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ}
\begin{code}
mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ : ∀ {i₁ i₂ o₁ o₂ s G} (g : TyGate G W⟶W) (c : ℂ G {s} i₁ o₁) (d : ℂ G {s} i₂ o₂) {cₛ dₛ xs ys}
→ mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ xs ys) ≈ₚ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ xs) (mealy ⟦ d ⟧ₛ[ g ] dₛ ys)
mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ _ _ _ {xs = x ∷ _} {y ∷ _} with ,-injective (splitAt′-++-inverse {xs = x} {y})
mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ {m} g c d {cₛ} {dₛ} {_ ∷ xs} {_ ∷ ys} | x≡ , y≡ rewrite x≡ | y≡ = refl ∷ₚ ♯ transₚ (≈-to-≈ₚ (≡-to-≈ sub))
(mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ g c d)
where sub = cong-app (cong₂ (λ z₁ z₂ → mealy ⟦ c ∥ d ⟧ₛ[ g ] ((proj₁ (⟦ c ⟧ₛ[ g ] cₛ z₁)) ∥ₛ (proj₁ (⟦ d ⟧ₛ[ g ] dₛ z₂)))) x≡ y≡)
(zipWith _++_ (♭ xs) (♭ ys))
\end{code}
%</mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ>
%<*mealy⟦⟧ₛ[–]-∥⇒zipWith++>
\AgdaTarget{mealy⟦⟧ₛ[–]-∥⇒zipWith++}
\begin{code}
mealy⟦⟧ₛ[–]-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ s G} (g : TyGate G W⟶W) (c : ℂ G {s} i₁ o₁) (d : ℂ G {s} i₂ o₂) {cₛ dₛ xs ys}
→ mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ xs ys) ≈ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ xs) (mealy ⟦ d ⟧ₛ[ g ] dₛ ys)
mealy⟦⟧ₛ[–]-∥⇒zipWith++ g c d = ≈ₚ-to-≈ (mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ g c d)
\end{code}
%</mealy⟦⟧ₛ[–]-∥⇒zipWith++>
%<*⟦⟧ω'[–]-∥⇒zipWith++>
\AgdaTarget{⟦⟧ω'[–]-∥⇒zipWith++}
\begin{code}
⟦⟧ω'[–]-∥⇒zipWith++ : ∀ {i₁ i₂ o₁ o₂ s G} (g : TyGate G W⟶W) (c : ℂ G {s} i₁ o₁) (d : ℂ G {s} i₂ o₂) {xs ys}
→ ⟦ c ∥ d ⟧ω'[ g ] (zipWith _++_ xs ys) ≈ zipWith _++_ (⟦ c ⟧ω'[ g ] xs) (⟦ d ⟧ω'[ g ] ys)
⟦⟧ω'[–]-∥⇒zipWith++ g c d = mealy⟦⟧ₛ[–]-∥⇒zipWith++ g c d
\end{code}
%</⟦⟧ω'[–]-∥⇒zipWith++>
\begin{code}
open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.SimulationState.Properties.SequentialCongruence (A : Atomic) where
open import Coinduction using (♯_; ♭)
open import Data.Stream using (Stream; _≈_; _∷_)
open import Data.Product using (_×_)
open import Relation.Binary.PropositionalEquality using (refl)
open import PiWare.Circuit using (ℂ)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.SimulationState A using (mealy; ⟦_⟧ω'[_])
\end{code}
%<*mealy-cong>
\AgdaTarget{mealy-cong}
\begin{code}
mealy-cong : ∀ {ℓ} {𝕊 : Set ℓ} {α β} {f : 𝕊 → α → (𝕊 × β)} {s xs ys} → xs ≈ ys → mealy f s xs ≈ mealy f s ys
mealy-cong {xs = x ∷ xs′} {.x ∷ ys′} (refl ∷ xs′≈ys′) = refl ∷ ♯ mealy-cong (♭ xs′≈ys′)
\end{code}
%</mealy-cong>
%<*⟦⟧ω'[–]-cong>
\AgdaTarget{⟦⟧ω'[–]-cong}
\begin{code}
⟦⟧ω'[–]-cong : ∀ {i o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i o) {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'[–]-cong _ _ = mealy-cong
\end{code}
%</⟦⟧ω'[–]-cong>
......@@ -88,9 +88,7 @@ import PiWare.Semantics.Simulation.Semigroup.Base
import PiWare.Semantics.Simulation.Semigroup.Op2
import PiWare.Semantics.Simulation.Testing
import PiWare.Semantics.Simulation
import PiWare.Semantics.SimulationState.Properties.SequentialCongruence
import PiWare.Semantics.SimulationState.Properties.SequentialParalleling
import PiWare.Semantics.SimulationState.Properties.SequentialSequencing
import PiWare.Semantics.SimulationState.Properties.Sequential
import PiWare.Semantics.SimulationState
import PiWare.Typed.Circuit
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment