Fix compilation issues from module rearrangement

parent 2d28f4ae
......@@ -9,7 +9,7 @@ open import Data.List.NonEmpty using (List⁺; _∷_) renaming (map to map⁺; l
open import Data.List.NonEmpty.Extra using (zipWith⁺; zip⁺; unzip⁺)
open import Data.Product using (uncurry′; _,_)
open import Data.Vec.Extra.Properties using (,-injective; suc-injective)
open import Data.Vec.Properties.Extra using (,-injective; suc-injective)
\end{code}
......
......@@ -6,7 +6,7 @@ open import Data.Product using (uncurry′; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
open import Data.List.Extra using (unzip)
open import Data.Vec.Extra.Properties using (,-injective; suc-injective)
open import Data.Vec.Properties.Extra using (,-injective; suc-injective)
\end{code}
......
......@@ -11,8 +11,7 @@ open import Function using (_∘′_; id)
open import Algebra.FunctionProperties using (Involutive)
open import Data.List using (List; _∷ʳ_; _++_; []; _∷_; map; reverse; [_]) renaming (monoid to []-monoid)
open import Data.List.NonEmpty using (List⁺; toList; _∷_; _∷⁺_; _⁺∷ʳ_; _∷ʳ′_; _⁺++⁺_; snocView) renaming (head to head⁺; tail to tail⁺; map to map⁺; _∷ʳ_ to _∷⁺ʳ_)
open import Data.List.NonEmpty.Extra using (tails⁺)
open import Data.List.NonEmpty.Extended using (inits⁺′; inits⁺; reverse⁺′)
open import Data.List.NonEmpty.Extra using (inits⁺′; inits⁺; reverse⁺′; tails⁺)
open import Data.List.Properties using (map-id; map-cong; map-compose; map-++-commute; reverse-map-commute; unfold-reverse; reverse-++-commute; reverse-involutive)
open import Data.Nat using (zero; suc)
......
......@@ -14,7 +14,7 @@ open import Data.Vec using (Vec; _∷_; tabulate; lookup; allFin)
open import Data.Vec.Equality using () renaming (module PropositionalEquality to VPE)
open VPE using (from-≡) renaming (_≈_ to _≈ᵥ_)
open import Data.Vec.Properties using (lookup-allFin; tabulate∘lookup)
open import Data.Vec.Extra.Properties using (tabulate-cong)
open import Data.Vec.Properties.Extra using (tabulate-cong)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; module ≡-Reasoning; cong)
open import Function.Bijection.Sets using (_RightInverseOf′_)
......
......@@ -18,8 +18,8 @@ open import Data.Nat using (zero; suc)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec using (Vec; []; _∷_; _++_; [_]; head; tabulate; lookup; splitAt; replicate)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Extra.Properties using (tabulate-cong)
open import Data.Vec.Properties using (lookup∘tabulate; tabulate∘lookup)
open import Data.Vec.Properties.Extra using (tabulate-cong)
open import Data.Serializable using (_⇕_; ⇕⊤; ⇕×)
open import Data.Serializable.Bool using (⇕Bool)
......@@ -103,7 +103,7 @@ lemmaRegNNeverLoad : ∀ {n} → zipWith _++_ (repeat [ false ]) (repeat (replic
lemmaRegNNeverLoad = refl ∷ (♯ lemmaRegNNeverLoad)
proofRegNNeverLoad : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat false) xs) ≈ repeat (replicate false)
proofRegNNeverLoad {zero} {xs} = runᶜ-const {x⁰⁺ = zipWith _∷_ (repeat false) xs} (replicate false)
proofRegNNeverLoad {zero} {xs} = runᶜ-const {xs = zipWith _∷_ (repeat false) xs} (replicate false)
proofRegNNeverLoad {suc n} {xs} = beginₛ
⟦ regn (suc n) ⟧ω (zipWith _∷_ (repeat false) xs)
≈⟨ reflₛ ⟩
......@@ -128,7 +128,7 @@ lemmaRegNAlwaysLoad {xs = x ∷ xs} with splitAt 1 x
lemmaRegNAlwaysLoad {xs = .(xh ++ xt) ∷ xs} | xh , xt , refl = refl ∷ (♯ lemmaRegNAlwaysLoad)
proofRegNAlwaysLoad : ∀ {n xs} → ⟦ regn n ⟧ω (zipWith _∷_ (repeat true) xs) ≈ xs
proofRegNAlwaysLoad {zero} {xs} = transₛ (runᶜ-const {x⁰⁺ = zipWith _∷_ (repeat true) xs} []) lemma-repeat-empty
proofRegNAlwaysLoad {zero} {xs} = transₛ (runᶜ-const {xs = zipWith _∷_ (repeat true) xs} []) lemma-repeat-empty
proofRegNAlwaysLoad {suc n} {xs} = beginₛ
⟦ regn (suc n) ⟧ω (zipWith _∷_ (repeat true) xs)
≈⟨ reflₛ ⟩
......
......@@ -19,7 +19,7 @@ open import Data.Product using (proj₁; _×_; proj₂; _,_)
open import Data.Vec using (Vec; _∷_; []; [_]; head; tail; _∷ʳ_; _++_; splitAt; tabulate; lookup) renaming (zipWith to zipWithᵥ)
open import Data.Vec.Properties using (tabulate∘lookup; lookup∘tabulate)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Extra.Properties using (tabulate-cong; ++-injective)
open import Data.Vec.Properties.Extra using (tabulate-cong; ++-injective)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Circuit using (Plug; _⟫_; _∥_)
......
......@@ -4,7 +4,11 @@ module PiWare.ProofSamples.RegN where
open import Function using (_$_; _∘′_; id)
open import Coinduction using (♯_)
open import Data.Bool.Base using (Bool) renaming (false to 𝔽; true to 𝕋)
open import Data.Nat using (_+_; suc; _+⋎_; zero; _*_)
open import Data.Nat.Base using (_+_; suc; _+⋎_; zero; _*_)
open import Data.Nat.Properties using () renaming (isCommutativeSemiring to ℕ-isCommSemiring)
open import Algebra.Structures using (module IsCommutativeSemiring; module IsCommutativeMonoid)
open IsCommutativeSemiring ℕ-isCommSemiring using (*-isCommutativeMonoid)
open IsCommutativeMonoid *-isCommutativeMonoid using () renaming (identity to *-id)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Vec using ([]; _∷_; [_]; _++_; head; Vec; _⋎_; replicate; splitAt)
open import Data.Vec.Extra using (splitAt′)
......@@ -26,7 +30,7 @@ open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates; W)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧)
open import PiWare.Samples.BoolTrioSeq using (reg)
open import PiWare.Samples.RegN using (+⋎-*2; *-right-unit; regn-regs; regn-equalise; regn-join; regn-distribute; regn)
open import PiWare.Samples.RegN using (+⋎-*2; regn-regs; regn-equalise; regn-join; regn-distribute; regn)
open import PiWare.ProofSamples.BoolTrioSeq using (proofRegNeverLoad; proofRegAlwaysLoad)
open import PiWare.ProofSamples.EmptySeq using (runᶜ-const)
open import PiWare.ProofSamples.EqPlug Atomic-Bool using (vecCoerce; unfold-vecCoerce; vecCoerce-rightInverse; eq⤨⊑ωid)
......@@ -44,10 +48,10 @@ p₂∘split1 = proj₂ ∘′ splitAt′ 1
vc* : ∀ {ℓ} {α : Set ℓ} n → Vec α n → Vec α (n * 1)
vc* n v = vecCoerce (sym (*-right-unit n)) v
vc* n = vecCoerce $ sym ((proj₂ *-id) n)
vc⋎ : ∀ {ℓ} {α : Set ℓ} n → Vec α (n +⋎ n) → Vec α (n * 2)
vc⋎ n v = vecCoerce (+⋎-*2 n) v
vc⋎ n = vecCoerce (+⋎-*2 n)
-- TODO: for any data abstraction
......@@ -95,7 +99,7 @@ map-⋎-replicate {n} {xs = x ∷ _} = ⋎-replicate {n} {xs = x} ∷ ♯ map-
vecCoerce-replicate : ∀ {n ℓ} {α : Set ℓ} {y : α} → (vc* (suc n)) (replicate y) ≡ y ∷ (vc* n) (replicate y)
vecCoerce-replicate {n} = unfold-vecCoerce {≡₁ = sym (*-right-unit (suc n))} {sym (*-right-unit n)}
vecCoerce-replicate {n} = unfold-vecCoerce {≡₁ = sym $ (proj₂ *-id) (suc n)} {sym $ (proj₂ *-id) n}
repeat-replicate : ∀ {n α} {y : α} → zipWith _++_ (repeat [ y ]) (map (vc* n) $ repeat (replicate y)) ≈ map (vc* (suc n)) (repeat (replicate y))
......@@ -132,7 +136,7 @@ map-id-Stream-Vec0 {xs = [] ∷ _} = refl ∷ ♯ map-id-Stream-Vec0
vecCoerce-p₁p₂-split1 : ∀ {n ℓ} {α : Set ℓ} {xs : Vec α (suc n)} → p₁∘split1 xs ++ (vc* n) (p₂∘split1 xs) ≡ (vc* (suc n)) xs
vecCoerce-p₁p₂-split1 {xs = xs} with splitAt 1 xs
vecCoerce-p₁p₂-split1 {n} | _ ∷ [] , _ , refl = sym (unfold-vecCoerce {≡₁ = sym (*-right-unit (suc n))} {sym (*-right-unit n)})
vecCoerce-p₁p₂-split1 {n} | _ ∷ [] , _ , refl = sym (unfold-vecCoerce {≡₁ = sym $ (proj₂ *-id) (suc n)} {sym $ (proj₂ *-id) n})
map-vecCoerce-p₁p₂-split1 : ∀ {n α} {xs : Stream (Vec α (suc n))} → zipWith _++_ (map p₁∘split1 xs) (map (vc* n) (map p₂∘split1 xs)) ≈ map (vc* (suc n)) xs
......@@ -181,11 +185,11 @@ reg-remove-eq-plugs {n} {v} {xs} {ys} p = beginₛ
⟦ regn-join n ⟧ω (⟦ regn-regs n ⟧ω (map (λ x → (vc⋎ n) (x ⋎ replicate v)) xs))
≈⟨ ⟦⟧ω[_]-cong {c = regn-join n} spec-B₃ p ⟩
⟦ regn-join n ⟧ω (map (vc* n) ys)
≈⟨ eq⤨⊑ωid {g = spec-B₃} {p = *-right-unit n} {x⁰⁺ = map (vc* n) ys} ⟩
map (vecCoerce (*-right-unit n)) (map (vc* n) ys)
≈⟨ eq⤨⊑ωid {g = spec-B₃} {p = (proj₂ *-id) n} {x⁰⁺ = map (vc* n) ys} ⟩
map (vecCoerce $ (proj₂ *-id) n) (map (vc* n) ys)
≈⟨ symₛ map-compose ⟩
map (vecCoerce (*-right-unit n) ∘′ vc* n) ys
≈⟨ map-cong-fun (vecCoerce-rightInverse {p = *-right-unit n}) ⟩
map (vecCoerce ((proj₂ *-id) n) ∘′ vc* n) ys
≈⟨ map-cong-fun (vecCoerce-rightInverse {p = (proj₂ *-id) n}) ⟩
map id ys
≈⟨ map-id ⟩
ys ∎ₛ
......
......@@ -13,7 +13,7 @@ open import Data.List.NonEmpty using (_∷_)
open import Data.Nat using (zero; suc; _+_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Data.Vec using (Vec; lookup; tabulate; replicate; []; _∷_; _∷ʳ_; _++_; _⋎_)
open import Data.Vec.Extra.Properties using (tabulate-cong)
open import Data.Vec.Properties.Extra using (tabulate-cong)
open import Data.Stream.Properties using (module Setoidₛ)
open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-≈; ≈-to-≈ₚ; reflₚ; transₚ)
......
......@@ -14,9 +14,9 @@ open CommutativeSemiring commutativeSemiring-∨-∧ using () renaming (+-identi
open import PiWare.Circuit using (ℂ; σ; C; Gate; _⟫_; _∥_)
open import PiWare.Plugs using (id⤨; id⤨₁; fork×⤨; swap⤨)
open import PiWare.Patterns using (foldrℂ)
open import PiWare.Gates.BoolTrio using (⊥ℂ'; ⊤ℂ'; ¬ℂ'; ∧ℂ'; ∨ℂ') renaming (BoolTrio to B₃)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Patterns Atomic-Bool using (linear-reductor)
open import PiWare.Semantics.Simulation Atomic-Bool using (W; W⟶W) renaming (module WithGates to SimulationWithGates)
open import PiWare.Semantics.Simulation.Compliance Atomic-Bool using () renaming (module WithGates to ComplianceWithGates)
open import PiWare.Semantics.Simulation.BoolTrio using (spec-∧ℂ) renaming (spec to spec-B₃)
......@@ -69,7 +69,7 @@ open ComplianceWithGates spec-B₃ using (_⫃_)
\AgdaTarget{andN}
\begin{code}
andN : ∀ n → ℂ B₃ {σ} (n * 1) 1
andN n = (foldrℂ Atomic-Bool n) ∧ℂ ⊤ℂ
andN n = (linear-reductor n) ∧ℂ ⊤ℂ
\end{code}
%</andN>
......
......@@ -6,18 +6,17 @@ module PiWare.Semantics.Simulation.Properties.SequentialParalleling (A : Atomic)
open import Function using (_∘′_; id)
open import Coinduction using (♯_; ♭)
open import Data.List.NonEmpty using (_∷_; length) renaming (map to map⁺)
open import Data.List.NonEmpty.Extra using (unzip⁺; splitAt⁺)
open import Data.List.NonEmpty.Extended using (zipWith⁺; zip⁺)
open import Data.List.NonEmpty.Extended.Properties using (zipWith⁺-map⁺-zip⁺; unzip⁺-zip⁺-inverse)
open import Data.Nat using (suc)
open import Data.List.NonEmpty.Extra using (unzip⁺; splitAt⁺; zipWith⁺; zip⁺)
open import Data.List.NonEmpty.Properties.Extra using (zipWith⁺-map⁺-zip⁺; unzip⁺-zip⁺-inverse)
open import Data.Nat.Base using (suc)
open import Data.Product using (_,_; uncurry′; map)
open import Data.Vec using (_++_)
open import Data.Vec.Extra using (splitAt′)
open import Data.Vec.Extra.Properties using (splitAt′-++-inverse)
open import Data.Vec.Properties.Extra using (splitAt′-++-inverse)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; module ≡-Reasoning)
open import Data.Stream using (_∷_; zipWith; _≈_)
open import Data.Stream.Properties using (module Setoidₛ)
open import Data.Stream.Extra.Properties using (map⁺-compose; map⁺-id; map⁺-cong)
open import Data.Stream.Properties.Extra using (map⁺-compose; map⁺-id; map⁺-cong)
open import Data.CausalStream using (runᶜ′)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
......
......@@ -8,7 +8,7 @@ open import Coinduction using (♯_; ♭)
open import Data.Stream using (Stream; _∷_; head; tail; map; take; drop; repeat; iterate; zipWith; lookup; _≈_; map-cong; head-cong; tail-cong)
open import Data.Stream.Equality.FromPointwiseEquality using (lookup≗⇒≈)
open import Data.Stream.Extra using (take⁺) renaming (inits⁺ to sinits⁺)
open import Data.Stream.Extra.Properties using
open import Data.Stream.Properties.Extra using
( lookup-drop; unfold'⁺-reverse⁺′; unfold-take⁺; lemma-drop-tail; lemma-lookup-drop; lemma-lookup-inits⁺-take⁺
; lemma-lookup-map; map⁺-id; map⁺-cong; reverse⁺′-involutive; map⁺-compose; lemma-tails⁺-inits⁺
; reverse⁺′-map⁺-commute; lemma-inits⁺-take⁺-inits⁺; map⁺-take⁺-mapₛ; take⁺-cong)
......@@ -16,9 +16,8 @@ open import Data.Stream.Properties using (≡-to-≈; module Setoidₛ; module E
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; cong; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Data.List.NonEmpty using (_∷_; _∷⁺_; _⁺∷ʳ_) renaming (map to map⁺)
open import Data.List.NonEmpty.Extra using (tails⁺)
open import Data.List.NonEmpty.Extended using (reverse⁺′; inits⁺)
open import Data.Nat using (zero; suc)
open import Data.List.NonEmpty.Extra using (tails⁺; reverse⁺′; inits⁺)
open import Data.Nat.Base using (zero; suc)
open import Data.CausalStream using (runᶜ′)
open import PiWare.Circuit using (ℂ; _⟫_)
......
......@@ -37,15 +37,14 @@ import Data.Stream.Equality.FromPointwiseEquality -- M
import Data.Stream.Equality.FromPrefixEquality -- M
import Data.Stream.Equality.NAD -- M
import Data.Stream.Equality.WithTrans -- M
import Data.Stream.Extra.Properties -- M
import Data.Stream.Extra -- M
import Data.Stream.Properties -- M
import Data.Stream.Properties.Extra -- M
import Data.Vec.Extra.Properties -- M
import Data.Vec.Extra
import Data.Vec.Forall
import Data.Vec.Padding
import Data.Vec.Properties.Extra
import Data.Vec.Properties.Extra -- M
import Function.Bijection.Sets
import Function.Extra
......
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