0 | module Data.Graph.Indexed.Util

  2 | import Data.Array

  3 | import Data.Array.Index

  4 | import Data.Array.Mutable

  5 | import Data.AssocList.Indexed

  6 | import Data.Graph.Indexed.Types

  7 | import Data.Linear.Traverse1

  8 | import Data.List

  9 | import Data.SortedMap

 10 | import Data.SortedSet

 11 | import Data.String

 12 | import Data.Vect

 14 | %default total

 21 | export %inline

 22 | lupdNodes : {k : _} -> MArray s k (Adj k e n) -> (n -> n) -> F1' s

 23 | lupdNodes r f = mupdate {label $= f} r

 25 | parameters (r : MArray s k (Adj k e n))

 27 |   ||| Updates the node label at the given position in a mutable graph.

 28 |   export %inline

 29 |   lupdNode : (n1 : Fin k) -> (n -> n) -> F1' s

 30 |   lupdNode n1 f = modify r n1 {label $= f}

 32 |   ||| Sets the node label at the given position in a mutable graph.

 33 |   export %inline

 34 |   lsetNode : (n1 : Fin k) -> n -> F1' s

 35 |   lsetNode n1 v = modify r n1 {label := v}

 37 |   ||| Insert a single edge into a mutable array-representation of a graph.

 38 |   export

 39 |   linsEdge : Edge k e ->F1' s

 40 |   linsEdge (E n1 n2 el) t =

 41 |     let _ # t := modify r n1 {neighbours $= insert n2 el} t

 42 |      in modify r n2 {neighbours $= insert n1 el} t

 44 |   ||| Delete a single edge from a mutable array-representation of a graph.

 45 |   export

 46 |   ldelEdge : (n1, n2 : Fin k) -> F1' s

 47 |   ldelEdge n1 n2 t =

 48 |     let _ # t := modify r n1 {neighbours $= delete n2} t

 49 |      in modify r n2 {neighbours $= delete n1} t

 51 |   ||| Insert a bunch of edges into a mutable array-representation of a graph.

 52 |   export %inline

 53 |   linsEdges : List (Edge k e) -> F1' s

 54 |   linsEdges = traverse1_ linsEdge

 56 |   ||| Insert a bunch of edges into a mutable array-representation of a graph.

 57 |   export %inline

 58 |   ldelEdges : List (Fin k, Fin k) -> F1' s

 59 |   ldelEdges = traverse1_ (\(x,y) => ldelEdge x y)

 63 | ctxtEdges : Fin k -> Adj k e n -> SnocList (Edge k e)

 64 | ctxtEdges x (A _ ns) = foldlKV acc [<] ns

 66 |   where

 67 |     acc : Fin k -> SnocList (Edge k e) -> e -> SnocList (Edge k e)

 68 |     acc y sp v with (compare x y) proof eq

 69 |       _ | LT = sp :< E x y v

 70 |       _ | _  = sp

 78 | contexts : {k : _} -> IGraph k e n -> List (Context k e n)

 79 | contexts = foldrKV (\x,(A l ns),cs => C x l ns :: cs) [] . graph

 82 | export %inline

 83 | nodes : {k : _} -> (0 _ : IGraph k e n) -> List (Fin k)

 84 | nodes _ = allFinsFast k

 88 | labNodes  : {k : _} -> IGraph k e n -> List (Fin k, n)

 89 | labNodes = foldrKV (\x,(A l _),cs => (x,l) :: cs) [] . graph

 93 | labels  : {k : _} -> IGraph k e n -> List n

 94 | labels = foldr (\(A l _) => (l ::)) [] . graph

 98 | export %inline

 99 | adj : IGraph k e n -> Fin k -> Adj k e n

100 | adj (IG g) k = at g k

103 | export %inline

104 | lab : IGraph k e n -> Fin k -> n

105 | lab g = label . adj g

109 | export %inline

110 | neighboursAsAL : IGraph k e n -> Fin k -> AssocList k e

111 | neighboursAsAL g = neighbours . adj g

115 | export %inline

