Finish ℂ[_]

parent 1213d469
......@@ -22,8 +22,9 @@ open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; con
open ≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)
open import Data.CausalStream using (runᶜ′; runᶜ-const)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Circuit using (ℂ; C; Plug; _⟫_; _∥_)
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.Plugs using (nil⤨)
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation Atomic-Bool using (module WithGates; W)
......@@ -43,7 +44,7 @@ open _⇕_ (⇕× ⦃ ⇕Bool ⦄ ⦃ ⇕Bool ⦄) using () renaming (⇓ to ⇓
%<*regn-plug>
\AgdaTarget{regn-plug}
\begin{code}
regn-plug : {n : ℕ} → C B₃ (2 + n) (3 + n)
regn-plug : {n : ℕ} → C (2 + n) (3 + n)
regn-plug = Plug ((# 1) ∷ (# 0) ∷ (# 0) ∷ tabulate (raise 2)) -- load (bit #0) duplicated
\end{code}
%</regn-plug>
......@@ -55,7 +56,7 @@ regn-plug = Plug ((# 1) ∷ (# 0) ∷ (# 0) ∷ tabulate (raise 2)) -- load (bi
%<*regn>
\AgdaTarget{regn}
\begin{code}
regn : ∀ n → ℂ B₃ (1 + n) n
regn : ∀ n → ℂ (1 + n) n
regn zero = nil⤨
regn (suc n) = regn-plug {n} ⟫ (reg ∥ regn n)
\end{code}
......
......@@ -4,7 +4,7 @@ module PiWare.Semantics.AreaAnalysis where
open import Data.Nat.Base using (ℕ; _+_)
open import PiWare.Interface using (Ix)
open import PiWare.Circuit using (ℂ; σ)
open import PiWare.Circuit using (ℂ[_]; σ)
open import PiWare.Circuit.Algebra using (ℂσA; ℂA; cataℂσ; cataℂ; TyGate; TyPlug; Ty⟫; Ty∥)
\end{code}
......@@ -66,7 +66,7 @@ areaσ[ g ] = record { GateA = g; PlugA = plugA; _⟫A_ = seqA {X} {X} {X}; _∥
%<*area-combinational>
\AgdaTarget{⟦\_⟧ₐ[\_]}
\begin{code}
⟦_⟧ₐ[_] : ∀ {i o G} → ℂ G {σ} i o → TyGate G Area → Area i o
⟦_⟧ₐ[_] : ∀ {i o G} → ℂ[ G ] {σ} i o → TyGate G Area → Area i o
⟦ c ⟧ₐ[ g ] = cataℂσ Area areaσ[ g ] c
\end{code}
%</area-combinational>
......@@ -89,7 +89,7 @@ area[_] {G} g = record { GateA = GateA (areaσ[_] {G} g)
%<*area-sequential>
\AgdaTarget{⟦\_⟧ωₐ[\_]}
\begin{code}
⟦_⟧ωₐ[_] : ∀ {i o G} → ℂ G i o → TyGate G Area → Area i o
⟦_⟧ωₐ[_] : ∀ {i o G} → ℂ[ G ] i o → TyGate G Area → Area i o
⟦ c ⟧ωₐ[ g ] = cataℂ Area Area areaσ[ g ] area[ g ] c
\end{code}
%</area-sequential>
......@@ -111,7 +111,7 @@ module WithGates {G} (g : TyGate G Area) where
%<*area-combinational-with-gates>
\AgdaTarget{⟦\_⟧ₐ}
\begin{code}
⟦_⟧ₐ : ∀ {i o} → ℂ G {σ} i o → Area i o
⟦_⟧ₐ : ∀ {i o} → ℂ[ G ] {σ} i o → Area i o
⟦_⟧ₐ = ⟦_⟧ₐ[ g ]
\end{code}
%</area-combinational-with-gates>
......@@ -128,7 +128,7 @@ module WithGates {G} (g : TyGate G Area) where
%<*area-sequential-with-gates>
\AgdaTarget{⟦\_⟧ωₐ}
\begin{code}
⟦_⟧ωₐ : ∀ {i o} → ℂ G i o → Area i o
⟦_⟧ωₐ : ∀ {i o} → ℂ[ G ] i o → Area i o
⟦_⟧ωₐ = ⟦_⟧ωₐ[ g ]
\end{code}
%</area-sequential-with-gates>
......@@ -16,7 +16,7 @@ open module X {ℓ} {α : Set ℓ} = UsingVectorEquality (setoid α) using (xs++
open VPE using (_≈_; to-≡; from-≡; _++-cong_) renaming (refl to reflᵥ)
open ≡-Reasoning using (begin_; _∎; _≡⟨_⟩_; _≡⟨⟩_)
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; adaptEqO; adaptEqIO)
......@@ -29,7 +29,7 @@ open import PiWare.Semantics.Simulation.Properties.Plugs A using (id⤨⫃id[_];
%<*adaptEqI-noop>
\AgdaTarget{adaptEqI-noop}
\begin{code}
adaptEqI-noop : ∀ {i i′ o G} {g : TyGate G W⟶W} {i≡ : i ≡ i′} (c : ℂ G i o) → adaptEqI i≡ c ≋[ g ] c
adaptEqI-noop : ∀ {i i′ o G} {g : TyGate G W⟶W} {i≡ : i ≡ i′} (c : ℂ[ G ] i o) → adaptEqI i≡ c ≋[ g ] c
adaptEqI-noop {i≡ = p} c rewrite p = ≋-refl
\end{code}
%</adaptEqI-noop>
......@@ -38,7 +38,7 @@ adaptEqI-noop {i≡ = p} c rewrite p = ≋-refl
%<*adaptEqO-noop>
\AgdaTarget{adaptEqO-noop}
\begin{code}
adaptEqO-noop : ∀ {i o o′ G} {g : TyGate G W⟶W} {o≡ : o ≡ o′} (c : ℂ G i o) → adaptEqO o≡ c ≋[ g ] c
adaptEqO-noop : ∀ {i o o′ G} {g : TyGate G W⟶W} {o≡ : o ≡ o′} (c : ℂ[ G ] i o) → adaptEqO o≡ c ≋[ g ] c
adaptEqO-noop {o≡ = p} c rewrite p = ≋-refl
\end{code}
%</adaptEqO-noop>
......@@ -47,7 +47,7 @@ adaptEqO-noop {o≡ = p} c rewrite p = ≋-refl
%<*adaptEqIO-noop>
\AgdaTarget{adaptEqIO-noop}
\begin{code}
adaptEqIO-noop : ∀ {i i′ o o′ G} {g : TyGate G W⟶W} {i≡ : i ≡ i′} {o≡ : o ≡ o′} (c : ℂ G i o) → adaptEqIO i≡ o≡ c ≋[ g ] c
adaptEqIO-noop : ∀ {i i′ o o′ G} {g : TyGate G W⟶W} {i≡ : i ≡ i′} {o≡ : o ≡ o′} (c : ℂ[ G ] i o) → adaptEqIO i≡ o≡ c ≋[ g ] c
adaptEqIO-noop {i≡ = pᵢ} {pₒ} c rewrite pᵢ | pₒ = ≋-refl
\end{code}
%</adaptEqIO-noop>
......@@ -60,7 +60,7 @@ infixl 4 _⟫-cong_
%<*seq-cong>
\AgdaTarget{⟫-cong}
\begin{code}
_⟫-cong_ : ∀ {i₁ i₂ m₁ m₂ o₁ o₂ G} {g : TyGate G W⟶W} {c₁ : ℂ G i₁ m₁} {d₁ : ℂ G m₁ o₁} {c₂ : ℂ G i₂ m₂} {d₂ : ℂ G m₂ o₂}
_⟫-cong_ : ∀ {i₁ i₂ m₁ m₂ o₁ o₂ G} {g : TyGate G W⟶W} {c₁ : ℂ[ G ] i₁ m₁} {d₁ : ℂ[ G ] m₁ o₁} {c₂ : ℂ[ G ] i₂ m₂} {d₂ : ℂ[ G ] m₂ o₂}
→ c₁ ≋[ g ] c₂ → d₁ ≋[ g ] d₂ → (c₁ ⟫ d₁) ≋[ g ] (c₂ ⟫ d₂)
(refl≋ refl c₁≊c₂) ⟫-cong (refl≋ refl d₁≊d₂) = ≅⇒≋ (d₁≊d₂ ∘ c₁≊c₂ ∘ reflᵥ)
\end{code}
......@@ -70,7 +70,7 @@ _⟫-cong_ : ∀ {i₁ i₂ m₁ m₂ o₁ o₂ G} {g : TyGate G W⟶W} {c₁ :
%<*seq-right-identity>
\AgdaTarget{⟫-right-identity}
\begin{code}
⟫-right-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ G i o) → c ⟫ id⤨ ≋[ g ] c
⟫-right-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ[ G ] i o) → c ⟫ id⤨ ≋[ g ] c
⟫-right-identity {g = g } c = ≅⇒≋ (id⤨⫅id[ g ] ∘ ⟦ c ⟧[ g ])
\end{code}
%</seq-right-identity>
......@@ -79,7 +79,7 @@ _⟫-cong_ : ∀ {i₁ i₂ m₁ m₂ o₁ o₂ G} {g : TyGate G W⟶W} {c₁ :
%<*seq-left-identity>
\AgdaTarget{⟫-left-identity}
\begin{code}
⟫-left-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ G i o) → id⤨ ⟫ c ≋[ g ] c
⟫-left-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ[ G ] i o) → id⤨ ⟫ c ≋[ g ] c
⟫-left-identity {g = g} c = ≅⇒≋ (from-≡ ∘ cong ⟦ c ⟧[ g ] ∘ id⤨⫃id[ g ])
\end{code}
%</seq-left-identity>
......@@ -88,7 +88,7 @@ _⟫-cong_ : ∀ {i₁ i₂ m₁ m₂ o₁ o₂ G} {g : TyGate G W⟶W} {c₁ :
%<*seq-assoc>
\AgdaTarget{⟫-assoc}
\begin{code}
⟫-assoc : ∀ {i m n o G} {g : TyGate G W⟶W} (c₁ : ℂ G i m) (c₂ : ℂ G m n) (c₃ : ℂ G n o) → (c₁ ⟫ c₂) ⟫ c₃ ≋[ g ] c₁ ⟫ (c₂ ⟫ c₃)
⟫-assoc : ∀ {i m n o G} {g : TyGate G W⟶W} (c₁ : ℂ[ G ] i m) (c₂ : ℂ[ G ] m n) (c₃ : ℂ[ G ] n o) → (c₁ ⟫ c₂) ⟫ c₃ ≋[ g ] c₁ ⟫ (c₂ ⟫ c₃)
⟫-assoc c₁ c₂ c₃ = ≅⇒≋ (from-≡ ∘ λ _ → refl)
\end{code}
%</seq-assoc>
......@@ -101,7 +101,7 @@ infixr 5 _∥-cong_
\AgdaTarget{_∥-cong_}
\begin{code}
_∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶W} {c₁ : ℂ G i₁ o₁} {d₁ : ℂ G j₁ p₁} {c₂ : ℂ G i₂ o₂} {d₂ : ℂ G j₂ p₂}
_∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶W} {c₁ : ℂ[ G ] i₁ o₁} {d₁ : ℂ[ G ] j₁ p₁} {c₂ : ℂ[ G ] i₂ o₂} {d₂ : ℂ[ G ] j₂ p₂}
→ c₁ ≋[ g ] c₂ → d₁ ≋[ g ] d₂ → (c₁ ∥ d₁) ≋[ g ] (c₂ ∥ d₂)
(refl≋ refl c₁≊c₂) ∥-cong (refl≋ refl d₁≊d₂) = ≅⇒≋ (λ _ → (c₁≊c₂ (reflᵥ _)) ++-cong (d₁≊d₂ (reflᵥ _)))
\end{code}
......@@ -111,7 +111,7 @@ _∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶
%<*par-left-identity>
\AgdaTarget{∥-left-identity}
\begin{code}
∥-left-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ G i o) → nil⤨₀ ∥ c ≋[ g ] c
∥-left-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ[ G ] i o) → nil⤨₀ ∥ c ≋[ g ] c
∥-left-identity _ = ≅⇒≋ (λ _ → reflᵥ _)
\end{code}
%</par-left-identity>
......@@ -120,7 +120,7 @@ _∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶
%<*par-right-identity-prime>
\AgdaTarget{∥-right-identity≊}
\begin{code}
∥-right-identity≊ : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ G i o) → c ∥ nil⤨₀ ≊[ g ] c
∥-right-identity≊ : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ[ G ] i o) → c ∥ nil⤨₀ ≊[ g ] c
∥-right-identity≊ {g = g} c w≈w′ rewrite to-≡ (proj₁∘splitAt-last≈ w≈w′) = xs++[]=xs (⟦ c ⟧[ g ] _)
\end{code}
%</par-right-identity-prime>
......@@ -128,7 +128,7 @@ _∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶
%<*par-right-identity>
\AgdaTarget{∥-right-identity}
\begin{code}
∥-right-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ G i o) → c ∥ nil⤨₀ ≋[ g ] c
∥-right-identity : ∀ {i o G} {g : TyGate G W⟶W} (c : ℂ[ G ] i o) → c ∥ nil⤨₀ ≋[ g ] c
∥-right-identity {i} {o} c = refl≋ (+-right-identity i) (∥-right-identity≊ c)
\end{code}
%</par-right-identity>
......@@ -137,7 +137,7 @@ _∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶
%<*par-assoc-prime>
\AgdaTarget{∥-assoc≊}
\begin{code}
∥-assoc≊ : ∀ {i₁ o₁ i₂ o₂ i₃ o₃ G} {g : TyGate G W⟶W} (c₁ : ℂ G i₁ o₁) (c₂ : ℂ G i₂ o₂) (c₃ : ℂ G i₃ o₃) → (c₁ ∥ c₂) ∥ c₃ ≊[ g ] c₁ ∥ (c₂ ∥ c₃)
∥-assoc≊ : ∀ {i₁ o₁ i₂ o₂ i₃ o₃ G} {g : TyGate G W⟶W} (c₁ : ℂ[ G ] i₁ o₁) (c₂ : ℂ[ G ] i₂ o₂) (c₃ : ℂ[ G ] i₃ o₃) → (c₁ ∥ c₂) ∥ c₃ ≊[ g ] c₁ ∥ (c₂ ∥ c₃)
∥-assoc≊ {i₁} {_} {i₂} {g = g} c₁ c₂ c₃ {w} {w′} w≈w′
rewrite to-≡ (++-assoc-split₁ {i₁} w≈w′) | to-≡ (++-assoc-split₂ {i₁} w≈w′) | sym (to-≡ (++-assoc-split₃ {i₁} w≈w′))
= ++-assoc (⟦ c₁ ⟧[ g ] w₁) (⟦ c₂ ⟧[ g ] w₂) (⟦ c₃ ⟧[ g ] w₃)
......@@ -150,7 +150,7 @@ _∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶
%<*par-assoc>
\AgdaTarget{∥-assoc}
\begin{code}
∥-assoc : ∀ {i₁ o₁ i₂ o₂ i₃ o₃ G} {g : TyGate G W⟶W} {c₁ : ℂ G i₁ o₁} {c₂ : ℂ G i₂ o₂} {c₃ : ℂ G i₃ o₃} → (c₁ ∥ c₂) ∥ c₃ ≋[ g ] c₁ ∥ (c₂ ∥ c₃)
∥-assoc : ∀ {i₁ o₁ i₂ o₂ i₃ o₃ G} {g : TyGate G W⟶W} {c₁ : ℂ[ G ] i₁ o₁} {c₂ : ℂ[ G ] i₂ o₂} {c₃ : ℂ[ G ] i₃ o₃} → (c₁ ∥ c₂) ∥ c₃ ≋[ g ] c₁ ∥ (c₂ ∥ c₃)
∥-assoc {i₁} {_} {i₂} {_} {i₃} {g = g} {c₁} {c₂} {c₃} = refl≋ (+-assoc i₁ i₂ i₃) (∥-assoc≊ c₁ c₂ c₃)
\end{code}
%</par-assoc>
......@@ -159,7 +159,7 @@ _∥-cong_ : ∀ {i₁ o₁ j₁ p₁ i₂ o₂ j₂ p₂ G} {g : TyGate G W⟶
%<*rows-to-cols-prime>
\AgdaTarget{rows-to-cols≡}
\begin{code}
rows-to-cols≡ : ∀ {i₁ m₁ o₁ i₂ m₂ o₂ G} {g : TyGate G W⟶W} (f₁ : ℂ G i₁ m₁) (f₂ : ℂ G i₂ m₂) (g₁ : ℂ G m₁ o₁) (g₂ : ℂ G m₂ o₂)
rows-to-cols≡ : ∀ {i₁ m₁ o₁ i₂ m₂ o₂ G} {g : TyGate G W⟶W} (f₁ : ℂ[ G ] i₁ m₁) (f₂ : ℂ[ G ] i₂ m₂) (g₁ : ℂ[ G ] m₁ o₁) (g₂ : ℂ[ G ] m₂ o₂)
→ ∀ w → ⟦ (f₁ ∥ f₂) ⟫ (g₁ ∥ g₂) ⟧[ g ] w ≡ ⟦ (f₁ ⟫ g₁) ∥ (f₂ ⟫ g₂) ⟧[ g ] w
rows-to-cols≡ {i₁} {g = g} f₁ f₂ _ _ w rewrite splitAt++ ((⟦ f₁ ⟧[ g ] ∘ ₁ ∘ splitAt i₁) w) ((⟦ f₂ ⟧[ g ] ∘ ₂′ ∘ splitAt i₁) w) = refl
\end{code}
......@@ -169,7 +169,7 @@ rows-to-cols≡ {i₁} {g = g} f₁ f₂ _ _ w rewrite splitAt++ ((⟦ f₁ ⟧[
%<*rows-to-cols>
\AgdaTarget{rows-to-cols}
\begin{code}
rows-to-cols : ∀ {i₁ m₁ o₁ i₂ m₂ o₂ G} {g : TyGate G W⟶W} (f₁ : ℂ G i₁ m₁) (f₂ : ℂ G i₂ m₂) (g₁ : ℂ G m₁ o₁) (g₂ : ℂ G m₂ o₂)
rows-to-cols : ∀ {i₁ m₁ o₁ i₂ m₂ o₂ G} {g : TyGate G W⟶W} (f₁ : ℂ[ G ] i₁ m₁) (f₂ : ℂ[ G ] i₂ m₂) (g₁ : ℂ[ G ] m₁ o₁) (g₂ : ℂ[ G ] m₂ o₂)
→ (f₁ ∥ f₂) ⟫ (g₁ ∥ g₂) ≋[ g ] (f₁ ⟫ g₁) ∥ (f₂ ⟫ g₂)
rows-to-cols {i₁} {m₁} {g = g} f₁ f₂ g₁ g₂ = ≅⇒≋ (from-≡ ∘ (rows-to-cols≡ f₁ f₂ g₁ g₂))
\end{code}
......@@ -179,7 +179,7 @@ rows-to-cols {i₁} {m₁} {g = g} f₁ f₂ g₁ g₂ = ≅⇒≋ (from-≡ ∘
%<*cols-to-rows>
\AgdaTarget{cols-to-rows}
\begin{code}
cols-to-rows : ∀ {i₁ m₁ o₁ i₂ m₂ o₂ G} {g : TyGate G W⟶W} (f₁ : ℂ G i₁ m₁) (f₂ : ℂ G i₂ m₂) (g₁ : ℂ G m₁ o₁) (g₂ : ℂ G m₂ o₂)
cols-to-rows : ∀ {i₁ m₁ o₁ i₂ m₂ o₂ G} {g : TyGate G W⟶W} (f₁ : ℂ[ G ] i₁ m₁) (f₂ : ℂ[ G ] i₂ m₂) (g₁ : ℂ[ G ] m₁ o₁) (g₂ : ℂ[ G ] m₂ o₂)
→ (f₁ ⟫ g₁) ∥ (f₂ ⟫ g₂) ≋[ g ] (f₁ ∥ f₂) ⟫ (g₁ ∥ g₂)
cols-to-rows f₁ f₂ g₁ g₂ = ≋-sym (rows-to-cols f₁ f₂ g₁ g₂)
\end{code}
......
......@@ -15,7 +15,7 @@ open import Data.List.NonEmpty using (_∷_)
open import PiWare.Gates using (Gates)
open Gates using (|in|; |out|)
open import PiWare.Circuit using (ℂ; C; Gate; Plug)
open import PiWare.Circuit using (C[_]; Gate; Plug)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Semantics.Simulation A using (W⟶W; ⟦_⟧[_]; ⟦_⟧ω[_]; ⟦_⟧ᶜ[_])
......@@ -41,5 +41,5 @@ proof-gate {g = g} pp (x ∷ xs) = ≈ₚ-to-≈ $ lemma-gate {g = g} pp (♭ xs
-- The property we would actually like to have
ω-extends-σ : Set₁
ω-extends-σ = ∀ {i o G} {g : TyGate G W⟶W} {c : C G i o} {f} → ⟦ c ⟧[ g ] ≗ f → ∀ ins → ⟦ c ⟧ω[ g ] ins ≈ map f ins
ω-extends-σ = ∀ {i o G} {g : TyGate G W⟶W} {c : C[ G ] i o} {f} → ⟦ c ⟧[ g ] ≗ f → ∀ ins → ⟦ c ⟧ω[ g ] ins ≈ map f ins
\end{code}
\begin{code}
module PiWare.Semantics.Simulation.Properties.NoExtension where
open import Function using (_$_; _∘′_; id)
open import Coinduction using (♯_; ♭)
open import Data.Bool
open import Data.Stream
open import Function using (_∘′_)
open import Data.Bool using () renaming (false to 𝔽; true to 𝕋)
open import Data.Fin using () renaming (zero to Fz; suc to Fs)
open import Data.Vec using ([]; _∷_; [_]; head)
open import Data.Stream using (repeat; _∷_)
open import Data.Empty using (⊥)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; sym; trans; inspect; [_])
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.Atomic.Bool using (Atomic-Bool)
open import PiWare.Semantics.Simulation.Properties.Extension Atomic-Bool using (ω-extends-σ)
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to b₃)
import Data.Fin as F
import Data.Vec as V
import Data.Empty as E
open import PiWare.Atomic.Bool using (Atomic-Bool)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Semantics.Simulation.Properties.Extension Atomic-Bool
open import PiWare.Semantics.Simulation.BoolTrio using () renaming (spec to spec-B₃)
open import PiWare.Circuit using (σ; ω; C; Plug)
badC : C 2 1
badC {σ} = Plug (Fz ∷ [])
badC {ω} = Plug (Fs Fz ∷ [])
badCircuit : C B₃ 2 1
badCircuit {σ} = Plug (F.zero V.∷ V.[])
badCircuit {ω} = Plug ((F.suc F.zero) V.∷ V.[])
badBehaviour : ω-extends-σ → E.⊥
badBehaviour e with e {g = spec-B₃} {c = badCircuit} {f = V.[_] ∘′ V.head} (λ {(x₁ V.∷ x₂ V.∷ V.[]) → refl}) (repeat (true V.∷ false V.∷ V.[]))
badBehaviour e | () ∷ xs≈
¬ω-extends-σ : ¬ ω-extends-σ
¬ω-extends-σ e with e {g = b₃} {c = badC} {f = [_] ∘′ head} (λ {(_ ∷ _ ∷ []) → refl}) (repeat (𝕋 ∷ 𝔽 ∷ []))
¬ω-extends-σ _ | () ∷ xs≈
\end{code}
......@@ -7,27 +7,27 @@ open import Data.Product using (proj₁)
open import PiWare.Gates using (Gates)
open import PiWare.Plugs using (id⤨₁)
open import PiWare.Circuit using (C; _⟫_; _∥_)
open import PiWare.Circuit using (C[_]; _⟫_; _∥_)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.Simulation.Equality A using (_≋[_]_)
\end{code}
%<*C2>
\AgdaTarget{C₂}
%<*C₂[_]>
\AgdaTarget{C₂[\_]}
\begin{code}
C₂ : Gates → Set
C₂ G = C G 2 1
C₂[_] : Gates → Set
C₂[ G ] = C[ G ] 2 1
\end{code}
%</C2>
%</C₂[_]>
%<*IsSemigroupC2>
\AgdaTarget{IsSemigroupC₂}
\begin{code}
IsSemigroupC₂ : ∀ {G} (g : TyGate G W⟶W) → C₂ G → Set
IsSemigroupC₂ g c = c ∥ id⤨₁ ⟫ c ≋[ g ] id⤨₁ ∥ c ⟫ c
IsSemigroupC₂[_] : ∀ {G} (g : TyGate G W⟶W) → C₂[ G ] → Set
IsSemigroupC₂[ g ] c = c ∥ id⤨₁ ⟫ c ≋[ g ] id⤨₁ ∥ c ⟫ c
\end{code}
%</IsSemigroupC2>
......@@ -36,7 +36,7 @@ IsSemigroupC₂ g c = c ∥ id⤨₁ ⟫ c ≋[ g ] id⤨₁ ∥ c ⟫ c
\AgdaTarget{SemigroupC₂}
\begin{code}
record SemigroupC₂ {G} (g : TyGate G W⟶W) : Set where
field ⊕C : C₂ G
isSemigroup : IsSemigroupC₂ g ⊕C
field ⊕C : C₂[ G ]
isSemigroup : IsSemigroupC₂[ g ] ⊕C
\end{code}
%</SemigroupC2>
......@@ -17,7 +17,7 @@ open import PiWare.Circuit using (Gate; _⟫_; _∥_)
open import PiWare.Plugs using (id⤨₁)
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W)
open import PiWare.Semantics.Simulation.Semigroup.Base A using (C₂; IsSemigroupC₂; SemigroupC₂)
open import PiWare.Semantics.Simulation.Semigroup.Base A using (C₂[_]; IsSemigroupC₂[_]; SemigroupC₂)
open import PiWare.Semantics.Simulation.Equality A using (_≅[_]_; ≅⇒≋)
\end{code}
......@@ -62,7 +62,7 @@ Op₂TyGate _⊕_ = const (Op₂W₂⟶W₁ _⊕_)
%<*Op2C>
\AgdaTarget{⊕C}
\begin{code}
⊕C : C₂ Op₂Gates
⊕C : C₂[ Op₂Gates ]
⊕C = Gate ⊕'
\end{code}
%</Op2C>
......@@ -83,7 +83,7 @@ module _ (_⊕_ : Op₂ Atom) where
%<*Op2IsSemigroupC2>
\AgdaTarget{Op₂IsSemigroupC₂}
\begin{code}
Op₂IsSemigroupC₂ : ⦃ sg : IsSemigroup (_≡_ {A = Atom}) _⊕_ ⦄ → IsSemigroupC₂ (Op₂TyGate _⊕_) ⊕C
Op₂IsSemigroupC₂ : ⦃ sg : IsSemigroup (_≡_ {A = Atom}) _⊕_ ⦄ → IsSemigroupC₂[ Op₂TyGate _⊕_ ] ⊕C
Op₂IsSemigroupC₂ ⦃ sg ⦄ = ≅⇒≋ (Op₂IsSemigroupC₂≅ ⦃ sg ⦄)
\end{code}
%</Op2IsSemigroupC2>
......
......@@ -10,7 +10,7 @@ open Atomic A using () renaming (finite to finiteAtom)
open import Data.HVec using (vec↑)
open import Data.Finite using (Finite; Finite-Vec)
open Finite using () renaming (from to fromFin)
open import PiWare.Circuit using (ℂ)
open import PiWare.Circuit using (ℂ[_])
open import PiWare.Circuit.Algebra using (TyGate)
open import PiWare.Semantics.Simulation A using (W⟶W) renaming (module WithGates to SimulationWithGates)
--open import PiWare.Semantics.Simulation.Compliance A using (∀-W; _⊑?[_]_at_; _⊑?[_]_) renaming (module WithGates to ComplianceWithGates)
......
......@@ -13,7 +13,7 @@ open import Data.Stream.Equality.WithTrans using (_≈ₚ_; _∷ₚ_; ≈ₚ-to-
open import Data.Product using (_×_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong-app; cong₂)
open import PiWare.Circuit using (ℂ; _∥_; _⟫_)
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; _∥ₛ_; _⟫ₛ_)
......@@ -33,7 +33,7 @@ mealy-cong {xs = x ∷ xs′} {.x ∷ ys′} (refl ∷ xs′≈ys′) = refl ∷
%<*⟦⟧ω'[–]-cong>
\AgdaTarget{⟦⟧ω'[–]-cong}
\begin{code}
⟦⟧ω'[–]-cong : ∀ {i o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i o) {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'[–]-cong : ∀ {i o s G} (g : TyGate G W⟶W) (c : ℂ[ G ] {s} i o) {xs ys} → xs ≈ ys → ⟦ c ⟧ω'[ g ] xs ≈ ⟦ c ⟧ω'[ g ] ys
⟦⟧ω'[–]-cong _ _ = mealy-cong
\end{code}
%</⟦⟧ω'[–]-cong>
......@@ -43,7 +43,7 @@ mealy-cong {xs = x ∷ xs′} {.x ∷ ys′} (refl ∷ xs′≈ys′) = refl ∷
%<*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⟦⟧ₛ[–]-⟫⇒∘ : ∀ {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}
......@@ -53,7 +53,7 @@ mealy⟦⟧ₛ[–]-⟫⇒∘ g c d {xs = _ ∷ _} = refl ∷ ♯ mealy⟦⟧ₛ
%<*⟦⟧ω'[–]-⟫⇒∘>
\AgdaTarget{⟦⟧ω'[–]-⟫⇒∘}
\begin{code}
⟦⟧ω'[–]-⟫⇒∘ : ∀ {i m o s G} (g : TyGate G W⟶W) (c : ℂ G {s} i m) (d : ℂ G {s} m o) {xs}
⟦⟧ω'[–]-⟫⇒∘ : ∀ {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}
......@@ -65,7 +65,7 @@ mealy⟦⟧ₛ[–]-⟫⇒∘ g c d {xs = _ ∷ _} = refl ∷ ♯ mealy⟦⟧ₛ
%<*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⟦⟧ₛ[–]-∥⇒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))
......@@ -79,7 +79,7 @@ mealy⟦⟧ₛ[–]-∥⇒zipWith++ₚ {m} g c d {cₛ} {dₛ} {_ ∷ xs}
%<*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⟦⟧ₛ[–]-∥⇒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}
......@@ -89,7 +89,7 @@ mealy⟦⟧ₛ[–]-∥⇒zipWith++ g c d = ≈ₚ-to-≈ (mealy⟦⟧ₛ[–]-
%<*⟦⟧ω'[–]-∥⇒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}
⟦⟧ω'[–]-∥⇒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}
......
......@@ -14,28 +14,28 @@ open Gates using (|in|; |out|)
open Atomic A using (Atom)
import PiWare.Circuit as Circuit
open Circuit using (ℂ; IsComb; Gate; Plug; DelayLoop; _⟫_; _∥_)
open Circuit using (ℂ[_]; IsComb; Gate; Plug; DelayLoop; _⟫_; _∥_)
open Circuit using (σ; ω) public
\end{code}
-- "High-level" circuit types, packing the synthesizable instances
%<*Circuit-typed>
\AgdaTarget{ℂ}
\AgdaTarget{ℂ̂[\_]}
\begin{code}
record ℂ̂ (G : Gates) {s : IsComb} (α β : Set) {i j : Ix} : Set where
record ℂ̂[_] (G : Gates) {s : IsComb} (α β : Set) {i j : Ix} : Set where
constructor Mkℂ̂
field ⦃ α̂ ⦄ : (α ⇕ Atom) {i}
⦃ β̂ ⦄ : (β ⇕ Atom) {j}
base : ℂ G {s} i j
base : ℂ[ G ] {s} i j
\end{code}
%</Circuit-typed>
%<*Circuit-any-typed>
\AgdaTarget{𝐂̂}
\AgdaTarget{Ĉ[\_]}
\begin{code}
Ĉ : (G : Gates) (α β : Set) {i j : Ix} → Set
G α β {i} {j} = ∀ {s} → ℂ̂ G {s} α β {i} {j}
[_] : (G : Gates) (α β : Set) {i j : Ix} → Set
[ G ] α β {i} {j} = ∀ {s} → ℂ̂[ G ] {s} α β {i} {j}
\end{code}
%</Circuit-any-typed>
......@@ -44,7 +44,7 @@ Ĉ G α β {i} {j} = ∀ {s} → ℂ̂ G {s} α β {i} {j}
%<*gateC>
\AgdaTarget{gateℂ̂}
\begin{code}
gateℂ̂ : ∀ {α β G} g ⦃ α̂ : (α ⇕ Atom) {|in| G g} ⦄ ⦃ β̂ : (β ⇕ Atom) {|out| G g} ⦄ → Ĉ G α β
gateℂ̂ : ∀ {α β G} g ⦃ α̂ : (α ⇕ Atom) {|in| G g} ⦄ ⦃ β̂ : (β ⇕ Atom) {|out| G g} ⦄ → Ĉ[ G ] α β
gateℂ̂ g ⦃ α̂ ⦄ ⦃ β̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Gate g)
\end{code}
%</gateC>
......@@ -53,7 +53,7 @@ gateℂ̂ g ⦃ α̂ ⦄ ⦃ β̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Gate
%<*plugC>
\AgdaTarget{plugℂ̂}
\begin{code}
plugℂ̂ : ∀ {α i β j G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ → i ⤪ j → Ĉ G α β {i} {j}
plugℂ̂ : ∀ {α i β j G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ → i ⤪ j → Ĉ[ G ] α β {i} {j}
plugℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ f = Mkℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Plug f)
\end{code}
%</plugC>
......@@ -63,7 +63,7 @@ plugℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ f = Mkℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Plug
\AgdaTarget{delayℂ̂}
\begin{code}
delayℂ̂ : ∀ {i j k α β γ G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ ⦃ γ̂ : (γ ⇕ Atom) {k} ⦄
→ ℂ̂ G {σ} (α × γ) (β × γ) {i + k} {j + k} → ℂ̂ G {ω} α β {i} {j}
→ ℂ̂[ G ] {σ} (α × γ) (β × γ) {i + k} {j + k} → ℂ̂[ G ] {ω} α β {i} {j}
delayℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Mkℂ̂ c) = Mkℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (DelayLoop c)
\end{code}
%</delayC>
......@@ -77,7 +77,7 @@ infixl 8 _⟫̂_
\AgdaTarget{\_⟫̂\_}
\begin{code}
_⟫̂_ : ∀ {i k j α γ β s G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ ⦃ γ̂ : (γ ⇕ Atom) {k} ⦄
→ ℂ̂ G {s} α γ {i} {k} → ℂ̂ G {s} γ β {k} {j} → ℂ̂ G {s} α β {i} {j}
→ ℂ̂[ G ] {s} α γ {i} {k} → ℂ̂[ G ] {s} γ β {k} {j} → ℂ̂[ G ] {s} α β {i} {j}
_⟫̂_ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Mkℂ̂ c) (Mkℂ̂ d) = Mkℂ̂ ⦃ α̂ ⦄ ⦃ β̂ ⦄ (c ⟫ d)
\end{code}
%</seq>
......@@ -91,7 +91,29 @@ infixr 9 _∥̂_
\AgdaTarget{\_∥̂\_}
\begin{code}
_∥̂_ : ∀ {i k j l α γ β δ s G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ γ̂ : (γ ⇕ Atom) {k} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ ⦃ δ̂ : (δ ⇕ Atom) {l} ⦄
→ ℂ̂ G {s} α γ {i} {k} → ℂ̂ G {s} β δ {j} {l} → ℂ̂ G {s} (α × β) (γ × δ) {i + j} {k + l}
→ ℂ̂[ G ] {s} α γ {i} {k} → ℂ̂[ G ] {s} β δ {j} {l} → ℂ̂[ G ] {s} (α × β) (γ × δ) {i + j} {k + l}
_∥̂_ ⦃ α̂ ⦄ ⦃ γ̂ ⦄ ⦃ β̂ ⦄ ⦃ δ̂ ⦄ (Mkℂ̂ c) (Mkℂ̂ d) = Mkℂ̂ ⦃ ⇕× ⦃ α̂ ⦄ ⦃ β̂ ⦄ ⦄ ⦃ ⇕× ⦃ γ̂ ⦄ ⦃ δ̂ ⦄ ⦄ (c ∥ d)
\end{code}
%</par>
\begin{code}
module WithGates (G : Gates) where
\end{code}
%<*Circuit-typed-with-gates>
\AgdaTarget{ℂ̂}
\begin{code}
ℂ̂ : {s : IsComb} (α β : Set) {i j : Ix} → Set
ℂ̂ {s} α β {i} {j} = ℂ̂[ G ] {s} α β {i} {j}
\end{code}
%</Circuit-typed>
%<*Circuit-any-typed-with-gates>
\AgdaTarget{Ĉ}
\begin{code}
Ĉ : (α β : Set) {i j : Ix} → Set
Ĉ α β {i} {j} = Ĉ[ G ] α β {i} {j}
\end{code}
%</Circuit-any-typed-with-gates>
......@@ -7,7 +7,7 @@ open import Data.Nat.Base using (ℕ; _*_)
open import Data.Vec using (Vec)
open import Data.Serializable using (_⇕_; ⇕Vec)
open import PiWare.Typed.Circuit A using (ℂ̂; Mkℂ̂)
open import PiWare.Typed.Circuit A using (ℂ̂[_]; Mkℂ̂)
open import PiWare.Patterns A using (parsN; seqsN)
open Atomic A using (Atom)
\end{code}
......@@ -16,7 +16,7 @@ open Atomic A using (Atom)
%<*parsN-typed>
\AgdaTarget{parsN̂}
\begin{code}
parsN̂ : ∀ {k i j α β s G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ → ℂ̂ G {s} α β {i} {j} → ℂ̂ G {s} (Vec α k) (Vec β k) {k * i} {k * j}
parsN̂ : ∀ {k i j α β s G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ → ℂ̂[ G ] {s} α β {i} {j} → ℂ̂[ G ] {s} (Vec α k) (Vec β k) {k * i} {k * j}
parsN̂ {k} {i} {j} {s = s} ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Mkℂ̂ c) = Mkℂ̂ ⦃ ⇕Vec ⦃ α̂ ⦄ ⦄ ⦃ ⇕Vec ⦃ β̂ ⦄ ⦄ (parsN {k} {i} {j} {s} c)
\end{code}
%</parsN-typed>
......@@ -25,7 +25,7 @@ parsN̂ {k} {i} {j} {s = s} ⦃ α̂ ⦄ ⦃ β̂ ⦄ (Mkℂ̂ c) = Mkℂ̂ ⦃
%<*seqsN-typed>
\AgdaTarget{seqsN̂}
\begin{code}
seqsN̂ : ∀ k {j α s G} ⦃ α̂ : (α ⇕ Atom) {j} ⦄ → ℂ̂ G {s} α α {j} {j} → ℂ̂ G {s} α α {j} {j}
seqsN̂ : ∀ k {j α s G} ⦃ α̂ : (α ⇕ Atom) {j} ⦄ → ℂ̂[ G ] {s} α α {j} {j} → ℂ̂[ G ] {s} α α {j} {j}
seqsN̂ k {s = s} ⦃ α̂ ⦄ (Mkℂ̂ c) = Mkℂ̂ ⦃ α̂ ⦄ ⦃ α̂ ⦄ (seqsN k {s} c)
\end{code}
%</seqsN-typed>
......@@ -14,7 +14,7 @@ open import Algebra.Operations (CommutativeSemiring.semiring ℕ-commSemiring) u
open import Data.Serializable using (_⇕_; ⇕×; ⇕Vec; ⇕⊤)
open Atomic A using (Atom)
open import PiWare.Gates using (Gates)
open import PiWare.Typed.Circuit A using (Ĉ; Mkℂ̂)
open import PiWare.Typed.Circuit A using (Ĉ[_]; Mkℂ̂)
open import PiWare.Plugs
using ( nil⤨; id⤨; id⤨₁; swap⤨; swap⤨₁; intertwine⤨; head⤨; vecHalf⤨; cons⤨; cons⤨₁
; nil⤨₀; vecHalfPow⤨; fst⤨; snd⤨; singleton⤨; forkVec⤨; fork×⤨; uncons⤨; uncons⤨₁ )
......@@ -24,7 +24,7 @@ open import PiWare.Plugs
%<*nil-plug-typed>
\AgdaTarget{nil⤨̂}
\begin{code}
nil⤨̂ : ∀ {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ G α ⊤
nil⤨̂ : ∀ {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ[ G ] α ⊤
nil⤨̂ ⦃ α̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ ⇕⊤ ⦄ nil⤨
\end{code}
%</nil-plug-typed>
......@@ -32,7 +32,7 @@ nil⤨̂ ⦃ α̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ ⇕⊤ ⦄ nil⤨
%<*nil-plug-typed-zero>
\AgdaTarget{nil⤨̂₀}
\begin{code}
nil⤨̂₀ : ∀ {G} → Ĉ G ⊤ ⊤
nil⤨̂₀ : ∀ {G} → Ĉ[ G ] ⊤ ⊤
nil⤨̂₀ = Mkℂ̂ ⦃ ⇕⊤ ⦄ ⦃ ⇕⊤ ⦄ nil⤨₀
\end{code}
%</nil-plug-typed-zero>
......@@ -41,7 +41,7 @@ nil⤨̂₀ = Mkℂ̂ ⦃ ⇕⊤ ⦄ ⦃ ⇕⊤ ⦄ nil⤨₀
%<*id-plug-typed>
\AgdaTarget{id⤨̂}
\begin{code}
id⤨̂ : ∀ {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ G α α
id⤨̂ : ∀ {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ[ G ] α α
id⤨̂ ⦃ α̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ α̂ ⦄ id⤨
\end{code}
%</id-plug-typed>
......@@ -49,7 +49,7 @@ id⤨̂ ⦃ α̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ α̂ ⦄ id⤨
%<*id-plug-typed-one>
\AgdaTarget{id⤨̂₁}
\begin{code}
id⤨̂₁ : ∀ {α G} ⦃ α̂ : (α ⇕ Atom) {1} ⦄ → Ĉ G α α
id⤨̂₁ : ∀ {α G} ⦃ α̂ : (α ⇕ Atom) {1} ⦄ → Ĉ[ G ] α α
id⤨̂₁ ⦃ α̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ α̂ ⦄ id⤨₁
\end{code}
%</id-plug-typed-one>
......@@ -58,7 +58,7 @@ id⤨̂₁ ⦃ α̂ ⦄ = Mkℂ̂ ⦃ α̂ ⦄ ⦃ α̂ ⦄ id⤨₁
%<*swap-plug-typed>
\AgdaTarget{swap⤨̂}
\begin{code}
swap⤨̂ : ∀ {i j α β G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ → Ĉ G (α × β) (β × α)
swap⤨̂ : ∀ {i j α β G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ → Ĉ[ G ] (α × β) (β × α)
swap⤨̂ {i} {j} ⦃ α̂ ⦄ ⦃ β̂ ⦄ = Mkℂ̂ ⦃ ⇕× ⦃ α̂ ⦄ ⦃ β̂ ⦄ ⦄ ⦃ ⇕× ⦃ β̂ ⦄ ⦃ α̂ ⦄ ⦄ (swap⤨ {i} {j})
\end{code}
%</swap-plug-typed>
......@@ -66,7 +66,7 @@ swap⤨̂ {i} {j} ⦃ α̂ ⦄ ⦃ β̂ ⦄ = Mkℂ̂ ⦃ ⇕× ⦃ α̂ ⦄ ⦃
%<*swap-plug-typed-one>
\AgdaTarget{swap⤨̂₁}
\begin{code}
swap⤨̂₁ : ∀ {α β G} ⦃ α̂ : (α ⇕ Atom) {1} ⦄ ⦃ β̂ : (β ⇕ Atom) {1} ⦄ → Ĉ G (α × β) (β × α)
swap⤨̂₁ : ∀ {α β G} ⦃ α̂ : (α ⇕ Atom) {1} ⦄ ⦃ β̂ : (β ⇕ Atom) {1} ⦄ → Ĉ[ G ] (α × β) (β × α)
swap⤨̂₁ ⦃ α̂ ⦄ ⦃ β̂ ⦄ = Mkℂ̂ ⦃ ⇕× ⦃ α̂ ⦄ ⦃ β̂ ⦄ ⦄ ⦃ ⇕× ⦃ β̂ ⦄ ⦃ α̂ ⦄ ⦄ swap⤨₁
\end{code}
%</swap-plug-typed-one>
......@@ -76,7 +76,7 @@ swap⤨̂₁ ⦃ α̂ ⦄ ⦃ β̂ ⦄ = Mkℂ̂ ⦃ ⇕× ⦃ α̂ ⦄ ⦃ β̂
\AgdaTarget{intertwine⤨̂}
\begin{code}
intertwine⤨̂ : ∀ {i j k l α β γ δ G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ ⦃ β̂ : (β ⇕ Atom) {j} ⦄ ⦃ γ̂ : (γ ⇕ Atom) {k} ⦄ ⦃ δ̂ : (δ ⇕ Atom) {l} ⦄
→ Ĉ G ((α × β) × (γ × δ)) ((α × γ) × (β × δ))
→ Ĉ[ G ] ((α × β) × (γ × δ)) ((α × γ) × (β × δ))
intertwine⤨̂ {i} {j} {k} {l} ⦃ α̂ ⦄ ⦃ β̂ ⦄ ⦃ γ̂ ⦄ ⦃ δ̂ ⦄ = Mkℂ̂ ⦃ ⇕× ⦃ ⇕× ⦃ α̂ ⦄ ⦃ β̂ ⦄ ⦄ ⦃ ⇕× ⦃ γ̂ ⦄ ⦃ δ̂ ⦄ ⦄ ⦄
⦃ ⇕× ⦃ ⇕× ⦃ α̂ ⦄ ⦃ γ̂ ⦄ ⦄ ⦃ ⇕× ⦃ β̂ ⦄ ⦃ δ̂ ⦄ ⦄ ⦄
(intertwine⤨ {i} {j} {k} {l})
......@@ -88,7 +88,7 @@ intertwine⤨̂ {i} {j} {k} {l} ⦃ α̂ ⦄ ⦃ β̂ ⦄ ⦃ γ̂ ⦄ ⦃ δ̂
%<*head-plug-typed>
\AgdaTarget{head⤨̂}
\begin{code}
head⤨̂ : ∀ n {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ G (Vec α (suc n)) α
head⤨̂ : ∀ n {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ[ G ] (Vec α (suc n)) α
head⤨̂ n {i} ⦃ α̂ ⦄ = Mkℂ̂ ⦃ ⇕Vec ⦃ α̂ ⦄ ⦄ ⦃ α̂ ⦄ (head⤨ n {i})
\end{code}
%</head-plug-typed>
......@@ -97,7 +97,7 @@ head⤨̂ n {i} ⦃ α̂ ⦄ = Mkℂ̂ ⦃ ⇕Vec ⦃ α̂ ⦄ ⦄ ⦃ α̂ ⦄
%<*uncons-plug-typed>
\AgdaTarget{uncons⤨̂}
\begin{code}
uncons⤨̂ : ∀ n {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ G (Vec α (suc n)) (α × Vec α n)
uncons⤨̂ : ∀ n {i α G} ⦃ α̂ : (α ⇕ Atom) {i} ⦄ → Ĉ[ G ] (Vec α (suc n)) (α × Vec α n)