Agda-2.2.8: A dependently typed functional programming language and proof assistant

Agda.Utils.Warshall

Synopsis

# Documentation

type Matrix a = Array (Int, Int) 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

Instances

 Eq Weight Ord Weight Show Weight SemiRing Weight

# 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

data Constraint Source

Constructors

 NewFlex FlexId Scope Arc Node Int Node

Instances

 Show Constraint

data Graph Source

Constructors

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

data LegendMatrix a b c Source

Constructors

 LegendMatrix Fieldsmatrix :: Matrix a rowdescr :: Int -> b coldescr :: Int -> c

Instances

 (Show a, Show b, Show c) => Show (LegendMatrix a b c)

data SizeExpr Source

Constructors

 SizeVar RigidId Int SizeConst Weight

Instances

 Show SizeExpr

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

newtype Distance Source

Constructors

 Dist Nat

lookupEdge :: Ord n => n -> n -> AdjList n e -> Maybe eSource

edges :: Ord n => AdjList n e -> [(n, n, e)]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.

Check that no edges are added between components.