Agda.TypeChecking.SizedTypes.WarshallSolver

Documentation

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]

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]

Compute list of edges that target a given node.

Note: expensive for unidirectional graph representations.

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

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

Floyd-Warshall algorithm.

Edge weights

data Weight

Constructors

Offset Offset

Infinity

Instances

Pretty Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Weight -> Doc

prettyPrec :: Int -> Weight -> Doc

prettyList :: [Weight] -> Doc

Dioid Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

compose :: Weight -> Weight -> Weight

unitCompose :: Weight

MeetSemiLattice Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

meet :: Weight -> Weight -> Weight

Top Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

top :: Weight

isTop :: Weight -> Bool

Negative Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Weight -> Bool

Enum Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

succ :: Weight -> Weight

pred :: Weight -> Weight

toEnum :: Int -> Weight

fromEnum :: Weight -> Int

enumFrom :: Weight -> [Weight]

enumFromThen :: Weight -> Weight -> [Weight]

enumFromTo :: Weight -> Weight -> [Weight]

enumFromThenTo :: Weight -> Weight -> Weight -> [Weight]

Num Weight

Partial implementation of Num.

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

(+) :: Weight -> Weight -> Weight

(-) :: Weight -> Weight -> Weight

(*) :: Weight -> Weight -> Weight

negate :: Weight -> Weight

abs :: Weight -> Weight

signum :: Weight -> Weight

fromInteger :: Integer -> Weight

Show Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

showsPrec :: Int -> Weight -> ShowS

show :: Weight -> String

showList :: [Weight] -> ShowS

Eq Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

(==) :: Weight -> Weight -> Bool

(/=) :: Weight -> Weight -> Bool

Ord Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

compare :: Weight -> Weight -> Ordering

(<) :: Weight -> Weight -> Bool

(<=) :: Weight -> Weight -> Bool

(>) :: Weight -> Weight -> Bool

(>=) :: Weight -> Weight -> Bool

max :: Weight -> Weight -> Weight

min :: Weight -> Weight -> Weight

Plus Offset Weight Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Offset -> Weight -> Weight

Plus Weight Offset Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: Weight -> Offset -> Weight

