Agda-2.5.1.2: 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 # Methods(==) :: Weight -> Weight -> Bool #(/=) :: Weight -> Weight -> Bool # Source # Methods(<) :: Weight -> Weight -> Bool #(<=) :: Weight -> Weight -> Bool #(>) :: Weight -> Weight -> Bool #(>=) :: Weight -> Weight -> Bool #max :: Weight -> Weight -> Weight #min :: Weight -> Weight -> Weight # Source # MethodsshowsPrec :: Int -> Weight -> ShowS #showList :: [Weight] -> ShowS # Source # Methods

data Node Source #

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

 Source # Methods(==) :: Node -> Node -> Bool #(/=) :: Node -> Node -> Bool # Source # Methodscompare :: Node -> Node -> Ordering #(<) :: Node -> Node -> Bool #(<=) :: Node -> Node -> Bool #(>) :: Node -> Node -> Bool #(>=) :: Node -> Node -> Bool #max :: Node -> Node -> Node #min :: Node -> Node -> Node # Source # MethodsshowsPrec :: Int -> Node -> ShowS #show :: Node -> String #showList :: [Node] -> ShowS #

data Rigid Source #

Constructors

 RConst Weight RVar RigidId

Instances

 Source # Methods(==) :: Rigid -> Rigid -> Bool #(/=) :: Rigid -> Rigid -> Bool # Source # Methods(<) :: Rigid -> Rigid -> Bool #(<=) :: Rigid -> Rigid -> Bool #(>) :: Rigid -> Rigid -> Bool #(>=) :: Rigid -> Rigid -> Bool #max :: Rigid -> Rigid -> Rigid #min :: Rigid -> Rigid -> Rigid # Source # MethodsshowsPrec :: Int -> Rigid -> ShowS #show :: Rigid -> String #showList :: [Rigid] -> ShowS #

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.

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 # MethodsshowList :: [Constraint] -> ShowS #

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 # MethodsshowsPrec :: Int -> LegendMatrix a b c -> ShowS #show :: LegendMatrix a b c -> String #showList :: [LegendMatrix a b c] -> ShowS #

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 # MethodsshowList :: [SizeExpr] -> ShowS #

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 :: AdjList n e -> [(n, n, e)] Source #

Check that no edges get longer when completing a graph.

Check that all transitive edges are added.

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

Check that no edges are added between components.