Safe Haskell  None 

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 String (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 String [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 String (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 String ([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, Show r, Show f) => Polarities f > HypGraph r f > ConGraph r f > Either String (Solution r f)
 solveGraphs :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) => Polarities f > HypGraph r f > ConGraphs r f > Either String (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 String ()
 iterateSolver :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) => Polarities f > HypGraph r f > [Constraint' r f] > Solution r f > Either String (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 #
FloydWarshall algorithm.
Edge weights
Instances
Enum Weight Source #  
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver  
Eq Weight Source #  
Num Weight Source #  Partial implementation of 
Ord Weight Source #  
Defined in Agda.TypeChecking.SizedTypes.WarshallSolver  
Show Weight Source #  
Dioid Weight Source #  
MeetSemiLattice Weight Source #  
Top Weight Source #  
Pretty Weight Source #  
Negative Weight Source #  
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 Int Source #  
Negative Offset Source #  
Negative Label Source #  
Negative Weight 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 
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
Eq Label Source #  
Ord Label Source #  
Show Label Source #  
Dioid Label Source #  
MeetSemiLattice Label Source #  
Top Label Source #  
Pretty Label Source #  
Negative 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 #  
(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 #  
(Show rigid, Show flex) => Show (Node rigid flex) Source #  
(Pretty rigid, Pretty flex) => Pretty (Node rigid flex) Source #  
(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 #  
(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 
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 String (HypGraph rigid flex) Source #
simplifyWithHypotheses :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) => HypGraph rigid flex > [Constraint' rigid flex] > Either String [Constraint' rigid flex] Source #
constraintGraph :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] > HypGraph r f > Either String (ConGraph r f) Source #
constraintGraphs :: (Ord r, Ord f, Pretty r, Pretty f) => [Constraint' r f] > HypGraph r f > Either String ([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 reflexivetransitive.
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 reflexivetransitive.
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, Show r, Show f) => Polarities f > HypGraph r f > ConGraph r f > Either String (Solution r f) Source #
solveGraphs :: (Ord r, Ord f, Pretty r, Pretty 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, Pretty r, Pretty 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.
:: (Ord r, Ord f, Pretty r, Pretty 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 String (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.