Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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) aSource
warshall :: SemiRing a => Matrix a -> Matrix aSource
type AdjList node edge = Map node [(node, edge)]Source
warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edgeSource
data Weight Source
Constructors
Finite Int
Infinite
show/hide Instances
inc :: Weight -> Int -> WeightSource
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
show/hide Instances
data Rigid Source
Constructors
RConst Weight
RVar RigidId
show/hide Instances
type NodeId = IntSource
type RigidId = IntSource
type FlexId = IntSource
type Scope = RigidId -> BoolSource
isBelow :: Rigid -> Weight -> Rigid -> BoolSource
data Constraint Source
Constructors
NewFlex FlexId Scope
Arc Node Int Node
show/hide Instances
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 GraphSource
addFlex :: FlexId -> Scope -> GM ()Source
addNode :: Node -> GM IntSource
addEdge :: Node -> Int -> Node -> GM ()Source
addConstraint :: Constraint -> GM ()Source
buildGraph :: Constraints -> GraphSource
mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix WeightSource
data LegendMatrix a b c Source
Constructors
LegendMatrix
matrix :: Matrix a
rowdescr :: Int -> b
coldescr :: Int -> c
show/hide Instances
(Show a, Show b, Show c) => Show (LegendMatrix a b c)
type Solution = Map Int SizeExprSource
data SizeExpr Source
Constructors
SizeVar Int Int
SizeConst Weight
show/hide Instances
sizeRigid :: Rigid -> Int -> SizeExprSource
solve :: Constraints -> Maybe SolutionSource
genGraph :: Ord node => Float -> Gen edge -> [node] -> Gen (AdjList node edge)Source
newtype Distance Source
Constructors
Dist Nat
show/hide Instances
genGraph_ :: Nat -> Gen (AdjList Nat Distance)Source
lookupEdge :: Ord n => n -> n -> AdjList n e -> Maybe eSource
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' edgeSource
Check that all transitive edges are added.
tests :: IO BoolSource
Check that no edges are added between components.
Produced by Haddock version 2.4.2