Agda-2.4.2.4: A dependently typed functional programming language and proof assistant

Agda.Utils.Warshall

Description

Construct a graph from constraints ``` x + n y becomes x ---(-n)--- y x n + y becomes x ---(+n)--- y ``` the default edge (= no edge) is labelled with infinity.

Building the graph involves keeping track of the node names. We do this in a finite map, assigning consecutive numbers to nodes.

Synopsis

Documentation

type Matrix a = Array (Int, Int) a Source

type AdjList node edge = Map node [(node, edge)] Source

warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edge Source

Warshall's algorithm on a graph represented as an adjacency list.

data Weight Source

Edge weight in the graph, forming a semi ring.

Constructors

 Finite Int Infinite

Instances

 Source Source Source Source

data Node Source

Nodes of the graph are either - flexible variables (with identifiers drawn from `Int`), - rigid variables (also identified by `Int`s), or - constants (like 0, infinity, or anything between).

Constructors

 Rigid Rigid Flex FlexId

Instances

 Source Source Source

data Rigid Source

Constructors

 RConst Weight RVar RigidId

Instances

 Source Source Source

type Scope = RigidId -> Bool Source

Which rigid variables a flex may be instatiated to.

`isBelow r w r'` checks, if `r` and `r'` are connected by `w` (meaning `w` not infinite), whether `r + w <= r'`. Precondition: not the same rigid variable.

data Constraint Source

A constraint is an edge in the graph.

Constructors

 NewFlex FlexId Scope Arc Node Int Node For `Arc v1 k v2` at least one of `v1` or `v2` is a `MetaV` (Flex), the other a `MetaV` or a `Var` (Rigid). If `k <= 0` this means `suc^(-k) v1 <= v2` otherwise `v1 <= suc^k v3`.

Instances

 Source

data Graph Source

Constructors

 Graph FieldsflexScope :: Map FlexId ScopeScope for each flexible var.nodeMap :: Map Node NodeIdNode labels to node numbers.intMap :: Map NodeId NodeNode numbers to node labels.nextNode :: NodeIdNumber of nodes `n`.graph :: NodeId -> NodeId -> WeightThe edges (restrict to `[0..n[`).

The empty graph: no nodes, edges are all undefined (infinity weight).

type GM = State Graph Source

The Graph Monad, for constructing a graph iteratively.

addFlex :: FlexId -> Scope -> GM () Source

Lookup identifier of a node. If not present, it is added first.

addEdge :: Node -> Int -> Node -> GM () Source

`addEdge n1 k n2` improves the weight of egde `n1->n2` to be at most `k`. Also adds nodes if not yet present.

data LegendMatrix a b c Source

A matrix with row descriptions in `b` and column descriptions in `c`.

Constructors

 LegendMatrix Fieldsmatrix :: Matrix a rowdescr :: Int -> b coldescr :: Int -> c

Instances

 (Show a, Show b, Show c) => Show (LegendMatrix a b c) Source

A solution assigns to each flexible variable a size expression which is either a constant or a `v + n` for a rigid variable `v`.

data SizeExpr Source

Constructors

 SizeVar RigidId Int e.g. x + 5 SizeConst Weight a number or infinity

Instances

 Source

`sizeRigid r n` returns the size expression corresponding to `r + n`

genGraph :: Ord node => Float -> Gen edge -> [node] -> Gen (AdjList node edge) Source

lookupEdge :: Ord n => n -> n -> AdjList n e -> Maybe e Source

edges :: Ord n => AdjList n e -> [(n, n, e)] Source

prop_smaller :: Nat -> Property Source

Check that no edges get longer when completing a graph.

prop_path :: Nat -> Property Source

Check that all transitive edges are added.

mapNodes :: (Ord node, Ord node') => (node -> node') -> AdjList node edge -> AdjList node' edge Source

prop_disjoint :: Nat -> Property Source

Check that no edges are added between components.

prop_stable :: Nat -> Property Source