ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.SizedTypes.WarshallSolver

18 types
2 classes
52 values

PackageAgda-2.7.0.1
Exports72
LanguageHaskell2010
LicenceMIT
SourceWarshallSolver.hs

typetype Graph r f a = Graph (Node r f) a

typetype Edge' r f a = Edge (Node r f) a

typetype Key r f = Edge' r f ()

typetype Nodes r f = Nodes (Node r f)

typetype LabelledEdge r f = Edge' r f Label

valuesrc :: Edge n e -> n

valuedest :: Edge n e -> n

valuelookupEdge :: Ord n => Graph n e -> n -> n -> Maybe e

valuegraphToList :: Graph n e -> [Edge n e]

valuegraphFromList :: Ord n => [Edge n e] -> Graph n e

valueinsertEdge

:: (Ord n, MeetSemiLattice e, Top e)
=> Edge n e
-> Graph n e
-> Graph n e

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

Compute list of edges that start in a given node.

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

Compute list of edges that target a given node.

Note: expensive for unidirectional graph representations.

valuesetFoldl :: (b -> a -> b) -> b -> Set a -> b

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

valuetransClos :: (Ord n, Dioid a) => Graph n a -> Graph n a

Floyd-Warshall algorithm.

Edge weights

2 declarations

datadata Weight

Constructors

Offset Offset
Infinity

Instances13Enum, Eq, Num, Ord, Show, Pretty, …

