Add WithGates submodule to SimulationState

parent 566cdda0
......@@ -20,10 +20,13 @@ open Setoidₛ using () renaming (refl to reflₛ; sym to symₛ; trans to trans
open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; cong) renaming ([_] to [_]ᵣ)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Semantics.Simulation Atomic-Bool using (delay′; module WithGates)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_])
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
open WithGates b₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_]; ℂₛ)
renaming (module WithGates to WithGatesₛ)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open WithGatesₛ spec-B₃ using (⟦_⟧ₛ; ⟦_⟧ω')
open import PiWare.Samples.BoolTrioSeq using (toggle; shift; reg; regCore)
open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
......@@ -87,7 +90,7 @@ singleton∘lookup0 {x = _ ∷ []} = refl
%<*lemmaShiftₚ>
\AgdaTarget{lemmaShiftₚ}
\begin{code}
lemmaShiftₚ : ∀ {c ins} → mealy ⟦ shift ⟧ₛ[ b₃ ] (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ₚ ⇓ c ∷ ♯ ins
lemmaShiftₚ : ∀ {c ins} → mealy ⟦ shift ⟧ₛ (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ₚ ⇓ c ∷ ♯ ins
lemmaShiftₚ {c} {x ∷ _} = singleton∘lookup1 {x = x} ∷ₚ ♯ transₚ lemmaShiftₚ (singleton∘lookup0 {x = x} ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShiftₚ>
......@@ -96,7 +99,7 @@ lemmaShiftₚ {c} {x ∷ _} = singleton∘lookup1 {x = x} ∷ₚ ♯ transₚ le
%<*lemmaShift>
\AgdaTarget{lemmaShift}
\begin{code}
lemmaShift : ∀ {c ins} → mealy ⟦ shift ⟧ₛ[ b₃ ] (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ ⇓ c ∷ ♯ ins
lemmaShift : ∀ {c ins} → mealy ⟦ shift ⟧ₛ (DelayLoopₛ (⇓ c) Plugₛ) ins ≈ ⇓ c ∷ ♯ ins
lemmaShift = ≈ₚ-to-≈ $ lemmaShiftₚ ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
%</lemmaShift>
......@@ -105,7 +108,7 @@ lemmaShift = ≈ₚ-to-≈ $ lemmaShiftₚ ⟨ transₚ ⟩ (refl ∷ₚ ♯ ref
%<*proofShift′>
\AgdaTarget{proofShift′}
\begin{code}
proofShift′ : ∀ {ins} → ⟦ shift ⟧ω'[ b₃ ] ins ≈ ⇓ 𝔽 ∷ ♯ ins
proofShift′ : ∀ {ins} → ⟦ shift ⟧ω' ins ≈ ⇓ 𝔽 ∷ ♯ ins
proofShift′ {x ∷ xs} = singleton∘lookup1 {x = x} ∷ ♯ transₛ lemmaShift (singleton∘lookup0 ∷ ♯ reflₛ)
\end{code}
%</proofShift′>
......@@ -168,11 +171,23 @@ proofToggle = toggle-runᶜ′-𝕋 (toggleᶜ-start {[]})
%</proofToggle>
\begin{code}
stateToggle𝔽 stateToggle𝕋 : ℂₛ B₃ toggle
\end{code}
%<*stateToggle𝔽-𝕋>
\AgdaTarget{stateToggle𝔽, stateToggle𝕋}
\begin{code}
stateToggle𝔽 = Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝔽) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)
stateToggle𝕋 = Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝕋) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)
\end{code}
%</stateToggle𝔽-stateToggle𝕋>
%<*proofToggle𝔽-𝕋-types>
\AgdaTarget{proofToggle𝔽′, proofToggle𝕋′}
\begin{code}
proofToggle𝔽′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ[ b₃ ] (Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝔽) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)) ins ≈ₚ map ⇓ (iterate not 𝕋)
proofToggle𝕋′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ[ b₃ ] (Gateₛ ⟫ₛ DelayLoopₛ (⇓ 𝕋) ((Gateₛ ⟫ₛ Gateₛ) ⟫ₛ Plugₛ)) ins ≈ₚ map ⇓ (iterate not 𝔽)
proofToggle𝔽′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ stateToggle𝔽 ins ≈ₚ map ⇓ (iterate not 𝕋)
proofToggle𝕋′ : ∀ {ins} → mealy ⟦ toggle ⟧ₛ stateToggle𝕋 ins ≈ₚ map ⇓ (iterate not 𝔽)
\end{code}
%</proofToggle𝔽-𝕋-types>
......@@ -186,7 +201,7 @@ proofToggle𝕋′ {_ ∷ _} = refl ∷ₚ ♯ transₚ proofToggle𝔽′ (refl
%<*proofToggle′>
\AgdaTarget{proofToggle′}
\begin{code}
proofToggle′ : ∀ {ins} → ⟦ toggle ⟧ω'[ b₃ ] ins ≈ map ⇓ (iterate not 𝕋)
proofToggle′ : ∀ {ins} → ⟦ toggle ⟧ω' ins ≈ map ⇓ (iterate not 𝕋)
proofToggle′ = ≈ₚ-to-≈ proofToggle𝔽′
\end{code}
%</proofToggle′>
......
......@@ -16,6 +16,7 @@ open import PiWare.Gates using (Gates)
open import PiWare.Circuit using (IsComb; σ; ω; ℂ; Gate; Plug; _⟫_; _∥_; DelayLoop)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Semantics.Simulation A using (W; W⟶W; plugσ)
\end{code}
......@@ -91,7 +92,29 @@ mealy f s (x ∷ xs) = proj₂ (f s x) ∷ ♯ mealy f (proj₁ (f s x)) (♭ xs
%<*⟦_⟧ω'[_]>
\AgdaTarget{⟦_⟧ω'[_]}
\begin{code}
⟦_⟧ω'[_] : ∀ {i o G} → ℂ G {ω} i o → TyGate G W⟶W → (Stream (W i) → Stream (W o))
⟦_⟧ω'[_] : ∀ {i o s G} → ℂ G {s} i o → TyGate G W⟶W → (Stream (W i) → Stream (W o))
⟦ c ⟧ω'[ g ] = mealy ⟦ c ⟧ₛ[ g ] (defaultₛ c)
\end{code}
%</⟦_⟧ω'[_]>
\begin{code}
module WithGates {G} (g : TyGate G W⟶W) where
\end{code}
%<*⟦_⟧ₛ>
\AgdaTarget{⟦\_⟧ₛ}
\begin{code}
⟦_⟧ₛ : ∀ {i o s} (c : ℂ G {s} i o) → (ℂₛ G c → W i → (ℂₛ G c × W o))
⟦_⟧ₛ = ⟦_⟧ₛ[ g ]
\end{code}
%</⟦_⟧ₛ>
%<*⟦_⟧ω'>
\AgdaTarget{⟦\_⟧ω'}
\begin{code}
⟦_⟧ω' : ∀ {i o s} (c : ℂ G {s} i o) → (Stream (W i) → Stream (W o))
⟦_⟧ω' = ⟦_⟧ω'[ g ]
\end{code}
%</⟦_⟧ω'>
......@@ -28,7 +28,7 @@ mealy-cong {xs = x ∷ xs} {.x ∷ ys} (refl ∷ xs≈ys) = refl ∷ ♯ (mealy-
%<*⟦⟧ω'-cong>
\AgdaTarget{⟦⟧ω'-cong}
\begin{code}
⟦⟧ω'-cong : ∀ {i o G} {g : TyGate G W⟶W} {c : ℂ G i o} {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'-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>
......@@ -45,7 +45,7 @@ lemma∥ = ≈ₚ-to-≈ lemma∥ₚ
%<*proof∥>
\AgdaTarget{proof∥}
\begin{code}
proof∥ : ∀ {i₁ i₂ o₁ o₂ G} {g : TyGate G W⟶W} {c : ℂ G i₁ o₁} {d : ℂ G i₂ o₂} {ins₁ ins₂}
proof∥ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {ins₁ ins₂}
→ ⟦ c ∥ d ⟧ω'[ g ] (zipWith _++_ ins₁ ins₂) ≈ zipWith _++_ (⟦ c ⟧ω'[ g ] ins₁) (⟦ d ⟧ω'[ g ] ins₂)
proof∥ = lemma∥
\end{code}
......
......@@ -27,7 +27,7 @@ lemma⟫ {ins = x ∷ xs} = refl ∷ (♯ lemma⟫)
%<*proof⟫>
\AgdaTarget{proof⟫}
\begin{code}
proof⟫ : ∀ {i m o G} {g : TyGate G W⟶W} {c : ℂ G i m} {d : ℂ G m o} {ins} → ⟦ c ⟫ d ⟧ω'[ g ] ins ≈ ⟦ d ⟧ω'[ g ] (⟦ c ⟧ω'[ g ] ins)
proof⟫ : ∀ {i m o s G} {g : TyGate G W⟶W} {c : ℂ G {s} i m} {d : ℂ G {s} m o} {ins} → ⟦ c ⟫ d ⟧ω'[ g ] ins ≈ ⟦ d ⟧ω'[ g ] (⟦ c ⟧ω'[ g ] ins)
proof⟫ = lemma⟫
\end{code}
%</proof⟫>
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