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

Safe HaskellNone

Agda.Utils.Warshall

Contents

Synopsis

Documentation

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

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

data Rigid

Constructors

RConst Weight 
RVar RigidId 

Instances

type NodeId = Int

type RigidId = Int

type FlexId = Int

type Scope = RigidId -> Bool

data Constraint

Instances

type GM = State Graph

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

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) 

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

data SizeExpr

Instances

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

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)]

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.