Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Documentation

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.

Constructors

Finite Int 
Infinite 

Instances

Instances details
Pretty Weight Source # 
Instance details

Defined in Agda.Utils.Warshall

SemiRing Weight Source # 
Instance details

Defined in Agda.Utils.Warshall

Show Weight Source # 
Instance details

Defined in Agda.Utils.Warshall

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

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

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

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

data Graph Source #

Constructors

Graph 

Fields

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.

Constructors

LegendMatrix 

Fields

Instances

Instances details
(Pretty a, Pretty b, Pretty c) => Pretty (LegendMatrix a b c) Source # 
Instance details

Defined in Agda.Utils.Warshall

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 #

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

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

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