Idris2Doc : Data.Graph.Indexed.Ring.Relevant.Types

Data.Graph.Indexed.Ring.Relevant.Types

(source)
Reexports
import public Data.Graph.Indexed
import public Data.Graph.Indexed.Subgraph
import public Data.Graph.Indexed.Query.Util
Definitions
record Path : Nat -> Type
  A shortest path of length `length` from a starting node to node `last`.
  `combos` is the number of shortest paths of the same length leading
  from `first` to `last`.
  Node `first` is the first node after the root node, and is used to
  check if two paths are disjoint.

  Totality: total
  Visibility: public export
  Constructor: 
P : Nat -> SnocList (Fin k) -> Bool -> Fin k -> Fin k -> Nat -> Path k

  Projections:
  
.combos : Path k -> Nat
  Number of paths of the same length from `root` to
  `last`. This is later used to compute the size of
  a family of relevant cycles
  
.first : Path k -> Fin k
  The first non-root node in the path
  
.keep : Path k -> Bool
  True, if all nodes in the path are smaller than the root
  
  This flag is used for efficiency, as it allows us to avoid
  computing the same cycle more than once.
  
.last : Path k -> Fin k
  The last node in the path
  
.length : Path k -> Nat
  Number of nodes in the path (including the root node).
  
.path : Path k -> SnocList (Fin k)
  The accumulated path viewed from the right

  Hints:
  
Eq (Path k)
  
Show (Path k)
.length : Path k -> Nat
  Number of nodes in the path (including the root node).

  Totality: total
  Visibility: public export
length : Path k -> Nat
  Number of nodes in the path (including the root node).

  Totality: total
  Visibility: public export
.path : Path k -> SnocList (Fin k)
  The accumulated path viewed from the right

  Totality: total
  Visibility: public export
path : Path k -> SnocList (Fin k)
  The accumulated path viewed from the right

  Totality: total
  Visibility: public export
.keep : Path k -> Bool
  True, if all nodes in the path are smaller than the root
  
  This flag is used for efficiency, as it allows us to avoid
  computing the same cycle more than once.

  Totality: total
  Visibility: public export
keep : Path k -> Bool
  True, if all nodes in the path are smaller than the root
  
  This flag is used for efficiency, as it allows us to avoid
  computing the same cycle more than once.

  Totality: total
  Visibility: public export
.first : Path k -> Fin k
  The first non-root node in the path

  Totality: total
  Visibility: public export
first : Path k -> Fin k
  The first non-root node in the path

  Totality: total
  Visibility: public export
.last : Path k -> Fin k
  The last node in the path

  Totality: total
  Visibility: public export
last : Path k -> Fin k
  The last node in the path

  Totality: total
  Visibility: public export
.combos : Path k -> Nat
  Number of paths of the same length from `root` to
  `last`. This is later used to compute the size of
  a family of relevant cycles

  Totality: total
  Visibility: public export
combos : Path k -> Nat
  Number of paths of the same length from `root` to
  `last`. This is later used to compute the size of
  a family of relevant cycles

  Totality: total
  Visibility: public export
record NCycle : Nat -> Type
  A family of cycles in a graph of order `k`.

  Totality: total
  Visibility: public export
  Constructor: 
NC : List (Fin k) -> (size : Nat) -> Nat -> {auto 0 _ : LTE 3 size} -> NCycle k

  Projections:
  
.combos : NCycle k -> Nat
  Number of members in the family.
  
.path : NCycle k -> List (Fin k)
  A single representative of the cycle family.
  
0 .prf : ({rec:0} : NCycle k) -> LTE 3 (size {rec:0})
  A cycle consists of at least three nodes
  
.size : NCycle k -> Nat
  Length of the cycle.

  Hints:
  
Cast (NCycle k) (Cycle k)
  
Eq (NCycle k)
  
Show (NCycle k)
.path : NCycle k -> List (Fin k)
  A single representative of the cycle family.

  Totality: total
  Visibility: public export
path : NCycle k -> List (Fin k)
  A single representative of the cycle family.

  Totality: total
  Visibility: public export
