
   0 | ||| This module provides utilities used to compute families of relevant cycles
   1 | ||| as described by Vismara et al in "Union of all the minimum cycle bases of a graph"
   2 | ||| (The Electronic Journal of Combinatorics 4 (1997)).
   3 | |||
   4 | ||| In particular, it computes candidates of relevant cycle familes.
   5 | module Data.Graph.Indexed.Ring.Relevant.Candidates
   6 | 
   7 | import Data.Graph.Indexed.Ring.Relevant.ShortestPath
   8 | import Data.Graph.Indexed.Ring.Relevant.Types
   9 | import Data.SnocList
  10 | 
  11 | %default total
  12 | 
  13 | export
  14 | origin : ISubgraph o k e n -> NCycle o -> NCycle k
  15 | origin g = {path $= map (Subgraph.origin g)}
  16 | 
  17 | isolate : {o : _} -> ISubgraph (S o) k e n -> Maybe (NCycle k)
  18 | isolate {o = n@(S (S _))} g =
  19 |   Just $ NC (map (origin g) $ nodes g ++ [FZ]) (S n) 1
  20 | isolate               g = Nothing
  21 | 
  22 | notLast : Fin k -> SnocList (Fin k) -> Bool
  23 | notLast x (_ :< y :< _) = x /= y
  24 | notLast x _             = True
  25 | 
  26 | revOnto : SnocList a -> SnocList a -> List a
  27 | revOnto sx [<] = sx <>> []
  28 | revOnto sx (sy:<y) = revOnto (sx :< y) sy
  29 | 
  30 | appMaybe : SnocList a -> Maybe a -> SnocList a
  31 | appMaybe sc = maybe sc (sc:<)
  32 | 
  33 | gte3 : Nat -> Maybe (Subset Nat (LTE 3))
  34 | gte3 n =
  35 |   case tryLTE {n} 3 of
  36 |     Just0 prf => Just (Element n prf)
  37 |     Nothing0  => Nothing
  38 | 
  39 | parameters {o    : Nat}
  40 |            (g    : ISubgraph o k e Nat)
  41 |            (root : Fin o)
  42 |            (rdeg : Nat)
  43 | 
  44 |   connector : SnocList (Fin o) -> SnocList (Fin o) -> Fin o -> Bool
  45 |   connector sx sy x = smaller root rdeg g x && notLast x sx && notLast x sy
  46 | 
  47 |   -- Takes a list of reverse paths starting all from the same node and
  48 |   -- sorted by length (this is by construction: the `shortestPaths` algorithm
  49 |   -- will produce shorter paths earlier than longer paths), pairs every
  50 |   -- path with all successors of equal length (resulting in odd cycles) and
  51 |   -- one node longer (resulting in even cycles), and connect the two parts if
  52 |   -- they form a proper elementary cycle.
  53 |   cycleSystem : List (NCycle o)
  54 |   cycleSystem = go [<] (shortestPaths g root)
  55 |     where
  56 |       -- computes an odd cycle by concatenating two paths ending
  57 |       --
  58 |       %inline
  59 |       odd : (p1,p2 : Path o) -> Maybe (NCycle o)
  60 |       odd p1 p2 =
  61 |         flip map (gte3 (pred $ p1.length + p2.length)) $ \(Element s _) =>
  62 |           NC (revOnto p1.path p2.path) s (p1.combos * p2.combos)
  63 | 
  64 |       %inline
  65 |       even : (p1,p2 : Path o) -> Fin o -> Maybe (NCycle o)
  66 |       even p1 p2 x =
  67 |         if connector p1.path p2.path x
  68 |           then
  69 |             flip map (gte3 (p1.length + p2.length)) $ \(Element s _) =>
  70 |               NC (revOnto (p1.path :< x) p2.path) s (p1.combos * p2.combos)
  71 |           else Nothing
  72 | 
  73 |       addCs : SnocList (NCycle o) -> Path o -> List (Path o) -> SnocList (NCycle o)
  74 |       addCs sc p [] = sc
  75 |       addCs sc p@(P len1 p1 _ f1 l1 _) (q@(P len2 p2 _ f2 l2 _)::qs) =
  76 |         let True  := len1 == len2     | False => sc
  77 |             False := f1 == f2         | True  => addCs sc p qs
  78 |             False := adjacent g l1 l2 | True  => addCs (appMaybe sc $ odd p q) p qs
  79 |             ns    := keys $ intersect (neighboursAsAL g l1) (neighboursAsAL g l2)
  80 |          in addCs (sc <>< mapMaybe (even p q) ns) p qs
  81 | 
  82 |       -- for the current path, we take from the remaining paths those
  83 |       -- that are at most one node longer and try to pair them to
  84 |       -- form a cycle.
  85 |       go : SnocList (NCycle o) -> List (Path o) -> List (NCycle o)
  86 |       go sxs []        = sxs <>> []
  87 |       go sxs (p :: ps) = go (addCs sxs p ps) ps
  88 | 
  89 | findCandidates : Subgraph k e Nat -> Candidates k e
  90 | findCandidates (G 0 g) = Empty
  91 | findCandidates sg@(G (S k) g) =
  92 |   case filter ((2 <) . deg g) (nodes g) of
  93 |     [] => maybe Empty (Isolate sg) (isolate g)
  94 |     ns => System (S k) g (ns >>= \n => cycleSystem g n (deg g n))
  95 | 
  96 | ||| Computes the potential relevant cycle familes for a biconnected
  97 | ||| component of a graph.
  98 | export %inline
  99 | componentCandidates : Subgraph k e n -> Candidates k e
 100 | componentCandidates = findCandidates . toDegs
 101 | 
 102 | ||| Cuts a graph into strongly connected components and computes
 103 | ||| the potential relevant cycle families for each component in
 104 | ||| isolation.
 105 | export
 106 | candidates : {k : _} -> IGraph k e n -> List (Candidates k e)
 107 | candidates = map componentCandidates . biconnectedComponents
 108 |