Enum WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Eq WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Num WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Partial implementation of Num.
Ord WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Show WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Pretty WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Dioid WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
MeetSemiLattice WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Top WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus Offset Weight WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus Weight Offset WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus (SizeExpr' r f) Weight (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver

classclass Negative a where

Test for negativity, used to detect negative cycles.

Methods

negative :: a -> Bool

Instances7Negative, …

Negative OffsetDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative WeightDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative IntDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative a => Negative (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
An edge is negative if its label is.
(Ord r, Ord f, Negative a) => Negative (Graph r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
A graph is negative if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.
(Ord r, Ord f, Negative a) => Negative (Graphs r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver

Edge labels

2 declarations

datadata Label

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
- lcmp :: Cmp
- loffset :: Offset
LInf
Nodes not connected.

Instances10Eq, Ord, Show, Pretty, Dioid, MeetSemiLattice, …

Eq LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Ord LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Show LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Pretty LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Dioid LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
MeetSemiLattice LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Top LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative LabelDefined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord r, Ord f) => SetToInfty f (ConGraph r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Plus (SizeExpr' r f) Label (SizeExpr' r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver

valuetoWeight :: Label -> Weight

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

Semiring with idempotent + == dioid

0 declarations

Graphs

0 declarations

Nodes

datadata Node rigid flex

Constructors

NodeZero
NodeInfty
NodeRigid rigid
NodeFlex flex

Instances13SetToInfty, Eq, Ord, Show, Pretty, Dioid, …

Eq f => SetToInfty f (Node r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord r, Ord f) => SetToInfty f (ConGraph r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Eq f => SetToInfty f (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Eq rigid, Eq flex) => Eq (Node rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord rigid, Ord flex) => Ord (Node rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Show rigid, Show flex) => Show (Node rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Pretty rigid, Pretty flex) => Pretty (Node rigid flex)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord r, Ord f, Top a) => Top (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Negative a => Negative (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
An edge is negative if its label is.
(Ord r, Ord f, Negative a) => Negative (Graph r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
A graph is negative if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.
(Ord r, Ord f, Negative a) => Negative (Graphs r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver

valueisFlexNode :: Node rigid flex -> Maybe flex

valueisZeroNode :: Node rigid flex -> Bool

valueisInftyNode :: Node rigid flex -> Bool

valuenodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex

Edges

Graphs

typetype Graphs r f a = [Graph r f a]

A graph forest.

valueemptyGraphs :: Graphs r f a

valuementions

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

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

valueaddEdge

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

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

valuereflClos

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

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

valueimplies

:: (Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a, Negative a)
=> Graph r f a
-> Graph r f a
-> Bool

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.

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

valueedgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex

valuegraphFromConstraints

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

Build a graph from list of simplified constraints.

valuegraphsFromConstraints

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

Build a graph from list of simplified constraints.

typetype Error = TCM Doc

Error messages produced by the solver.

typetype CTrans r f = Constraint' r f -> Either Error [Constraint' r f]

valuesimplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f

typetype Hyp = Constraint

typetype Hyp' = Constraint'

typetype HypGraph r f = Graph r f Label

valuehypGraph

:: (Ord rigid, Ord flex, Pretty rigid, Pretty flex)
=> Set rigid
-> [Hyp' rigid flex]
-> Either Error (HypGraph rigid flex)

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

valuesimplifyWithHypotheses

:: (Ord rigid, Ord flex, Pretty rigid, Pretty flex)
=> HypGraph rigid flex
-> [Constraint' rigid flex]
-> Either Error [Constraint' rigid flex]

typetype ConGraph r f = Graph r f Label

valueconstraintGraph

:: (Ord r, Ord f, Pretty r, Pretty f)
=> [Constraint' r f]
-> HypGraph r f
-> Either Error (ConGraph r f)

typetype ConGraphs r f = Graphs r f Label

valueconstraintGraphs

:: (Ord r, Ord f, Pretty r, Pretty f)
=> [Constraint' r f]
-> HypGraph r f
-> Either Error ([f], ConGraphs r f)

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

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

classclass SetToInfty f a where

Methods

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

Instances3SetToInfty

Eq f => SetToInfty f (Node r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
(Ord r, Ord f) => SetToInfty f (ConGraph r f)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver
Eq f => SetToInfty f (Edge' r f a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.SizedTypes.WarshallSolver

Compute solution from constraint graph.

19 declarations

typetype Bound r f = Map f (Set (SizeExpr' r f))

Lower or upper bound for a flexible variable

valueemptyBound :: Bound r f

datadata Bounds r f

Constructors

Bounds
- lowerBounds :: Bound r f
- upperBounds :: Bound r f
- mustBeFinite :: Set f
  These metas are < ∞.

valueedgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)

Compute a lower bound for a flexible from an edge.

valueedgeToUpperBound :: LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)

Compute an upper bound for a flexible from an edge.

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

Compute the lower bounds for all flexibles in a graph.

valuegraphToUpperBounds

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

Compute the upper bounds for all flexibles in a graph.

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

Compute the bounds for all flexibles in a graph.

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

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

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

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

valuecommonSuccs

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

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.

valuecommonPreds

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

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.

valuelub'

:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)

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

valueglb'

:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> (Node r f, Offset)
-> (Node r f, Offset)
-> Maybe (SizeExpr' r f)

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

valuelub

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

Compute the least upper bound (sup).

valueglb

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

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

valuefindRigidBelow

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

valuesolveGraph

:: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> ConGraph r f
-> Either Error (Solution r f)

valuesolveGraphs

:: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
=> Polarities f
-> HypGraph r f
-> ConGraphs r f
-> Either Error (Solution r f)

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

Verify solution

2 declarations

valueverifySolution

:: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
=> HypGraph r f
-> [Constraint' r f]
-> Solution r f
-> Either Error ()

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

valueiterateSolver

:: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
=> Polarities f
Meta variable polarities (prefer lower or upper solution?).
-> HypGraph r f
Hypotheses (assumed to have no metas, so, fixed during iteration).
-> [Constraint' r f]
Constraints to solve.
-> Solution r f
Previous substitution (already applied to constraints).
-> Either Error (Solution r f)
Accumulated substition.

Iterate solver until no more metas can be solved.

This might trigger a (wanted) error on the second iteration (see Issue 2096) which would otherwise go unnoticed.

Tests

2 declarations

valuetestSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]

valuetestLub :: (Pretty f, Ord f, Show f) => Maybe (SizeExpr' [Char] f)