.size : NCycle k -> Nat
  Length of the cycle.

  Totality: total
  Visibility: public export
size : NCycle k -> Nat
  Length of the cycle.

  Totality: total
  Visibility: public export
.combos : NCycle k -> Nat
  Number of members in the family.

  Totality: total
  Visibility: public export
combos : NCycle k -> Nat
  Number of members in the family.

  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : NCycle k) -> LTE 3 (size {rec:0})
  A cycle consists of at least three nodes

  Totality: total
  Visibility: public export
0 prf : ({rec:0} : NCycle k) -> LTE 3 (size {rec:0})
  A cycle consists of at least three nodes

  Totality: total
  Visibility: public export
0 Edg : Nat -> Type
  Totality: total
  Visibility: public export
0 ECycle : Nat -> Type
  Totality: total
  Visibility: public export
record Cycle : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
C : NCycle k -> ECycle k -> SortedSet (Fin k) -> SortedSet (Edg k) -> Cycle k

  Projections:
  
.ecycle : Cycle k -> ECycle k
  
.edgeset : Cycle k -> SortedSet (Edg k)
  
.ncycle : Cycle k -> NCycle k
  
.nodeset : Cycle k -> SortedSet (Fin k)

  Hints:
  
Cast (NCycle k) (Cycle k)
  
Eq (Cycle k)
  
Show (Cycle k)
.ncycle : Cycle k -> NCycle k
  Totality: total
  Visibility: public export
ncycle : Cycle k -> NCycle k
  Totality: total
  Visibility: public export
.ecycle : Cycle k -> ECycle k
  Totality: total
  Visibility: public export
ecycle : Cycle k -> ECycle k
  Totality: total
  Visibility: public export
.nodeset : Cycle k -> SortedSet (Fin k)
  Totality: total
  Visibility: public export
nodeset : Cycle k -> SortedSet (Fin k)
  Totality: total
  Visibility: public export
.edgeset : Cycle k -> SortedSet (Edg k)
  Totality: total
  Visibility: public export
edgeset : Cycle k -> SortedSet (Edg k)
  Totality: total
  Visibility: public export
.nodes : Cycle k -> List (Fin k)
  Totality: total
  Visibility: export
ecycle : List (Fin k) -> ECycle k
  Totality: total
  Visibility: export
sharedNodes : Cycle k -> Cycle k -> List (Fin k)
  Returns the list of nodes two cycles have in common.

  Totality: total
  Visibility: export
numSharedNodes : Cycle k -> Cycle k -> Nat
  Returns the number of nodes shared by two cycles.

  Totality: total
  Visibility: export
sharedEdges : Cycle k -> Cycle k -> List (Edg k)
  Returns the list of edges two cycles have in common.

  Totality: total
  Visibility: export
numSharedEdges : Cycle k -> Cycle k -> Nat
  Returns the number of nodes shared by two cycles.

  Totality: total
  Visibility: export
isFusedTo : Cycle k -> Cycle k -> Bool
  True, if the two cycles share a single edge and no additional node.

  Totality: total
  Visibility: export
isSpiro : Cycle k -> Cycle k -> Bool
  True, if the two cycles share a single node.

  Totality: total
  Visibility: export
record CycleSets : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
CS : List (Cycle k) -> List (Cycle k) -> CycleSets k

  Projections:
  
.cr : CycleSets k -> List (Cycle k)
  
.mcb : CycleSets k -> List (Cycle k)

  Hints:
  
Eq (CycleSets k)
  
Show (CycleSets k)
.cr : CycleSets k -> List (Cycle k)
  Totality: total
  Visibility: public export
cr : CycleSets k -> List (Cycle k)
  Totality: total
  Visibility: public export
.mcb : CycleSets k -> List (Cycle k)
  Totality: total
  Visibility: public export
mcb : CycleSets k -> List (Cycle k)
  Totality: total
  Visibility: public export
data Candidates : Nat -> Type -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
Empty : Candidates k e
  
Isolate : Subgraph k e Nat -> NCycle k -> Candidates k e
  
System : (o : Nat) -> ISubgraph o k e Nat -> List (NCycle o) -> Candidates k e