Agda.Termination.CallGraph

Call graphs and related concepts, more or less as defined in "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch.

Calls

type Node = Int

Call graph nodes.

Machine integer Int is sufficient, since we cannot index more than we have addresses on our machine.

type Call cinfo = Edge Node Node (CMSet cinfo)

Calls are edges in the call graph. It can be labelled with several call matrices if there are several pathes from one function to another.

mkCall :: Node -> Node -> CallMatrix -> cinfo -> Call cinfo

Make a call with a single matrix.

mkCall' :: Monoid cinfo => Node -> Node -> CallMatrix -> Call cinfo

Make a call with empty cinfo.

source :: Edge s t e -> s

Outgoing node.

target :: Edge s t e -> t

Incoming node.

callMatrixSet :: Call cinfo -> CMSet cinfo

(>*<) :: (CallComb a, ?cutoff :: CutOff) => a -> a -> a

Call graphs

newtype CallGraph cinfo

A call graph is a set of calls. Every call also has some associated meta information, which should be Monoidal so that the meta information for different calls can be combined when the calls are combined.

Constructors

CallGraph

Fields

theCallGraph :: Graph Node Node (CMSet cinfo)

Instances

Show cinfo => Show (CallGraph cinfo)

Monoid cinfo => Monoid (CallGraph cinfo)

CallGraph is a monoid under union.

Pretty cinfo => Pretty (CallGraph cinfo)

Displays the recursion behaviour corresponding to a call graph.

targetNodes :: CallGraph cinfo -> Set Node

Returns all the nodes with incoming edges. Somewhat expensive. O(e).

fromList :: Monoid cinfo => [Call cinfo] -> CallGraph cinfo

Converts a list of calls with associated meta information to a call graph.

toList :: CallGraph cinfo -> [Call cinfo]

Converts a call graph to a list of calls with associated meta information.

empty :: CallGraph cinfo

Creates an empty call graph.

null :: CallGraph cinfo -> Bool

Check whether the call graph is completely disconnected.

union :: Monoid cinfo => CallGraph cinfo -> CallGraph cinfo -> CallGraph cinfo

Takes the union of two call graphs.

insert :: Monoid cinfo => Node -> Node -> CallMatrix -> cinfo -> CallGraph cinfo -> CallGraph cinfo

Inserts a call into a call graph.

complete :: (?cutoff :: CutOff) => Monoid cinfo => CallGraph cinfo -> CallGraph cinfo

Call graph comparison. A graph cs' is ``worse'' than cs if it has a new edge (call) or a call got worse, which means that one of its elements that was better or equal to Le moved a step towards Un.

A call graph is complete if combining it with itself does not make it any worse. This is sound because of monotonicity: By combining a graph with itself, it can only get worse, but if it does not get worse after one such step, it gets never any worse.

complete cs completes the call graph cs. A call graph is complete if it contains all indirect calls; if f -> g and g -> h are present in the graph, then f -> h should also be present.

completionStep :: (?cutoff :: CutOff) => Monoid cinfo => CallGraph cinfo -> CallGraph cinfo -> (CallGraph cinfo, CallGraph cinfo)

Tests

tests :: IO Bool