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

Safe Haskell | None
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

Eq Weight Source # |
Instance details Defined in Agda.Utils.Warshall Methods (==) :: Weight -> Weight -> Bool Source # (/=) :: Weight -> Weight -> Bool Source #
Ord Weight Source # |
Instance details Defined in Agda.Utils.Warshall Methods compare :: Weight -> Weight -> Ordering Source # (<) :: Weight -> Weight -> Bool Source # (<=) :: Weight -> Weight -> Bool Source # (>) :: Weight -> Weight -> Bool Source # (>=) :: Weight -> Weight -> Bool Source # max :: Weight -> Weight -> Weight Source # min :: Weight -> Weight -> Weight Source #
Show Weight Source # |
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> Weight -> ShowS Source # show :: Weight -> String Source # showList :: [Weight] -> ShowS 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 #

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 `Int`s), or - constants (like 0, infinity, or anything between).

Constructors

Rigid Rigid |
Flex FlexId |

Instances

Eq Node Source # |
Instance details Defined in Agda.Utils.Warshall Methods (==) :: Node -> Node -> Bool Source # (/=) :: Node -> Node -> Bool Source #
Ord Node Source # |
Instance details Defined in Agda.Utils.Warshall Methods compare :: Node -> Node -> Ordering Source # (<) :: Node -> Node -> Bool Source # (<=) :: Node -> Node -> Bool Source # (>) :: Node -> Node -> Bool Source # (>=) :: Node -> Node -> Bool Source # max :: Node -> Node -> Node Source # min :: Node -> Node -> Node Source #
Show Node Source # |
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> Node -> ShowS Source # show :: Node -> String Source # showList :: [Node] -> ShowS Source #

data Rigid Source #

Constructors

RConst Weight |
RVar RigidId |

Instances

Eq Rigid Source # |
Instance details Defined in Agda.Utils.Warshall Methods (==) :: Rigid -> Rigid -> Bool Source # (/=) :: Rigid -> Rigid -> Bool Source #
Ord Rigid Source # |
Instance details Defined in Agda.Utils.Warshall Methods compare :: Rigid -> Rigid -> Ordering Source # (<) :: Rigid -> Rigid -> Bool Source # (<=) :: Rigid -> Rigid -> Bool Source # (>) :: Rigid -> Rigid -> Bool Source # (>=) :: Rigid -> Rigid -> Bool Source # max :: Rigid -> Rigid -> Rigid Source # min :: Rigid -> Rigid -> Rigid Source #
Show Rigid Source # |
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> Rigid -> ShowS Source # show :: Rigid -> String Source # showList :: [Rigid] -> ShowS Source #

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

Show Constraint Source # |
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> Constraint -> ShowS Source # show :: Constraint -> String Source # showList :: [Constraint] -> ShowS 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

(Show a, Show b, Show c) => Show (LegendMatrix a b c) Source # |
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> LegendMatrix a b c -> ShowS Source # show :: LegendMatrix a b c -> String Source # showList :: [LegendMatrix a b c] -> ShowS 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

Show SizeExpr Source # |
Instance details Defined in Agda.Utils.Warshall Methods showsPrec :: Int -> SizeExpr -> ShowS Source # show :: SizeExpr -> String Source # showList :: [SizeExpr] -> ShowS Source #

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

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

solve :: Constraints -> Maybe Solution Source #