Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- type Graph r f a = Graph (Node r f) a
- type Edge' r f a = Edge (Node r f) a
- type Key r f = Edge' r f ()
- type Nodes r f = Nodes (Node r f)
- type LabelledEdge r f = Edge' r f Label
- src :: Edge n e -> n
- dest :: Edge n e -> n
- lookupEdge :: Ord n => Graph n e -> n -> n -> Maybe e
- graphToList :: Graph n e -> [Edge n e]
- graphFromList :: Ord n => [Edge n e] -> Graph n e
- insertEdge :: (Ord n, MeetSemiLattice e, Top e) => Edge n e -> Graph n e -> Graph n e
- outgoing :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
- incoming :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
- setFoldl :: (b -> a -> b) -> b -> Set a -> b
- transClos :: forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
- data Weight
- class Negative a where
- data Label
- toWeight :: Label -> Weight
- data Node rigid flex
- isFlexNode :: Node rigid flex -> Maybe flex
- isZeroNode :: Node rigid flex -> Bool
- isInftyNode :: Node rigid flex -> Bool
- nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
- type Graphs r f a = [Graph r f a]
- emptyGraphs :: Graphs r f a
- mentions :: (Ord r, Ord f) => Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
- addEdge :: (Ord r, Ord f, MeetSemiLattice a, Top a) => Edge' r f a -> Graphs r f a -> Graphs r f a
- reflClos :: (Ord r, Ord f, Dioid a) => Set (Node r f) -> Graph r f a -> Graph r f a
- implies :: (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
- nodeFromSizeExpr :: SizeExpr' rigid flex -> (Node rigid flex, Offset)
- edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
- graphFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graph rigid flex Label
- graphsFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graphs rigid flex Label
- type Hyp = Constraint
- type Hyp' = Constraint'
- type HypGraph r f = Graph r f Label
- hypGraph :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) => Set rigid -> [Hyp' rigid flex] -> Either Error (HypGraph rigid flex)
- hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label
- simplifyWithHypotheses :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) => HypGraph rigid flex -> [Constraint' rigid flex] -> Either Error [Constraint' rigid flex]
- type ConGraph r f = Graph r f Label
- constraintGraph :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either Error (ConGraph r f)
- type ConGraphs r f = Graphs r f Label
- constraintGraphs :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either Error ([f], ConGraphs r f)
- infinityFlexs :: (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
- class SetToInfty f a where
- setToInfty :: [f] -> a -> a
- type Bound r f = Map f (Set (SizeExpr' r f))
- emptyBound :: Bound r f
- data Bounds r f = Bounds {
- lowerBounds :: Bound r f
- upperBounds :: Bound r f
- mustBeFinite :: Set f
- edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
- edgeToUpperBound :: LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
- graphToLowerBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
- graphToUpperBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> (Bound r f, Set f)
- bounds :: (Ord r, Ord f) => ConGraph r f -> Bounds r f
- smallest :: (Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
- largest :: (Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
- commonSuccs :: (Ord r, Ord f) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
- commonPreds :: (Ord r, Ord f) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
- lub' :: forall r f. (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)
- glb' :: forall r f. (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)
- lub :: (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)
- glb :: (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)
- findRigidBelow :: (Ord r, Ord f) => HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
- solveGraph :: (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)
- solveGraphs :: (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)
- verifySolution :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) => HypGraph r f -> [Constraint' r f] -> Solution r f -> Either Error ()
- iterateSolver :: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) => Polarities f -> HypGraph r f -> [Constraint' r f] -> Solution r f -> Either Error (Solution r f)
- testSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]
- testLub :: (Pretty f, Ord f, Show f) => Maybe (SizeExpr' [Char] f)
Documentation
type LabelledEdge r f = Edge' r f Label Source #
graphToList :: Graph n e -> [Edge n e] Source #
insertEdge :: (Ord n, MeetSemiLattice e, Top e) => Edge n e -> Graph n e -> Graph n 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 a -> Graph n a Source #
Floyd-Warshall algorithm.
Edge weights
Instances
Pretty Weight Source # | |
Dioid Weight Source # | |
MeetSemiLattice Weight Source # | |
Top Weight Source # | |
Negative Weight Source # | |
Enum Weight Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver | |
Num Weight Source # | Partial implementation of |
Show Weight Source # | |
Eq Weight Source # | |
Ord Weight Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver | |
Plus Offset Weight Weight Source # | |
Plus Weight Offset Weight Source # | |
Plus (SizeExpr' r f) Weight (SizeExpr' r f) Source # | |
class Negative a where Source #
Test for negativity, used to detect negative cycles.
Instances
Negative Offset Source # | |
Negative Label Source # | |
Negative Weight Source # | |
Negative Int 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 |
(Ord r, Ord f, Negative a) => Negative (Graphs r f a) Source # | |
Edge labels
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. ]
Instances
Pretty Label Source # | |
Dioid Label Source # | |
MeetSemiLattice Label Source # | |
Top Label Source # | |
Negative Label Source # | |
Show Label Source # | |
Eq Label Source # | |
Ord Label Source # | |
(Ord r, Ord f) => SetToInfty f (ConGraph r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> ConGraph r f -> ConGraph r f Source # | |
Plus (SizeExpr' r f) Label (SizeExpr' r f) Source # | |
Semiring with idempotent +
== dioid
Graphs
Nodes
Instances
(Ord r, Ord f) => SetToInfty f (ConGraph r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> ConGraph r f -> ConGraph r f Source # | |
Eq f => SetToInfty f (Node r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> Node r f -> Node r f Source # | |
Eq f => SetToInfty f (Edge' r f a) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> Edge' r f a -> Edge' r f a Source # | |
(Pretty rigid, Pretty flex) => Pretty (Node rigid flex) Source # | |
(Show rigid, Show flex) => Show (Node rigid flex) Source # | |
(Eq rigid, Eq flex) => Eq (Node rigid flex) Source # | |
(Ord rigid, Ord flex) => Ord (Node rigid flex) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver compare :: Node rigid flex -> Node rigid flex -> Ordering # (<) :: Node rigid flex -> Node rigid flex -> Bool # (<=) :: Node rigid flex -> Node rigid flex -> Bool # (>) :: Node rigid flex -> Node rigid flex -> Bool # (>=) :: Node rigid flex -> Node rigid flex -> Bool # max :: Node rigid flex -> Node rigid flex -> Node rigid flex # min :: Node rigid flex -> Node rigid flex -> Node rigid flex # | |
(Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) Source # | |
(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) Source # | |
(Ord r, Ord f, Top a) => Top (Edge' 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 |
(Ord r, Ord f, Negative a) => Negative (Graphs r f a) Source # | |
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 #
Edges
Graphs
emptyGraphs :: Graphs r f a Source #
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, 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, Pretty r, Pretty f, Pretty a, Top a, Ord a, Negative a) => Graph r f a -> Graph r f a -> Bool Source #
h
if any edge in implies
gg
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.
edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex 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 Hyp = Constraint Source #
type Hyp' = Constraint' Source #
hypGraph :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) => Set rigid -> [Hyp' rigid flex] -> Either Error (HypGraph rigid flex) Source #
simplifyWithHypotheses :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) => HypGraph rigid flex -> [Constraint' rigid flex] -> Either Error [Constraint' rigid flex] Source #
constraintGraph :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either Error (ConGraph r f) Source #
constraintGraphs :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] -> HypGraph r f -> Either Error ([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 #
setToInfty :: [f] -> a -> a Source #
Instances
(Ord r, Ord f) => SetToInfty f (ConGraph r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> ConGraph r f -> ConGraph r f Source # | |
Eq f => SetToInfty f (Node r f) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> Node r f -> Node r f Source # | |
Eq f => SetToInfty f (Edge' r f a) Source # | |
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver setToInfty :: [f] -> Edge' r f a -> Edge' r f a Source # |
Compute solution from constraint graph.
emptyBound :: Bound r f Source #
Bounds | |
|
edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f) Source #
Compute a lower bound for a flexible from an edge.
edgeToUpperBound :: 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) => 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) => 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, Pretty r, Pretty 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, Pretty r, Pretty 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, Pretty r, Pretty 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, Pretty r, Pretty 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.
solveGraph :: (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) Source #
solveGraphs :: (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) Source #
Solve a forest of constraint graphs relative to a hypotheses graph. Concatenate individual solutions.
Verify solution
verifySolution :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) => HypGraph r f -> [Constraint' r f] -> Solution r f -> Either Error () Source #
Check that after substitution of the solution, constraints are implied by hypotheses.
:: (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.