Safe Haskell  None 

Language  Haskell98 
 type ArgumentIndex = Int
 newtype CallMatrix' a = CallMatrix {
 mat :: Matrix ArgumentIndex a
 type CallMatrix = CallMatrix' Order
 class CallComb a where
 data CallMatrixAug cinfo = CallMatrixAug {
 augCallMatrix :: CallMatrix
 augCallInfo :: cinfo
 noAug :: Monoid cinfo => CallMatrix > CallMatrixAug cinfo
 newtype CMSet cinfo = CMSet {
 cmSet :: Favorites (CallMatrixAug cinfo)
 insert :: CallMatrixAug cinfo > CMSet cinfo > CMSet cinfo
 union :: CMSet cinfo > CMSet cinfo > CMSet cinfo
 toList :: CMSet cinfo > [CallMatrixAug cinfo]
 callMatrix :: Size ArgumentIndex > Gen CallMatrix
 tests :: IO Bool
Documentation
type ArgumentIndex = Int Source
Call matrix indices = function argument indices.
Machine integer Int
is sufficient, since we cannot index more arguments
than we have addresses on our machine.
newtype CallMatrix' a Source
Call matrices.
A call matrix for a call f > g
has dimensions ar(g) × ar(f)
.
Each column corresponds to one formal argument of caller f
.
Each row corresponds to one argument in the call to g
.
In the presence of dot patterns, a call argument can be related
to several different formal arguments of f
.
See e.g. testsucceedDotPatternTermination.agda
:
data D : Nat > Set where cz : D zero c1 : forall n > D n > D (suc n) c2 : forall n > D n > D n f : forall n > D n > Nat f .zero cz = zero f .(suc n) (c1 n d) = f n (c2 n d) f n (c2 .n d) = f n d
Call matrices (without guardedness) are
1 1 n < suc n and n < c1 n d ? = c2 n d <= c1 n d = 1 n <= n and n < c2 n d ? 1 d < c2 n d
Here is a part of the original documentation for call matrices (kept for historical reasons):
This datatype encodes information about a single recursive
function application. The columns of the call matrix stand for
source
function arguments (patterns). The rows of the matrix stand for
target
function arguments. Element (i, j)
in the matrix should
be computed as follows:
CallMatrix  

Functor CallMatrix' Source  
Foldable CallMatrix' Source  
Traversable CallMatrix' Source  
Arbitrary CallMatrix Source  
Pretty CallMatrix Source  
CallComb CallMatrix Source  Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:

Eq a => Eq (CallMatrix' a) Source  
Ord a => Ord (CallMatrix' a) Source  
(Show a, HasZero a) => Show (CallMatrix' a) Source  
(CoArbitrary a, HasZero a) => CoArbitrary (CallMatrix' a) Source  
PartialOrd a => PartialOrd (CallMatrix' a) Source  
NotWorse (CallMatrix' Order) Source  
HasZero a => Diagonal (CallMatrix' a) a Source 
type CallMatrix = CallMatrix' Order Source
Call matrix multiplication and call combination.
CallComb CallMatrix Source  Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:

Monoid cinfo => CallComb (CMSet cinfo) Source  Call matrix set product is the Cartesian product. 
Monoid cinfo => CallComb (CallMatrixAug cinfo) Source  Augmented call matrix multiplication. 
Call matrix augmented with path information.
data CallMatrixAug cinfo Source
Call matrix augmented with path information.
CallMatrixAug  

Eq cinfo => Eq (CallMatrixAug cinfo) Source  
Show cinfo => Show (CallMatrixAug cinfo) Source  
CoArbitrary cinfo => CoArbitrary (CallMatrixAug cinfo) Source  
Arbitrary cinfo => Arbitrary (CallMatrixAug cinfo) Source  
PartialOrd (CallMatrixAug cinfo) Source  
Pretty cinfo => Pretty (CallMatrixAug cinfo) Source  
NotWorse (CallMatrixAug cinfo) Source  
Monoid cinfo => CallComb (CallMatrixAug cinfo) Source  Augmented call matrix multiplication. 
Diagonal (CallMatrixAug cinfo) Order Source  
Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source 
noAug :: Monoid cinfo => CallMatrix > CallMatrixAug cinfo Source
Nonaugmented call matrix.
Sets of incomparable call matrices augmented with path information.
Sets of incomparable call matrices augmented with path information.
Use overloaded null
, empty
, singleton
, mappend
.
CMSet  

Show cinfo => Show (CMSet cinfo) Source  
Monoid (CMSet cinfo) Source  
CoArbitrary cinfo => CoArbitrary (CMSet cinfo) Source  
Arbitrary cinfo => Arbitrary (CMSet cinfo) Source  
Null (CMSet cinfo) Source  
Pretty cinfo => Pretty (CMSet cinfo) Source  
Monoid cinfo => CallComb (CMSet cinfo) Source  Call matrix set product is the Cartesian product. 
Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source 
insert :: CallMatrixAug cinfo > CMSet cinfo > CMSet cinfo Source
Insert into a call matrix set.
toList :: CMSet cinfo > [CallMatrixAug cinfo] Source
Convert into a list of augmented call matrices.
Printing
Generators and tests
CallMatrix
callMatrix :: Size ArgumentIndex > Gen CallMatrix Source
Generates a call matrix of the given size.