116 | neighboursAsPairs : IGraph k e n -> Fin k -> List (Fin k, e)

117 | neighboursAsPairs g = pairs . neighboursAsAL g

120 | export %inline

121 | neighbours : IGraph k e n -> Fin k -> List (Fin k)

122 | neighbours g = keys . neighboursAsAL g

125 | export %inline

126 | edgesTo : IGraph k e n -> Fin k -> List (Edge k e)

127 | edgesTo g k =

128 |   let A _ ns := adj g k

129 |    in mapMaybe (\(n,l) => mkEdge k n l) $ pairs ns

134 | lneighbours : IGraph k e n -> Fin k -> List (Fin k, n)

135 | lneighbours g = map (\x => (x, lab g x)) . neighbours g

140 | lneighboursAsAL : IGraph k e n -> Fin k -> AssocList k (e, n)

141 | lneighboursAsAL g = mapKV (\x => (, lab g x)) . neighboursAsAL g

145 | neighbourLabels : IGraph k e n -> Fin k -> List n

146 | neighbourLabels g = map (lab g) . neighbours g

149 | export %inline

150 | edgeLabels : IGraph k e n -> Fin k -> List e

151 | edgeLabels g = values . neighbours . adj g

155 | elab : IGraph k e n -> Fin k -> Fin k -> Maybe e

156 | elab (IG g) x y = lookup y . neighbours $ at g x

160 | edge : IGraph k e n -> Fin k -> Fin k -> Maybe (Edge k e)

161 | edge g x y = elab g x y >>= mkEdge x y

165 | adjacent : IGraph k e n -> Fin k -> Fin k -> Bool

166 | adjacent g x y = isJust $ elab g x y

170 | edges  : {k : _} -> IGraph k e n -> List (Edge k e)

171 | edges (IG g) = foldrKV (\x,adj,es => ctxtEdges x adj <>> es) [] g

175 | size : {k : _} -> IGraph k e n -> Nat

176 | size = length . edges

180 | deg : IGraph k e n -> Fin k -> Nat

181 | deg g = length . neighbours g

185 | hasNeighbour : IGraph k e n -> Fin k -> Fin k -> Bool

186 | hasNeighbour g k = isJust . elab g k

194 | empty : IGraph 0 e n

195 | empty = IG empty

197 | 0 mapLen : (f : a -> b) -> (as : List a) -> length (map f as) === length as

198 | mapLen f []        = Refl

199 | mapLen f (x :: xs) = cong S $ mapLen f xs

203 | mkGraphL : (ns : List n) -> List (Edge (length ns) e) -> IGraph (length ns) e n

204 | mkGraphL ns es =

205 |   IG $ allocListWith ns (`A` empty) $ \r,t =>

206 |     let _ # t := linsEdges r es t

207 |      in unsafeFreeze r t

211 | mkGraph : {k : _} -> (ns : Vect k n) -> List (Edge k e) -> IGraph k e n

212 | mkGraph ns es =

213 |   IG $ allocVect (map (`A` empty) ns) $ \r,t =>

214 |     let _ # t := linsEdges r es t

215 |      in unsafeFreeze r t

223 | mkGraphRev : {k : _} -> (ns : Vect k n) -> List (Edge k e) -> IGraph k e n

224 | mkGraphRev ns es =

225 |  IG $ allocVectRev (map (`A` empty) ns) $ \r,t =>

226 |    let _ # t := linsEdges r es t

227 |     in unsafeFreeze r t

229 | export %inline

230 | generate : (k : Nat) -> (Fin k -> Adj k e n) -> IGraph k e n

231 | generate k f = IG $ generate k f

238 | export %inline

239 | mapCtxt :

240 |      {k : _}

241 |   -> (Fin k -> Adj k e n -> Adj k e1 n1)

242 |   -> IGraph k e n

243 |   -> IGraph k e1 n1

244 | mapCtxt fun (IG g) = IG $ mapWithIndex fun g

247 | export %inline

248 | mapWithCtxt :

249 |      {k : _}

250 |   -> (Fin k -> Adj k e n -> n1)