Plus (SizeExpr' r f) Weight (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: SizeExpr' r f -> Weight -> SizeExpr' r f

class Negative a where

Test for negativity, used to detect negative cycles.

Methods

negative :: a -> Bool

Instances

Negative Offset

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Offset -> Bool

Negative Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Label -> Bool

Negative Weight

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Weight -> Bool

Negative Int

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Int -> Bool

Negative a => Negative (Edge' r f a)

An edge is negative if its label is.

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Edge' r f a -> Bool

(Ord r, Ord f, Negative a) => Negative (Graph r f a)

A graph is negative if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Graph r f a -> Bool

(Ord r, Ord f, Negative a) => Negative (Graphs r f a)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Graphs r f a -> Bool

Edge labels

data 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

Fields

• lcmp :: Cmp
• loffset :: Offset

LInf

Nodes not connected.

Instances

Pretty Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Label -> Doc

prettyPrec :: Int -> Label -> Doc

prettyList :: [Label] -> Doc

Dioid Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

compose :: Label -> Label -> Label

unitCompose :: Label

MeetSemiLattice Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

meet :: Label -> Label -> Label

Top Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

top :: Label

isTop :: Label -> Bool

Negative Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Label -> Bool

Show Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

showsPrec :: Int -> Label -> ShowS

show :: Label -> String

showList :: [Label] -> ShowS

Eq Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

(==) :: Label -> Label -> Bool

(/=) :: Label -> Label -> Bool

Ord Label

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

compare :: Label -> Label -> Ordering

(<) :: Label -> Label -> Bool

(<=) :: Label -> Label -> Bool

(>) :: Label -> Label -> Bool

(>=) :: Label -> Label -> Bool

max :: Label -> Label -> Label

min :: Label -> Label -> Label

(Ord r, Ord f) => SetToInfty f (ConGraph r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> ConGraph r f -> ConGraph r f

Plus (SizeExpr' r f) Label (SizeExpr' r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

plus :: SizeExpr' r f -> Label -> SizeExpr' r f

toWeight :: Label -> Weight

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

Semiring with idempotent + == dioid

Graphs

Nodes

data Node rigid flex

Constructors

NodeZero

NodeInfty

NodeRigid rigid

NodeFlex flex

Instances

(Ord r, Ord f) => SetToInfty f (ConGraph r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> ConGraph r f -> ConGraph r f

Eq f => SetToInfty f (Node r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> Node r f -> Node r f

Eq f => SetToInfty f (Edge' r f a)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> Edge' r f a -> Edge' r f a

(Pretty rigid, Pretty flex) => Pretty (Node rigid flex)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

pretty :: Node rigid flex -> Doc

prettyPrec :: Int -> Node rigid flex -> Doc

prettyList :: [Node rigid flex] -> Doc

(Show rigid, Show flex) => Show (Node rigid flex)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

showsPrec :: Int -> Node rigid flex -> ShowS

show :: Node rigid flex -> String

showList :: [Node rigid flex] -> ShowS

(Eq rigid, Eq flex) => Eq (Node rigid flex)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

(==) :: Node rigid flex -> Node rigid flex -> Bool

(/=) :: Node rigid flex -> Node rigid flex -> Bool

(Ord rigid, Ord flex) => Ord (Node rigid flex)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

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)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

compose :: Edge' r f a -> Edge' r f a -> Edge' r f a

unitCompose :: Edge' r f a

(Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

meet :: Edge' r f a -> Edge' r f a -> Edge' r f a

(Ord r, Ord f, Top a) => Top (Edge' r f a)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

top :: Edge' r f a

isTop :: Edge' r f a -> Bool

Negative a => Negative (Edge' r f a)

An edge is negative if its label is.

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Edge' r f a -> Bool

(Ord r, Ord f, Negative a) => Negative (Graph r f a)

A graph is negative if it contains a negative loop (diagonal edge). Makes sense on transitive graphs.

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Graph r f a -> Bool

(Ord r, Ord f, Negative a) => Negative (Graphs r f a)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

negative :: Graphs r f a -> Bool

isFlexNode :: Node rigid flex -> Maybe flex

isZeroNode :: Node rigid flex -> Bool

isInftyNode :: Node rigid flex -> Bool

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

Edges

Graphs

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

A graph forest.

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)

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

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

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

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)

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

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

Build a graph from list of simplified constraints.

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

Build a graph from list of simplified constraints.

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)

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

class SetToInfty f a where

Methods

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

Instances

(Ord r, Ord f) => SetToInfty f (ConGraph r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> ConGraph r f -> ConGraph r f

Eq f => SetToInfty f (Node r f)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> Node r f -> Node r f

Eq f => SetToInfty f (Edge' r f a)

Defined in Agda.TypeChecking.SizedTypes.WarshallSolver

Methods

setToInfty :: [f] -> Edge' r f a -> Edge' r f a

Compute solution from constraint graph.

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

Lower or upper bound for a flexible variable

emptyBound :: Bound r f

data Bounds r f

Constructors

Bounds

Fields

• lowerBounds :: Bound r f
• upperBounds :: Bound r f
• mustBeFinite :: Set f

  These metas are < ∞.

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

Compute a lower bound for a flexible from an edge.

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

Compute an upper bound for a flexible from an edge.

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

Compute the lower bounds for all flexibles in a graph.

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

Compute the upper bounds for all flexibles in a graph.

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

Compute the bounds for all flexibles in a graph.

smallest :: (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).

largest :: (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).

commonSuccs :: (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.

commonPreds :: (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.

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)

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)

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)

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)

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

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)

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 ()

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

iterateSolver

Arguments

:: (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

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

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