Safe Haskell | None |
---|
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 = Mat (Matrix Integer Order)
- decr :: [cutoff :: Int] => Int -> Order
- increase :: Int -> Order -> Order
- decrease :: Int -> Order -> Order
- (.*.) :: [cutoff :: Int] => Order -> Order -> Order
- supremum :: [cutoff :: Int] => [Order] -> Order
- infimum :: [cutoff :: Int] => [Order] -> Order
- decreasing :: Order -> Bool
- le :: Order
- lt :: Order
- unknown :: Order
- orderMat :: Matrix Integer Order -> Order
- type Index = Integer
- newtype CallMatrix = CallMatrix {}
- (>*<) :: [cutoff :: Int] => 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 :: [cutoff :: Int] => Monoid meta => CallGraph meta -> CallGraph meta
- prettyBehaviour :: Show meta => CallGraph meta -> Doc
- tests :: IO Bool
Structural orderings
In the paper referred to above, there is an order R with
.
Unknown
<=
Le
<=
Lt
This is generalized to
where
Unknown
<=
'Decr k'Decr 1
replaces Lt
and Decr 0
replaces Le
.
A negative decrease means an increase. The generalization
allows the termination checker to record an increase by 1 which
can be compensated by a following decrease by 2 which results in
an overall decrease.
However, the termination checker of the paper itself terminates because
there are only finitely many different call-matrices. To maintain
termination of the terminator we set a cutoff
point which determines
how high the termination checker can count. This value should be
set by a global or file-wise option.
See Call
for more information.
TODO: document orders which are call-matrices themselves.
(.*.) :: [cutoff :: Int] => Order -> Order -> OrderSource
Multiplication of Order
s. (Corresponds to sequential
composition.)
supremum :: [cutoff :: Int] => [Order] -> OrderSource
The supremum of a (possibly empty) list of Order
s.
More information (i.e., more decrease) is bigger.
Unknown
is no information, thus, smallest.
infimum :: [cutoff :: Int] => [Order] -> OrderSource
The infimum of a (non empty) list of Order
s.
Unknown
is the least element, thus, dominant.
decreasing :: Order -> BoolSource
orderMat :: Matrix Integer Order -> OrderSource
Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.
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 :: [cutoff :: Int] => 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.
prettyBehaviour :: Show meta => CallGraph meta -> DocSource
Displays the recursion behaviour corresponding to a call graph.