Safe Haskell | None |
---|---|
Language | Haskell98 |
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.
- 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
- data Weight
- inc :: Weight -> Int -> Weight
- data Node
- data Rigid
- type NodeId = Int
- type RigidId = Int
- type FlexId = Int
- type Scope = RigidId -> Bool
- infinite :: Rigid -> Bool
- isBelow :: Rigid -> Weight -> Rigid -> Bool
- data Constraint
- type Constraints = [Constraint]
- emptyConstraints :: Constraints
- data Graph = Graph {}
- initGraph :: Graph
- type GM = State Graph
- addFlex :: FlexId -> Scope -> GM ()
- addNode :: Node -> GM Int
- addEdge :: Node -> Int -> Node -> GM ()
- addConstraint :: Constraint -> GM ()
- buildGraph :: Constraints -> Graph
- mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight
- data LegendMatrix a b c = LegendMatrix {}
- type Solution = Map Int SizeExpr
- emptySolution :: Solution
- extendSolution :: Solution -> Int -> SizeExpr -> Solution
- data SizeExpr
- sizeRigid :: Rigid -> Int -> SizeExpr
- solve :: Constraints -> Maybe Solution
- genGraph :: Ord node => Float -> Gen edge -> [node] -> Gen (AdjList node edge)
- newtype Distance = Dist Nat
- 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
- newEdge :: Nat -> Nat -> Distance -> AdjList Nat Distance -> AdjList Nat Distance
- genPath :: Nat -> Nat -> Nat -> AdjList Nat Distance -> Gen (AdjList Nat Distance)
- prop_path :: Nat -> Property
- mapNodes :: (Ord node, Ord node') => (node -> node') -> AdjList node edge -> AdjList node' edge
- prop_disjoint :: Nat -> Property
- prop_stable :: Nat -> Property
- tests :: IO Bool
Documentation
warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edge Source
Warshall's algorithm on a graph represented as an adjacency list.
Edge weight in the graph, forming a semi ring.
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).
isBelow :: Rigid -> Weight -> Rigid -> Bool Source
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.
type Constraints = [Constraint] Source
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.
addConstraint :: Constraint -> GM () Source
buildGraph :: Constraints -> Graph Source
data LegendMatrix a b c Source
A matrix with row descriptions in b
and column descriptions in c
.
(Show a, Show b, Show c) => Show (LegendMatrix a b c) |
type Solution = Map Int SizeExpr 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
.
sizeRigid :: Rigid -> Int -> SizeExpr Source
sizeRigid r n
returns the size expression corresponding to r + n
solve :: Constraints -> Maybe Solution Source
lookupEdge :: Ord n => n -> n -> AdjList n e -> Maybe e Source
prop_smaller :: Nat -> Property Source
Check that no edges get longer when completing a graph.
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