blob: 447f00829f8a3f7e8c7231abf19d227b7a64316a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
{-# OPTIONS --without-K --safe #-}
open import Data.Hypergraph.Label using (HypergraphLabel)
open import Level using (Level; 0ℓ)
module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where
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 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 Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning)
open import Function using (_⟶ₛ_; Func; _∘_)
module HL = HypergraphLabel HL
open HL using (Label)
open Vec using (Vector)
open Func
record Edge (v : ℕ) : Set ℓ where
constructor mkEdge
field
{arity} : ℕ
label : Label arity
ports : Fin arity → Fin v
map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m
map f edge = record
{ label = label
; ports = Vec.map f ports
}
where
open Edge edge
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≈
module E = Edge E
module E′ = Edge E′
field
≡arity : E.arity ≡ E′.arity
≡label : HL.cast ≡arity E.label ≡ E′.label
≡ports : E.ports ≋ E′.ports ∘ Fin.cast ≡arity
≈-refl : {x : Edge v} → x ≈ x
≈-refl {x} = record
{ ≡arity = ≡.refl
; ≡label = HL.≈-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 = ≡.sym ∘ ≡ports-sym
}
where
open _≈_ x≈y
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 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
{ refl = ≈-refl
; sym = ≈-sym
; trans = ≈-trans
}
show : Edge v → String
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 (≡.cong f ∘ ≡p)
|
