Fixed all compilation except for Typed

parent 21e9df0d
......@@ -3,36 +3,34 @@ open import PiWare.Atomic using (Atomic)
module PiWare.Semantics.SimulationState.Properties.SequentialParalleling (A : Atomic) where
open import Coinduction
open import Data.Stream
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷_; ≈ₚ-to-≈; ≈-to-≈ₚ) renaming (refl to sreflₚ; trans to stransₚ)
open import Data.Stream.Properties
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
import Relation.Binary.PropositionalEquality as P
open import Coinduction using (♯_; ♭)
open import Data.Stream using (zipWith; _≈_; _∷_)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; ≈-to-≈ₚ; reflₚ; transₚ)
open import Data.Stream.Properties using (≡-to-≈)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong-app; cong₂)
open import Data.Product using (_,_; proj₁)
open import Data.Vec using (_++_)
open import Data.Vec.Properties.Extra using (,-injective; splitAt′-++-inverse)
open import PiWare.Circuit using (IsComb; σ; ω; ℂ; Gate; Plug; _⟫_; _∥_; DelayLoop)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.SimulationState A using (⟦_⟧ᶜ'[_]; ⟦_⟧ω'[_]; mapAccum; _∥ₛ_)
open import PiWare.Semantics.SimulationState A using (⟦_⟧ₛ[_]; ⟦_⟧ω'[_]; mealy; _∥ₛ_)
import Data.Nat as N
import Data.Product as P
import Data.Vec as V
import Data.Vec.Extra as VE
import Data.Vec.Extra.Properties as VEP
import Data.Vec.Properties as VP
postulate lemma∥ₚ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {cₛ dₛ} {ins₁ ins₂} → mapAccum ⟦ c ∥ d ⟧ᶜ'[ g ] (cₛ ∥ₛ dₛ) (zipWith V._++_ ins₁ ins₂) ≈ₚ zipWith V._++_ (mapAccum ⟦ c ⟧ᶜ'[ g ] cₛ ins₁) (mapAccum ⟦ d ⟧ᶜ'[ g ] dₛ ins₂)
--lemma∥ₚ {ins₁ = i₁ ∷ is₁} {i₂ ∷ is₂} with VEP.,-injective (VEP.splitAt′-++-inverse {as = i₁} {bs = i₂})
--lemma∥ₚ {m} {g = g} {c} {d} {cₛ} {dₛ} {i₁ ∷ is₁} {i₂ ∷ is₂} | i₁≡ P., i₂≡ rewrite i₁≡ | i₂≡ = refl ∷ (♯ stransₚ (≈-to-≈ₚ (≡-to-≈ sub)) lemma∥ₚ)
-- where sub = P.cong-app (P.cong₂ (λ z₁ z₂ → mapAccum ⟦ c ∥ d ⟧ᶜ'[ g ] ((P.proj₁ (⟦ c ⟧ᶜ'[ g ] cₛ z₁)) ∥ₛ (P.proj₁ (⟦ d ⟧ᶜ'[ g ] dₛ z₂)))) i₁≡ i₂≡)
-- (zipWith V._++_ (♭ is₁) (♭ is₂))
lemma∥ₚ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {cₛ dₛ} {ins₁ ins₂} → mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ ins₁ ins₂) ≈ₚ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ ins₁) (mealy ⟦ d ⟧ₛ[ g ] dₛ ins₂)
lemma∥ₚ {ins₁ = i₁ ∷ is₁} {i₂ ∷ is₂} with ,-injective (splitAt′-++-inverse {xs = i₁} {ys = i₂})
lemma∥ₚ {m} {g = g} {c} {d} {cₛ} {dₛ} {i₁ ∷ is₁} {i₂ ∷ is₂} | i₁≡ , i₂≡ rewrite i₁≡ | i₂≡ = refl ∷ₚ ♯ transₚ (≈-to-≈ₚ (≡-to-≈ sub)) lemma∥ₚ
where sub = cong-app (cong₂ (λ z₁ z₂ → mealy ⟦ c ∥ d ⟧ₛ[ g ] ((proj₁ (⟦ c ⟧ₛ[ g ] cₛ z₁)) ∥ₛ (proj₁ (⟦ d ⟧ₛ[ g ] dₛ z₂)))) i₁≡ i₂≡)
(zipWith _++_ (♭ is₁) (♭ is₂))
lemma∥ : ∀ {i₁ i₂ o₁ o₂ s G} {g : TyGate G W⟶W} {c : ℂ G {s} i₁ o₁} {d : ℂ G {s} i₂ o₂} {cₛ dₛ ins₁ ins₂} →
mapAccum ⟦ c ∥ d ⟧ᶜ'[ g ] (cₛ ∥ₛ dₛ) (zipWith V._++_ ins₁ ins₂) ≈ zipWith V._++_ (mapAccum ⟦ c ⟧ᶜ'[ g ] cₛ ins₁) (mapAccum ⟦ d ⟧ᶜ'[ g ] dₛ ins₂)
mealy ⟦ c ∥ d ⟧ₛ[ g ] (cₛ ∥ₛ dₛ) (zipWith _++_ ins₁ ins₂) ≈ zipWith _++_ (mealy ⟦ c ⟧ₛ[ g ] cₛ ins₁) (mealy ⟦ d ⟧ₛ[ g ] dₛ ins₂)
lemma∥ = ≈ₚ-to-≈ lemma∥ₚ
proof∥ : ∀ {i₁ i₂ o₁ o₂ G} {g : TyGate G W⟶W} {c : ℂ G i₁ o₁} {d : ℂ G i₂ o₂} {ins₁ ins₂} →
⟦ c ∥ d ⟧ω'[ g ] (zipWith V._++_ ins₁ ins₂) ≈ zipWith V._++_ (⟦ c ⟧ω'[ g ] ins₁) (⟦ d ⟧ω'[ g ] ins₂)
⟦ c ∥ d ⟧ω'[ g ] (zipWith _++_ ins₁ ins₂) ≈ zipWith _++_ (⟦ c ⟧ω'[ g ] ins₁) (⟦ d ⟧ω'[ g ] ins₂)
proof∥ = lemma∥
\end{code}
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