Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Construct a graph from constraints x + n y becomes x ---(-n)--- y x n + y becomes x ---(+n)--- y the default edge (= no edge) is labelled with infinity.

Building the graph involves keeping track of the node names. We do this in a finite map, assigning consecutive numbers to nodes.



type Matrix a = Array (Int, Int) a Source

type AdjList node edge = Map node [(node, edge)] Source

warshallG :: (SemiRing edge, Ord node) => AdjList node edge -> AdjList node edge Source

Warshall's algorithm on a graph represented as an adjacency list.

data Weight Source

Edge weight in the graph, forming a semi ring.


Finite Int 

data Node Source

Nodes of the graph are either - flexible variables (with identifiers drawn from Int), - rigid variables (also identified by Ints), or - constants (like 0, infinity, or anything between).


Rigid Rigid 
Flex FlexId 

type Scope = RigidId -> Bool Source

Which rigid variables a flex may be instatiated to.

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

isBelow r w r' checks, if r and r' are connected by w (meaning w not infinite), whether r + w <= r'. Precondition: not the same rigid variable.

data Constraint Source

A constraint is an edge in the graph.


NewFlex FlexId Scope 
Arc Node Int Node

For Arc v1 k v2 at least one of v1 or v2 is a MetaV (Flex), the other a MetaV or a Var (Rigid). If k <= 0 this means suc^(-k) v1 <= v2 otherwise v1 <= suc^k v3.

data Graph Source




flexScope :: Map FlexId Scope

Scope for each flexible var.

nodeMap :: Map Node NodeId

Node labels to node numbers.

intMap :: Map NodeId Node

Node numbers to node labels.

nextNode :: NodeId

Number of nodes n.

graph :: NodeId -> NodeId -> Weight

The edges (restrict to [0..n[).

initGraph :: Graph Source

The empty graph: no nodes, edges are all undefined (infinity weight).

type GM = State Graph Source

The Graph Monad, for constructing a graph iteratively.

addFlex :: FlexId -> Scope -> GM () Source

Add a size meta node.

addNode :: Node -> GM Int Source

Lookup identifier of a node. If not present, it is added first.

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

addEdge n1 k n2 improves the weight of egde n1->n2 to be at most k. Also adds nodes if not yet present.

data LegendMatrix a b c Source

A matrix with row descriptions in b and column descriptions in c.




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


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

type Solution = Map Int SizeExpr Source

A solution assigns to each flexible variable a size expression which is either a constant or a v + n for a rigid variable v.

data SizeExpr Source


SizeVar RigidId Int

e.g. x + 5

SizeConst Weight

a number or infinity


sizeRigid :: Rigid -> Int -> SizeExpr Source

sizeRigid r n returns the size expression corresponding to r + n

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

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

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

prop_smaller :: Nat -> Property Source

Check that no edges get longer when completing a graph.

prop_path :: Nat -> Property Source

Check that all transitive edges are added.

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

prop_disjoint :: Nat -> Property Source

Check that no edges are added between components.

prop_stable :: Nat -> Property Source