
   0 | module Data.Graph.Indexed.Ring.Relevant
   1 | 
   2 | import Data.Bits
   3 | import Data.Graph.Indexed.Ring.Relevant.Candidates
   4 | import Data.List
   5 | import Data.SortedMap
   6 | 
   7 | import public Data.Graph.Indexed.Ring.Relevant.Types
   8 | 
   9 | %default total
  10 | 
  11 | --------------------------------------------------------------------------------
  12 | --          Relevant Cycles and MCB
  13 | --------------------------------------------------------------------------------
  14 | 
  15 | export
  16 | computeCyclomaticN : {k : _} -> IGraph k e n -> Nat
  17 | computeCyclomaticN g = S (size g) `minus` k
  18 | 
  19 | 0 EdgMap : Nat -> Type
  20 | EdgMap k = SortedMap (Edg k) Integer
  21 | 
  22 | -- Compute a sortedMap corresponding to a mapping from all edges of a graph to their
  23 | -- respective bit pattern.
  24 | getBitsEdges : {k : _} -> (g : IGraph k e n) -> EdgMap k
  25 | getBitsEdges g = setBits (map ignore $ edges g) 1 empty
  26 |   where
  27 |     setBits : List (Edg k) -> Integer -> EdgMap k -> EdgMap k
  28 |     setBits []        bitp sm = sm
  29 |     setBits (y :: xs) bitp sm = setBits xs (shiftL bitp 1) (insert y bitp sm)
  30 | 
  31 | -- Computes the bit pattern corresponding to the edges included in the given cycle.
  32 | -- The cycle is represented as node pairs corresponding to the cyclic edges.
  33 | -- The sortedMap is a maping from each edge of the graph (node pairs) to the bit
  34 | -- pattern corresponding to this edge.
  35 | getBitsRing : EdgMap k -> Integer -> List (Fin k) -> Integer
  36 | getBitsRing sm i (x::xs@(y::_)) = case mkEdge x y () >>= lookup' sm of
  37 |   Nothing => getBitsRing sm i xs -- impossible case
  38 |   Just z  => getBitsRing sm (i .|. z) xs
  39 | getBitsRing sm i _ = i
  40 | 
  41 | -- Tests if two integers have the same significant bit.
  42 | -- LT -> same significant bit, else distinct significant bit.
  43 | testSigBit : Integer -> Integer -> Ordering
  44 | testSigBit i j = compare (xor i j) (i .&. j)
  45 | 
  46 | -- Tests if a ring, represented as a bit pattern of edges, is linearly independet
  47 | -- from the given set of rings. Returns the modified set if the ring is linearly
  48 | -- independet and a boolan to indicate wheter the ring is linearly independent.
  49 | isInSet :
  50 |      (ring : Integer)
  51 |   -> (processedRs : SnocList (Integer))
  52 |   -> (unprocessedRs : List (Integer))
  53 |   -> (List Integer, Bool)
  54 | isInSet ring sy  []        = (sy <>> [ring], True)
  55 | isInSet ring sy  (x :: xs) =
  56 |   case testSigBit ring x of
  57 |     LT => -- same significant bit
  58 |       let remainder := xor ring x
  59 |            in if remainder == 0
  60 |                 then (sy <>> x :: xs, False)
  61 |                 else isInSet remainder (sy :< x) xs
  62 |     _  => -- distinct significant bit
  63 |       case compare ring x of
  64 |         GT => (sy :< ring <>> x :: xs, True)
  65 |         _  => isInSet ring (sy :< x) xs
  66 | 
  67 | record BCycle (k : Nat) where
  68 |   constructor BC
  69 |   ncycle : NCycle k
  70 |   bitp   : Integer
  71 | 
  72 | 0 BCycles : Nat -> Type
  73 | BCycles = List . BCycle
  74 | 
  75 | -- Recursive function to compute the set of relevant rings and minimum cycle basis.
  76 | getCrAndMCB' :
  77 |      (v, size: Nat)
  78 |   -> (sm, eq : List Integer)
  79 |   -> (xs, cr, mcb : BCycles k)
  80 |   -> (BCycles k, BCycles k)
  81 | getCrAndMCB' v size sm eq []        cr mcb = (cr,mcb)
  82 | getCrAndMCB' v size sm eq (c :: cs) cr mcb =
  83 |   case c.ncycle.size > size of
  84 |     True => case length mcb == v of
  85 |       True  => (cr,mcb)
  86 |       False => case isInSet c.bitp [<] eq of
  87 |         (_,     False) => -- neither in Cr nor MCB, continue
  88 |           getCrAndMCB' v size eq eq cs cr mcb
  89 |         (neweq, True)  => -- in Cr and MCB
  90 |           getCrAndMCB' v c.ncycle.size eq neweq cs (c :: cr) (c :: mcb)
  91 |     False => case isInSet c.bitp [<] sm of
  92 |       (_, False) => -- neither in Cr nor MCB, continue
  93 |         getCrAndMCB' v size sm eq cs cr mcb
  94 |       (_, True)  =>
  95 |         case isInSet c.bitp [<] eq of
  96 |           (_,     False) => -- in Cr but not MCB
  97 |             getCrAndMCB' v c.ncycle.size sm eq cs (c :: cr) mcb
  98 |           (neweq, True)  => -- in Cr and MCB
  99 |             getCrAndMCB' v c.ncycle.size sm neweq cs (c :: cr) (c :: mcb)
 100 | 
 101 | -- Initalizes the recursive function getCrAndMCB' to get the relevant cycles and MCB
 102 | -- from the cyclomatic number and the set of potentially relevant cycles (CI', given
 103 | -- as a list of pairs with cycle size and the cycle represented as a bit pattern of edges).
 104 | -- The potentially relevant cycles are ordered by size.
 105 | getCrAndMCB : Nat -> BCycles k -> (BCycles k, BCycles k)
 106 | getCrAndMCB v xs = getCrAndMCB' v 0 [] [] xs [] []
 107 | 
 108 | convert : ISubgraph o k e n -> (BCycles o, BCycles o) -> CycleSets k
 109 | convert g (m,b) = CS (map conv m) (map conv b)
 110 |   where
 111 |     conv : BCycle o -> Cycle k
 112 |     conv (BC c _) = cast {from = NCycle k} $ {path $= map (origin g)} c
 113 | 
 114 | fromCandidates : Candidates k e -> CycleSets k
 115 | fromCandidates Empty = CS [] []
 116 | fromCandidates (Isolate x nc) = let c := cast {to = Cycle k} nc in CS [c] [c]
 117 | fromCandidates (System o g xss) =
 118 |   let ebits := getBitsEdges g
 119 |       ci'   := sortBy (compare `on` size) xss
 120 |       cs    := map (getCycle ebits) ci'
 121 |       v     := computeCyclomaticN g
 122 |    in convert g $ getCrAndMCB v cs
 123 | 
 124 |    where getCycle : EdgMap o -> NCycle o ->  BCycle o
 125 |          getCycle ebits nc = BC nc $ getBitsRing ebits 0 nc.path
 126 | 
 127 | ||| computes the relevant cycles and minimum cycle basis
 128 | ||| for a biconnected component in a graph.
 129 | export %inline
 130 | componentCycles : Subgraph k e n -> CycleSets k
 131 | componentCycles = fromCandidates . componentCandidates
 132 | 
 133 | ||| computes the relevant cycles and minimum cycle basis for a graph
 134 | export
 135 | computeCrAndMCB : {k : _} -> IGraph k e n -> CycleSets k
 136 | computeCrAndMCB g =
 137 |   let css := map fromCandidates (candidates g)
 138 |    in CS (css >>= cr) (css >>= mcb)
 139 |