Safe Haskell  SafeInfered 

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
 (.*.) :: [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 callmatrices. 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 filewise option.
See Call
for more information.
TODO: document orders which are callmatrices 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.
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.