Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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
Pretty CallMatrix Source # 
Instance details

Defined in Agda.Termination.CallMatrix

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

Methods

notWorse :: CallMatrix -> CallMatrix -> Bool Source #

Functor CallMatrix' Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

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

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)

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

Methods

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

show :: CallMatrix' a -> String

showList :: [CallMatrix' a] -> ShowS

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

Defined in Agda.Termination.CallMatrix

Methods

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

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

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

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

(>*<) :: 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
Pretty cinfo => Pretty (CallMatrixAug cinfo) Source # 
Instance details

Defined in Agda.Termination.CallMatrix

Methods

pretty :: CallMatrixAug cinfo -> Doc Source #

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

prettyList :: [CallMatrixAug cinfo] -> Doc 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 #

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

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
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 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 #

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