Safe Haskell  None 

Language  Haskell2010 
Synopsis
 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]
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  

Instances
type CallMatrix = CallMatrix' Order Source #
class CallComb a where Source #
Call matrix multiplication and call combination.
Instances
CallComb CallMatrix Source #  Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:

Defined in Agda.Termination.CallMatrix (>*<) :: CallMatrix > CallMatrix > CallMatrix Source #  
Monoid cinfo => CallComb (CMSet cinfo) Source #  Call matrix set product is the Cartesian product. 
Monoid cinfo => CallComb (CallMatrixAug cinfo) Source #  Augmented call matrix multiplication. 
Defined in Agda.Termination.CallMatrix (>*<) :: CallMatrixAug cinfo > CallMatrixAug cinfo > CallMatrixAug cinfo Source # 
Call matrix augmented with path information.
data CallMatrixAug cinfo Source #
Call matrix augmented with path information.
CallMatrixAug  

Instances
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  

Instances
Show cinfo => Show (CMSet cinfo) Source #  
Semigroup (CMSet cinfo) Source #  
Monoid (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 #  
Defined in Agda.Termination.CallMatrix singleton :: CallMatrixAug cinfo > CMSet cinfo Source # 
toList :: CMSet cinfo > [CallMatrixAug cinfo] Source #
Convert into a list of augmented call matrices.