Agda.Utils.Warshall

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.

Documentation

type Matrix a = Array (Int, Int) a

warshall :: SemiRing a => Matrix a -> Matrix a

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

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

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

data Weight

Edge weight in the graph, forming a semi ring.

Constructors

Finite Int

Infinite

Instances

Eq Weight

Ord Weight

Show Weight

SemiRing Weight

inc :: Weight -> Int -> Weight

data Node

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

Constructors

Rigid Rigid

Flex FlexId

Instances

Eq Node

Ord Node

Show Node

data Rigid

Constructors

RConst Weight

RVar RigidId

Instances

Eq Rigid

Ord Rigid

Show Rigid

type NodeId = Int

type RigidId = Int

type FlexId = Int

type Scope = RigidId -> Bool

Which rigid variables a flex may be instatiated to.

infinite :: Rigid -> Bool

isBelow :: Rigid -> Weight -> Rigid -> Bool

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

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

Show Constraint

type Constraints = [Constraint]

emptyConstraints :: [a]

data Graph

Constructors

Graph

Fields

flexScope :: Map FlexId Scope

Scope for each flexible var.

nodeMap :: Map Node NodeId

Node labels to node numbers.

intMap :: Map NodeId Node

Node numbers to node labels.

nextNode :: NodeId

Number of nodes n.

graph :: NodeId -> NodeId -> Weight

The edges (restrict to [0..n[).

initGraph :: Graph

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

type GM = State Graph

The Graph Monad, for constructing a graph iteratively.

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

Add a size meta node.

addNode :: Node -> GM Int

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

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

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

addConstraint :: Constraint -> GM ()

buildGraph :: Constraints -> Graph

mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight

data LegendMatrix a b c

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

Constructors

LegendMatrix

Fields

matrix :: Matrix a

rowdescr :: Int -> b

coldescr :: Int -> c

Instances

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

type Solution = Map Int SizeExpr

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

emptySolution :: Map k a

extendSolution :: Ord k => Map k a -> k -> a -> Map k a

data SizeExpr

Constructors

SizeVar RigidId Int

e.g. x + 5

SizeConst Weight

a number or infinity

Instances

Show SizeExpr

sizeRigid :: Rigid -> Int -> SizeExpr

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

solve :: Constraints -> Maybe Solution

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

newtype Distance

Constructors

Dist Nat

Instances

Enum Distance

Eq Distance

Integral Distance

Num Distance

Ord Distance

Real Distance

Show Distance

SemiRing Distance

genGraph_ :: Nat -> Gen (AdjList Nat Distance)

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

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

prop_smaller :: Nat -> Property

Check that no edges get longer when completing a graph.

newEdge :: Ord k => k -> t -> t1 -> Map k [(t, t1)] -> Map k [(t, t1)]

genPath :: Nat -> Nat -> Nat -> AdjList Nat Distance -> Gen (AdjList Nat Distance)

prop_path :: Nat -> Property

Check that all transitive edges are added.

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

prop_disjoint :: Nat -> Property

Check that no edges are added between components.

prop_stable :: Nat -> Property

tests :: IO Bool