Add new hypergraph definitions

2 files changed, 79 insertions, 0 deletions

diff --git a/Data/Castable.agda b/Data/Castable.agda
new file mode 100644
index 0000000..2c6932e
--- /dev/null
+++ b/Data/Castable.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Castable where
+
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; trans; subst)
+
+record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
+
+  field
+    cast : {e e′ : A} → .(e ≡ e′) → B e → B e′
+    cast-trans
+        : {m n o : A}
+        → .(eq₁ : m ≡ n)
+          .(eq₂ : n ≡ o)
+          (x : B m)
+        → cast eq₂ (cast eq₁ x) ≡ cast (trans eq₁ eq₂) x
+    cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x
+    subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x
+
+record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where
+  field
+    B : A → Set ℓ₂
+    isCastable : IsCastable B
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
new file mode 100644
index 0000000..a2157fb
--- /dev/null
+++ b/Data/Hypergraph/Base.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Hypergraph.Base where
+
+open import Data.Castable using (IsCastable)
+open import Data.Nat.Base using (ℕ)
+open import Data.Fin using (Fin)
+
+import Data.Vec.Base as VecBase
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Relation.Binary.PropositionalEquality as ≡
+
+open import Relation.Binary using (Rel; IsDecTotalOrder)
+open import Data.Nat.Base using (ℕ)
+open import Level using (Level; suc; _⊔_)
+
+record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+  field
+    Label : ℕ → Set ℓ
+    isCastable : IsCastable Label
+    _[_≈_] : (n : ℕ) → Rel (Label n) ℓ
+    _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+    decTotalOrder : (n : ℕ) → IsDecTotalOrder (n [_≈_]) (n [_≤_])
+  open IsCastable isCastable public
+
+module Edge (HL : HypergraphLabel) where
+
+  open HypergraphLabel HL using (Label; cast)
+  open VecBase using (Vec)
+
+  record Edge (v : ℕ) : Set where
+    field
+      {arity} : ℕ
+      label : Label arity
+      ports : Vec (Fin v) arity
+
+  open ≡ using (_≡_)
+  open VecCast using (_≈[_]_)
+
+  record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
+    module E = Edge E
+    module E′ = Edge E′
+    field
+      ≡arity : E.arity ≡ E′.arity
+      ≡label : cast ≡arity E.label ≡ E′.label
+      ≡ports : E.ports ≈[ ≡arity ] E′.ports
+
+module HypergraphList (HL : HypergraphLabel) where
+
+  open import Data.List.Base using (List)
+  open Edge HL using (Edge)
+
+  record Hypergraph (v : ℕ) : Set where
+    field
+      edges : List (Edge v)