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

Safe HaskellNone

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

addEdge :: Node -> Int -> Node -> GM ()Source

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) 

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

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

prop_smaller :: Nat -> PropertySource

Check that no edges get longer when completing a graph.

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

prop_path :: Nat -> PropertySource

Check that all transitive edges are added.

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

prop_disjoint :: Nat -> PropertySource

Check that no edges are added between components.