Fixed parse errors with new version of Agda, work with Agda b63826d

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 (sz ⦃ fα ⦄ * sz ⦃ fβ ⦄)}
→ Fin* (sz ⦃ fα ⦄) (sz ⦃ 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 ((sz ⦃ fα ⦄) * (sz ⦃ fβ ⦄)) → α × β
from× ⦃ fα ⦄ ⦃ fβ ⦄ = from×′ ∘ ⨂ (sz ⦃ fα ⦄) (sz ⦃ 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 ((sz ⦃ fα ⦄) * (sz ⦃ 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 { sz = (sz ⦃ fα ⦄) * (sz ⦃ 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 (sz ⦃ 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 (sz ⦃ fα ⦄ ^ n) → Vec α n
\end{code}
%</fromVec>
......@@ -104,7 +104,7 @@ 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
Finite-Vec {n} {_} {α} ⦃ fα ⦄ = record { sz = sz ⦃ fα ⦄ ^ n
; mapping = record { to = toVec
; from = fromVec
; inverse-of = fromVec≡toVec⁻¹ } }
......
......@@ -13,11 +13,11 @@ open import Data.Fin.Properties.Extra using (eq?ⁿ)
%<*Finite>
\AgdaTarget{Finite, |α|, mapping}
\AgdaTarget{Finite, sz, mapping}
\begin{code}
record Finite {ℓ} (α : Set ℓ) : Set ℓ where
field |α| : ℕ
mapping : α ↔′ Fin |α|
field sz : ℕ
mapping : α ↔′ Fin sz
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 { sz = 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| = sz
Atom# = Fin sz
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 (szIn; szOut)
\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 ] (szIn G g#) (szOut 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 (szIn; szOut)
\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 (szIn G g#) (szOut G g#)
\end{code}
%</combinator-type-gate>
......
......@@ -6,10 +6,10 @@ open import PiWare.Interface using (Ix)
%<*Gates>
\AgdaTarget{Gates, |in|, |out|, Gate\#}
\AgdaTarget{Gates, szIn, szOut, Gate\#}
\begin{code}
record Gates : Set₁ where
field Gate# : Set
|in| |out| : Gate# → Ix
szIn szOut : Gate# → Ix
\end{code}
%</Gates>
......@@ -15,16 +15,16 @@ data BoolTrioGate : Set where
%</BoolTrioGate>
%<*ins-outs>
\AgdaTarget{|in|, |out|}
\AgdaTarget{szIn, szOut}
\begin{code}
|in| |out| : BoolTrioGate → Ix
|out| _ = 1
szIn szOut : BoolTrioGate → Ix
szOut _ = 1
|in| ⊥ℂ' = 0
|in| ⊤ℂ' = 0
|in| ¬ℂ' = 1
|in| ∧ℂ' = 2
|in| ∨ℂ' = 2
szIn ⊥ℂ' = 0
szIn ⊤ℂ' = 0
szIn ¬ℂ' = 1
szIn ∧ℂ' = 2
szIn ∨ℂ' = 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| }
; szIn = szIn
; szOut = szOut }
\end{code}
%</BoolTrio>
......@@ -15,11 +15,11 @@ data NandGate : Set where ⊼ℂ' : NandGate
%<*ins-outs>
\AgdaTarget{|in|, |out|}
\AgdaTarget{szIn, szOut}
\begin{code}
|in| |out| : NandGate → Ix
|in| ⊼ℂ' = 2
|out| ⊼ℂ' = 1
szIn szOut : NandGate → Ix
szIn ⊼ℂ' = 2
szOut ⊼ℂ' = 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| }
; szIn = szIn
; szOut = szOut }
\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 (szIn; szOut)
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 (szIn G h) (szOut 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 (szIn G h) (szOut 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; szIn = const 2; szOut = 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 (szIn; szOut)
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) {szIn G g} ⦄ ⦃ β̂ : (β ⇕ Atom) {szOut 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