Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Termination.CallMatrix

Synopsis

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:

  • 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

Instances

Instances details
CallComb CallMatrix 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).

Instance details

Defined in Agda.Termination.CallMatrix

NotWorse CallMatrix Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Pretty CallMatrix Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Foldable CallMatrix' Source # 
Instance details

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' Source # 
Instance details

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' Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

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

PartialOrd a => PartialOrd (CallMatrix' a) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

(HasZero a, Show a) => Show (CallMatrix' a) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Eq a => Eq (CallMatrix' a) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Ord a => Ord (CallMatrix' a) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

HasZero a => Diagonal (CallMatrix' a) a Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

diagonal :: CallMatrix' a -> [a] Source #

class CallComb a where Source #

Call matrix multiplication and call combination.

Methods

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

Instances

Instances details
CallComb CallMatrix 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).

Instance details

Defined in Agda.Termination.CallMatrix

Monoid cinfo => CallComb (CMSet cinfo) Source #

Call matrix set product is the Cartesian product.

Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

Monoid cinfo => CallComb (CallMatrixAug cinfo) Source #

Augmented call matrix multiplication.

Instance details

Defined 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 

Fields

Instances

Instances details
Monoid cinfo => CallComb (CallMatrixAug cinfo) Source #

Augmented call matrix multiplication.

Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

NotWorse (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

notWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool Source #

PartialOrd (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Pretty cinfo => Pretty (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Show cinfo => Show (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

showsPrec :: Int -> CallMatrixAug cinfo -> ShowS #

show :: CallMatrixAug cinfo -> String #

showList :: [CallMatrixAug cinfo] -> ShowS #

Eq cinfo => Eq (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

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

Diagonal (CallMatrixAug cinfo) Order Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

diagonal :: CallMatrixAug cinfo -> [Order] Source #

Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

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 

Fields

Instances

Instances details
Monoid cinfo => CallComb (CMSet cinfo) Source #

Call matrix set product is the Cartesian product.

Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

Null (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

empty :: CMSet cinfo Source #

null :: CMSet cinfo -> Bool Source #

Pretty cinfo => Pretty (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CMSet cinfo -> Doc Source #

prettyPrec :: Int -> CMSet cinfo -> Doc Source #

prettyList :: [CMSet cinfo] -> Doc Source #

Monoid (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

mempty :: CMSet cinfo #

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

mconcat :: [CMSet cinfo] -> CMSet cinfo #

Semigroup (CMSet cinfo) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

showsPrec :: Int -> CMSet cinfo -> ShowS #

show :: CMSet cinfo -> String #

showList :: [CMSet cinfo] -> ShowS #

Collection (Call cinfo) (CallGraph cinfo) Source # 
Instance details

Defined in Agda.Termination.CallGraph

Methods

fromList :: [Call cinfo] -> CallGraph cinfo Source #

Singleton (Call cinfo) (CallGraph cinfo) Source # 
Instance details

Defined in Agda.Termination.CallGraph

Methods

singleton :: Call cinfo -> CallGraph cinfo Source #

Singleton (CallMatrixAug cinfo) (CMSet cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

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.

Printing