
   0 | module Data.Graph.Indexed.Ring.Relevant.Types
   1 | 
   2 | import public Data.Graph.Indexed
   3 | import public Data.Graph.Indexed.Subgraph
   4 | import public Data.Graph.Indexed.Query.Util
   5 | import Data.Nat
   6 | import Data.SortedSet as SS
   7 | import Derive.Prelude
   8 | 
   9 | %default total
  10 | %language ElabReflection
  11 | 
  12 | ||| A shortest path of length `length` from a starting node to node `last`.
  13 | ||| `combos` is the number of shortest paths of the same length leading
  14 | ||| from `first` to `last`.
  15 | ||| Node `first` is the first node after the root node, and is used to
  16 | ||| check if two paths are disjoint.
  17 | public export
  18 | record Path (k : Nat) where
  19 |   constructor P
  20 |   ||| Number of nodes in the path (including the root node).
  21 |   length : Nat
  22 | 
  23 |   ||| The accumulated path viewed from the right
  24 |   path   : SnocList (Fin k)
  25 | 
  26 |   ||| True, if all nodes in the path are smaller than the root
  27 |   |||
  28 |   ||| This flag is used for efficiency, as it allows us to avoid
  29 |   ||| computing the same cycle more than once.
  30 |   keep   : Bool
  31 | 
  32 |   ||| The first non-root node in the path
  33 |   first  : Fin k
  34 | 
  35 |   ||| The last node in the path
  36 |   last   : Fin k
  37 | 
  38 |   ||| Number of paths of the same length from `root` to
  39 |   ||| `last`. This is later used to compute the size of
  40 |   ||| a family of relevant cycles
  41 |   combos : Nat
  42 | 
  43 | %runElab deriveIndexed "Path" [Show,Eq]
  44 | 
  45 | ||| A family of cycles in a graph of order `k`.
  46 | public export
  47 | record NCycle (k : Nat) where
  48 |   constructor NC
  49 |   ||| A single representative of the cycle family.
  50 |   path   : List (Fin k)
  51 | 
  52 |   ||| Length of the cycle.
  53 |   size   : Nat
  54 | 
  55 |   ||| Number of members in the family.
  56 |   combos : Nat
  57 | 
  58 |   ||| A cycle consists of at least three nodes
  59 |   {auto 0 prf : LTE 3 size}
  60 | 
  61 | %runElab deriveIndexed "NCycle" [Show,Eq]
  62 | 
  63 | public export
  64 | 0 Edg : Nat -> Type
  65 | Edg k = Edge k ()
  66 | 
  67 | public export
  68 | 0 ECycle : Nat -> Type
  69 | ECycle k = List (Edg k)
  70 | 
  71 | public export
  72 | record Cycle (k: Nat) where
  73 |   constructor C
  74 |   ncycle  : NCycle k
  75 |   ecycle  : ECycle k
  76 |   nodeset : SortedSet (Fin k)
  77 |   edgeset : SortedSet (Edg k)
  78 | 
  79 | export
  80 | (.nodes) : Cycle k -> List (Fin k)
  81 | (.nodes) c = drop 1 c.ncycle.path
  82 | 
  83 | %runElab deriveIndexed "Cycle" [Show,Eq]
  84 | 
  85 | export
  86 | ecycle : List (Fin k) -> ECycle k
  87 | ecycle (x::y::xs) =
  88 |   case mkEdge x y () of
  89 |     Just e  => e :: ecycle (y::xs)
  90 |     Nothing => ecycle (y::xs)
  91 | ecycle _ = []
  92 | 
  93 | export
  94 | Cast (NCycle k) (Cycle k) where
  95 |   cast n =
  96 |    let es := ecycle n.path
  97 |     in C n es (SS.fromList n.path) (SS.fromList es)
  98 | 
  99 | ||| Returns the list of nodes two cycles have in common.
 100 | export
 101 | sharedNodes : (cx,cy : Cycle k) -> List (Fin k)
 102 | sharedNodes cx cy =
 103 |   case cx.ncycle.size <= cy.ncycle.size of
 104 |     True  => filter (`contains` cy.nodeset) cx.nodes
 105 |     False => filter (`contains` cx.nodeset) cy.nodes
 106 | 
 107 | ||| Returns the number of nodes shared by two cycles.
 108 | export
 109 | numSharedNodes : (cx,cy : Cycle k) -> Nat
 110 | numSharedNodes cx cy =
 111 |   case cx.ncycle.size <= cy.ncycle.size of
 112 |     True  => count (`contains` cy.nodeset) cx.nodes
 113 |     False => count (`contains` cx.nodeset) cy.nodes
 114 | 
 115 | ||| Returns the list of edges two cycles have in common.
 116 | export
 117 | sharedEdges : (cx,cy : Cycle k) -> List (Edg k)
 118 | sharedEdges cx cy =
 119 |   case cx.ncycle.size <= cy.ncycle.size of
 120 |     True  => filter (`contains` cy.edgeset) cx.ecycle
 121 |     False => filter (`contains` cx.edgeset) cy.ecycle
 122 | 
 123 | ||| Returns the number of nodes shared by two cycles.
 124 | export
 125 | numSharedEdges : (cx,cy : Cycle k) -> Nat
 126 | numSharedEdges cx cy =
 127 |   case cx.ncycle.size <= cy.ncycle.size of
 128 |     True  => count (`contains` cy.edgeset) cx.ecycle
 129 |     False => count (`contains` cx.edgeset) cy.ecycle
 130 | 
 131 | ||| True, if the two cycles share a single edge and no additional node.
 132 | export
 133 | isFusedTo : (cx,cy : Cycle k) -> Bool
 134 | isFusedTo cx cy = numSharedNodes cx cy == 2 && numSharedEdges cx cy == 1
 135 | 
 136 | ||| True, if the two cycles share a single node.
 137 | export
 138 | isSpiro : (cx,cy : Cycle k) -> Bool
 139 | isSpiro cx cy = numSharedNodes cx cy == 1
 140 | 
 141 | public export
 142 | record CycleSets (k : Nat) where
 143 |   constructor CS
 144 |   cr  : List (Cycle k)
 145 |   mcb : List (Cycle k)
 146 | 
 147 | %runElab deriveIndexed "CycleSets" [Show,Eq]
 148 | 
 149 | public export
 150 | data Candidates : (k : Nat) -> (e : Type) -> Type where
 151 |   Empty   : Candidates k e
 152 |   Isolate : Subgraph k e Nat -> NCycle k -> Candidates k e
 153 |   System  :
 154 |        (o : Nat)
 155 |     -> ISubgraph o k e Nat
 156 |     -> List (NCycle o)
 157 |     -> Candidates k e
 158 |