tct-2.0.1: A Complexity Analyser for Term Rewrite Systems

Portabilityunportable
Stabilityunstable
MaintainerMartin Avanzini <martin.avanzini@uibk.ac.at>
Safe HaskellSafe-Infered

Tct.Method.DP.DependencyGraph

Contents

Description

This module provides dependency graphs.

Synopsis

Unified Graph Interface

Datatypes

type DependencyGraph n e = Gr n e

DependencyGraph n e is a Graph with node-labels n and edge-labels e

data Strictness

Constructors

StrictDP 
WeakDP 

Instances

type NodeId = Node

A node in the dependency graph. Most operations work on NodeIds. Use lookupNodeLabel to get the label of the node

Operations

nodes :: DependencyGraph n e -> [NodeId]

Returns the set of nodes.

lnodes :: DependencyGraph n e -> [(NodeId, n)]

Returns the set of nodes together with their labels.

roots :: DependencyGraph n e -> [NodeId]

Returns the list of nodes without predecessor.

leafs :: DependencyGraph n e -> [NodeId]

Returns the list of nodes without successor.

lookupNodeLabel :: DependencyGraph n e -> NodeId -> Maybe n

Returns the label of the given node, if present.

lookupNodeLabel' :: DependencyGraph n e -> NodeId -> n

Returns the label of the given node, if present. Otherwise an exception is raised

lookupNode :: Eq n => DependencyGraph n e -> n -> Maybe NodeId

Returns the node with given label.

lookupNode' :: Eq n => DependencyGraph n e -> n -> NodeId

Returns the node with given label. Otherwise an exception is raised

withNodeLabels :: DependencyGraph n e -> [NodeId] -> [(NodeId, Maybe n)]

List version of lookupNodeLabel.

withNodeLabels' :: DependencyGraph n e -> [NodeId] -> [(NodeId, n)]

List version of lookupNodeLabel'.

inverse :: DependencyGraph n e -> DependencyGraph n e

Returns the same graph with edges inversed.

topsort :: DependencyGraph n e -> [NodeId]

returns a topologically sorted set of nodes.

sccs :: DependencyGraph n e -> [[NodeId]]

returns the list of strongly connected components, including trivial ones.

undirect :: Eq e => DependencyGraph n e -> DependencyGraph n e

Make the graph undirected, i.e. for every edge from A to B, there exists an edge from B to A.

successors :: DependencyGraph n e -> NodeId -> [NodeId]

Returns the list of successors in a given node.

reachablesDfs :: DependencyGraph n e -> [NodeId] -> [NodeId]

reachable gr ns closes the list of nodes ns under the successor relation with respect to ns in a depth-first manner.

reachablesBfs :: DependencyGraph n e -> [NodeId] -> [NodeId]

reachable gr ns closes the list of nodes ns under the successor relation with respect to ns in a breath-first manner.

lsuccessors :: DependencyGraph n e -> NodeId -> [(NodeId, n, e)]

Returns the list of successors in a given node, including their labels.

predecessors :: DependencyGraph n e -> NodeId -> [NodeId]

Returns the list of predecessors in a given node.

lpredecessors :: DependencyGraph n e -> NodeId -> [(NodeId, n, e)]

Returns the list of predecessors in a given node, including their labels.

isEdgeTo :: DependencyGraph n e -> NodeId -> NodeId -> Bool

isEdgeTo dg n1 n2 checks wheter n2 is a successor of n1 in the dependency graph dg

isLEdgeTo :: Eq e => DependencyGraph n e -> NodeId -> e -> NodeId -> Bool

isLEdgeTo dg n1 l n2 checks wheter n2 is a successor of n1 in the dependency graph dg, where the edge from n1 to n2 is labeled by l.

subGraph :: DependencyGraph n e -> [NodeId] -> DependencyGraph n e

Computes the subgraph based on the given nodes.

Dependency Graph

Datatype

type DG = DependencyGraph DGNode Int

The dependency graph.

type DGNode = (Strictness, Rule)

Nodes of the DG are labeled by rules and their strictness-annotation.

data Approximation

Constructors

EdgStar

EDG* approximation

Trivial

Fully connected graph

ICapStar

Generalised EDG*

Instances

defaultApproximation :: Approximation

Construct an estimated dependency graph, using the given approximation.

estimatedDependencyGraph :: Approximation -> Problem -> DG

Congruence Graph

Datatype

type CDG = DependencyGraph CDGNode (Rule, Int)

The congruence dependency graph.

data CDGNode

Constructors

CongrNode 

Fields

theSCC :: [(NodeId, DGNode)]
 
isCyclic :: Bool
 

Instances

Operations

toCongruenceGraph :: DG -> CDG

Computes the congruence graph of a given dependency graph.

allRulesFromNode :: CDG -> NodeId -> [(Strictness, Rule)]

Returns the list of annotated rules of the given node.

allRulesFromNodes :: CDG -> [NodeId] -> [(Strictness, Rule)]

List version of allRulesFromNode.

congruence :: CDG -> NodeId -> [NodeId]

congruence cdg n returns the nodes from the original dependency graph (i.e., the one given to toCongruenceGraph) that is denoted by the congruence-node n.

isCyclicNode :: CDG -> NodeId -> Bool

isCyclicNode cdg n returns True iff there is an edge from a node in congruence cdg n to congruence cdg n in the original dependency graph (i.e., the one given to toCongruenceGraph).

Utilities

pprintCWDGNode :: CDG -> Signature -> Variables -> NodeId -> Doc

pprintCWDGNode cdg sig vars node is a default printer for the CDG-node node. It shows the nodes of the dependency graph denoted by node as a set.

pprintCWDG :: CDG -> Signature -> Variables -> ([NodeId] -> NodeId -> Doc) -> Doc

Default pretty printer for CDGs. Prints the given CDG in a tree-like shape.

pprintNodeSet :: [NodeId] -> Doc

Default pretty printer for set of nodes.

toGraphViz :: [(DG, Signature, Variables)] -> Bool -> DotGraph String

translates DG into a GraphViz graph.

saveGraphViz :: [(DG, Signature, Variables)] -> Bool -> FilePath -> IO FilePath

output DG as Svg.

graphvizShowDG :: [(DG, Signature, Variables)] -> IO ()

show a DG in a GraphViz canvas. * Misc

pprintLabeledRules :: PrettyPrintable l => String -> Signature -> Variables -> [(l, Rule)] -> Doc