Data.Graph.Indexed.Types

(source)

A representation for sparse, simple, undirected
labeled graphs, indexed by their order and backed by an
immutable array for fast O(1) node lookups.

This module provides only the data types plus
interface implementations.

Definitions

0 CompFin : Fin k -> Fin k -> Ordering

Totality: total
Visibility: public export

record Edge : Nat -> Type -> Type

  A labeled edge in a simple, undirected graph.
  Since edges go in both directions and loops are not allowed,
  we can enforce without loss of generality
  that `node2 > node1 = True`.

Totality: total
Visibility: public export
Constructor:

E : (node1 : Fin k) -> (node2 : Fin k) -> e -> {auto 0 _ : CompFin node1 node2 = LT} -> Edge k e

Projections:

.label : Edge k e -> e
.node1 : Edge k e -> Fin k
.node2 : Edge k e -> Fin k
0 .prf : ({rec:0} : Edge k e) -> CompFin (node1 {rec:0}) (node2 {rec:0}) = LT

Hints:

Eq e => Eq (Edge k e)
Foldable (Edge k)
Functor (Edge k)
Ord e => Ord (Edge k e)
Show e => Show (Edge k e)
Traversable (Edge k)

.node1 : Edge k e -> Fin k

Totality: total
Visibility: public export

node1 : Edge k e -> Fin k

Totality: total
Visibility: public export

.node2 : Edge k e -> Fin k

Totality: total
Visibility: public export

node2 : Edge k e -> Fin k

Totality: total
Visibility: public export

.label : Edge k e -> e

Totality: total
Visibility: public export

label : Edge k e -> e

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Edge k e) -> CompFin (node1 {rec:0}) (node2 {rec:0}) = LT

Totality: total
Visibility: public export

0 prf : ({rec:0} : Edge k e) -> CompFin (node1 {rec:0}) (node2 {rec:0}) = LT

Totality: total
Visibility: public export

fromNat : (x : Nat) -> (y : Nat) -> {auto 0 _ : LT x k} -> {auto 0 _ : LT y k} -> {auto 0 _ : LT x y} -> e -> Edge k e

Totality: total
Visibility: export

weakenEdge : Edge k e -> Edge (S k) e

Totality: total
Visibility: export

weakenEdgeN : (0 m : Nat) -> Edge k e -> Edge (k + m) e

Totality: total
Visibility: export

incEdge : (k : Nat) -> Edge m e -> Edge (k + m) e

  Increase both nodes in an edge by the same natural number

Totality: total
Visibility: export

compositeEdge : Fin k -> Fin m -> e -> Edge (k + m) e

  Creates an edge between two nodes from different graphs,
  resulting in a new edge of their composite graph.
  
  Note: This assumes that nodes in the first graph (of order `k`)
        will stay the same, while nodes in the second graph
        (of order `m`) will be increased by `k`.

Totality: total
Visibility: export

mkEdge : Fin k -> Fin k -> e -> Maybe (Edge k e)

  Tries to create an edge from two nodes plus a label.
  
  Returns `Nothing` in case the two nodes are identical.

Totality: total
Visibility: public export

tryFromNat : Nat -> Nat -> e -> Maybe (Edge k e)

  Tries to create an edge from two natural numbers plus a label.
  
  Returns `Nothing` in case the two numbers are not in the correct
  range or are identical.

Totality: total
Visibility: export

edge : Fin k -> e -> Edge (S k) e

Totality: total
Visibility: public export

record Adj : Nat -> Type -> Type -> Type

  Adjacency info of a `Node` in a labeled graph.
  
  This consists of the node's label plus
  a list of all its neighboring nodes and
  the labels of the edges connecting them.
  
  This is what is stored in underlying `BitMap`
  representing the graph.

Totality: total
Visibility: public export
Constructor:

A : n -> AssocList k e -> Adj k e n

Projections:

.label : Adj k e n -> n
.neighbours : Adj k e n -> AssocList k e

Hints:

Bifoldable (Adj k)
Bifunctor (Adj k)
Bitraversable (Adj k)
Eq e => Eq n => Eq (Adj k e n)
Foldable (Adj k e)
Functor (Adj k e)
Show e => Show n => Show (Adj k e n)
Traversable (Adj k e)

.label : Adj k e n -> n

Totality: total
Visibility: public export

label : Adj k e n -> n

Totality: total
Visibility: public export

.neighbours : Adj k e n -> AssocList k e

Totality: total
Visibility: public export

neighbours : Adj k e n -> AssocList k e

Totality: total
Visibility: public export

weakenAdj : Adj k e n -> Adj (S k) e n

Totality: total
Visibility: export

weakenAdjN : (0 m : Nat) -> Adj k e n -> Adj (k + m) e n

Totality: total
Visibility: export

fromLabel : n -> Adj k e n

Totality: total
Visibility: export

record Context : Nat -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor:

C : Fin k -> n -> AssocList k e -> Context k e n

Projections:

.label : Context k e n -> n
.neighbours : Context k e n -> AssocList k e
.node : Context k e n -> Fin k

Hints:

Bifoldable (Context k)
Bifunctor (Context k)
Bitraversable (Context k)
Eq e => Eq n => Eq (Context k e n)
Foldable (Context k e)
Functor (Context k e)
Show e => Show n => Show (Context k e n)
Traversable (Context k e)

.node : Context k e n -> Fin k

Totality: total
Visibility: public export

node : Context k e n -> Fin k

Totality: total
Visibility: public export

.label : Context k e n -> n

Totality: total
Visibility: public export

label : Context k e n -> n

Totality: total
Visibility: public export

.neighbours : Context k e n -> AssocList k e

Totality: total
Visibility: public export

neighbours : Context k e n -> AssocList k e

Totality: total
Visibility: public export

record IGraph : Nat -> Type -> Type -> Type

  An order-indexed graph.

Totality: total
Visibility: public export
Constructor:

IG : IArray k (Adj k e n) -> IGraph k e n

Projection:

.graph : IGraph k e n -> IArray k (Adj k e n)

Hints:

Bifoldable (IGraph k)
Bifunctor (IGraph k)
Bitraversable (IGraph k)
Eq e => Eq n => Eq (IGraph k e n)
Foldable (IGraph k e)
Functor (IGraph k e)
Show e => Show n => Show (IGraph k e n)
Traversable (IGraph k e)

.graph : IGraph k e n -> IArray k (Adj k e n)

Totality: total
Visibility: public export

graph : IGraph k e n -> IArray k (Adj k e n)

Totality: total
Visibility: public export

record Graph : Type -> Type -> Type

  A graph together with its order

Totality: total
Visibility: public export
Constructor:

G : (order : Nat) -> IGraph order e n -> Graph e n

Projections:

.graph : ({rec:0} : Graph e n) -> IGraph (order {rec:0}) e n
.order : Graph e n -> Nat

Hints:

Bifoldable Graph
Bifunctor Graph
Bitraversable Graph
Eq e => Eq n => Eq (Graph e n)
Foldable (Graph e)
Functor (Graph e)
Show e => Show n => Show (Graph e n)
Traversable (Graph e)

.order : Graph e n -> Nat

Totality: total
Visibility: public export

order : Graph e n -> Nat

Totality: total
Visibility: public export

.graph : ({rec:0} : Graph e n) -> IGraph (order {rec:0}) e n

Totality: total
Visibility: public export

graph : ({rec:0} : Graph e n) -> IGraph (order {rec:0}) e n

Totality: total
Visibility: public export