Call graphs and related concepts, more or less as defined in "A Predicative Analysis of Structural Recursion" by Andreas Abel and Thorsten Altenkirch.
- data Order
- (.*.) :: Order -> Order -> Order
- supremum :: [Order] -> Order
- type Index = Integer
- newtype CallMatrix = CallMatrix {}
- (>*<) :: Call -> Call -> Call
- callMatrixInvariant :: CallMatrix -> Bool
- data Call = Call {}
- callInvariant :: Call -> Bool
- data CallGraph meta
- callGraphInvariant :: CallGraph meta -> Bool
- fromList :: Monoid meta => [(Call, meta)] -> CallGraph meta
- toList :: CallGraph meta -> [(Call, meta)]
- empty :: CallGraph meta
- union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph meta
- insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph meta
- complete :: Monoid meta => CallGraph meta -> CallGraph meta
- showBehaviour :: Show meta => CallGraph meta -> String
- tests :: IO Bool
Structural orderings
(.*.) :: Order -> Order -> OrderSource
Multiplication of Order
s. (Corresponds to sequential
composition.)
Call matrices
newtype CallMatrix Source
Call matrices. Note the call matrix invariant
(callMatrixInvariant
).
callMatrixInvariant :: CallMatrix -> BoolSource
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 thej
-th argument to thetarget
function is structurally strictly smaller than thei
-th pattern. -
Le
(less than or equal) if thej
-th argument to thetarget
function is structurally smaller than thei
-th pattern. -
Unknown
otherwise.
The structural ordering used is defined in the paper referred to above.
callInvariant :: Call -> BoolSource
Call
invariant.
Call graphs
A call graph is a set of calls. Every call also has some
associated meta information, which should be Monoid
al so that the
meta information for different calls can be combined when the calls
are combined.
callGraphInvariant :: CallGraph meta -> BoolSource
CallGraph
invariant.
fromList :: Monoid meta => [(Call, meta)] -> CallGraph metaSource
Converts a list of calls with associated meta information to a call graph.
toList :: CallGraph meta -> [(Call, meta)]Source
Converts a call graph to a list of calls with associated meta information.
union :: Monoid meta => CallGraph meta -> CallGraph meta -> CallGraph metaSource
Takes the union of two call graphs.
insert :: Monoid meta => Call -> meta -> CallGraph meta -> CallGraph metaSource
Inserts a call into a call graph.
complete :: Monoid meta => CallGraph meta -> CallGraph metaSource
completes the call graph complete
cscs
. 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.
showBehaviour :: Show meta => CallGraph meta -> StringSource
Displays the recursion behaviour corresponding to a call graph.