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

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

Defined in Agda.Termination.CallMatrix

Methods

(>*<) :: CallMatrix -> CallMatrix -> CallMatrix

NotWorse CallMatrix

Defined in Agda.Termination.CallMatrix

Methods

notWorse :: CallMatrix -> CallMatrix -> Bool

Pretty CallMatrix

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrix -> Doc

prettyPrec :: Int -> CallMatrix -> Doc

prettyList :: [CallMatrix] -> Doc

Foldable CallMatrix'

Defined in Agda.Termination.CallMatrix

Methods

fold :: Monoid m => CallMatrix' m -> m

foldMap :: Monoid m => (a -> m) -> CallMatrix' a -> m

foldMap' :: Monoid m => (a -> m) -> CallMatrix' a -> m

foldr :: (a -> b -> b) -> b -> CallMatrix' a -> b

foldr' :: (a -> b -> b) -> b -> CallMatrix' a -> b

foldl :: (b -> a -> b) -> b -> CallMatrix' a -> b

foldl' :: (b -> a -> b) -> b -> CallMatrix' a -> b

foldr1 :: (a -> a -> a) -> CallMatrix' a -> a

foldl1 :: (a -> a -> a) -> CallMatrix' a -> a

toList :: CallMatrix' a -> [a]

null :: CallMatrix' a -> Bool

length :: CallMatrix' a -> Int

elem :: Eq a => a -> CallMatrix' a -> Bool

maximum :: Ord a => CallMatrix' a -> a

minimum :: Ord a => CallMatrix' a -> a

sum :: Num a => CallMatrix' a -> a

product :: Num a => CallMatrix' a -> a

Traversable CallMatrix'

Defined in Agda.Termination.CallMatrix

Methods

traverse :: Applicative f => (a -> f b) -> CallMatrix' a -> f (CallMatrix' b)

sequenceA :: Applicative f => CallMatrix' (f a) -> f (CallMatrix' a)

mapM :: Monad m => (a -> m b) -> CallMatrix' a -> m (CallMatrix' b)

sequence :: Monad m => CallMatrix' (m a) -> m (CallMatrix' a)

Functor CallMatrix'

Defined in Agda.Termination.CallMatrix

Methods

fmap :: (a -> b) -> CallMatrix' a -> CallMatrix' b

(<$) :: a -> CallMatrix' b -> CallMatrix' a

PartialOrd a => PartialOrd (CallMatrix' a)

Defined in Agda.Termination.CallMatrix

Methods

comparable :: Comparable (CallMatrix' a)

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

Defined in Agda.Termination.CallMatrix

Methods

showsPrec :: Int -> CallMatrix' a -> ShowS

show :: CallMatrix' a -> String

showList :: [CallMatrix' a] -> ShowS

Eq a => Eq (CallMatrix' a)

Defined in Agda.Termination.CallMatrix

Methods

(==) :: CallMatrix' a -> CallMatrix' a -> Bool

(/=) :: CallMatrix' a -> CallMatrix' a -> Bool

Ord a => Ord (CallMatrix' a)

Defined in Agda.Termination.CallMatrix

Methods

compare :: CallMatrix' a -> CallMatrix' a -> Ordering

(<) :: CallMatrix' a -> CallMatrix' a -> Bool

(<=) :: CallMatrix' a -> CallMatrix' a -> Bool

(>) :: CallMatrix' a -> CallMatrix' a -> Bool

(>=) :: CallMatrix' a -> CallMatrix' a -> Bool

max :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a

min :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a

HasZero a => Diagonal (CallMatrix' a) a

Defined in Agda.Termination.CallMatrix

Methods

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

Defined in Agda.Termination.CallMatrix

Methods

(>*<) :: CallMatrix -> CallMatrix -> CallMatrix

Monoid cinfo => CallComb (CMSet cinfo)

Call matrix set product is the Cartesian product.

Defined in Agda.Termination.CallMatrix

Methods

(>*<) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo

Monoid cinfo => CallComb (CallMatrixAug cinfo)

Augmented call matrix multiplication.

Defined in Agda.Termination.CallMatrix

Methods

(>*<) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> CallMatrixAug cinfo

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

Monoid cinfo => CallComb (CallMatrixAug cinfo)

Augmented call matrix multiplication.

Defined in Agda.Termination.CallMatrix

Methods

(>*<) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> CallMatrixAug cinfo

NotWorse (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

notWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool

PartialOrd (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

comparable :: Comparable (CallMatrixAug cinfo)

Pretty cinfo => Pretty (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrixAug cinfo -> Doc

prettyPrec :: Int -> CallMatrixAug cinfo -> Doc

prettyList :: [CallMatrixAug cinfo] -> Doc

Show cinfo => Show (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

showsPrec :: Int -> CallMatrixAug cinfo -> ShowS

show :: CallMatrixAug cinfo -> String

showList :: [CallMatrixAug cinfo] -> ShowS

Eq cinfo => Eq (CallMatrixAug cinfo)

Defined in Agda.Termination.CallMatrix

Methods

(==) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool

(/=) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool

Diagonal (CallMatrixAug cinfo) Order

Defined in Agda.Termination.CallMatrix

Methods

diagonal :: CallMatrixAug cinfo -> [Order]

Singleton (CallMatrixAug cinfo) (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

singleton :: CallMatrixAug cinfo -> CMSet cinfo

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

Non-augmented call matrix.

Sets of incomparable call matrices augmented with path information.

newtype CMSet cinfo

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

Constructors

CMSet

Fields

• cmSet :: Favorites (CallMatrixAug cinfo)

Instances

Monoid cinfo => CallComb (CMSet cinfo)

Call matrix set product is the Cartesian product.

Defined in Agda.Termination.CallMatrix

Methods

(>*<) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo

Null (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

empty :: CMSet cinfo

null :: CMSet cinfo -> Bool

Pretty cinfo => Pretty (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CMSet cinfo -> Doc

prettyPrec :: Int -> CMSet cinfo -> Doc

prettyList :: [CMSet cinfo] -> Doc

Monoid (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

mempty :: CMSet cinfo

mappend :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo

mconcat :: [CMSet cinfo] -> CMSet cinfo

Semigroup (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

(<>) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo

sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo

stimes :: Integral b => b -> CMSet cinfo -> CMSet cinfo

Show cinfo => Show (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

showsPrec :: Int -> CMSet cinfo -> ShowS

show :: CMSet cinfo -> String

showList :: [CMSet cinfo] -> ShowS

Collection (Call cinfo) (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

fromList :: [Call cinfo] -> CallGraph cinfo

Singleton (Call cinfo) (CallGraph cinfo)

Defined in Agda.Termination.CallGraph

Methods

singleton :: Call cinfo -> CallGraph cinfo

Singleton (CallMatrixAug cinfo) (CMSet cinfo)

Defined in Agda.Termination.CallMatrix

Methods

singleton :: CallMatrixAug cinfo -> CMSet cinfo

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