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

Safe Haskell | None

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
- infinite :: Rigid -> Bool
- isBelow :: Rigid -> Weight -> Rigid -> Bool
- data Constraint
  - = NewFlex FlexId Scope
  - | Arc Node Int Node
- type Constraints = [Constraint]
- emptyConstraints :: [a]
- data Graph = Graph {
  - flexScope :: Map FlexId Scope
  - nodeMap :: Map Node NodeId
  - intMap :: Map NodeId Node
  - nextNode :: NodeId
  - graph :: NodeId -> NodeId -> Weight
  }
- 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 {
  - matrix :: Matrix a
  - rowdescr :: Int -> b
  - coldescr :: Int -> c
  }
- type Solution = Map Int SizeExpr
- emptySolution :: Map k a
- extendSolution :: Ord k => Map k a -> k -> a -> Map k a
- data SizeExpr
  - = SizeVar RigidId 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)]
- prop_smaller :: Nat -> Property
- newEdge :: Ord k => k -> t -> t1 -> Map k [(t, t1)] -> Map k [(t, t1)]
- 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

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

Constructors

Finite Int |
Infinite |

Instances

Eq Weight |
Ord Weight |
Show Weight |
SemiRing Weight |

inc :: Weight -> Int -> Weight

# flexible variables (with identifiers drawn from Int),

# rigid variables (also identified by Ints), or

# constants (like 0, infinity, or anything between)

data Node

Constructors

Rigid Rigid |
Flex FlexId |

Instances

Eq Node |
Ord Node |
Show Node |

data Rigid

Constructors

RConst Weight |
RVar RigidId |

Instances

Eq Rigid |
Ord Rigid |
Show Rigid |

type NodeId = Int

type RigidId = Int

type FlexId = Int

type Scope = RigidId -> Bool

infinite :: Rigid -> Bool

isBelow :: Rigid -> Weight -> Rigid -> Bool

data Constraint

Constructors

NewFlex FlexId Scope |
Arc Node Int Node |

Instances

Show Constraint |

type Constraints = [Constraint]

emptyConstraints :: [a]

data Graph

Constructors

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

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

Constructors

LegendMatrix |
Fields 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

emptySolution :: Map k a

extendSolution :: Ord k => Map k a -> k -> a -> Map k a

data SizeExpr

Constructors

SizeVar RigidId Int |
SizeConst Weight |

Instances

Show SizeExpr |

sizeRigid :: Rigid -> Int -> SizeExpr

solve :: Constraints -> Maybe Solution

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

newtype Distance

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)

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

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

prop_smaller :: Nat -> Property

Check that no edges get longer when completing a graph.

newEdge :: Ord k => k -> t -> t1 -> Map k [(t, t1)] -> Map k [(t, t1)]

genPath :: Nat -> Nat -> Nat -> AdjList Nat Distance -> Gen (AdjList Nat Distance)

prop_path :: Nat -> Property

Check that all transitive edges are added.

mapNodes :: (Ord node, Ord node') => (node -> node') -> AdjList node edge -> AdjList node' edge

prop_disjoint :: Nat -> Property

Check that no edges are added between components.

prop_stable :: Nat -> Property

tests :: IO Bool