Agda-2.6.0: 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 # Instance detailsDefined in Agda.Termination.CallMatrix Methodsfmap :: (a -> b) -> CallMatrix' a -> CallMatrix' b #(<\$) :: a -> CallMatrix' b -> CallMatrix' a # Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodsfold :: Monoid m => CallMatrix' m -> 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 # Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodstraverse :: 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) # Source # Instance detailsDefined in Agda.Termination.CallMatrix MethodsprettyList :: [CallMatrix] -> Doc Source # Source # Call matrix multiplication.f --(m1)--> g --(m2)--> h is combined to f --(m2 mul m1)--> hNote 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). Instance detailsDefined in Agda.Termination.CallMatrix Methods Eq a => Eq (CallMatrix' a) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methods(==) :: CallMatrix' a -> CallMatrix' a -> Bool #(/=) :: CallMatrix' a -> CallMatrix' a -> Bool # Ord a => Ord (CallMatrix' a) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodscompare :: 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, Show a) => Show (CallMatrix' a) Source # Instance detailsDefined in Agda.Termination.CallMatrix MethodsshowsPrec :: Int -> CallMatrix' a -> ShowS #show :: CallMatrix' a -> String #showList :: [CallMatrix' a] -> ShowS # Source # Instance detailsDefined in Agda.Termination.CallMatrix Methods Source # Instance detailsDefined in Agda.Termination.CallMatrix Methods HasZero a => Diagonal (CallMatrix' a) a Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodsdiagonal :: 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)--> hNote 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). Instance detailsDefined in Agda.Termination.CallMatrix Methods Monoid cinfo => CallComb (CMSet cinfo) Source # Call matrix set product is the Cartesian product. Instance detailsDefined in Agda.Termination.CallMatrix Methods(>*<) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo Source # Monoid cinfo => CallComb (CallMatrixAug cinfo) Source # Augmented call matrix multiplication. Instance detailsDefined in Agda.Termination.CallMatrix Methods(>*<) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> CallMatrixAug cinfo Source #

# 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 # Instance detailsDefined in Agda.Termination.CallMatrix Methods(==) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool #(/=) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool # Show cinfo => Show (CallMatrixAug cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix MethodsshowsPrec :: Int -> CallMatrixAug cinfo -> ShowS #show :: CallMatrixAug cinfo -> String #showList :: [CallMatrixAug cinfo] -> ShowS # PartialOrd (CallMatrixAug cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methods Pretty cinfo => Pretty (CallMatrixAug cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodspretty :: CallMatrixAug cinfo -> Doc Source #prettyPrec :: Int -> CallMatrixAug cinfo -> Doc Source #prettyList :: [CallMatrixAug cinfo] -> Doc Source # NotWorse (CallMatrixAug cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix MethodsnotWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool Source # Monoid cinfo => CallComb (CallMatrixAug cinfo) Source # Augmented call matrix multiplication. Instance detailsDefined in Agda.Termination.CallMatrix Methods(>*<) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> CallMatrixAug cinfo Source # Diagonal (CallMatrixAug cinfo) Order Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodsdiagonal :: CallMatrixAug cinfo -> [Order] Source # Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodssingleton :: 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 # Instance detailsDefined in Agda.Termination.CallMatrix MethodsshowsPrec :: Int -> CMSet cinfo -> ShowS #show :: CMSet cinfo -> String #showList :: [CMSet cinfo] -> ShowS # Semigroup (CMSet cinfo) Source # Instance detailsDefined 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 # Monoid (CMSet cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodsmempty :: CMSet cinfo #mappend :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo #mconcat :: [CMSet cinfo] -> CMSet cinfo # Null (CMSet cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodsempty :: CMSet cinfo Source #null :: CMSet cinfo -> Bool Source # Pretty cinfo => Pretty (CMSet cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodspretty :: CMSet cinfo -> Doc Source #prettyPrec :: Int -> CMSet cinfo -> Doc Source #prettyList :: [CMSet cinfo] -> Doc Source # Monoid cinfo => CallComb (CMSet cinfo) Source # Call matrix set product is the Cartesian product. Instance detailsDefined in Agda.Termination.CallMatrix Methods(>*<) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo Source # Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source # Instance detailsDefined in Agda.Termination.CallMatrix Methodssingleton :: 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.