
  0 | module Data.Graph.Indexed.Ring.Util
  1 | 
  2 | import Data.SortedSet
  3 | import Data.Graph.Indexed
  4 | import Data.SnocList
  5 | 
  6 | %default total
  7 | 
  8 | ||| A set of unlabeled edges of order `k`
  9 | public export
 10 | 0 EdgeSet : (k : Nat) -> Type
 11 | EdgeSet k = SortedSet (Edge k ())
 12 | 
 13 | ||| Adds an unlabeled edge to an edge set.
 14 | |||
 15 | ||| The edge set is returned unmodified, if the two nodes are
 16 | ||| identical.
 17 | export
 18 | addEdge : EdgeSet k -> Fin k -> Fin k -> EdgeSet k
 19 | addEdge es x y = maybe es (`insert` es) (mkEdge x y ())
 20 | 
 21 | ||| Adds an unlabeled edge to an edge set.
 22 | |||
 23 | ||| The edge set is returned unmodified, if the two natural numbers
 24 | ||| are not valid distinct nodes of order `k`.
 25 | export
 26 | addNatEdge : {k : _} -> EdgeSet k -> Nat -> Nat -> EdgeSet k
 27 | addNatEdge es x y =
 28 |   let Just fx := tryNatToFin x | Nothing => es
 29 |       Just fy := tryNatToFin y | Nothing => es
 30 |    in addEdge es fx fy
 31 | 
 32 | ||| Converts a list of pairs of natural number to an edge set of
 33 | ||| order `k`. Invalid pairs of nodes are silently dropped.
 34 | export
 35 | toEdgeSet : {k : _} -> List (Nat,Nat) -> EdgeSet k
 36 | toEdgeSet = foldl (\es,(x,y) => addNatEdge es x y) empty
 37 | 
 38 | nodePairs : SnocList (a,a) -> List a -> SnocList (a,a)
 39 | nodePairs sp []     = sp
 40 | nodePairs sp (h::t) = nodePairs (sp <>< map (h,) t) t
 41 | 
 42 | ||| True, if the given node is a member of a three-membered cycle.
 43 | |||
 44 | ||| For sparse graphs, this check can be performed in linear time without
 45 | ||| performing a proper ring detection, just be checking if two of the
 46 | ||| neighbours of the given node are adjacent.
 47 | export
 48 | inThreeMemberedRing : IGraph k e n -> Fin k -> Bool
 49 | inThreeMemberedRing g x =
 50 |   any (\(a,b) => adjacent g a b) (nodePairs [<] (neighbours g x))
 51 |