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

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

data Rigid Source

Constructors RConst Weight RVar RigidId

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

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

type Solution = Map Int SizeExpr Source

data SizeExpr Source

Constructors SizeVar Int Int SizeConst Weight

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

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.6.0