251 |   -> IGraph k e n

252 |   -> IGraph k e n1

253 | mapWithCtxt fun = mapCtxt (\x,adj => adj $> fun x adj)

256 | export %inline

257 | mapAdj : {k : _} -> (Adj k e n -> Adj k f m) -> IGraph k e n -> IGraph k f m

258 | mapAdj fun (IG g) = IG $ map fun g

261 | export %inline

262 | mapWithAdj : {k : _} -> (Adj k e n -> m) -> IGraph k e n -> IGraph k e m

263 | mapWithAdj fun = mapAdj (\adj => adj $> fun adj)

266 | traverseCtxt :

267 |      {k : _}

268 |   -> {auto app : Applicative f}

269 |   -> (Fin k -> Adj k e n -> f (Adj k e1 n1))

270 |   -> IGraph k e n

271 |   -> f (IGraph k e1 n1)

272 | traverseCtxt fun (IG g) = IG <$> traverseWithIndex fun g

275 | traverseWithCtxt :

276 |      {k : _}

277 |   -> {auto app : Applicative f}

278 |   -> (Fin k -> Adj k e n -> f n1)

279 |   -> IGraph k e n

280 |   -> f (IGraph k e n1)

281 | traverseWithCtxt fun = traverseCtxt (\x,a => (`A` a.neighbours) <$> fun x a)

291 | updateNodes : {k : _} -> Fin k -> (f,g : m -> n) -> IGraph k e m -> IGraph k e n

292 | updateNodes x f g = mapWithCtxt (\y,a => if x == y then f a.label else g a.label)

295 | export %inline

296 | updateNode : {k : _} -> Fin k -> (n -> n) -> IGraph k e n -> IGraph k e n

297 | updateNode x f = updateNodes x f id

300 | export %inline

301 | setNode : {k : _} -> Fin k -> n -> IGraph k e n -> IGraph k e n

302 | setNode x = updateNode x . const

309 | updateEdges :

310 |      {k : _}

311 |   -> (x,y : Fin k)

312 |   -> (f,g : e -> e2)

313 |   -> IGraph k e n

314 |   -> IGraph k e2 n

315 | updateEdges x y f g =

316 |   mapCtxt $ \k,(A l a) =>

317 |    A l $

318 |      if      k == x then mapKV (\m,l => if m == y then f l else g l) a

319 |      else if k == y then mapKV (\m,l => if m == x then f l else g l) a

320 |      else    map g a

323 | export %inline

324 | updateEdge :

325 |      {k : _}

326 |   -> (x,y : Fin k)

327 |   -> (f : e -> e)

328 |   -> IGraph k e n

329 |   -> IGraph k e n

330 | updateEdge x y f = updateEdges x y f id

334 | insEdges : {k : _} -> List (Edge k e) -> IGraph k e n -> IGraph k e n

335 | insEdges es g =

336 |   IG $ allocGen k (adj g) $ \r,t =>

337 |     let _ # t := linsEdges r es t

338 |      in unsafeFreeze r t

341 | export %inline

342 | insEdge : {k : _} -> Edge k e -> IGraph k e n -> IGraph k e n

343 | insEdge = insEdges . pure

347 | delEdges : {k : _} -> List (Fin k, Fin k) -> IGraph k e n -> IGraph k e n

348 | delEdges ps g = IG $ allocGen k (adj g) $ \r,t =>

349 |   let _ # t := ldelEdges r ps t

350 |    in unsafeFreeze r t

353 | export %inline

354 | delEdge : {k : _} -> (x,y : Fin k) -> IGraph k e n -> IGraph k e n

355 | delEdge x y = delEdges [(x,y)]

359 | insNodes : {k,m : _} -> IGraph k e n -> (ns : Vect m n) -> IGraph (k + m) e n

360 | insNodes (IG g) ns =

361 |   let g'  := map (weakenAdjN m) g

362 |    in IG $ append g' (map fromLabel (array ns))

366 | insNodesAndEdges :

367 |      {k,m : _}

368 |   -> IGraph k e n

369 |   -> (ns : Vect m n)

