diff options
| -rw-r--r-- | Data/Circuit.agda | 66 | ||||
| -rw-r--r-- | Data/Circuit/Gate.agda | 4 |
2 files changed, 68 insertions, 2 deletions
diff --git a/Data/Circuit.agda b/Data/Circuit.agda new file mode 100644 index 0000000..0be86f9 --- /dev/null +++ b/Data/Circuit.agda @@ -0,0 +1,66 @@ +{-# OPTIONS --without-K --safe #-} + +open import Level using (Level; _⊔_) + +module Data.Circuit {c ℓ : Level} where + +import Data.List as List + +open import Data.Circuit.Gate using (Gates) + +open import Data.Fin using (Fin) +open import Data.Hypergraph {c} {ℓ} Gates + using + ( Hypergraph + ; mkHypergraph + ; Hypergraphₛ + ; module Edge + ; normalize + ; _≈_ + ; mk≈ + ) +open import Data.Nat using (ℕ) +open import Relation.Binary using (Rel; Setoid) +open import Function.Bundles using (Func; _⟶ₛ_) + +open List using (List) +open Edge using (Edge; ≈-Edge⇒≡) + +Circuit : ℕ → Set c +Circuit = Hypergraph + +map : {n m : ℕ} → (Fin n → Fin m) → Circuit n → Circuit m +map f (mkHypergraph edges) = mkHypergraph (List.map (Edge.map f) edges) + +Circuitₛ : ℕ → Setoid c (c ⊔ ℓ) +Circuitₛ = Hypergraphₛ + +open Func +open Edge.Sort using (sort) + +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ′) +open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺) +open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise; Pointwise-≡⇒≡) +open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation) + +import Data.Permutation.Sort as ↭-Sort + +mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m +mapₛ {n} {m} f .to = map f +mapₛ {n} {m} f .cong {mkHypergraph xs} {mkHypergraph ys} x≈y = mk≈ ≡-norm + where + open _≈_ x≈y using (↭-edges) + open ↭-Sort (Edge.decTotalOrder {m}) using (sorted-≋) + open import Function.Reasoning + xs′ ys′ : List (Edge m) + xs′ = List.map (Edge.map f) xs + ys′ = List.map (Edge.map f) ys + ≡-norm : mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′) + ≡-norm = ↭-edges ∶ xs ↭ ys + |> map⁺ (Edge.map f) ∶ xs′ ↭ ys′ + |> ↭⇒↭ₛ′ Edge.≈-Edge-IsEquivalence ∶ Permutation Edge.≈-Edge xs′ ys′ + |> sorted-≋ ∶ Pointwise Edge.≈-Edge (sort xs′) (sort ys′) + |> PW.map ≈-Edge⇒≡ ∶ Pointwise _≡_ (sort xs′) (sort ys′) + |> Pointwise-≡⇒≡ ∶ sort xs′ ≡ sort ys′ + |> ≡.cong mkHypergraph ∶ mkHypergraph (sort xs′) ≡ mkHypergraph (sort ys′) diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda index 8ce7e0a..f4b55de 100644 --- a/Data/Circuit/Gate.agda +++ b/Data/Circuit/Gate.agda @@ -108,8 +108,8 @@ _≟_ {n} x y = Dec.map′ toℕ-injective (cong (toℕ n)) (toℕ n x Nat.≟ t _≤?_ : {n : ℕ} → Decidable (n [_≤_]) _≤?_ {n} x y = toℕ n x Nat.≤? toℕ n y -GateLabel : HypergraphLabel -GateLabel = record +Gates : HypergraphLabel +Gates = record { Label = Gate ; showLabel = showGate ; isCastable = record |