diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/Circuit/Convert.agda | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda index ce6de69..8562e92 100644 --- a/Data/Circuit/Convert.agda +++ b/Data/Circuit/Convert.agda @@ -2,12 +2,14 @@ module Data.Circuit.Convert where +open import Level using (0ℓ) + open import Data.Nat.Base using (ℕ) -open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate) +open import Data.Circuit.Gate using (Gate; Gates; cast-gate; cast-gate-is-id; subst-is-cast-gate) open import Data.Fin.Base using (Fin) -open import Data.Hypergraph.Edge GateLabel using (Edge) -open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph) -open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph) +open import Data.Hypergraph.Edge Gates using (Edge) +open import Data.Hypergraph.Base {0ℓ} Gates using (Hypergraph; normalize; mkHypergraph) +open import Data.Hypergraph.Setoid {0ℓ} {0ℓ} Gates using (Hypergraphₛ; _≈_) open import Data.Permutation using (fromList-↭; toList-↭) open import Data.List using (length) open import Data.Vec.Functional using (toVec; fromVec; toList; fromList) @@ -21,7 +23,7 @@ open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_) import Function.Reasoning as →-Reasoning import Data.List.Relation.Binary.Permutation.Propositional as L import Data.Vec.Functional.Relation.Binary.Permutation as V -import DecorationFunctor.Hypergraph.Labeled as LabeledHypergraph +import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′) @@ -45,7 +47,7 @@ from {v} H = record asEdge : Fin h → Edge v asEdge e = record { label = l e ; ports = toVec (j e) } -to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′) +to-cong : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → Hypergraph-same (to H) (to H′) to-cong {v} {H} {H′} ≈H = record { ↔h = flip ρ ; ≗a = ≗a @@ -54,18 +56,18 @@ to-cong {v} {H} {H′} ≈H = record } where open Edge using (arity; ports; label) - open ≈-Hypergraph ≈H + open _≈_ ≈H open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ) open import Data.Fin.Base using (cast) open import Data.Fin.Properties using (cast-is-id) ρ : Fin (length H′.edges) ↔ Fin (length H.edges) - ρ = proj₁ (fromList-↭ ↭edges) + ρ = proj₁ (fromList-↭ ↭-edges) open ≡.≡-Reasoning edges≗ρ∘edges′ : (i : Fin (length H.edges)) → fromList H.edges i ≡ fromList H′.edges (ρ ⟨$⟩ˡ i) edges≗ρ∘edges′ i = begin fromList H.edges i ≡⟨ ≡.cong (fromList H.edges) (inverseʳ ρ) ⟨ - fromList H.edges (ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ i)) ≡⟨ proj₂ (fromList-↭ ↭edges) (ρ ⟨$⟩ˡ i) ⟩ + fromList H.edges (ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ i)) ≡⟨ proj₂ (fromList-↭ ↭-edges) (ρ ⟨$⟩ˡ i) ⟩ fromList H′.edges (ρ ⟨$⟩ˡ i) ∎ ≗a : (e : Fin (Hypergraph′.h (to H))) @@ -90,21 +92,21 @@ to-cong {v} {H} {H′} ≈H = record ≡.refl module _ {v : ℕ} where - open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡) + open import Data.Hypergraph.Edge Gates using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡) open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭) open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋) open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map) open import Data.Product.Base using (_,_) open import Data.Hypergraph.Label using (HypergraphLabel) - open HypergraphLabel GateLabel using (isCastable) + open HypergraphLabel Gates using (isCastable) open import Data.Castable using (IsCastable) open IsCastable isCastable using (≈-reflexive; ≈-sym; ≈-trans) from-cong : {H H′ : Hypergraph′ v} → Hypergraph-same H H′ - → ≈-Hypergraph (from H) (from H′) + → from H ≈ from H′ from-cong {H} {H′} ≈H = record - { ≡sorted = ≡sorted + { ≡-normalized = ≡-normalized } where module H = Hypergraph′ H @@ -182,17 +184,17 @@ module _ {v : ℕ} where open Hypergraph using (edges) open →-Reasoning - ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′) - ≡sorted = + ≡-normalized : normalize (from H) ≡ normalize (from H′) + ≡-normalized = flip ↔h , H∘ρ≗H′ ∶ asEdge H V.↭ asEdge H′ |> toList-↭ ∶ toList (asEdge H) L.↭ toList (asEdge H′) |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′)) |> sorted-≋ ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′))) |> map ≈-Edge⇒≡ ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′))) |> Pointwise-≡⇒≡ ∶ sort (edges (from H)) ≡ sort (edges (from H′)) - |> ≡.cong mkHypergraph ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′) + |> ≡.cong mkHypergraph ∶ normalize (from H) ≡ normalize (from H′) -equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v) +equiv : (v : ℕ) → Equivalence (Hypergraphₛ v) (Hypergraph-Setoid′ v) equiv v = record { to = to ; from = from |