Refactor list-based hypergraphs

4 files changed, 91 insertions, 57 deletions

diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
new file mode 100644
index 0000000..2e8498c
--- /dev/null
+++ b/Data/Hypergraph.agda
@@ -0,0 +1,14 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Base {c} HL public
+open import Data.Hypergraph.Setoid {c} {ℓ} HL public
+
+import Data.Hypergraph.Edge HL as HypergraphEdge
+
+module Edge = HypergraphEdge
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
index 6988cf0..0910e02 100644
--- a/Data/Hypergraph/Base.agda
+++ b/Data/Hypergraph/Base.agda
@@ -1,26 +1,25 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Level using (Level)
 open import Data.Hypergraph.Label using (HypergraphLabel)
 
-module Data.Hypergraph.Base (HL : HypergraphLabel) where
+module Data.Hypergraph.Base {ℓ : Level} (HL : HypergraphLabel) where
 
-open import Data.Hypergraph.Edge HL using (Edge; decTotalOrder; showEdge)
-open import Data.List.Base using (List; map)
+import Data.Hypergraph.Edge HL as Edge
+
+open import Data.List using (List; map)
 open import Data.Nat.Base using (ℕ)
 open import Data.String using (String; unlines)
 
-import Data.List.Sort as Sort
+open Edge using (Edge)
 
-record Hypergraph (v : ℕ) : Set where
+record Hypergraph (v : ℕ) : Set ℓ where
   constructor mkHypergraph
   field
     edges : List (Edge v)
 
-sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
-sortHypergraph {v} H = record { edges = sort edges }
-  where
-    open Hypergraph H
-    open Sort decTotalOrder using (sort)
+normalize : {v : ℕ} → Hypergraph v → Hypergraph v
+normalize (mkHypergraph e) = mkHypergraph (Edge.sort e)
 
-showHypergraph : {v : ℕ} → Hypergraph v → String
-showHypergraph record { edges = e} = unlines (map showEdge e)
+show : {v : ℕ} → Hypergraph v → String
+show (mkHypergraph e) = unlines (map Edge.show e)
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 13b9278..7d0fa7c 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -4,12 +4,21 @@ open import Data.Hypergraph.Label using (HypergraphLabel)
 
 module Data.Hypergraph.Edge (HL : HypergraphLabel) where
 
+import Data.List.Sort as ListSort
+import Data.Fin as Fin
+import Data.Fin.Properties as FinProp
+import Data.Vec as Vec
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Data.Vec.Relation.Binary.Lex.Strict as Lex
+import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Properties.DecTotalOrder as DTOP
+import Relation.Binary.Properties.StrictTotalOrder as STOP
 
 open import Relation.Binary using (Rel; IsStrictTotalOrder; Tri; Trichotomous; _Respects_)
 open import Data.Castable using (IsCastable)
 open import Data.Fin using (Fin)
 open import Data.Fin.Show using () renaming (show to showFin)
-open import Data.Nat.Base using (ℕ; _<_)
+open import Data.Nat using (ℕ; _<_)
 open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Data.String using (String; _<+>_)
@@ -20,18 +29,10 @@ open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Nullary using (¬_)
 
-import Data.Fin.Base as Fin
-import Data.Fin.Properties as FinProp
-import Data.Vec.Base as VecBase
-import Data.Vec.Relation.Binary.Equality.Cast as VecCast
-import Data.Vec.Relation.Binary.Lex.Strict as Lex
-import Relation.Binary.PropositionalEquality as ≡
-import Relation.Binary.Properties.DecTotalOrder as DTOP
-import Relation.Binary.Properties.StrictTotalOrder as STOP
 
 module HL = HypergraphLabel HL
 open HL using (Label; cast; cast-is-id)
-open VecBase using (Vec)
+open Vec using (Vec)
 
 record Edge (v : ℕ) : Set where
   field
@@ -39,6 +40,14 @@ record Edge (v : ℕ) : Set where
     label : Label arity
     ports : Vec (Fin v) arity
 
+map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m
+map {n} {m} f edge = record
+    { label = label
+    ; ports = Vec.map f ports
+    }
+  where
+    open Edge edge
+
 open ≡ using (_≡_)
 open VecCast using (_≈[_]_)
 
@@ -105,7 +114,7 @@ data <-Edge {v : ℕ} : Edge v → Edge v → Set where
       : {x y : Edge v}
         (≡a : Edge.arity x ≡ Edge.arity y)
         (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y)
-      → VecBase.cast ≡a (Edge.ports x) << Edge.ports y
+      → Vec.cast ≡a (Edge.ports x) << Edge.ports y
       → <-Edge x y
 
 <-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y
@@ -324,8 +333,8 @@ strictTotalOrder {v} = record
     ; isStrictTotalOrder = isStrictTotalOrder {v}
     }
 
