Fix function names using '|' (pipe)

New agda version gave perse error
parent 700d635f
......@@ -24,8 +24,8 @@ open Finite ⦃ … ⦄
%<*from-product-view>
\AgdaTarget{from×′}
\begin{code}
from×′ : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} ⦃ fα : Finite α ⦄ ⦃ fβ : Finite β ⦄ {i : Fin (|α| ⦃ fα ⦄ * |α| ⦃ fβ ⦄)}
→ Fin* (|α| ⦃ fα ⦄) (|α| ⦃ fβ ⦄) i → α × β
from×′ : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} ⦃ fα : Finite α ⦄ ⦃ fβ : Finite β ⦄ {i : Fin (#α ⦃ fα ⦄ * #α ⦃ fβ ⦄)}
→ Fin* (#α ⦃ fα ⦄) (#α ⦃ fβ ⦄) i → α × β
from×′ ⦃ fα ⦄ ⦃ fβ ⦄ (is* ia ib) = from ia , from ib
\end{code}
%</from-product-view>
......@@ -35,8 +35,8 @@ from×′ ⦃ fα ⦄ ⦃ fβ ⦄ (is* ia ib) = from ia , from ib
\AgdaTarget{from×}
\begin{code}
from× : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} ⦃ fα : Finite α ⦄ ⦃ fβ : Finite β ⦄
→ Fin ((|α| ⦃ fα ⦄) * (|α| ⦃ fβ ⦄)) → α × β
from× ⦃ fα ⦄ ⦃ fβ ⦄ = from×′ ∘ ⨂ (|α| ⦃ fα ⦄) (|α| ⦃ fβ ⦄)
→ Fin ((#α ⦃ fα ⦄) * (#α ⦃ fβ ⦄)) → α × β
from× ⦃ fα ⦄ ⦃ fβ ⦄ = from×′ ∘ ⨂ (#α ⦃ fα ⦄) (#α ⦃ fβ ⦄)
\end{code}
%</from-product>
......@@ -44,7 +44,7 @@ from× ⦃ fα ⦄ ⦃ fβ ⦄ = from×′ ∘ ⨂ (|α| ⦃ fα ⦄) (|α| ⦃
%<*to-product>
\AgdaTarget{to×}
\begin{code}
to× : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} ⦃ fα : Finite α ⦄ ⦃ fβ : Finite β ⦄ → α × β → Fin ((|α| ⦃ fα ⦄) * (|α| ⦃ fβ ⦄))
to× : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} ⦃ fα : Finite α ⦄ ⦃ fβ : Finite β ⦄ → α × β → Fin ((#α ⦃ fα ⦄) * (#α ⦃ fβ ⦄))
to× (a , b) = to a *ₙ to b
\end{code}
%</to-product>
......@@ -63,7 +63,7 @@ postulate from×≡to×⁻¹ : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set
\AgdaTarget{Finite-×}
\begin{code}
Finite-× : ∀ {ℓ₁ ℓ₂} {α : Set ℓ₁} {β : Set ℓ₂} ⦃ fα : Finite α ⦄ ⦃ fβ : Finite β ⦄ → Finite (α × β)
Finite-× ⦃ fα ⦄ ⦃ fβ ⦄ = record { |α| = (|α| ⦃ fα ⦄) * (|α| ⦃ fβ ⦄)
Finite-× ⦃ fα ⦄ ⦃ fβ ⦄ = record { #α = (#α ⦃ fα ⦄) * (#α ⦃ fβ ⦄)
; mapping = record { to = to×
; from = from×
; inverse-of = from×≡to×⁻¹ } }
......@@ -76,7 +76,7 @@ Finite-× ⦃ fα ⦄ ⦃ fβ ⦄ = record { |α| = (|α| ⦃ fα ⦄) * (
%<*toVec>
\AgdaTarget{toVec}
\begin{code}
toVec : ∀ {n ℓ} {α : Set ℓ} ⦃ fα : Finite α ⦄ → Vec α n → Fin (|α| ⦃ fα ⦄ ^ n)
toVec : ∀ {n ℓ} {α : Set ℓ} ⦃ fα : Finite α ⦄ → Vec α n → Fin ( ⦃ fα ⦄ ^ n)
toVec [] = Fz
toVec ⦃ fα ⦄ (x ∷ xs) = to-Vec-ind
where postulate to-Vec-ind : _
......@@ -87,7 +87,7 @@ toVec ⦃ fα ⦄ (x ∷ xs) = to-Vec-ind
%<*fromVec>
\AgdaTarget{fromVec}
\begin{code}
postulate fromVec : ∀ {n ℓ} {α : Set ℓ} ⦃ fα : Finite α ⦄ → Fin (|α| ⦃ fα ⦄ ^ n) → Vec α n
postulate fromVec : ∀ {n ℓ} {α : Set ℓ} ⦃ fα : Finite α ⦄ → Fin ( ⦃ fα ⦄ ^ n) → Vec α n
\end{code}
%</fromVec>
......@@ -104,8 +104,8 @@ postulate fromVec≡toVec⁻¹ : ∀ {n ℓ} {α : Set ℓ} ⦃ fα : Finite α
\AgdaTarget{Finite-Vec}
\begin{code}
Finite-Vec : ∀ {n ℓ} {α : Set ℓ} ⦃ fα : Finite α ⦄ → Finite (Vec α n)
Finite-Vec {n} {_} {α} ⦃ fα ⦄ = record { |α| = |α| ⦃ fα ⦄ ^ n
; mapping = record { to = toVec
Finite-Vec {n} {_} {α} ⦃ fα ⦄ = record { #α = #α ⦃ fα ⦄ ^ n
; mapping = record { to = toVec
; from = fromVec
; inverse-of = fromVec≡toVec⁻¹ } }
\end{code}
......
......@@ -16,8 +16,8 @@ open import Data.Fin.Properties.Extra using (eq?ⁿ)
\AgdaTarget{Finite, |α|, mapping}
\begin{code}
record Finite {ℓ} (α : Set ℓ) : Set ℓ where
field |α| : ℕ
mapping : α ↔′ Fin |α|
field : ℕ
mapping : α ↔′ Fin
open Inverse′ mapping public
\end{code}
......
......@@ -76,7 +76,7 @@ instance
\AgdaTarget{Finite-Bool}
\begin{code}
Finite-Bool : Finite Bool
Finite-Bool = record { |α| = 2
Finite-Bool = record { = 2
; mapping = record { to = boolTo
; from = boolFrom
; inverse-of = boolFrom⇆boolTo } }
......
......@@ -20,8 +20,8 @@ record Atomic : Set₁ where
open FiniteNonEmpty enum public
|Atom| = |α|
Atom# = Fin |α|
|Atom| =
Atom# = Fin
decSetoidA : DecSetoid _ _
decSetoidA = decSetoid _≟A_
......
......@@ -6,7 +6,7 @@ open import Data.Nat.Base using (ℕ; _+_)
open import PiWare.Interface using (Ix)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Gates using (Gates)
open Gates using (|in|; |out|)
open Gates using (#in; #out)
\end{code}
......@@ -40,7 +40,7 @@ infixr 5 _∥_
\AgdaTarget{ℂ[\_], Gate, DelayLoop, Plug, \_⟫\_, \_∥\_}
\begin{code}
data ℂ[_] G where
Gate : ∀ g# → C[ G ] (|in| G g#) (|out| G g#)
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
......
......@@ -7,7 +7,7 @@ open import PiWare.Interface using (Ix)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Circuit using (ℂ[_]; σ; Gate; Plug; DelayLoop; _⟫_; _∥_)
open import PiWare.Gates using (Gates)
open Gates using (|in|; |out|)
open Gates using (#in; #out)
\end{code}
......@@ -15,7 +15,7 @@ open Gates using (|in|; |out|)
\AgdaTarget{TyGate}
\begin{code}
TyGate : (G : Gates) → (Ix → Ix → Set) → Set
TyGate G F = ∀ g# → F (|in| G g#) (|out| G g#)
TyGate G F = ∀ g# → F (#in G g#) (#out G g#)
\end{code}
%</combinator-type-gate>
......
......@@ -10,6 +10,6 @@ open import PiWare.Interface using (Ix)
\begin{code}
record Gates : Set₁ where
field Gate# : Set
|in| |out| : Gate# → Ix
#in #out : Gate# → Ix
\end{code}
%</Gates>
......@@ -17,14 +17,14 @@ data BoolTrioGate : Set where
%<*ins-outs>
\AgdaTarget{|in|, |out|}
\begin{code}
|in| |out| : BoolTrioGate → Ix
|out| _ = 1
#in #out : BoolTrioGate → Ix
#out _ = 1
|in| ⊥ℂ' = 0
|in| ⊤ℂ' = 0
|in| ¬ℂ' = 1
|in| ∧ℂ' = 2
|in| ∨ℂ' = 2
#in ⊥ℂ' = 0
#in ⊤ℂ' = 0
#in ¬ℂ' = 1
#in ∧ℂ' = 2
#in ∨ℂ' = 2
\end{code}
%</ins-outs>
......@@ -34,7 +34,7 @@ data BoolTrioGate : Set where
\begin{code}
BoolTrio : Gates
BoolTrio = record { Gate# = BoolTrioGate
; |in| = |in|
; |out| = |out| }
; #in = #in
; #out = #out }
\end{code}
%</BoolTrio>
......@@ -17,9 +17,9 @@ data NandGate : Set where ⊼ℂ' : NandGate
%<*ins-outs>
\AgdaTarget{|in|, |out|}
\begin{code}
|in| |out| : NandGate → Ix
|in| ⊼ℂ' = 2
|out| ⊼ℂ' = 1
#in #out : NandGate → Ix
#in ⊼ℂ' = 2
#out ⊼ℂ' = 1
\end{code}
%</ins-outs>
......@@ -29,7 +29,7 @@ data NandGate : Set where ⊼ℂ' : NandGate
\begin{code}
Nand : Gates
Nand = record { Gate# = NandGate
; |in| = |in|
; |out| = |out| }
; #in = #in
; #out = #out }
\end{code}
%</Nand>
......@@ -16,7 +16,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_; refl)
open import Relation.Nullary using (¬_)
open import PiWare.Gates using (Gates)
open Gates using (|in|; |out|)
open Gates using (#in; #out)
open import PiWare.Gates.BoolTrio using () renaming (BoolTrio to B₃)
open import PiWare.Plugs.Core using (_⤪_)
open import PiWare.Circuit using (C[_]; Gate; Plug; σ; ω)
......@@ -47,7 +47,7 @@ runᶜ′⟦⟧ᶜ⇒⟦⟧-Plug {g = g} eq {x⁰} (x¹ ∷ x²⁺) rewrite eq x
%<*runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate>
\AgdaTarget{runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate}
\begin{code}
runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| G h) (|out| G h)}
runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (#in G h) (#out G h)}
→ ⟦ Gate h ⟧[ g ] ≗ f → (∀ {x⁰ x⁻} x⁺ → runᶜ′ ⟦ Gate h ⟧ᶜ[ g ] (x⁰ ∷ x⁻) x⁺ ≈ₚ f x⁰ ∷ ♯ map f x⁺)
runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq {x⁰} (x¹ ∷ x²⁺) rewrite eq x⁰ = refl ∷ₚ ♯ transₚ (runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq (♭ x²⁺)) (refl ∷ₚ ♯ reflₚ)
\end{code}
......@@ -56,7 +56,7 @@ runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq {x⁰} (x¹ ∷ x²⁺) rewrite eq x
%<*⟦⟧ω⇒⟦⟧-Gate>
\AgdaTarget{⟦⟧ω⇒⟦⟧-Gate}
\begin{code}
⟦⟧ω⇒⟦⟧-Gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (|in| G h) (|out| G h)}
⟦⟧ω⇒⟦⟧-Gate : ∀ {G h} {g : TyGate G W⟶W} {f : W⟶W (#in G h) (#out G h)}
→ ⟦ Gate h ⟧[ g ] ≗ f → (∀ xs → ⟦ Gate h ⟧ω[ g ] xs ≈ map f xs)
⟦⟧ω⇒⟦⟧-Gate {g = g} eq (x⁰ ∷ x⁺) = ≈ₚ-to-≈ $ runᶜ′⟦⟧ᶜ⇒⟦⟧-Gate {g = g} eq (♭ x⁺) ⟨ transₚ ⟩ (refl ∷ₚ ♯ reflₚ)
\end{code}
......
......@@ -37,7 +37,7 @@ data ⊕Gate : Set where ⊕' : ⊕Gate
\AgdaTarget{Op₂Gates}
\begin{code}
Op₂Gates : Gates
Op₂Gates = record { Gate# = ⊕Gate; |in| = const 2; |out| = const 1 }
Op₂Gates = record { Gate# = ⊕Gate; #in = const 2; #out = const 1 }
\end{code}
%</Op2Gates>
......
......@@ -10,7 +10,7 @@ open import Data.Product using (_×_)
open import Data.Serializable using (_⇕_; ⇕×)
open import PiWare.Interface using (Ix)
open import PiWare.Plugs.Core using (_⤪_)
open Gates using (|in|; |out|)
open Gates using (#in; #out)
open Atomic A using (Atom)
import PiWare.Circuit as Circuit
......@@ -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>
......
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