Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Utils.Warshall

Description

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.

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 :: Constraints
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 :: Solution
extendSolution :: Solution -> Int -> SizeExpr -> Solution
data SizeExpr
- = SizeVar RigidId Int
- | SizeConst Weight
sizeRigid :: Rigid -> Int -> SizeExpr
solve :: Constraints -> Maybe Solution

Documentation

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

warshall :: SemiRing a => Matrix a -> Matrix 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.

Constructors

Finite Int
Infinite

Instances

Instances details

Pretty Weight Source #
Instance details Defined in Agda.Utils.Warshall Methods pretty :: Weight -> Doc Source # prettyPrec :: Int -> Weight -> Doc Source # prettyList :: [Weight] -> Doc Source #
SemiRing Weight Source #
Instance details Defined in Agda.Utils.Warshall Methods ozero :: Weight Source # oone :: Weight Source # oplus :: Weight -> Weight -> Weight Source # otimes :: Weight -> Weight -> Weight Source #
Show Weight Source #
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> Weight -> ShowS # show :: Weight -> String # showList :: [Weight] -> ShowS #
Eq Weight Source #
Instance details Defined in Agda.Utils.Warshall Methods (==) :: Weight -> Weight -> Bool # (/=) :: Weight -> Weight -> Bool #
Ord Weight Source #
Instance details Defined in Agda.Utils.Warshall Methods compare :: Weight -> Weight -> Ordering # (<) :: Weight -> Weight -> Bool # (<=) :: Weight -> Weight -> Bool # (>) :: Weight -> Weight -> Bool # (>=) :: Weight -> Weight -> Bool # max :: Weight -> Weight -> Weight # min :: Weight -> Weight -> Weight #

inc :: Weight -> Int -> Weight Source #

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

Constructors

Rigid Rigid
Flex FlexId

Instances

Instances details

Pretty Node Source #
Instance details Defined in Agda.Utils.Warshall Methods pretty :: Node -> Doc Source # prettyPrec :: Int -> Node -> Doc Source # prettyList :: [Node] -> Doc Source #
Eq Node Source #
Instance details Defined in Agda.Utils.Warshall Methods (==) :: Node -> Node -> Bool # (/=) :: Node -> Node -> Bool #
Ord Node Source #
Instance details Defined in Agda.Utils.Warshall Methods compare :: Node -> Node -> Ordering # (<) :: Node -> Node -> Bool # (<=) :: Node -> Node -> Bool # (>) :: Node -> Node -> Bool # (>=) :: Node -> Node -> Bool # max :: Node -> Node -> Node # min :: Node -> Node -> Node #

data Rigid Source #

Constructors

RConst Weight
RVar RigidId

Instances

Instances details

Eq Rigid Source #
Instance details Defined in Agda.Utils.Warshall Methods (==) :: Rigid -> Rigid -> Bool # (/=) :: Rigid -> Rigid -> Bool #
Ord Rigid Source #
Instance details Defined in Agda.Utils.Warshall Methods compare :: Rigid -> Rigid -> Ordering # (<) :: Rigid -> Rigid -> Bool # (<=) :: Rigid -> Rigid -> Bool # (>) :: Rigid -> Rigid -> Bool # (>=) :: Rigid -> Rigid -> Bool # max :: Rigid -> Rigid -> Rigid # min :: Rigid -> Rigid -> Rigid #

type NodeId = Int Source #

type RigidId = Int Source #

type FlexId = Int Source #

type Scope = RigidId -> Bool Source #

Which rigid variables a flex may be instatiated to.

infinite :: Rigid -> Bool Source #

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.

Constructors

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`.

Instances

Instances details

Pretty Constraint Source #
Instance details Defined in Agda.Utils.Warshall Methods pretty :: Constraint -> Doc Source # prettyPrec :: Int -> Constraint -> Doc Source # prettyList :: [Constraint] -> Doc Source #

type Constraints = [Constraint] Source #

emptyConstraints :: Constraints Source #

data Graph Source #

Constructors

Graph
Fields 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.

addConstraint :: Constraint -> GM () Source #

buildGraph :: Constraints -> Graph Source #

mkMatrix :: Int -> (Int -> Int -> Weight) -> Matrix Weight Source #

data LegendMatrix a b c Source #

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

Constructors

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

Instances

Instances details

(Pretty a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) Source #
Instance details Defined in Agda.Utils.Warshall Methods pretty :: LegendMatrix a b c -> Doc Source # prettyPrec :: Int -> LegendMatrix a b c -> Doc Source # prettyList :: [LegendMatrix a b c] -> Doc 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.

emptySolution :: Solution Source #

extendSolution :: Solution -> Int -> SizeExpr -> Solution Source #

data SizeExpr Source #

Constructors

SizeVar RigidId Int	e.g. x + 5
SizeConst Weight	a number or infinity

Instances

Instances details

Pretty SizeExpr Source #
Instance details Defined in Agda.Utils.Warshall Methods pretty :: SizeExpr -> Doc Source # prettyPrec :: Int -> SizeExpr -> Doc Source # prettyList :: [SizeExpr] -> Doc Source #

sizeRigid :: Rigid -> Int -> SizeExpr Source #

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

solve :: Constraints -> Maybe Solution Source #