Agda.Termination.CallMatrix

Documentation

type ArgumentIndex = Int

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

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:

• lt (less than) if the j-th argument to the target function is structurally strictly smaller than the i-th pattern.

  • le (less than or equal) if the j-th argument to the target function is structurally smaller than the i-th pattern.
  • unknown otherwise.

Constructors

CallMatrix

Fields

mat :: Matrix ArgumentIndex a

Instances

Functor CallMatrix'

Foldable CallMatrix'

Traversable CallMatrix'

Arbitrary CallMatrix

Pretty CallMatrix

CallComb CallMatrix

Call matrix multiplication.

f --(m1)--> g --(m2)--> h is combined to f --(m2 mul m1)--> h

Note the reversed order of multiplication: The matrix c1 of the second call g-->h in the sequence f-->g-->h is multiplied with the matrix c2 of the first call.

Preconditions: m1 has dimensions ar(g) × ar(f). m2 has dimensions ar(h) × ar(g).

Postcondition: m1 >*< m2 has dimensions ar(h) × ar(f).

Eq a => Eq (CallMatrix' a)

Ord a => Ord (CallMatrix' a)

(Show a, HasZero a) => Show (CallMatrix' a)

(CoArbitrary a, HasZero a) => CoArbitrary (CallMatrix' a)

PartialOrd a => PartialOrd (CallMatrix' a)

NotWorse (CallMatrix' Order)

HasZero a => Diagonal (CallMatrix' a) a

type CallMatrix = CallMatrix' Order

class CallComb a where

Call matrix multiplication and call combination.

Methods

(>*<) :: (?cutoff :: CutOff) => a -> a -> a

Instances

CallComb CallMatrix

Call matrix multiplication.

f --(m1)--> g --(m2)--> h is combined to f --(m2 mul m1)--> h

Note the reversed order of multiplication: The matrix c1 of the second call g-->h in the sequence f-->g-->h is multiplied with the matrix c2 of the first call.

Preconditions: m1 has dimensions ar(g) × ar(f). m2 has dimensions ar(h) × ar(g).

Postcondition: m1 >*< m2 has dimensions ar(h) × ar(f).

Monoid cinfo => CallComb (CMSet cinfo)

Call matrix set product is the Cartesian product.

Monoid cinfo => CallComb (CallMatrixAug cinfo)

Augmented call matrix multiplication.

Monoid cinfo => CallComb (Call cinfo)

Call combination.

f --(c1)--> g --(c2)--> h is combined to f --(c1 >*c2)-- h

Precondition: source c1 == target c2

Call matrix augmented with path information.

data CallMatrixAug cinfo

Call matrix augmented with path information.

Constructors

CallMatrixAug

Fields

augCallMatrix :: CallMatrix

The matrix of the (composed call).

augCallInfo :: cinfo

Meta info, like call path.

Instances

Eq cinfo => Eq (CallMatrixAug cinfo)

Show cinfo => Show (CallMatrixAug cinfo)

Arbitrary cinfo => Arbitrary (CallMatrixAug cinfo)

CoArbitrary cinfo => CoArbitrary (CallMatrixAug cinfo)

PartialOrd (CallMatrixAug cinfo)

Pretty cinfo => Pretty (CallMatrixAug cinfo)

NotWorse (CallMatrixAug cinfo)

Monoid cinfo => CallComb (CallMatrixAug cinfo)

Augmented call matrix multiplication.

Diagonal (CallMatrixAug cinfo) Order

noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo

Non-augmented call matrix.

Sets of incomparable call matrices augmented with path information.

newtype CMSet cinfo

Constructors

CMSet

Fields

cmSet :: Favorites (CallMatrixAug cinfo)

Instances

Show cinfo => Show (CMSet cinfo)

Arbitrary cinfo => Arbitrary (CMSet cinfo)

CoArbitrary cinfo => CoArbitrary (CMSet cinfo)

Monoid (CMSet cinfo)

Pretty cinfo => Pretty (CMSet cinfo)

Monoid cinfo => CallComb (CMSet cinfo)

Call matrix set product is the Cartesian product.

Monoid cinfo => CallComb (Call cinfo)

Call combination.

f --(c1)--> g --(c2)--> h is combined to f --(c1 >*c2)-- h

Precondition: source c1 == target c2

empty :: CMSet cinfo

An empty call matrix set.

null :: CMSet cinfo -> Bool

Call matrix is empty?

singleton :: CallMatrixAug cinfo -> CMSet cinfo

A singleton call matrix set.

insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo

Insert into a call matrix set.

union :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo

Union two call matrix sets.

toList :: CMSet cinfo -> [CallMatrixAug cinfo]

Convert into a list of augmented call matrices.

Printing

Generators and tests

CallMatrix

callMatrix :: Size ArgumentIndex -> Gen CallMatrix

Generates a call matrix of the given size.

CallMatrixAug

All tests

tests :: IO Bool