1 | module Data.Graph.Util
3 | import Data.AssocList
5 | import Data.Graph.Types
8 | import Data.Prim.Bits32
17 | delNeighbour : Node -> Adj e n -> Adj e n
18 | delNeighbour n (MkAdj lbl ns) = MkAdj lbl (delete n ns)
20 | delEdgeTo : Node -> GraphRep e n -> (Node,e) -> GraphRep e n
21 | delEdgeTo n m (n2,_) = update n2 (delNeighbour n) m
23 | delNeighbours : Node -> GraphRep e n -> AssocList e -> GraphRep e n
24 | delNeighbours n g = foldlKV (delEdgeTo n) g
26 | addEdge : Node -> e -> Adj e n -> Adj e n
27 | addEdge k lbl (MkAdj l ns) = MkAdj l $
insert k lbl ns
29 | addEdgeTo : Node -> GraphRep e n -> (Node,e) -> GraphRep e n
30 | addEdgeTo k m (n2,lbl) = update n2 (addEdge k lbl) m
32 | addEdgesTo : Node -> GraphRep e n -> AssocList e -> GraphRep e n
33 | addEdgesTo n g = foldlKV (addEdgeTo n) g
35 | toContext : (Node,Adj e n) -> Context e n
36 | toContext (k,MkAdj l es) = MkContext k l es
38 | toLNode : (Node,Adj e n) -> LNode n
39 | toLNode (k,MkAdj l _) = MkLNode k l
43 | ctxtEdges : Context e n -> List (LEdge e)
44 | ctxtEdges (MkContext k _ ns) = go Nil (pairs ns)
47 | go : List (LEdge e) -> List (Node,e) -> List (LEdge e)
48 | go es Nil = reverse es
49 | go es ((j,lbl) :: t) = case comp j k of
50 | GT _ _ p => go (MkLEdge (MkEdge k j p) lbl :: es) t
63 | match : (node : Node) -> Graph e n -> Decomp e n
64 | match node (MkGraph g) = case lookup node g of
66 | Just (MkAdj lbl ns) =>
67 | let g1 := MkGraph $
delNeighbours node (delete node g) ns
68 | ctxt := MkContext node lbl ns
74 | matchAny : Graph e n -> Decomp e n
75 | matchAny (MkGraph g) = case decomp g of
77 | Match k (MkAdj lbl ns) m =>
78 | Split (MkContext k lbl ns) (MkGraph $
delNeighbours k m ns)
86 | isEmpty : Graph e n -> Bool
87 | isEmpty = isEmpty . graph
91 | contexts : Graph e n -> List (Context e n)
92 | contexts = map toContext . pairs . graph
96 | labNodes : Graph e n -> List (LNode n)
97 | labNodes = map toLNode . pairs . graph
101 | lab : Graph e n -> Node -> Maybe n
102 | lab (MkGraph m) v = label <$> lookup v m
106 | elab : Graph e n -> Node -> Node -> Maybe e
107 | elab (MkGraph g) k j = lookup k g >>= \(MkAdj _ ns) => lookup j ns
111 | nodes : Graph e n -> List Node
112 | nodes = map fst . pairs . graph
116 | gelem : Node -> Graph e n -> Bool
117 | gelem v = isJust . lookup v . graph
121 | order : Graph e n -> Nat
122 | order = length . labNodes
126 | labEdges : Graph e n -> List (LEdge e)
127 | labEdges = foldMap ctxtEdges . contexts
131 | edges : Graph e n -> List Edge
132 | edges = map edge . labEdges
136 | size : Graph e n -> Nat
137 | size = length . labEdges
141 | lneighbours : Graph e n -> Node -> List (Node,e)
142 | lneighbours (MkGraph g) k = case lookup k g of
143 | Just (MkAdj _ ns) => pairs ns
149 | neighbourLabels : Graph e n -> Node -> List (n,e)
150 | neighbourLabels g = mapMaybe (\(k,l) => (,l) <$> lab g k) . lneighbours g
154 | neighbours : Graph e n -> Node -> List Node
155 | neighbours g = map fst . lneighbours g
159 | deg : Graph e n -> Node -> Nat
160 | deg g = length . lneighbours g
164 | hasNeighbour : Graph e n -> Node -> Node -> Bool
165 | hasNeighbour g k = isJust . elab g k
169 | hasEdge : Graph e n -> Edge -> Bool
170 | hasEdge g (MkEdge k j _) = hasNeighbour g k j
174 | hasLEdge : Eq e => Graph e n -> LEdge e -> Bool
175 | hasLEdge g (MkLEdge (MkEdge k j _) le) = maybe False (le ==) $
elab g k j
189 | add : Context e n -> Graph e n -> Graph e n
190 | add (MkContext k lbl ns) (MkGraph m) =
191 | let m1 := insert k (MkAdj lbl ns) m
192 | in MkGraph $
addEdgesTo k m1 ns
196 | ufold : (Context e n -> c -> c) -> c -> Graph e n -> c
197 | ufold f acc g = case matchAny g of
198 | Split ctxt gr => f ctxt (ufold f acc $
assert_smaller g gr)
203 | gmap : (Context e1 n1 -> Context e2 n2) -> Graph e1 n1 -> Graph e2 n2
204 | gmap f = ufold (\c => add (f c)) (MkGraph empty)
210 | insNode : Node -> (lbl : n) -> Graph e n -> Graph e n
211 | insNode v l (MkGraph m) = MkGraph $
insert v (MkAdj l $
MkAL []) m
217 | insEdge : LEdge e -> Graph e n -> Graph e n
218 | insEdge (MkLEdge (MkEdge n1 n2 _) lbl) (MkGraph g) =
219 | let g1 := update n1 (addEdge n2 lbl) g
220 | in MkGraph $
update n2 (addEdge n1 lbl) g1
224 | insNodes : List (LNode n) -> Graph e n -> Graph e n
225 | insNodes vs g = foldl (\g2,(MkLNode k l) => insNode k l g2) g vs
229 | insEdges : List (LEdge e) -> Graph e n -> Graph e n
230 | insEdges es g = foldl (flip insEdge) g es
234 | delNode : Node -> Graph e n -> Graph e n
235 | delNode v g = case match v g of
241 | delNodes : List Node -> Graph e n -> Graph e n
242 | delNodes vs g = foldl (flip delNode) g vs
246 | delEdge : Edge -> Graph e n -> Graph e n
247 | delEdge (MkEdge i j _) g = case match i g of
248 | Split (MkContext n l ns) gr => add (MkContext n l (delete j ns)) gr
253 | delEdges : List Edge -> Graph e n -> Graph e n
254 | delEdges es g = foldl (flip delEdge) g es
259 | labnfilter : (LNode n -> Bool) -> Graph e n -> Graph e n
260 | labnfilter p gr = delNodes (map node . filter (not . p) $
labNodes gr) gr
265 | nfilter : (Node -> Bool) -> Graph e n -> Graph e n
266 | nfilter f = labnfilter (f . node)
271 | labfilter : (n -> Bool) -> Graph e n -> Graph e n
272 | labfilter f = labnfilter (f . label)
277 | pairWithNeighbours : Graph e n -> Graph e (n, List (n,e))
278 | pairWithNeighbours g =
279 | MkGraph $
mapWithKey (\k => map (,neighbourLabels g k)) (graph g)
284 | pairWithNeighbours' : Graph e n -> Graph e (n, List n)
285 | pairWithNeighbours' g =
286 | MkGraph $
mapWithKey (\k => map (,map fst $
neighbourLabels g k)) (graph g)
295 | empty = MkGraph empty
303 | mkGraph : List (LNode n) -> List (LEdge e) -> Graph e n
304 | mkGraph ns es = insEdges es (insNodes ns empty)
317 | Show e => Show n => Show (Graph e n) where
319 | showCon p "mkGraph" $
320 | showArg (labNodes g) ++ showArg (labEdges g)
322 | pl : Nat -> Node -> String
323 | pl n = padLeft n ' ' . show
327 | pretty : (e -> String) -> (n -> String) -> Graph e n -> String
328 | pretty de dn g = case matchAny g of
329 | Empty => "empty graph"
330 | Split (MkContext n _ _) _ =>
331 | let ns := sortBy (comparing node) $
labNodes g
332 | es := sortBy (comparing edge) $
labEdges g
333 | maxLen := length $
show n
335 | "Nodes:" :: map (dispNode maxLen) ns ++
336 | "\nEdges:" :: map (dispEdge maxLen) es
339 | dispNode : Nat -> LNode n -> String
340 | dispNode k (MkLNode n1 l) =
341 | #" \#{pl k n1} :> \#{dn l}"#
343 | dispEdge : Nat -> LEdge e -> String
344 | dispEdge k (MkLEdge (MkEdge n1 n2 _) l) =
345 | #" \#{pl k n1} <> \#{pl k n2} :> \#{de l}"#