|
Agda.Termination.CallGraph |
|
|
|
|
Description |
Call graphs and related concepts, more or less as defined in
"A Predicative Analysis of Structural Recursion" by
Andreas Abel and Thorsten Altenkirch.
|
|
Synopsis |
|
|
|
|
Structural orderings
|
|
|
The order called R in the paper referred to above. Note that
Unknown <= Le <= Lt.
See Call for more information.
TODO: document orders which are call-matrices themselves.
| Constructors | |
|
|
|
Multiplication of Orders. (Corresponds to sequential
composition.)
|
|
|
The supremum of a (possibly empty) list of Orders.
|
|
Call matrices
|
|
|
Call matrix indices.
|
|
|
|
|
|
Call combination.
Precondition: see <*>; furthermore the source of the first
argument should be equal to the target of the second one.
|
|
|
In a call matrix at most one element per row may be different
from Unknown.
|
|
Calls
|
|
|
This datatype encodes information about a single recursive
function application. The columns of the call matrix stand for
source function arguments (patterns); the first argument has
index 0, the second 1, and so on. The rows of the matrix stand for
target function arguments. Element (i, j) in the matrix should
be computed as follows:
- Lt (less than) if the j-th argument to the target
function is structurally strictly smaller than the i-th
pattern.
- Le (less than or equal) if the j-th argument to the
target function is structurally smaller than the i-th
pattern.
- Unknown otherwise.
The structural ordering used is defined in the paper referred to
above.
| Constructors | Call | | source :: Index | The function making the call.
| target :: Index | The function being called.
| cm :: CallMatrix | The call matrix describing the call.
|
|
|
|
|
|
Call invariant.
|
|
Call graphs
|
|
|
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.
|
|
|
|
CallGraph invariant.
|
|
|
Converts a list of calls with associated meta information to a
call graph.
|
|
|
Converts a call graph to a list of calls with associated meta
information.
|
|
|
Creates an empty call graph.
|
|
|
Takes the union of two call graphs.
|
|
|
Inserts a call into a call graph.
|
|
|
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.
|
|
|
Displays the recursion behaviour corresponding to a call graph.
|
|
Tests
|
|
|
|
Produced by Haddock version 2.6.0 |