370 |   -> (es : List (Edge (k + m) e))

371 |   -> IGraph (k + m) e n

372 | insNodesAndEdges g ns es = insEdges es $ insNodes g ns

377 | export %inline

378 | insNode : {k : _} -> IGraph k e n -> n -> IGraph (S k) e n

379 | insNode g v = rewrite plusCommutative 1 k in insNodes g [v]

382 | adjEdges : SortedMap (Fin x) (Fin y) -> Adj x e n -> Adj y e n

383 | adjEdges m (A l ns) =

384 |   let ps := mapMaybe (\(n,v) => (,v) <$> lookup n m) $ pairs ns

385 |    in A l $ fromList ps

387 | zipTR : SnocList (a,b) -> List a -> List b -> List (a,b)

388 | zipTR sx []        _         = sx <>> []

389 | zipTR sx _         []        = sx <>> []

390 | zipTR sx (x :: xs) (y :: ys) = zipTR (sx:<(x,y)) xs ys

393 | delNodes : {k : _} -> List (Fin k) -> IGraph k e n -> Graph e n

394 | delNodes {k = 0} _ _ = G _ empty

395 | delNodes {k = S x} ks (IG g) =

396 |   let set       := SortedSet.fromList ks

397 |       A (S y) h :=

398 |         filterWithKey (\x,_ => not (contains x set)) g | A 0 _ => G _ empty

399 |       finX      := filter (\x => not (contains x set)) $ allFinsFast (S x)

400 |       finY      := allFinsFast (S y)

401 |       proMap    := SortedMap.fromList $ zipTR [<] finX finY

402 |    in G (S y) (IG $ map (adjEdges proMap) h)

406 | delNode : {k : _} -> Fin k -> IGraph k e n -> Graph e n

407 | delNode = delNodes . pure

412 | mergeGraphsWithEdges :

413 |      {k,m : _}

414 |   -> (g1 : IGraph k e n)

415 |   -> (g2 : IGraph m e n)

416 |   -> List (Fin k, Fin m, e)

417 |   -> IGraph (k + m) e n

418 | mergeGraphsWithEdges {k} g t es =

419 |   let vNodes := label <$> toVect t.graph

420 |       cEdges := map (\(x,y,l) => compositeEdge x y l) es

421 |       lEdges := incEdge k <$> edges t

422 |    in insNodesAndEdges g vNodes (cEdges ++ lEdges)

426 | mergeGraphs :

427 |      {k,m : _}

428 |   -> (g1 : IGraph k e n)

429 |   -> (g2 : IGraph m e n)

430 |   -> IGraph (k + m) e n

431 | mergeGraphs {k} g t =

432 |   let vNodes := label <$> toVect t.graph

433 |       lEdges := incEdge k <$> edges t

434 |    in insNodesAndEdges g vNodes lEdges

441 | {k : _} -> Show e => Show n => Show (IGraph k e n) where

442 |   showPrec p g = showCon p "mkGraph" $ showArg (labels g) ++ showArg (edges g)

445 | Show e => Show n => Show (Graph e n) where

446 |   showPrec p (G o g) = showCon p "G" $ showArg o ++ showArg g

448 | pl : Nat -> Fin k -> String

449 | pl n = padLeft n ' ' . show . finToNat

452 | pretty : {k : _} -> (e -> String) -> (n -> String) -> IGraph k e n -> String

453 | pretty de dn g =

454 |   let ns     := labNodes g

455 |       es     := edges g

456 |       maxLen := length $ show k

457 |    in unlines $

458 |         "Nodes:"   :: map (dispNode maxLen) ns ++

459 |         "\nEdges:" :: map (dispEdge maxLen) es

461 |   where

462 |     dispNode : Nat -> (Fin k, n) -> String

463 |     dispNode k (n1,l) =

464 |       "  \{pl k n1} :> \{dn l}"

466 |     dispEdge : Nat -> Edge k e -> String

467 |     dispEdge k (E n1 n2 l) =

468 |       "E \{pl k n1} \{pl k n2}  \{de l}"