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

Agda.TypeChecking.SizedTypes.WarshallSolver

Synopsis

Documentation

type Graph r f a = Graph (Node r f) (Node r f) a Source

type Edge' r f a = Edge (Node r f) (Node r f) a Source

type Key r f = Edge' r f () Source

type Nodes r f = Nodes (Node r f) Source

src :: Edge s t e -> s Source

dest :: Edge s t e -> t Source

lookupEdge :: (Ord s, Ord t) => Graph s t e -> s -> t -> Maybe e Source

graphToList :: (Ord s, Ord t) => Graph s t e -> [Edge s t e] Source

graphFromList :: (Ord s, Ord t) => [Edge s t e] -> Graph s t e Source

insertEdge :: (Ord s, Ord t, MeetSemiLattice e, Top e) => Edge s t e -> Graph s t e -> Graph s t e Source

outgoing :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a] Source

Compute list of edges that start in a given node.

incoming :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a] Source

Compute list of edges that target a given node.

Note: expensive for unidirectional graph representations.

setFoldl :: (b -> a -> b) -> b -> Set a -> b Source

`Set.foldl` does not exist in legacy versions of the `containers` package.

transClos :: forall n a. (Ord n, Dioid a) => Graph n n a -> Graph n n a Source

Floyd-Warshall algorithm.

Edge weights

data Weight Source

Constructors

 Offset Offset Infinity

Instances

 Source Source Source Partial implementation of `Num`. Source Source Arbitrary Weight Source Source Source Source Source Source Source Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source

class Negative a where Source

Test for negativity, used to detect negative cycles.

Methods

negative :: a -> Bool Source