-showEdge : {v : ℕ} → Edge v → String
-showEdge record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p
+show : {v : ℕ} → Edge v → String
+show record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p
 
 open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public
 
@@ -333,3 +342,6 @@ open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) publ
 ≈-Edge⇒≡ {v} {record { label = l ; ports = p }} record { ≡arity = ≡.refl ; ≡label = ≡.refl ; ≡ports = ≡.refl }
   rewrite cast-is-id ≡.refl l
   rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
+
+module Sort {v} = ListSort (decTotalOrder {v})
+open Sort using (sort) public
diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda
index c39977d..d9cc024 100644
--- a/Data/Hypergraph/Setoid.agda
+++ b/Data/Hypergraph/Setoid.agda
@@ -1,47 +1,56 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Level using (Level; _⊔_)
 open import Data.Hypergraph.Label using (HypergraphLabel)
 
-module Data.Hypergraph.Setoid (HL : HypergraphLabel) where
+module Data.Hypergraph.Setoid {c ℓ : Level} (HL : HypergraphLabel) where
 
-open import Data.Hypergraph.Edge HL using (decTotalOrder)
-open import Data.Hypergraph.Base HL using (Hypergraph; sortHypergraph)
-open import Data.Nat.Base using (ℕ)
-open import Level using (0ℓ)
-open import Relation.Binary.Bundles using (Setoid)
+import Data.List.Relation.Binary.Permutation.Propositional as List-↭
+
+open import Data.Hypergraph.Edge HL using (module Sort)
+open import Data.Hypergraph.Base {c} HL using (Hypergraph; normalize)
+open import Data.Nat using (ℕ)
+open import Relation.Binary using (Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
-record ≈-Hypergraph {v : ℕ} (H H′ : Hypergraph v) : Set where
+-- an equivalence relation on hypergraphs
+record _≈_ {v : ℕ} (H H′ : Hypergraph v) : Set (c ⊔ ℓ) where
+
+  constructor mk≈
+
   module H = Hypergraph H
   module H′ = Hypergraph H′
+
   field
-    ≡sorted : sortHypergraph H ≡ sortHypergraph H′
+    ≡-normalized : normalize H ≡ normalize H′
+
   open Hypergraph using (edges)
-  ≡edges : edges (sortHypergraph H) ≡ edges (sortHypergraph H′)
-  ≡edges = ≡.cong edges ≡sorted
-  open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
-  open import Data.List.Sort decTotalOrder using (sort-↭)
-  ↭edges : H.edges ↭ H′.edges
-  ↭edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡edges) (sort-↭ H′.edges))
-
-≈-refl : {v : ℕ} {H : Hypergraph v} → ≈-Hypergraph H H
-≈-refl = record { ≡sorted = ≡.refl }
-
-≈-sym : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H
-≈-sym ≈H = record { ≡sorted = ≡.sym ≡sorted }
-  where
-    open ≈-Hypergraph ≈H 
-
-≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H″ → ≈-Hypergraph H H″
-≈-trans ≈H₁ ≈H₂ = record { ≡sorted = ≡.trans ≈H₁.≡sorted ≈H₂.≡sorted }
-  where
-    module ≈H₁ = ≈-Hypergraph ≈H₁
-    module ≈H₂ = ≈-Hypergraph ≈H₂
-
-Hypergraph-Setoid : (v : ℕ) → Setoid 0ℓ 0ℓ
-Hypergraph-Setoid v = record
+
+  ≡-edges : edges (normalize H) ≡ edges (normalize H′)
+  ≡-edges = ≡.cong edges ≡-normalized
+
+  open List-↭ using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
+  open Sort using (sort-↭)
+
+  ↭-edges : H.edges ↭ H′.edges
+  ↭-edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡-edges) (sort-↭ H′.edges))
+
+infixr 4 _≈_
+
+≈-refl : {v : ℕ} {H : Hypergraph v} → H ≈ H
+≈-refl = mk≈ ≡.refl
+
+≈-sym : {v : ℕ} {H H′ : Hypergraph v} → H ≈ H′ → H′ ≈ H
+≈-sym (mk≈ ≡n) = mk≈ (≡.sym ≡n)
+
+≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → H ≈ H′ → H′ ≈ H″ → H ≈ H″
+≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (≡.trans ≡n₁ ≡n₂)
+
+-- The setoid of labeled hypergraphs with v nodes
+Hypergraphₛ : ℕ → Setoid c (c ⊔ ℓ)
+Hypergraphₛ v = record
     { Carrier = Hypergraph v
-    ; _≈_ = ≈-Hypergraph
+    ; _≈_ = _≈_
     ; isEquivalence = record
         { refl = ≈-refl
         ; sym = ≈-sym