ℂ[_]

parent 8c38f88a
......@@ -19,15 +19,15 @@ data IsComb : Set where σ ω : IsComb
%<*Circuit-predecl>
\begin{code}
data ℂ (G : Gates) : {s : IsComb} → Ix → Ix → Set
data ℂ[_] (G : Gates) : {s : IsComb} → Ix → Ix → Set
\end{code}
%</Circuit-predecl>
%<*Circuit-any>
\AgdaTarget{C}
\AgdaTarget{C[\_]}
\begin{code}
C : (G : Gates) → Ix → Ix → Set
C G i o = ∀ {s} → ℂ G {s} i o
C[_] : (G : Gates) → Ix → Ix → Set
C[ G ] i o = ∀ {s} → ℂ[ G ] {s} i o
\end{code}
%</Circuit-any>
......@@ -37,15 +37,36 @@ infixr 5 _∥_
\end{code}
%<*Circuit>
\AgdaTarget{ℂ, Gate, DelayLoop, Plug, \_⟫\_, \_∥\_}
\AgdaTarget{ℂ[\_], Gate, DelayLoop, Plug, \_⟫\_, \_∥\_}
\begin{code}
data ℂ G where
Gate : ∀ g# → C G (|in| G g#) (|out| G g#)
Plug : ∀ {i o} → i ⤪ o → C G i o
data ℂ[_] G where
Gate : ∀ g# → C[ G ] (|in| G g#) (|out| G g#)
Plug : ∀ {i o} → i ⤪ o → C[ G ] i o
_⟫_ : ∀ {i m o s} → ℂ G {s} i m → ℂ G {s} m o → ℂ G {s} i o
_∥_ : ∀ {i₁ o₁ i₂ o₂ s} → ℂ G {s} i₁ o₁ → ℂ G {s} i₂ o₂ → ℂ G {s} (i₁ + i₂) (o₁ + o₂)
_⟫_ : ∀ {i m o s} → ℂ[ G ] {s} i m → ℂ[ G ] {s} m o → ℂ[ G ] {s} i o
_∥_ : ∀ {i₁ o₁ i₂ o₂ s} → ℂ[ G ] {s} i₁ o₁ → ℂ[ G ] {s} i₂ o₂ → ℂ[ G ] {s} (i₁ + i₂) (o₁ + o₂)
DelayLoop : ∀ {i o l} → ℂ G {σ} (i + l) (o + l) → ℂ G {ω} i o
DelayLoop : ∀ {i o l} → ℂ[ G ] {σ} (i + l) (o + l) → ℂ[ G ] {ω} i o
\end{code}
%</Circuit>
\begin{code}
module WithGates (G : Gates) where
\end{code}
%<*Circuit-with-gates>
\begin{code}
ℂ : {s : IsComb} → Ix → Ix → Set
ℂ {s} = ℂ[ G ] {s}
\end{code}
%</Circuit-with-gates>
%<*Circuit-any-with-gates>
\AgdaTarget{C}
\begin{code}
C : Ix → Ix → Set
C = C[ G ]
\end{code}
%</Circuit-any-with-gates>
......@@ -5,7 +5,7 @@ open import Data.Nat.Base using (_+_)
open import PiWare.Interface using (Ix)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Circuit using (ℂ; σ; Gate; Plug; DelayLoop; _⟫_; _∥_)
open import PiWare.Circuit using (ℂ[_]; σ; Gate; Plug; DelayLoop; _⟫_; _∥_)
open import PiWare.Gates using (Gates)
open Gates using (|in|; |out|)
\end{code}
......@@ -21,7 +21,7 @@ TyGate G F = ∀ g# → F (|in| G g#) (|out| G g#)
\begin{code}
TyPlug Ty⟫ Ty∥ : (Ix → Ix → Set) → Set
TyPlug Ty⟫ Ty∥ : (Ix → Ix → Set) → Set
\end{code}
%<*combinator-types-parameterized>
\AgdaTarget{TyGate, TyPlug, Ty⟫, Ty∥}
......@@ -60,7 +60,7 @@ module _ {G : Gates} where
%<*Circuit-combinational-cata>
\AgdaTarget{cataℂσ}
\begin{code}
cataℂσ : ∀ {i o} → ℂ G {σ} i o → F i o
cataℂσ : ∀ {i o} → ℂ[ G ] {σ} i o → F i o
cataℂσ (Gate g) = GateA g
cataℂσ (Plug f) = PlugA f
cataℂσ (c₁ ⟫ c₂) = cataℂσ c₁ ⟫A cataℂσ c₂
......@@ -92,7 +92,7 @@ module _ {G : Gates} where
%<*Circuit-cata>
\AgdaTarget{cataℂ}
\begin{code}
cataℂ : ∀ {i o} → ℂ G i o → F i o
cataℂ : ∀ {i o} → ℂ[ G ] i o → F i o
cataℂ (Gate g) = GateA g
cataℂ (Plug f) = PlugA f
cataℂ (DelayLoop c) = DelayLoopA (cataℂσ Fσ aσ c)
......
......@@ -11,7 +11,7 @@ open import Data.Nat.Properties.Simple using (+-right-identity)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst₂; cong)
open import Data.IVec using (Vec₂; []₂; _∷₂_; replicate₂)
open import PiWare.Circuit using (ℂ; σ; _⟫_; _∥_)
open import PiWare.Circuit using (ℂ[_]; σ; _⟫_; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Plugs using (id⤨; nil⤨)
open import PiWare.Patterns.Id using (adaptEqI)
......@@ -24,7 +24,7 @@ open import PiWare.Semantics.Simulation.Compliance A using (_⫉[_]_)
%<*pars>
\AgdaTarget{pars}
\begin{code}
pars : ∀ {n s G} {is os : Vec ℕ n} (cs : Vec₂ (ℂ G {s}) is os) → ℂ G {s} (sum is) (sum os)
pars : ∀ {n s G} {is os : Vec ℕ n} (cs : Vec₂ (ℂ[ G ] {s}) is os) → ℂ[ G ] {s} (sum is) (sum os)
pars {is = []} {[]} []₂ = nil⤨
pars {is = _ ∷ _} {_ ∷ _} (c ∷₂ cs) = c ∥ pars cs
\end{code}
......@@ -43,8 +43,8 @@ pars {is = _ ∷ _} {_ ∷ _} (c ∷₂ cs) = c ∥ pars cs
%<*parsN>
\AgdaTarget{parsN}
\begin{code}
parsN : ∀ {k i o s G} → ℂ G {s} i o → ℂ G {s} (k * i) (k * o)
parsN {k} {i} {o} {_} {G} c = subst₂ (ℂ G) (*-sum-replicate k i) (*-sum-replicate k o) (pars (replicate₂ {n = k} c))
parsN : ∀ {k i o s G} → ℂ[ G ] {s} i o → ℂ[ G ] {s} (k * i) (k * o)
parsN {k} {i} {o} {_} {G} c = subst₂ ℂ[ G ] (*-sum-replicate k i) (*-sum-replicate k o) (pars (replicate₂ {n = k} c))
\end{code}
%</parsN>
......@@ -53,8 +53,8 @@ parsN {k} {i} {o} {_} {G} c = subst₂ (ℂ G) (*-sum-replicate k i) (*-sum-repl
%<*seqs>
\AgdaTarget{seqs}
\begin{code}
seqs : ∀ {n io s G} → Vec (ℂ G {s} io io) n → ℂ G {s} io io
seqs {_} {io} {s} {G} = foldr (const (ℂ G {s} io io)) _⟫_ id⤨
seqs : ∀ {n io s G} → Vec (ℂ[ G ] {s} io io) n → ℂ[ G ] {s} io io
seqs {_} {io} {s} {G} = foldr (const (ℂ[ G ] {s} io io)) _⟫_ id⤨
\end{code}
%</seqs>
......@@ -62,7 +62,7 @@ seqs {_} {io} {s} {G} = foldr (const (ℂ G {s} io io)) _⟫_ id⤨
%<*seqsN>
\AgdaTarget{seqsN}
\begin{code}
seqsN : ∀ k {s io G} → ℂ G {s} io io → ℂ G {s} io io
seqsN : ∀ k {s io G} → ℂ[ G ] {s} io io → ℂ[ G ] {s} io io
seqsN k = seqs ∘′ replicate {n = k}
\end{code}
%</seqsN>
......@@ -71,7 +71,7 @@ seqsN k = seqs ∘′ replicate {n = k}
%<*row>
\AgdaTarget{row}
\begin{code}
row : ∀ {k a b c s G} → ℂ G {s} (a + b) (c + a) → ℂ G {s} (a + (k * b)) ((k * c) + a)
row : ∀ {k a b c s G} → ℂ[ G ] {s} (a + b) (c + a) → ℂ[ G ] {s} (a + (k * b)) ((k * c) + a)
row {zero} {a} {b} {c} _ = adaptEqI (sym (+-right-identity a)) id⤨
row {suc k} {a} {b} {c} f = ⊥ where postulate ⊥ : _
\end{code}
......@@ -80,7 +80,7 @@ row {suc k} {a} {b} {c} f = ⊥ where postulate ⊥ : _
%<*foldr-Circ>
\begin{code}
linear-reductor : ∀ n {k G} → ℂ G {σ} (k + k) k → ℂ G {σ} zero k → ℂ G {σ} (n * k) k
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}
......@@ -88,7 +88,7 @@ linear-reductor (suc n) {k} c e = id⤨ {k} ∥ (linear-reductor n) c e ⟫ c
\begin{code}
postulate
linear-reductor-spec : ∀ {n k G} {g : TyGate G W⟶W} (c : ℂ G {σ} (k + k) k) (e : ℂ G {σ} zero k)
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}
......@@ -5,7 +5,7 @@ open import Function using (flip; _∘′_)
open import Data.Nat.Base using (_+_)
open import Relation.Binary.PropositionalEquality using (_≡_; subst)
open import PiWare.Circuit using (ℂ; _⟫_; _∥_)
open import PiWare.Circuit using (ℂ[_]; _⟫_; _∥_)
open import PiWare.Plugs using (eq⤨)
\end{code}
......@@ -13,8 +13,8 @@ open import PiWare.Plugs using (eq⤨)
%<*adaptEqI>
\AgdaTarget{adaptEqI}
\begin{code}
adaptEqI : ∀ {i i′ o s G} (≡ᵢ : i ≡ i′) → ℂ G {s} i o → ℂ G {s} i′ o
adaptEqI {o = o} {s} {G} = subst (flip (ℂ G {s}) o)
adaptEqI : ∀ {i i′ o s G} (≡ᵢ : i ≡ i′) → ℂ[ G ] {s} i o → ℂ[ G ] {s} i′ o
adaptEqI {o = o} {s} {G} = subst (flip (ℂ[ G ] {s}) o)
\end{code}
%</adaptEqI>
......@@ -22,8 +22,8 @@ adaptEqI {o = o} {s} {G} = subst (flip (ℂ G {s}) o)
%<*adaptEqO>
\AgdaTarget{adaptEqO}
\begin{code}
adaptEqO : ∀ {i o o′ s G} (≡ₒ : o ≡ o′) → ℂ G {s} i o → ℂ G {s} i o′
adaptEqO {i} {s = s} {G} = subst (ℂ G {s} i)
adaptEqO : ∀ {i o o′ s G} (≡ₒ : o ≡ o′) → ℂ[ G ] {s} i o → ℂ[ G ] {s} i o′
adaptEqO {i} {s = s} {G} = subst (ℂ[ G ] {s} i)
\end{code}
%</adaptEqO>
......@@ -31,7 +31,7 @@ adaptEqO {i} {s = s} {G} = subst (ℂ G {s} i)
%<*adaptEqIO>
\AgdaTarget{adaptEqIO}
\begin{code}
adaptEqIO : ∀ {i i′ o o′ s G} (≡ᵢ : i ≡ i′) (≡ₒ : o ≡ o′) → ℂ G {s} i o → ℂ G {s} i′ o′
adaptEqIO : ∀ {i i′ o o′ s G} (≡ᵢ : i ≡ i′) (≡ₒ : o ≡ o′) → ℂ[ G ] {s} i o → ℂ[ G ] {s} i′ o′
adaptEqIO ≡ᵢ ≡ₒ = adaptEqO ≡ₒ ∘′ adaptEqI ≡ᵢ
\end{code}
%</adaptEqIO>
......@@ -45,7 +45,7 @@ infixl 4 _⟫[_]_
%<*seq-het>
\AgdaTarget{\_⟫[\_]\_}
\begin{code}
_⟫[_]_ : ∀ {i m₁ m₂ o s G} (c₁ : ℂ G {s} i m₁) (eq : m₁ ≡ m₂) (c₂ : ℂ G {s} m₂ o) → ℂ G {s} i o
_⟫[_]_ : ∀ {i m₁ m₂ o s G} (c₁ : ℂ[ G ] {s} i m₁) (eq : m₁ ≡ m₂) (c₂ : ℂ[ G ] {s} m₂ o) → ℂ[ G ] {s} i o
c₁ ⟫[ eq ] c₂ = c₁ ⟫ eq⤨ eq ⟫ c₂
\end{code}
%</seq-het>
......@@ -58,7 +58,7 @@ infixr 3 [_]_[_]∥_
%<*par-het-left>
\AgdaTarget{[\_]\_[\_]∥\_}
\begin{code}
[_]_[_]∥_ : ∀ {i₁ i₁′ i₂ o₁ o₁′ o₂ s G} (≡ᵢ : i₁ ≡ i₁′) (c₁ : ℂ G {s} i₁ o₁) (≡ₒ : o₁ ≡ o₁′) (c₂ : ℂ G {s} i₂ o₂) → ℂ G {s} (i₁′ + i₂) (o₁′ + o₂)
[_]_[_]∥_ : ∀ {i₁ i₁′ i₂ o₁ o₁′ o₂ s G} (≡ᵢ : i₁ ≡ i₁′) (c₁ : ℂ[ G ] {s} i₁ o₁) (≡ₒ : o₁ ≡ o₁′) (c₂ : ℂ[ G ] {s} i₂ o₂) → ℂ[ G ] {s} (i₁′ + i₂) (o₁′ + o₂)
[ ≡ᵢ ] c₁ [ ≡ₒ ]∥ c₂ = adaptEqIO ≡ᵢ ≡ₒ c₁ ∥ c₂
\end{code}
%</par-het-left>
......@@ -71,7 +71,7 @@ infixr 3 _∥[_]_[_]
%<*par-het-right>
\AgdaTarget{\_∥[\_]\_[\_]}
\begin{code}
_∥[_]_[_] : ∀ {i₁ i₂ i₂′ o₁ o₂ o₂′ s G} (c₁ : ℂ G {s} i₁ o₁) (≡ᵢ : i₂ ≡ i₂′) (c₂ : ℂ G {s} i₂ o₂) (≡ₒ : o₂ ≡ o₂′) → ℂ G {s} (i₁ + i₂′) (o₁ + o₂′)
_∥[_]_[_] : ∀ {i₁ i₂ i₂′ o₁ o₂ o₂′ s G} (c₁ : ℂ[ G ] {s} i₁ o₁) (≡ᵢ : i₂ ≡ i₂′) (c₂ : ℂ[ G ] {s} i₂ o₂) (≡ₒ : o₂ ≡ o₂′) → ℂ[ G ] {s} (i₁ + i₂′) (o₁ + o₂′)
c₁ ∥[ ≡ᵢ ] c₂ [ ≡ₒ ] = c₁ ∥ adaptEqIO ≡ᵢ ≡ₒ c₂
\end{code}
%</par-het-right>
......@@ -84,7 +84,7 @@ infixr 3 [_]_∥[_]_
%<*par-het-input>
\AgdaTarget{[\_]\_∥[\_]\_}
\begin{code}
[_]_∥[_]_ : ∀ {i₁ i₁′ i₂ i₂′ o₁ o₂ s G} (≡₁ : i₁ ≡ i₁′) (c₁ : ℂ G {s} i₁ o₁) (≡₂ : i₂ ≡ i₂′) (c₂ : ℂ G {s} i₂ o₂) → ℂ G {s} (i₁′ + i₂′) (o₁ + o₂)
[_]_∥[_]_ : ∀ {i₁ i₁′ i₂ i₂′ o₁ o₂ s G} (≡₁ : i₁ ≡ i₁′) (c₁ : ℂ[ G ] {s} i₁ o₁) (≡₂ : i₂ ≡ i₂′) (c₂ : ℂ[ G ] {s} i₂ o₂) → ℂ[ G ] {s} (i₁′ + i₂′) (o₁ + o₂)
[ ≡₁ ] c₁ ∥[ ≡₂ ] c₂ = adaptEqI ≡₁ c₁ ∥ adaptEqI ≡₂ c₂
\end{code}
%</par-het-input>
......@@ -97,7 +97,7 @@ infixr 3 _[_]∥_[_]
%<*par-het-output>
\AgdaTarget{\_[\_]∥\_[\_]}
\begin{code}
_[_]∥_[_] : ∀ {i₁ i₂ o₁ o₁′ o₂ o₂′ s G} (c₁ : ℂ G {s} i₁ o₁) (≡₁ : o₁ ≡ o₁′) (c₂ : ℂ G {s} i₂ o₂) (≡₂ : o₂ ≡ o₂′) → ℂ G {s} (i₁ + i₂) (o₁′ + o₂′)
_[_]∥_[_] : ∀ {i₁ i₂ o₁ o₁′ o₂ o₂′ s G} (c₁ : ℂ[ G ] {s} i₁ o₁) (≡₁ : o₁ ≡ o₁′) (c₂ : ℂ[ G ] {s} i₂ o₂) (≡₂ : o₂ ≡ o₂′) → ℂ[ G ] {s} (i₁ + i₂) (o₁′ + o₂′)
c₁ [ ≡₁ ]∥ c₂ [ ≡₂ ] = adaptEqO ≡₁ c₁ ∥ adaptEqO ≡₂ c₂
\end{code}
%</par-het-output>
......@@ -11,7 +11,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Vec.Extra using (VecNaturalT)
open import Category.NaturalT using (NaturalT)
open NaturalT using (op)
open import PiWare.Circuit using (C; ℂ; Plug)
open import PiWare.Circuit using (C[_]; ℂ[_]; Plug)
open import PiWare.Plugs.Core
using ( nil⤪; nil⤪₀; id⤪; id⤪₁; eq⤪; swap⤪; swap⤪₁; intertwine⤪; head⤪; vecHalf⤪; cons⤪₁
; vecHalfPow⤪; fst⤪; snd⤪; singleton⤪; forkVec⤪; fork×⤪; uncons⤪; uncons⤪₁; cons⤪)
......@@ -21,7 +21,7 @@ open import PiWare.Plugs.Core
%<*nil-plug>
\AgdaTarget{nil⤨}
\begin{code}
nil⤨ : ∀ {n G} → C G n 0
nil⤨ : ∀ {n G} → C[ G ] n 0
nil⤨ = Plug nil⤪
\end{code}
%</nil-plug>
......@@ -29,7 +29,7 @@ nil⤨ = Plug nil⤪
%<*nil-plug-zero>
\AgdaTarget{nil⤨₀}
\begin{code}
nil⤨₀ : ∀ {G} → C G 0 0
nil⤨₀ : ∀ {G} → C[ G ] 0 0
nil⤨₀ = Plug nil⤪₀
\end{code}
%</nil-plug-zero>
......@@ -38,7 +38,7 @@ nil⤨₀ = Plug nil⤪₀
%<*id-plug>
\AgdaTarget{id⤨}
\begin{code}
id⤨ : ∀ {n G} → C G n n
id⤨ : ∀ {n G} → C[ G ] n n
id⤨ = Plug id⤪
\end{code}
%</id-plug>
......@@ -46,7 +46,7 @@ id⤨ = Plug id⤪
%<*id-plug-one>
\AgdaTarget{id⤨₁}
\begin{code}
id⤨₁ : ∀ {G} → C G 1 1
id⤨₁ : ∀ {G} → C[ G ] 1 1
id⤨₁ = Plug id⤪₁
\end{code}
%</id-plug-one>
......@@ -55,7 +55,7 @@ id⤨₁ = Plug id⤪₁
%<*eq-plug>
\AgdaTarget{eq⤨}
\begin{code}
eq⤨ : ∀ {i o G} (p : i ≡ o) → C G i o
eq⤨ : ∀ {i o G} (p : i ≡ o) → C[ G ] i o
eq⤨ p = Plug (eq⤪ p)
\end{code}
%</eq-plug>
......@@ -64,7 +64,7 @@ eq⤨ p = Plug (eq⤪ p)
%<*swap-plug>
\AgdaTarget{swap⤨}
\begin{code}
swap⤨ : ∀ {n m G} → C G (n + m) (m + n)
swap⤨ : ∀ {n m G} → C[ G ] (n + m) (m + n)
swap⤨ {n} {m} = Plug (swap⤪ {n} {m})
\end{code}
%</swap-plug>
......@@ -72,7 +72,7 @@ swap⤨ {n} {m} = Plug (swap⤪ {n} {m})
%<*swap-plug-one>
\AgdaTarget{swap⤨₁}
\begin{code}
swap⤨₁ : ∀ {G} → C G (1 + 1) (1 + 1)
swap⤨₁ : ∀ {G} → C[ G ] (1 + 1) (1 + 1)
swap⤨₁ = Plug swap⤪₁
\end{code}
%</swap-plug-one>
......@@ -81,7 +81,7 @@ swap⤨₁ = Plug swap⤪₁
%<*intertwine-plug>
\AgdaTarget{intertwine⤨}
\begin{code}
intertwine⤨ : ∀ {a b c d G} → C G ((a + b) + (c + d)) ((a + c) + (b + d))
intertwine⤨ : ∀ {a b c d G} → C[ G ] ((a + b) + (c + d)) ((a + c) + (b + d))
intertwine⤨ {a} {b} {c} {d} = Plug (intertwine⤪ {a} {b} {c} {d})
\end{code}
%</intertwine-plug>
......@@ -90,7 +90,7 @@ intertwine⤨ {a} {b} {c} {d} = Plug (intertwine⤪ {a} {b} {c} {d})
%<*head-plug>
\AgdaTarget{head⤨}
\begin{code}
head⤨ : ∀ n {w G} → C G (suc n * w) w
head⤨ : ∀ n {w G} → C[ G ] (suc n * w) w
head⤨ n {w} = Plug (head⤪ n {w})
\end{code}
%</head-plug>
......@@ -99,7 +99,7 @@ head⤨ n {w} = Plug (head⤪ n {w})
%<*uncons-plug>
\AgdaTarget{uncons⤨}
\begin{code}
uncons⤨ : ∀ n {i G} → C G (suc n * i) (i + n * i)
uncons⤨ : ∀ n {i G} → C[ G ] (suc n * i) (i + n * i)
uncons⤨ n {i} = Plug (uncons⤪ n {i})
\end{code}
%</uncons-plug>
......@@ -107,7 +107,7 @@ uncons⤨ n {i} = Plug (uncons⤪ n {i})
%<*uncons-plug-one>
\AgdaTarget{uncons⤨₁}
\begin{code}
uncons⤨₁ : ∀ n {G} → C G (suc n * 1) (1 + n * 1)
uncons⤨₁ : ∀ n {G} → C[ G ] (suc n * 1) (1 + n * 1)
uncons⤨₁ n = Plug (uncons⤪₁ n)
\end{code}
%</uncons-plug-one>
......@@ -116,7 +116,7 @@ uncons⤨₁ n = Plug (uncons⤪₁ n)
%<*cons-plug>
\AgdaTarget{cons⤨}
\begin{code}
cons⤨ : ∀ n {i G} → C G (i + n * i) (suc n * i)
cons⤨ : ∀ n {i G} → C[ G ] (i + n * i) (suc n * i)
cons⤨ n {i} = Plug (cons⤪ n {i})
\end{code}
%</cons-plug>
......@@ -124,7 +124,7 @@ cons⤨ n {i} = Plug (cons⤪ n {i})
%<*cons-plug-one>
\AgdaTarget{cons⤨₁}
\begin{code}
cons⤨₁ : ∀ n {G} → C G (1 + n * 1) (suc n * 1)
cons⤨₁ : ∀ n {G} → C[ G ] (1 + n * 1) (suc n * 1)
cons⤨₁ n = Plug (cons⤪₁ n)
\end{code}
%</cons-plug-one>
......@@ -133,7 +133,7 @@ cons⤨₁ n = Plug (cons⤪₁ n)
%<*singleton-plug>
\AgdaTarget{singleton⤨}
\begin{code}
singleton⤨ : ∀ {w G} → C G w (1 * w)
singleton⤨ : ∀ {w G} → C[ G ] w (1 * w)
singleton⤨ {w} = Plug (singleton⤪ {w})
\end{code}
%</singleton-plug>
......@@ -142,7 +142,7 @@ singleton⤨ {w} = Plug (singleton⤪ {w})
%<*vecHalf-plug>
\AgdaTarget{vecHalf⤨}
\begin{code}
vecHalf⤨ : ∀ n {w G} → C G ((2 * (suc n)) * w) ((suc n) * w + (suc n) * w)
vecHalf⤨ : ∀ n {w G} → C[ G ] ((2 * (suc n)) * w) ((suc n) * w + (suc n) * w)
vecHalf⤨ n {w} = Plug (vecHalf⤪ n {w})
\end{code}
%</vecHalf-plug>
......@@ -151,7 +151,7 @@ vecHalf⤨ n {w} = Plug (vecHalf⤪ n {w})
%<*vecHalfPow-plug>
\AgdaTarget{vecHalfPow⤨}
\begin{code}
vecHalfPow⤨ : ∀ n {w G} → C G ((2 ^ (suc n)) * w) ((2 ^ n) * w + (2 ^ n) * w)
vecHalfPow⤨ : ∀ n {w G} → C[ G ] ((2 ^ (suc n)) * w) ((2 ^ n) * w + (2 ^ n) * w)
vecHalfPow⤨ n {w} = Plug (vecHalfPow⤪ n {w})
\end{code}
%</vecHalfPow-plug>
......@@ -160,7 +160,7 @@ vecHalfPow⤨ n {w} = Plug (vecHalfPow⤪ n {w})
%<*forkVec-plug>
\AgdaTarget{forkVec⤨}
\begin{code}
forkVec⤨ : ∀ n {k G} → C G k (n * k)
forkVec⤨ : ∀ n {k G} → C[ G ] k (n * k)
forkVec⤨ n {k} = Plug (forkVec⤪ n {k})
\end{code}
%</forkVec-plug>
......@@ -169,7 +169,7 @@ forkVec⤨ n {k} = Plug (forkVec⤪ n {k})
%<*forkProd-plug>
\AgdaTarget{fork×⤨}
\begin{code}
fork×⤨ : ∀ {w G} → C G w (w + w)
fork×⤨ : ∀ {w G} → C[ G ] w (w + w)
fork×⤨ {w} = Plug (fork×⤪ {w})
\end{code}
%</forkProd-plug>
......@@ -178,7 +178,7 @@ fork×⤨ {w} = Plug (fork×⤪ {w})
%<*fst-plug>
\AgdaTarget{fst⤨}
\begin{code}
fst⤨ : ∀ {m n G} → C G (m + n) m
fst⤨ : ∀ {m n G} → C[ G ] (m + n) m
fst⤨ {m} {n} = Plug (fst⤪ {m} {n})
\end{code}
%</fst-plug>
......@@ -187,7 +187,7 @@ fst⤨ {m} {n} = Plug (fst⤪ {m} {n})
%<*snd-plug>
\AgdaTarget{snd⤨}
\begin{code}
snd⤨ : ∀ {m n G} → C G (m + n) n
snd⤨ : ∀ {m n G} → C[ G ] (m + n) n
snd⤨ {m} = Plug (snd⤪ {m})
\end{code}
%</snd-plug>
......@@ -196,7 +196,7 @@ snd⤨ {m} = Plug (snd⤪ {m})
%<*plug-Vec-eta>
\AgdaTarget{plug-Vecη}
\begin{code}
plug-Vecη : ∀ {i o G} → VecNaturalT i o → C G i o
plug-Vecη : ∀ {i o G} → VecNaturalT i o → C[ G ] i o
plug-Vecη {i} η = Plug (op η (allFin i))
\end{code}
%</plug-Vec-eta>
......@@ -12,9 +12,10 @@ open import Data.Bool.Properties using (commutativeSemiring-∨-∧)
open import Algebra using (module CommutativeSemiring)
open CommutativeSemiring commutativeSemiring-∨-∧ using () renaming (+-identity to ∨-identity)
open import PiWare.Circuit using (ℂ; σ; C; Gate; _⟫_; _∥_)
open import PiWare.Plugs using (id⤨; id⤨₁; fork×⤨; swap⤨)
open import PiWare.Gates.BoolTrio using (⊥ℂ'; ⊤ℂ'; ¬ℂ'; ∧ℂ'; ∨ℂ') renaming (BoolTrio to B₃)
open import PiWare.Circuit using (σ; C[_]; Gate; _⟫_; _∥_) renaming (module WithGates to CircuitWithGates)
open import PiWare.Gates.BoolTrio using (⊥ℂ'; ⊤ℂ'; ¬ℂ'; ∧ℂ'; ∨ℂ'; BoolTrio)
open CircuitWithGates BoolTrio using (ℂ; C)
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)
......@@ -27,9 +28,9 @@ open ComplianceWithGates spec-B₃ using (_⫃_)
%<*fundamentals-type>
\begin{code}
⊥ℂ ⊤ℂ : C B₃ 0 1
∧ℂ ∨ℂ : C B₃ 2 1
¬ℂ : C B₃ 1 1
⊥ℂ ⊤ℂ : C 0 1
∧ℂ ∨ℂ : C 2 1
¬ℂ : C 1 1
\end{code}
%</fundamentals-type>
......@@ -48,7 +49,7 @@ open ComplianceWithGates spec-B₃ using (_⫃_)
%<*nand>
\AgdaTarget{⊼ℂ}
\begin{code}
⊼ℂ : C B₃ 2 1
⊼ℂ : C 2 1
⊼ℂ = ∧ℂ ⟫ ¬ℂ
\end{code}
%</nand>
......@@ -57,7 +58,7 @@ open ComplianceWithGates spec-B₃ using (_⫃_)
%<*xor>
\AgdaTarget{⊻ℂ}
\begin{code}
⊻ℂ : C B₃ 2 1
⊻ℂ : C 2 1
⊻ℂ = fork×⤨
⟫ (¬ℂ ∥ id⤨₁ ⟫ ∧ℂ) ∥ (id⤨₁ ∥ ¬ℂ ⟫ ∧ℂ)
⟫ ∨ℂ
......@@ -68,7 +69,7 @@ open ComplianceWithGates spec-B₃ using (_⫃_)
%<*andN>
\AgdaTarget{andN}
\begin{code}
andN : ∀ n → ℂ B₃ {σ} (n * 1) 1
andN : ∀ n → ℂ {σ} (n * 1) 1
andN n = (linear-reductor n) ∧ℂ ⊤ℂ
\end{code}
%</andN>
......@@ -78,7 +79,7 @@ andN n = (linear-reductor n) ∧ℂ ⊤ℂ
%<*hadd>
\AgdaTarget{hadd}
\begin{code}
hadd : C B₃ 2 2
hadd : C 2 2
hadd = fork×⤨
⟫ ⊻ℂ ∥ ∧ℂ
\end{code}
......@@ -89,7 +90,7 @@ hadd = fork×⤨
%<*fadd>
\AgdaTarget{fadd}
\begin{code}
fadd : C B₃ (1 + 2) (1 + 1)
fadd : C (1 + 2) (1 + 1)
fadd = id⤨₁ ∥ hadd
⟫ hadd ∥ id⤨₁
⟫ id⤨₁ ∥ ∨ℂ
......@@ -98,7 +99,7 @@ fadd = id⤨₁ ∥ hadd
\begin{code}
row : ∀ {k} n {G} → C G (k + (k + k)) (k + k) → C G (k + (n * k + n * k)) (n * k + k)
row : ∀ {k} n {G} → C[ G ] (k + (k + k)) (k + k) → C[ G ] (k + (n * k + n * k)) (n * k + k)
row {k} zero _ rewrite +-right-identity k = id⤨ {k}
row {k} (suc n) c = ⊥ where postulate ⊥ : _
-- id⤨ {k + k} ∥ swap⤨ {n * k} {k + n * k}
......@@ -110,7 +111,7 @@ row {k} (suc n) c = ⊥ where postulate ⊥ : _
%<*ripple>
\AgdaTarget{ripple}
\begin{code}
ripple : ∀ n → C B₃ (1 + (n + n)) (n + 1)
ripple : ∀ n → C (1 + (n + n)) (n + 1)
ripple zero = id⤨₁
ripple (suc n) = id⤨ {1 + 1} ∥ swap⤨ {n} {1 + n}
⟫ fadd ∥ id⤨ {n + n}
......
......@@ -22,15 +22,15 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; inspect; c
open import Data.CausalStream using (runᶜ′)
open import PiWare.Plugs.Core using (_⤪_; _⟫⤪_; _|⤪_; id⤪₁; swap⤪₁)
open import PiWare.Plugs using (swap⤨₁; fork×⤨)
open import PiWare.Circuit using (C; ℂ; Plug; DelayLoop; _⟫_)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Circuit using (Plug; DelayLoop; _⟫_) renaming (module WithGates to CircuitWithGates)
open import PiWare.Gates.BoolTrio using (BoolTrio)
open CircuitWithGates BoolTrio using (ℂ; C)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates; delay′)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open WithGates spec-B₃ using (⟦_⟧ω; ⟦_⟧ᶜ; ⟦_⟧)
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_]; ℂₛ)
renaming (module WithGates to WithGatesₛ)
open WithGatesₛ spec-B₃ using (⟦_⟧ₛ; ⟦_⟧ω')
open import PiWare.Semantics.SimulationState Atomic-Bool using (mealy; ⟦_⟧ₛ[_]; DelayLoopₛ; Plugₛ; Gateₛ; _⟫ₛ_; ⟦_⟧ω'[_]) renaming (module WithGates to WithGatesₛ)
open WithGatesₛ spec-B₃ using (⟦_⟧ₛ; ⟦_⟧ω'; ℂₛ)
open import PiWare.Samples.BoolTrioComb using (¬ℂ; ⊥ℂ; ∨ℂ)
open import PiWare.Samples.Muxes using (mux)
......@@ -46,7 +46,7 @@ open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓
%<*shift>
\AgdaTarget{shift}
\begin{code}
shift : ℂ B₃ 1 1
shift : ℂ 1 1
shift = DelayLoop swap⤨₁
\end{code}
%</shift>
......@@ -129,7 +129,7 @@ proofShift′ {x ∷ xs} = singleton∘lookup1 {x = x} ∷ ♯ transₛ lemmaShi
%<*toggle>
\AgdaTarget{toggle}
\begin{code}
toggle : ℂ B₃ 0 1
toggle : ℂ 0 1
toggle = ⊥ℂ ⟫ DelayLoop (∨ℂ ⟫ ¬ℂ ⟫ fork×⤨)
\end{code}
%</toggle>
......@@ -191,7 +191,7 @@ proofToggle = toggle-runᶜ′-𝕋 (toggleᶜ-start {[]})
\begin{code}
stateToggle𝔽 stateToggle𝕋 : ℂₛ B₃ toggle
stateToggle𝔽 stateToggle𝕋 : ℂₛ toggle
\end{code}
%<*stateToggle𝔽-𝕋>
\AgdaTarget{stateToggle𝔽, stateToggle𝕋}
......@@ -239,7 +239,7 @@ rotateL⤪₃ = swap⤪₁ |⤪ id⤪₁
%<*regCore>
\AgdaTarget{regCore}
\begin{code}
regCore : C B₃ 3 2
regCore : C 3 2
regCore = Plug rotateL⤪₃ ⟫ mux ⟫ fork×⤨
\end{code}
%</regCore>
......@@ -248,7 +248,7 @@ regCore = Plug rotateL⤪₃ ⟫ mux ⟫ fork×⤨
%<*reg>
\AgdaTarget{reg}
\begin{code}
reg : ℂ B₃ 2 1
reg : ℂ 2 1
reg = DelayLoop regCore
\end{code}
%</reg>
......
......@@ -13,8 +13,9 @@ open CommutativeSemiring commutativeSemiring-∨-∧ using () renaming (+-identi
open import PiWare.Plugs.Core using (_⤪_; _⟫⤪_; _|⤪_; id⤪; fork×⤪; intertwine⤪; swap⤪₁)
open import PiWare.Plugs using (fork×⤨; nil⤨; id⤨₁; fst⤨; snd⤨)
open import PiWare.Circuit using (C; _⟫_; _∥_; Plug)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Circuit using (_⟫_; _∥_; Plug) renaming (module WithGates to CircuitWithGates)
open import PiWare.Gates.BoolTrio using (BoolTrio)
open CircuitWithGates BoolTrio using (C)
open import PiWare.Samples.BoolTrioComb using (¬ℂ; ∧ℂ; ∨ℂ)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation Atomic-Bool using (W⟶W) renaming (module WithGates to SimulationWithGates)
......@@ -29,7 +30,7 @@ open ComplianceWithGates spec-B₃ using (_⫃_)
%<*mux>
\AgdaTarget{mux}
\begin{code}
mux : C B₃ 3 1
mux : C 3 1
mux = fork×⤨
⟫ (¬ℂ ∥ fst⤨₁ ⟫ ∧ℂ) ∥ (id⤨₁ ∥ snd⤨₁ ⟫ ∧ℂ)
⟫ ∨ℂ
......@@ -52,13 +53,13 @@ adapt⤪ n = fork×⤪ {1} |⤪ id⤪ {(1 + n) + (1 + n)}
\end{code}
%</adapt-fin>
\begin{code}
where intertwine⤪₁ = intertwine⤪ {1} {1} {1} {1}
where intertwine⤪₁ = intertwine⤪ {1} {1} {1} {1}
\end{code}
%<*adapt-plug>
\AgdaTarget{adapt⤨}
\begin{code}
adapt⤨ : ∀ n → C B₃ (1 + ((1 + n) + (1 + n))) ((1 + 1 + 1) + (1 + (n + n)))
adapt⤨ : ∀ n → C (1 + ((1 + n) + (1 + n))) ((1 + 1 + 1) + (1 + (n + n)))
adapt⤨ = Plug ∘ adapt⤪
\end{code}
%</adapt-plug>
......@@ -66,7 +67,7 @@ adapt⤨ = Plug ∘ adapt⤪
%<*muxN>
\AgdaTarget{muxN}
\begin{code}
muxN : ∀ n → C B₃ (1 + (n + n)) n
muxN : ∀ n → C (1 + (n + n)) n
muxN zero = nil⤨
muxN (suc n) = adapt⤨ n ⟫ mux ∥ muxN n
\end{code}
......
......@@ -25,8 +25,9 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong;
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
open import Data.CausalStream using (runᶜ′)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Circuit using (ℂ; C; Plug; DelayLoop; _⟫_; ω)
open import PiWare.Circuit using (Plug; DelayLoop; _⟫_; ω) renaming (module WithGates to CircuitWithGates)
open import PiWare.Gates.BoolTrio using (BoolTrio)
open CircuitWithGates BoolTrio using (ℂ; C)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Patterns Atomic-Bool using (parsN)
open import PiWare.Plugs using (eq⤨)
......@@ -49,7 +50,7 @@ open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓
%<*regn-distribute>
\AgdaTarget{regn-distribute}
\begin{code}
regn-distribute : ∀ n → C B₃ (suc n) (n +⋎ n)
regn-distribute : ∀ n → C (suc n) (n +⋎ n)
regn-distribute n = Plug $ tabulate (raise 1) ⋎ replicate {n = n} Fz
\end{code}
%</regn-distribute>
......@@ -79,7 +80,7 @@ regn-distribute n = Plug $ tabulate (raise 1) ⋎ replicate {n = n} Fz
%<*regn-n+⋎n≡n*2>
\AgdaTarget{regn-n+⋎n≡n*2}
\begin{code}
regn-n+⋎n≡n*2 : ∀ n → C B₃ (n +⋎ n) (n * 2)