Instances

 Source Source Source Source (Ord r, Ord f, Negative a) => Negative (Graphs r f a) Source Negative a => Negative (Edge' r f a) Source An edge is negative if its label is. (Ord r, Ord f, Negative a) => Negative (Graph r f a) Source A graph is `negative` if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.

Edge labels

data Label Source

Going from `Lt` to `Le` is `pred`, going from `Le` to `Lt` is `succ`.

`X --(R,n)--> Y` means `X (R) Y + n`. [ ... if `n` positive and `X + (-n) (R) Y` if `n` negative. ]

Constructors

 Label Fieldslcmp :: Cmp loffset :: Offset LInf Nodes not connected.

Instances

 Source Source Source Arbitrary Label Source Source Source Source Source Source (Ord r, Ord f) => SetToInfty f (ConGraph r f) Source Plus (SizeExpr' r f) Label (SizeExpr' r f) Source

Convert a label to a weight, decrementing in case of `Lt`.

Graphs

Nodes

data Node rigid flex Source

Constructors

 NodeZero NodeInfty NodeRigid rigid NodeFlex flex

Instances

 (Ord r, Ord f) => SetToInfty f (ConGraph r f) Source Eq f => SetToInfty f (Node r f) Source Eq f => SetToInfty f (Edge' r f a) Source (Eq rigid, Eq flex) => Eq (Node rigid flex) Source (Ord rigid, Ord flex) => Ord (Node rigid flex) Source (Show rigid, Show flex) => Show (Node rigid flex) Source (Show r, Show f, Show a, Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) Source (Show r, Show f, Show a, Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) Source (Ord r, Ord f, Top a) => Top (Edge' r f a) Source (Ord r, Ord f, Negative a) => Negative (Graphs r f a) Source Negative a => Negative (Edge' r f a) Source An edge is negative if its label is. (Ord r, Ord f, Negative a) => Negative (Graph r f a) Source A graph is `negative` if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.

isFlexNode :: Node rigid flex -> Maybe flex Source

isZeroNode :: Node rigid flex -> Bool Source

isInftyNode :: Node rigid flex -> Bool Source

nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex Source

Graphs

type Graphs r f a = [Graph r f a] Source

A graph forest.

mentions :: (Ord r, Ord f) => Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a) Source

Split a list of graphs `gs` into those that mention node `n` and those that do not. If `n` is zero or infinity, we regard it as "not mentioned".

addEdge :: (Ord r, Ord f, MeetSemiLattice a, Top a) => Edge' r f a -> Graphs r f a -> Graphs r f a Source

Add an edge to a graph forest. Graphs that share a node with the edge are joined.

reflClos :: (Ord r, Ord f, Show a, Dioid a) => Set (Node r f) -> Graph r f a -> Graph r f a Source

Reflexive closure. Add edges `0 -> n -> n -> oo` for all nodes `n`.

implies :: (Ord r, Ord f, Show r, Show f, Show a, Top a, Ord a, Negative a) => Graph r f a -> Graph r f a -> Bool Source

`h implies g` if any edge in `g` between rigids and constants is implied by a corresponding edge in `h`, which means that the edge in `g` carries at most the information of the one in `h`.

Application: Constraint implication: Constraints are compatible with hypotheses.

nodeFromSizeExpr :: SizeExpr' rigid flex -> (Node rigid flex, Offset) Source

graphFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graph rigid flex Label Source

Build a graph from list of simplified constraints.

graphsFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graphs rigid flex Label Source

Build a graph from list of simplified constraints.

type HypGraph r f = Graph r f Label Source

hypGraph :: (Ord rigid, Ord flex) => Set rigid -> [Hyp' rigid flex] -> Maybe (HypGraph rigid flex) Source

hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label Source

simplifyWithHypotheses :: (Ord rigid, Ord flex) => HypGraph rigid flex -> [Constraint' rigid flex] -> Maybe [Constraint' rigid flex] Source

type ConGraph r f = Graph r f Label Source

constraintGraph :: (Ord r, Ord f, Show r, Show f) => [Constraint' r f] -> HypGraph r f -> Maybe (ConGraph r f) Source

type ConGraphs r f = Graphs r f Label Source

constraintGraphs :: (Ord r, Ord f, Show r, Show f) => [Constraint' r f] -> HypGraph r f -> Maybe ([f], ConGraphs r f) Source

infinityFlexs :: (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f) Source

If we have an edge `X + n <= X` (with n >= 0), we must set `X = oo`.

class SetToInfty f a where Source

Methods

setToInfty :: [f] -> a -> a Source

Instances

 (Ord r, Ord f) => SetToInfty f (ConGraph r f) Source Eq f => SetToInfty f (Node r f) Source Eq f => SetToInfty f (Edge' r f a) Source

Compute solution from constraint graph.

type Bound r f = Map f (Set (SizeExpr' r f)) Source

Lower or upper bound for a flexible variable

data Bounds r f Source

Constructors

 Bounds FieldslowerBounds :: Bound r f upperBounds :: Bound r f mustBeFinite :: Set f

edgeToLowerBound :: (Ord r, Ord f) => LabelledEdge r f -> Maybe (f, SizeExpr' r f) Source

Compute a lower bound for a flexible from an edge.

edgeToUpperBound :: (Ord r, Ord f) => LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f) Source

Compute an upper bound for a flexible from an edge.

graphToLowerBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f Source

Compute the lower bounds for all flexibles in a graph.

graphToUpperBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> (Bound r f, Set f) Source

Compute the upper bounds for all flexibles in a graph.

bounds :: (Ord r, Ord f) => ConGraph r f -> Bounds r f Source

Compute the bounds for all flexibles in a graph.

smallest :: (Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f] Source

Compute the relative minima in a set of nodes (those that do not have a predecessor in the set).

largest :: (Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f] Source

Compute the relative maxima in a set of nodes (those that do not have a successor in the set).

commonSuccs :: (Ord r, Ord f, Dioid a) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a] Source

Given source nodes n1,n2,... find all target nodes m1,m2, such that for all j, there are edges n_i --l_ij--> m_j for all i. Return these edges as a map from target notes to a list of edges. We assume the graph is reflexive-transitive.

commonPreds :: (Ord r, Ord f, Dioid a) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a] Source

Given target nodes m1,m2,... find all source nodes n1,n2, such that for all j, there are edges n_i --l_ij--> m_j for all i. Return these edges as a map from target notes to a list of edges. We assume the graph is reflexive-transitive.

lub' :: forall r f. (Ord r, Ord f, Show r, Show f) => HypGraph r f -> (Node r f, Offset) -> (Node r f, Offset) -> Maybe (SizeExpr' r f) Source

Compute the sup of two different rigids or a rigid and a constant.

glb' :: forall r f. (Ord r, Ord f, Show r, Show f) => HypGraph r f -> (Node r f, Offset) -> (Node r f, Offset) -> Maybe (SizeExpr' r f) Source

Compute the inf of two different rigids or a rigid and a constant.

lub :: (Ord r, Ord f, Show r, Show f) => HypGraph r f -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f) Source

Compute the least upper bound (sup).

glb :: (Ord r, Ord f, Show r, Show f) => HypGraph r f -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f) Source

Compute the greatest lower bound (inf) of size expressions relative to a hypotheses graph.

findRigidBelow :: (Ord r, Ord f, Show r, Show f) => HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f) Source

solveGraph :: (Ord r, Ord f, Show r, Show f) => Polarities f -> HypGraph r f -> ConGraph r f -> Either String (Solution r f) Source

solveGraphs :: (Ord r, Ord f, Show r, Show f) => Polarities f -> HypGraph r f -> ConGraphs r f -> Either String (Solution r f) Source

Solve a forest of constraint graphs relative to a hypotheses graph. Concatenate individual solutions.

Verify solution

verifySolution :: (Ord r, Ord f, Show r, Show f) => HypGraph r f -> [Constraint' r f] -> Solution r f -> Either String () Source

Check that after substitution of the solution, constraints are implied by hypotheses.