Agda.Utils.Warshall

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.

Documentation

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

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

data Weight

Edge weight in the graph, forming a semi ring.

Constructors

Finite Int

Infinite

Instances

Eq Weight

Defined in Agda.Utils.Warshall

Methods

(==) :: Weight -> Weight -> Bool

(/=) :: Weight -> Weight -> Bool

Ord Weight

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

Show Weight

Defined in Agda.Utils.Warshall

Methods

showsPrec :: Int -> Weight -> ShowS

show :: Weight -> String

showList :: [Weight] -> ShowS

SemiRing Weight

Defined in Agda.Utils.Warshall

Methods

ozero :: Weight

oone :: Weight

oplus :: Weight -> Weight -> Weight

otimes :: Weight -> Weight -> Weight

inc :: Weight -> Int -> Weight

data Node

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

Eq Node

Defined in Agda.Utils.Warshall

Methods

(==) :: Node -> Node -> Bool

(/=) :: Node -> Node -> Bool

Ord Node

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

Show Node

Defined in Agda.Utils.Warshall

Methods

showsPrec :: Int -> Node -> ShowS

show :: Node -> String

showList :: [Node] -> ShowS

data Rigid

Constructors

RConst Weight

RVar RigidId

Instances

Eq Rigid

Defined in Agda.Utils.Warshall

Methods

(==) :: Rigid -> Rigid -> Bool

(/=) :: Rigid -> Rigid -> Bool

Ord Rigid

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

Show Rigid

Defined in Agda.Utils.Warshall

Methods

showsPrec :: Int -> Rigid -> ShowS

show :: Rigid -> String

showList :: [Rigid] -> ShowS

type NodeId = Int

type RigidId = Int

type FlexId = Int

type Scope = RigidId -> Bool

Which rigid variables a flex may be instatiated to.

infinite :: Rigid -> Bool

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

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

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

Show Constraint

Defined in Agda.Utils.Warshall

Methods

showsPrec :: Int -> Constraint -> ShowS

show :: Constraint -> String

showList :: [Constraint] -> ShowS

type Constraints = [Constraint]

emptyConstraints :: Constraints

data Graph

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

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

type GM = State Graph

The Graph Monad, for constructing a graph iteratively.

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

Add a size meta node.

addNode :: Node -> GM Int

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

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

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

buildGraph :: Constraints -> Graph

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

data LegendMatrix a b c

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

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

Defined in Agda.Utils.Warshall

Methods

showsPrec :: Int -> LegendMatrix a b c -> ShowS

show :: LegendMatrix a b c -> String

showList :: [LegendMatrix a b c] -> ShowS

type Solution = Map Int SizeExpr

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

extendSolution :: Solution -> Int -> SizeExpr -> Solution

data SizeExpr

Constructors

SizeVar RigidId Int

e.g. x + 5

SizeConst Weight

a number or infinity

Instances

Show SizeExpr

Defined in Agda.Utils.Warshall

Methods

showsPrec :: Int -> SizeExpr -> ShowS

show :: SizeExpr -> String

showList :: [SizeExpr] -> ShowS

sizeRigid :: Rigid -> Int -> SizeExpr

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

solve :: Constraints -> Maybe Solution