Agda.Termination.CallGraph

Call graph nodes.

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

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.

Make a call with a single matrix.

Make a call with empty cinfo.

Outgoing node.

Incoming node.

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.

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

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

Takes the union of two call graphs.

Inserts a call into a call graph.

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.