1 files changed, 197 insertions, 0 deletions
diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda
new file mode 100644
index 0000000..497b0cd
--- /dev/null
+++ b/Data/Circuit/Convert.agda
@@ -0,0 +1,197 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Convert where
+
+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.Fin.Base using (Fin)
+open import Function.Bundles using (Equivalence)
+open import Data.Hypergraph.Edge GateLabel using (Edge)
+open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph)
+open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph)
+open import Data.Permutation using (fromList-↭; toList-↭)
+open import Data.List using (length)
+open import Data.Vec.Functional using (toVec; fromVec; toList; fromList)
+open import Function.Base using (_∘_; id; _$_)
+
+import DecorationFunctor.Hypergraph.Labeled as LabeledHypergraph
+open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′)
+
+to : {v : ℕ} → Hypergraph v → Hypergraph′ v
+to H = record
+    { h = length edges
+    ; a = arity ∘ fromList edges
+    ; j = fromVec ∘ ports ∘ fromList edges
+    ; l = label ∘ fromList edges
+    }
+  where
+    open Edge using (arity; ports; label)
+    open Hypergraph H
+
+from : {v : ℕ} → Hypergraph′ v → Hypergraph v
+from {v} H = record
+    { edges = toList asEdge
+    }
+  where
+    open Hypergraph′ H
+    asEdge : Fin h → Edge v
+    asEdge e = record { label = l e ; ports = toVec (j e) }
+
+open import Data.Product.Base using (proj₁; proj₂)
+open import Data.Fin.Permutation using (flip)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′)
+to-cong {v} {H} {H′} ≈H = record
+    { ↔h = flip ρ
+    ; ≗a = ≗a
+    ; ≗j = ≗j
+    ; ≗l = ≗l
+    }
+  where
+    open Edge using (arity; ports; label)
+    open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_)
+    open import Function.Bundles using (_↔_)
+    open ≈-Hypergraph ≈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)
+
+    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)          ∎
+
+    ≗a : (e : Fin (Hypergraph′.h (to H)))
+        → Hypergraph′.a (to H) e
+        ≡ arity (fromList H′.edges (ρ ⟨$⟩ˡ e))
+    ≗a = ≡.cong arity ∘ edges≗ρ∘edges′
+
+    ≗j : (e : Fin (Hypergraph′.h (to H)))
+          (i : Fin (Hypergraph′.a (to H) e))
+        → fromVec (ports (fromList H.edges e)) i
+        ≡ fromVec (ports (fromList H′.edges (ρ ⟨$⟩ˡ e))) (cast (≗a e) i)
+    ≗j e i
+      rewrite edges≗ρ∘edges′ e
+      rewrite cast-is-id ≡.refl i = ≡.refl
+
+    ≗l : (e : Fin (Hypergraph′.h (to H)))
+        → label (fromList H.edges e)
+        ≡ cast-gate (≡.sym (≗a e)) (label (fromList H′.edges (ρ ⟨$⟩ˡ e)))
+    ≗l e
+      rewrite edges≗ρ∘edges′ e
+      rewrite cast-gate-is-id ≡.refl (label (fromList H′.edges (ρ ⟨$⟩ˡ e))) =
+          ≡.refl
+
+module _ {v : ℕ} where
+  open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-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.Permutation.Propositional using (_↭_)
+  open import Data.Vec.Functional.Relation.Binary.Permutation using () renaming (_↭_ to _↭′_)
+  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 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-cong {H} {H′} ≈H = record
+      { ≡sorted = ≡sorted
+      }
+    where
+      module H = Hypergraph′ H
+      module H′ = Hypergraph′ H′
+      open Hypergraph′
+      open Hypergraph-same ≈H using (↔h; ≗a; ≗l; ≗j; inverseˡ) renaming (from to f; to to t)
+      asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge v
+      asEdge H e = record { label = l H e ; ports = toVec (j H e) }
+
+      to-from : (e : Fin H′.h) → t (f e) ≡ e
+      to-from e = inverseˡ ≡.refl
+
+      a∘to-from : (e : Fin H′.h) → H′.a (t (f e)) ≡ H′.a e
+      a∘to-from = ≡.cong H′.a ∘ to-from
+
+      ≗a′ : (e : Fin H′.h) → H.a (f e) ≡ H′.a e
+      ≗a′ e = ≡.trans (≗a (f e)) (a∘to-from e)
+
+      l≗ : (e : Fin H.h) → cast-gate (≗a e) (H.l e) ≡ H′.l (t e)
+      l≗ e = ≈-sym (≡.sym (≗l e))
+
+      l∘to-from : (e : Fin H′.h) → cast-gate (a∘to-from e) (H′.l (t (f e))) ≡ H′.l e
+      l∘to-from e rewrite to-from e = ≈-reflexive ≡.refl
+
+      ≗l′ : (e : Fin H′.h) → cast-gate (≗a′ e) (H.l (f e)) ≡ H′.l e
+      ≗l′ e = ≈-trans {H.a _} (l≗ (f e)) (l∘to-from e)
+
+      import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+      open import Data.Vec using (cast) renaming (map to vecmap)
+      open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast)
+
+      open import Data.Fin.Base using () renaming (cast to fincast)
+      open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id)
+
+      j∘to-from
+          : (e : Fin H′.h) (i : Fin (H′.a (t (f e))))
+          → H′.j (t (f e)) i
+          ≡ H′.j e (fincast (a∘to-from e) i)
+      j∘to-from e i rewrite to-from e = ≡.cong (H′.j e) (≡.sym (fincast-is-id ≡.refl i))
+
+      open ≡.≡-Reasoning
+
+      ≗j′ : (e : Fin H′.h) (i : Fin (H.a (f e))) → H.j (f e) i ≡ H′.j e (fincast (≗a′ e) i)
+      ≗j′ e i = begin
+          H.j (f e) i                                   ≡⟨ ≗j (f e) i ⟩
+          H′.j (t (f e)) (fincast _ i)                  ≡⟨ j∘to-from e (fincast _ i) ⟩
+          H′.j e (fincast (a∘to-from e) (fincast _ i))  ≡⟨ ≡.cong (H′.j e) (fincast-trans (≗a (f e)) _ i) ⟩
+          H′.j e (fincast (≗a′ e) i)                    ∎
+
+      cast-toVec
+          : {n m : ℕ}
+            {A : Set}
+            (m≡n : m ≡ n)
+            (f : Fin n → A)
+          → cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f
+      cast-toVec m≡n f rewrite m≡n = begin
+          cast _ (toVec (f ∘ (fincast _)))  ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩
+          toVec (f ∘ fincast _)             ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩
+          vecmap f (toVec (fincast _))      ≡⟨ ≡.cong (vecmap f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩
+          vecmap f (toVec id)               ≡⟨ tabulate-∘ f id ⟨
+          toVec f                           ∎
+
+      ≗p′ : (e : Fin H′.h) → cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e)
+      ≗p′ e = begin
+          cast (≗a′ e) (toVec (H.j (f e)))    ≡⟨ ≡.cong (cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩
+          cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩
+          toVec (H′.j e)                      ∎
+
+      H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (flip ↔h Data.Fin.Permutation.⟨$⟩ʳ e) ≡ asEdge H′ e
+      H∘ρ≗H′ e = ≈-Edge⇒≡ record
+          { ≡arity = ≗a′ e
+          ; ≡label = ≗l′ e
+          ; ≡ports = ≗p′ e
+          }
+
+      ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′)
+      ≡sorted =
+          ≡.cong (λ x → record { edges = x } ) $
+          Pointwise-≡⇒≡ $
+          map ≈-Edge⇒≡ $
+          sorted-≋ $
+          toList-↭ $
+          flip ↔h , H∘ρ≗H′
+
+equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v)
+equiv v = record
+    { to = to
+    ; from = from
+    ; to-cong = to-cong
+    ; from-cong = from-cong
+    }