Agda.TypeChecking.SizedTypes.WarshallSolver

Documentation

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

type Edge' r f a = Edge (Node r f) (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 s t e -> s

dest :: Edge s t e -> t

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

graphToList :: Graph s t e -> [Edge s t e]

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

insertEdge :: (Ord s, Ord t, MeetSemiLattice e, Top e) => Edge s t e -> Graph s t e -> Graph s t 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 n a -> Graph n n a

Floyd-Warshall algorithm.

Edge weights

data Weight

Constructors

Offset Offset

Infinity

Instances

Enum Weight

Eq Weight

Num Weight

Partial implementation of Num.

Ord Weight

Show Weight

Arbitrary Weight

Dioid Weight

MeetSemiLattice Weight

Top Weight

Negative Weight

Plus Offset Weight Weight

Plus Weight Offset Weight

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 Int

Negative Offset

Negative Label

Negative Weight

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

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

An edge is negative if its label is.

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

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

Eq Label

Ord Label

Show Label

Arbitrary Label

Dioid Label

MeetSemiLattice Label

Top Label

Negative Label

AsWeightRelation Label

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

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)

Eq f => SetToInfty f (Node r f)

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

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

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

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

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

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

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

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

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

An edge is negative if its label is.

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

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, Show r, Show f, Show 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, Show rigid, Show 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, Show rigid, Show 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, Show r, Show 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, Show r, Show 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)

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)

Eq f => SetToInfty f (Node r f)

Eq f => SetToInfty f (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

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, 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, 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, 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, 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, Show r, Show f) => Polarities f -> HypGraph r f -> ConGraph r f -> Either String (Solution r f)

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

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

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

Tests

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

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