Commit 1d533191 authored by João Paulo Pizani Flor's avatar João Paulo Pizani Flor

Merge branch 'master' of gitlab.com:joaopizani/piware-agda

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