| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Utils.Warshall

Contents

flexible variables (with identifiers drawn from Int),
rigid variables (also identified by Ints), or
constants (like 0, infinity, or anything between)

Synopsis

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

= Finite Int
| Infinite

inc :: Weight -> Int -> Weight

data Node

= Rigid Rigid
| Flex FlexId

data Rigid

= RConst Weight
| RVar RigidId

type NodeId = Int
type RigidId = Int
type FlexId = Int
type Scope = RigidId -> Bool
isBelow :: Rigid -> Weight -> Rigid -> Bool

data Constraint

= NewFlex FlexId Scope
| Arc Node Int Node

type Constraints = [Constraint]

data Graph = Graph {

flexScope :: Map FlexId Scope
nodeMap :: Map Node NodeId
intMap :: Map NodeId Node
nextNode :: NodeId
graph :: NodeId -> NodeId -> Weight

}

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 {

matrix :: Matrix a
rowdescr :: Int -> b
coldescr :: Int -> c

}

type Solution = Map Int SizeExpr

data SizeExpr

= SizeVar Int Int
| SizeConst Weight

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)]
genPath :: Nat -> Nat -> Nat -> AdjList Nat Distance -> Gen (AdjList Nat Distance)
mapNodes :: (Ord node, Ord node') => (node -> node') -> AdjList node edge -> AdjList node' edge
tests :: IO Bool

Documentation

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

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

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

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

data Weight | Source

Constructors

Finite Int |
Infinite |

Instances

Eq Weight
Ord Weight
Show Weight
SemiRing Weight

inc :: Weight -> Int -> Weight | Source

flexible variables (with identifiers drawn from Int),
rigid variables (also identified by Ints), or
constants (like 0, infinity, or anything between)

data Node | Source

Constructors

Rigid Rigid |
Flex FlexId |

Instances

Eq Node
Ord Node
Show Node

data Rigid | Source

Constructors

RConst Weight |
RVar RigidId |

Instances

Eq Rigid
Ord Rigid
Show Rigid

type NodeId = Int | Source

type RigidId = Int | Source

type FlexId = Int | Source

type Scope = RigidId -> Bool | Source

isBelow :: Rigid -> Weight -> Rigid -> Bool | Source

data Constraint | Source

Constructors

NewFlex FlexId Scope |
Arc Node Int Node |

Instances

Show Constraint

type Constraints = [Constraint] | Source

data Graph | Source

Constructors

Graph |

flexScope :: Map FlexId Scope |
nodeMap :: Map Node NodeId |
intMap :: Map NodeId Node |
nextNode :: NodeId |
graph :: NodeId -> NodeId -> Weight |

type GM = State Graph | Source

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

addNode :: Node -> GM Int | Source

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

addConstraint :: Constraint -> GM () | Source

buildGraph :: Constraints -> Graph | Source

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

data LegendMatrix a b c | Source

Constructors

LegendMatrix |

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 | Source

data SizeExpr | Source

Constructors

SizeVar Int Int |
SizeConst Weight |

Instances

Show SizeExpr

sizeRigid :: Rigid -> Int -> SizeExpr | Source

solve :: Constraints -> Maybe Solution | Source

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

newtype Distance | Source

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) | Source

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

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

genPath :: Nat -> Nat -> Nat -> AdjList Nat Distance -> Gen (AdjList Nat Distance) | 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

Check that all transitive edges are added.

tests :: IO Bool | Source

Check that no edges are added between components.
Produced by Haddock version 2.4.2