Use functional vector in edge definition

1 files changed, 41 insertions, 31 deletions

diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 5c22a04..447f008 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -5,23 +5,24 @@ open import Data.Hypergraph.Label using (HypergraphLabel)
 open import Level using (Level; 0ℓ)
 module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where
 
-import Data.Vec as Vec
-import Data.Vec.Relation.Binary.Equality.Cast as VecCast
-import Relation.Binary.PropositionalEquality as ≡
+import Data.Vec.Functional as Vec
+import Data.Vec.Functional.Relation.Binary.Equality.Setoid as PW
+import Data.Fin.Properties as FinProp
 
-open import Data.Fin using (Fin)
+open import Data.Fin as Fin using (Fin)
 open import Data.Fin.Show using () renaming (show to showFin)
 open import Data.Nat using (ℕ)
 open import Data.String using (String; _<+>_)
 open import Data.Vec.Show using () renaming (show to showVec)
 open import Level using (0ℓ)
 open import Relation.Binary using (Setoid; IsEquivalence)
-open import Function using (_⟶ₛ_; Func)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
+open import Function using (_⟶ₛ_; Func; _∘_)
 
 module HL = HypergraphLabel HL
 
-open HL using (Label; cast; cast-is-id)
-open Vec using (Vec)
+open HL using (Label)
+open Vec using (Vector)
 open Func
 
 record Edge (v : ℕ) : Set ℓ where
@@ -29,7 +30,7 @@ record Edge (v : ℕ) : Set ℓ where
   field
     {arity} : ℕ
     label : Label arity
-    ports : Vec (Fin v) arity
+    ports : Fin arity → Fin v
 
 map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m
 map f edge = record
@@ -39,11 +40,10 @@ map f edge = record
   where
     open Edge edge
 
-open ≡ using (_≡_)
-open VecCast using (_≈[_]_)
-
 module _ {v : ℕ} where
 
+  open PW (≡.setoid (Fin v)) using (_≋_)
+
   -- an equivalence relation on edges with v nodes
   record _≈_ (E E′ : Edge v) : Set ℓ where
     constructor mk≈
@@ -51,34 +51,49 @@ module _ {v : ℕ} where
     module E′ = Edge E′
     field
       ≡arity : E.arity ≡ E′.arity
-      ≡label : cast ≡arity E.label ≡ E′.label
-      ≡ports : E.ports ≈[ ≡arity ] E′.ports
+      ≡label : HL.cast ≡arity E.label ≡ E′.label
+      ≡ports : E.ports ≋ E′.ports ∘ Fin.cast ≡arity
 
   ≈-refl : {x : Edge v} → x ≈ x
-  ≈-refl = record
+  ≈-refl {x} = record
       { ≡arity = ≡.refl
       ; ≡label = HL.≈-reflexive ≡.refl
-      ; ≡ports = VecCast.≈-reflexive ≡.refl
+      ; ≡ports = ≡.cong (Edge.ports x) ∘ ≡.sym ∘ FinProp.cast-is-id _
       }
 
   ≈-sym : {x y : Edge v} → x ≈ y → y ≈ x
   ≈-sym x≈y = record
       { ≡arity = ≡.sym ≡arity
       ; ≡label = HL.≈-sym ≡label
-      ; ≡ports = VecCast.≈-sym ≡ports
+      ; ≡ports = ≡.sym ∘ ≡ports-sym
       }
     where
       open _≈_ x≈y
-
-  ≈-trans : {i j k : Edge v} → i ≈ j → j ≈ k → i ≈ k
-  ≈-trans {i} {j} {k} i≈j j≈k = record
-      { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity
-      ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label
-      ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports
+      open ≡-Reasoning
+      ≡ports-sym : (i : Fin E′.arity) → E.ports (Fin.cast _ i) ≡ E′.ports i
+      ≡ports-sym i = begin
+          E.ports (Fin.cast _ i)                    ≡⟨ ≡ports (Fin.cast _ i) ⟩
+          E′.ports (Fin.cast ≡arity (Fin.cast _ i))
+            ≡⟨ ≡.cong E′.ports (FinProp.cast-involutive ≡arity _ i) ⟩
+          E′.ports i                                ∎
+
+  ≈-trans : {x y z : Edge v} → x ≈ y → y ≈ z → x ≈ z
+  ≈-trans {x} {y} {z} x≈y y≈z = record
+      { ≡arity = ≡.trans x≈y.≡arity y≈z.≡arity
+      ; ≡label = HL.≈-trans x≈y.≡label y≈z.≡label
+      ; ≡ports = ≡-ports
       }
     where
-      module i≈j = _≈_ i≈j
-      module j≈k = _≈_ j≈k
+      module x≈y = _≈_ x≈y
+      module y≈z = _≈_ y≈z
+      open ≡-Reasoning
+      ≡-ports : (i : Fin x≈y.E.arity) → x≈y.E.ports i ≡ y≈z.E′.ports (Fin.cast _ i)
+      ≡-ports i = begin
+          x≈y.E.ports i               ≡⟨ x≈y.≡ports i ⟩
+          y≈z.E.ports (Fin.cast _ i)  ≡⟨ y≈z.≡ports (Fin.cast _ i) ⟩
+          y≈z.E′.ports (Fin.cast y≈z.≡arity (Fin.cast _ i)) 
+            ≡⟨ ≡.cong y≈z.E′.ports (FinProp.cast-trans _ y≈z.≡arity i) ⟩
+          y≈z.E′.ports (Fin.cast _ i) ∎
 
   ≈-IsEquivalence : IsEquivalence _≈_
   ≈-IsEquivalence = record
@@ -88,16 +103,11 @@ module _ {v : ℕ} where
       }
 
   show : Edge v → String
-  show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin p
-
-  ≈⇒≡ : {x y : Edge v} → x ≈ y → x ≡ y
-  ≈⇒≡ {mkEdge l p} (mk≈ ≡.refl ≡.refl ≡.refl)
-    rewrite cast-is-id ≡.refl l
-    rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
+  show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin (Vec.toVec p)
 
 Edgeₛ : (v : ℕ) → Setoid ℓ ℓ
 Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} }
 
 mapₛ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
 mapₛ f .to = map f
-mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (VecCast.≈-cong′ (Vec.map f) ≡p)
+mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (≡.cong f ∘ ≡p)