Agda-2.4.2.4: A dependently typed functional programming language and proof assistant

Agda.Termination.CallMatrix

Synopsis

# Documentation

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:

• `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 Fieldsmat :: Matrix ArgumentIndex a

Instances

 Source Source Source Arbitrary CallMatrix Source Source Source 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) Source Ord a => Ord (CallMatrix' a) Source (Show a, HasZero a) => Show (CallMatrix' a) Source (CoArbitrary a, HasZero a) => CoArbitrary (CallMatrix' a) Source Source Source HasZero a => Diagonal (CallMatrix' a) a Source

class CallComb a where Source

Call matrix multiplication and call combination.

Methods

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

Instances

 Source 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) 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.

Constructors

 CallMatrixAug FieldsaugCallMatrix :: CallMatrixThe matrix of the (composed call).augCallInfo :: cinfoMeta info, like call path.

Instances

 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

Non-augmented call matrix.

# Sets of incomparable call matrices augmented with path information.

newtype CMSet cinfo Source

Sets of incomparable call matrices augmented with path information. Use overloaded `null`, `empty`, `singleton`, `mappend`.

Constructors

 CMSet FieldscmSet :: Favorites (CallMatrixAug cinfo)

Instances

 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.

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

Union two call matrix sets.

toList :: CMSet cinfo -> [CallMatrixAug cinfo] Source

Convert into a list of augmented call matrices.

# Generators and tests

## CallMatrix

Generates a call matrix of the given size.