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

Agda.Utils.Warshall

Contents

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

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

data Rigid Source

Constructors

RConst Weight 
RVar RigidId 

Instances

data LegendMatrix a b c Source

Constructors

LegendMatrix 

Fields

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

Instances

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

genGraph :: Ord node => Float -> Gen edge -> [node] -> Gen (AdjList node edge)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.