Commit 8c38f88a by João Paulo Pizani Flor

### Had forgotten to remove unused modules

parent c0b12c16
 ... ... @@ -92,8 +92,3 @@ postulate → linear-reductor n c e ⫉[ g ] foldr (const (W k)) (λ x y → ⟦ c ⟧[ g ] (x ++ y)) (⟦ e ⟧[ g ] []) ∘ (proj₁ ∘ group n k) \end{code} \begin{code} postulate lemma : ∀ {n ℓ} {α : Set ℓ} (v : Vec α n) → tabulate (λ i → lookup (lookup i (tabulate id)) v) ≡ v \end{code}
 \begin{code} open import PiWare.Atomic using (Atomic) module PiWare.Semantics.SimulationState.Properties.SequentialParalleling (A : Atomic) where 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 (ℂ; _∥_) 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⟦⟧ₛ[–]-∥⇒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++> \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} % %<*⟦⟧ω'[–]-∥⇒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} %
 \begin{code} open import PiWare.Atomic using (Atomic) module PiWare.Semantics.SimulationState.Properties.SequentialSequencing (A : Atomic) where open import Coinduction using (♯_) open import Data.Stream 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⟦⟧ₛ[–]-⟫⇒∘> \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} % %<*⟦⟧ω'[–]-⟫⇒∘> \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} %
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!