Touches

parent e38e9f3f
......@@ -15,7 +15,7 @@ open Finite ⦃ … ⦄
%<*forall-Finite>
\AgdaTarget{∀-Finite}
\begin{code}
∀-Finite : ∀ {ℓ} {α : Set ℓ} {P : α → Set} ⦃ fin : Finite α ⦄ {ps : vec↑ (tabulate (P ∘ from))} → (∀ x → P x)
∀-Finite : ∀ {ℓ} {α : Set ℓ} {P : α → Set} ⦃ fin : Finite α ⦄ {ps : vec↑ (tabulate (P ∘ from))} → (∀ (x : α) → P x)
∀-Finite {P = P} {ps} x = subst P (left-inverse-of x) $ ∀-Fin {P = P ∘ from} {ps} (to x)
\end{code}
%</forall-Finite>
......@@ -17,6 +17,7 @@ open import PiWare.Plugs using (id⤨; nil⤨)
open import PiWare.Patterns.Id using (adaptEqI)
open import PiWare.Semantics.Simulation A using (W; W⟶W; ⟦_⟧[_])
open import PiWare.Semantics.Simulation.Compliance A using (_⫉[_]_)
-- Should semantics be here?
\end{code}
......@@ -79,18 +80,20 @@ row {suc k} {a} {b} {c} f = ⊥ where postulate ⊥ : _
%<*foldr-Circ>
\begin{code}
foldrℂ : ∀ n {k G} → ℂ G {σ} (k + k) k → ℂ G {σ} zero k → ℂ G {σ} (n * k) k
foldrℂ zero {_} _ e = e
foldrℂ (suc n) {k} c e = id⤨ {k} ∥ (foldrℂ n) c e ⟫ c
linear-reductor : ∀ n {k G} → ℂ G {σ} (k + k) k → ℂ G {σ} zero k → ℂ G {σ} (n * k) k
linear-reductor zero {_} _ e = e
linear-reductor (suc n) {k} c e = id⤨ {k} ∥ (linear-reductor n) c e ⟫ c
\end{code}
%</foldr-Circ>
\begin{code}
postulate lemma : ∀ {n ℓ} {α : Set ℓ} (v : Vec α n) → tabulate (λ i → lookup (lookup i (tabulate id)) v) ≡ v
postulate
linear-reductor-spec : ∀ {n k G} {g : TyGate G W⟶W} (c : ℂ G {σ} (k + k) k) (e : ℂ G {σ} zero k)
→ 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 foldrℂ-spec : ∀ {n k G} {g : TyGate G W⟶W} (c : ℂ G {σ} (k + k) k) (e : ℂ G {σ} zero k)
→ foldrℂ n {k} c e ⫉[ g ] foldr (const (W k)) (λ x y → ⟦ c ⟧[ g ] (x ++ y)) (⟦ e ⟧[ g ] [])
∘ proj₁ ∘ group n k
postulate lemma : ∀ {n ℓ} {α : Set ℓ} (v : Vec α n) → tabulate (λ i → lookup (lookup i (tabulate id)) v) ≡ v
\end{code}
......@@ -2,25 +2,25 @@
-- An n-sized register based on the unit register
module PiWare.Samples.RegN' where
open import Data.Fin using (Fin; zero; suc; raise)
open import Data.Fin.Properties
open import Data.Nat using (ℕ; zero; suc)
open import Data.Nat.Properties.Simple
open import Data.Vec using (Vec; _∷_; tabulate)
open import Data.Fin using (#_; raise)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Vec using (_∷_; tabulate)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Circuit using (ℂ; C; Plug; _⟫_; _∥_)
open import PiWare.Plugs.Core using (nil⤪)
open import PiWare.Plugs using (nil⤨)
open import PiWare.Samples.BoolTrioSeq using (reg)
regn-plug : {n : ℕ} → C B₃ (suc (suc n)) (suc (suc (suc n)))
regn-plug = Plug (suc zero ∷ zero ∷ zero ∷ tabulate (raise (suc (suc zero))))
regn-plug : {n : ℕ} → C B₃ (2 + n) (3 + n)
regn-plug = Plug ((# 1) ∷ (# 0) ∷ (# 0) ∷ tabulate (raise 2)) -- load (bit #0) duplicated
-- An n-sized register
-- load ∷ inputs → out
-- (note that this is different from the wiring scheme of reg, input × load → out!)
regn : (n : ℕ) → ℂ B₃ (suc n) n
regn zero = Plug nil⤪
regn (suc n) = regn-plug {n} ⟫ (reg ∥ regn n)
-- load ∷ data → out
-- (note that this is different from the wiring scheme of reg, input load → out!)
regn : ∀ n → ℂ B₃ (1 + n) n
regn zero = nil⤨
regn (suc n) = regn-plug {n} ⟫ (reg ∥ regn n)
\end{code}
\begin{code}
-- An n-sized register based on the unit register
module PiWare.Samples.RegN where
open import Function using (_⟨_⟩_; _$_)
open import Data.Fin using (Fin; zero; suc; raise)
open import Data.Fin.Properties
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _+⋎_)
open import Data.Nat.Properties.Simple
open import Data.Product using (proj₂)
open import Data.Nat.Properties using () renaming (isCommutativeSemiring to ℕ-isCommSemiring)
open import Algebra.Structures using (IsCommutativeSemiring; IsCommutativeMonoid)
open IsCommutativeSemiring ℕ-isCommSemiring using (*-isCommutativeMonoid)
open IsCommutativeMonoid *-isCommutativeMonoid using () renaming (identity to *-id; comm to *-comm)
open import Data.Nat.Properties.Simple using (+-right-identity; +-comm)
open import Data.Vec using (Vec; replicate; _⋎_; tabulate)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
import Relation.Binary.PropositionalEquality as P
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
......@@ -19,31 +22,38 @@ open import PiWare.Plugs.Core using (eq⤪)
open import PiWare.Samples.BoolTrioSeq using (reg)
regn-distribute : (n : ℕ) → C B₃ (suc n) (n +⋎ n)
regn-distribute n = Plug (tabulate {n = n} (raise 1) ⋎ replicate {n = n} zero)
+⋎≡+ : ∀ n m → n +⋎ m ≡ n + m
+⋎≡+ zero m = refl
+⋎≡+ (suc n) m = cong suc (+⋎≡+ m n ⟨ trans ⟩ +-comm m n)
+⋎≡+ : (n m : ℕ) → n +⋎ m ≡ n + m
+⋎≡+ zero m = refl
+⋎≡+ (suc n) m = P.cong suc (trans (+⋎≡+ m n) (+-comm m n))
+⋎-*2 : (n : ℕ) → n +⋎ n ≡ n * 2
+⋎-*2 n = trans (+⋎≡+ n n) (trans (P.cong (n +_) (sym (+-right-identity n))) (*-comm 2 n))
regn-distribute : ∀ n → C B₃ (suc n) (n +⋎ n)
regn-distribute n = Plug $ tabulate (raise 1) ⋎ replicate {n = n} zero
regn-equalise : (n : ℕ) → C B₃ (n +⋎ n) (n * 2)
regn-equalise n = Plug (eq⤪ (+⋎-*2 n))
regn-regs : (n : ℕ) → ℂ B₃ (n * 2) (n * 1)
regn-regs n = parsN {k = n} reg
+⋎-*2 : ∀ n → n +⋎ n ≡ n * 2
+⋎-*2 n = begin
n +⋎ n ≡⟨ +⋎≡+ n n ⟩
n + n ≡⟨ cong (n +_) $ sym (+-right-identity n) ⟩
n + (n + 0) ≡⟨⟩
2 * n ≡⟨ *-comm 2 n ⟩
n * 2 ∎
regn-equalise : ∀ n → C B₃ (n +⋎ n) (n * 2)
regn-equalise n = Plug $ eq⤪ (+⋎-*2 n)
*-right-unit : (n : ℕ) → n * 1 ≡ n
*-right-unit n = trans (*-comm n 1) (+-right-identity n)
regn-join : ∀ n → C B₃ (n * 1) n
regn-join n = Plug $ eq⤪ ((proj₂ *-id) n)
regn-regs : ∀ n → ℂ B₃ (n * 2) (n * 1)
regn-regs n = parsN {k = n} reg
regn-join : (n : ℕ) → C B₃ (n * 1) n
regn-join n = Plug (eq⤪ (*-right-unit n))
-- An n-sized register
-- load ∷ inputs → out
-- (note that this is different from the wiring scheme of reg, input × load → out!)
regn : (n : ℕ) → ℂ B₃ (suc n) n
regn : ∀ n → ℂ B₃ (suc n) n
regn n = regn-distribute n ⟫ (regn-equalise n ⟫ regn-regs n ⟫ regn-join n)
\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