Data.Graph.Types

(source)

A representation for sparse, simple, undirected
labeled graphs.

This module provides only the data types plus
interface implementations.

Definitions

Node : Type

  A node in an undirected graph.

Totality: total
Visibility: public export

record Edge : Type

  An 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 `n2 > n1 = True`.

Totality: total
Visibility: public export
Constructor:

MkEdge : (node1 : Node) -> (node2 : Node) -> (0 _ : node2 > node1) -> Edge

Projections:

.node1 : Edge -> Node
.node2 : Edge -> Node
0 .prf : ({rec:0} : Edge) -> node2 {rec:0} > node1 {rec:0}

Hints:

Eq Edge
Ord Edge
Show Edge

.node1 : Edge -> Node

Totality: total
Visibility: public export

node1 : Edge -> Node

Totality: total
Visibility: public export

.node2 : Edge -> Node

Totality: total
Visibility: public export

node2 : Edge -> Node

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Edge) -> node2 {rec:0} > node1 {rec:0}

Totality: total
Visibility: public export

0 prf : ({rec:0} : Edge) -> node2 {rec:0} > node1 {rec:0}

Totality: total
Visibility: public export

mkEdge : Node -> Node -> Maybe Edge

Totality: total
Visibility: public export

(<>) : (i : Node) -> (j : Node) -> {auto 0 _ : j > i} -> Edge

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 4

record LNode : Type -> Type

  A labeled node in a graph.

Totality: total
Visibility: public export
Constructor:

MkLNode : Node -> n -> LNode n

Projections:

.label : LNode n -> n
.node : LNode n -> Node

Hints:

Eq a => Eq (LNode a)
Foldable LNode
Functor LNode
Show n => Show (LNode n)
Traversable LNode

.node : LNode n -> Node

Totality: total
Visibility: public export

node : LNode n -> Node

Totality: total
Visibility: public export

.label : LNode n -> n

Totality: total
Visibility: public export

label : LNode n -> n

Totality: total
Visibility: public export

(:>) : Node -> n -> LNode n

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 4

record LEdge : Type -> Type

  A labeled edge in an undirected graph

Totality: total
Visibility: public export
Constructor:

MkLEdge : Edge -> e -> LEdge e

Projections:

.edge : LEdge e -> Edge
.label : LEdge e -> e

Hints:

Eq a => Eq (LEdge a)
Foldable LEdge
Functor LEdge
Ord a => Ord (LEdge a)
Show e => Show (LEdge e)
Traversable LEdge

.edge : LEdge e -> Edge

Totality: total
Visibility: public export

edge : LEdge e -> Edge

Totality: total
Visibility: public export

.label : LEdge e -> e

Totality: total
Visibility: public export

label : LEdge e -> e

Totality: total
Visibility: public export

(:>) : Edge -> e -> LEdge e

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 4

record Adj : 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:

MkAdj : n -> AssocList e -> Adj e n

Projections:

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

Hints:

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

.label : Adj e n -> n

Totality: total
Visibility: public export

label : Adj e n -> n

Totality: total
Visibility: public export

.neighbours : Adj e n -> AssocList e

Totality: total
Visibility: public export

neighbours : Adj e n -> AssocList e

Totality: total
Visibility: public export

record Context : Type -> Type -> Type

  The Context of a `Node` in a labeled graph
  including the `Node` itself, its label, plus
  its direct neighbors together with the
  labels of the edges leading to them.

Totality: total
Visibility: public export
Constructor:

MkContext : Node -> n -> AssocList e -> Context e n

Projections:

.label : Context e n -> n
.neighbours : Context e n -> AssocList e
.node : Context e n -> Node

Hints:

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

.node : Context e n -> Node

Totality: total
Visibility: public export

node : Context e n -> Node

Totality: total
Visibility: public export

.label : Context e n -> n

Totality: total
Visibility: public export

label : Context e n -> n

Totality: total
Visibility: public export

.neighbours : Context e n -> AssocList e

Totality: total
Visibility: public export

neighbours : Context e n -> AssocList e

Totality: total
Visibility: public export

GraphRep : Type -> Type -> Type

  Internal representation of labeled graphs.

Totality: total
Visibility: public export

record Graph : Type -> Type -> Type

Totality: total
Visibility: public export
Constructor:

MkGraph : GraphRep e n -> Graph e n

Projection:

.graph : Graph e n -> GraphRep e n

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)

.graph : Graph e n -> GraphRep e n

Totality: total
Visibility: public export

graph : Graph e n -> GraphRep e n

Totality: total
Visibility: public export

data Decomp : Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Split : Context e n -> Graph e n -> Decomp e n
Empty : Decomp e n