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

Safe Haskell | None
Language | Haskell2010

Agda.Termination.CallMatrix

Contents

- Call matrix augmented with path information.
- Sets of incomparable call matrices augmented with path information.
- Printing

Synopsis

- type ArgumentIndex = Int
- newtype CallMatrix' a = CallMatrix {
  - mat :: Matrix ArgumentIndex a
  }
- type CallMatrix = CallMatrix' Order
- class CallComb a where
  - (>*<) :: (?cutoff :: CutOff) => a -> a -> a
- data CallMatrixAug cinfo = CallMatrixAug {
  - augCallMatrix :: CallMatrix
  - augCallInfo :: cinfo
  }
- noAug :: Monoid cinfo => CallMatrix -> CallMatrixAug cinfo
- newtype CMSet cinfo = CMSet {
  - cmSet :: Favorites (CallMatrixAug cinfo)
  }
- insert :: CallMatrixAug cinfo -> CMSet cinfo -> CMSet cinfo
- union :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo
- toList :: CMSet cinfo -> [CallMatrixAug cinfo]

# 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

- mat :: Matrix ArgumentIndex a

Instances

Functor CallMatrix' Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods fmap :: (a -> b) -> CallMatrix' a -> CallMatrix' b Source # (<$) :: a -> CallMatrix' b -> CallMatrix' a Source #
Foldable CallMatrix' Source # |

Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

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

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

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

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

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

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

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

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

null :: CallMatrix' a -> Bool Source #

length :: CallMatrix' a -> Int Source #

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

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

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

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

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

Traversable CallMatrix' Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods traverse :: Applicative f => (a -> f b) -> CallMatrix' a -> f (CallMatrix' b) Source # sequenceA :: Applicative f => CallMatrix' (f a) -> f (CallMatrix' a) Source # mapM :: Monad m => (a -> m b) -> CallMatrix' a -> m (CallMatrix' b) Source # sequence :: Monad m => CallMatrix' (m a) -> m (CallMatrix' a) Source #
Pretty CallMatrix Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods pretty :: CallMatrix -> Doc Source # prettyPrec :: Int -> CallMatrix -> Doc Source # prettyList :: [CallMatrix] -> Doc Source #

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 Methods (>*<) :: CallMatrix -> CallMatrix -> CallMatrix Source #
Eq a => Eq (CallMatrix' a) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods (==) :: CallMatrix' a -> CallMatrix' a -> Bool Source # (/=) :: CallMatrix' a -> CallMatrix' a -> Bool Source #
Ord a => Ord (CallMatrix' a) Source # |

Instance details

Defined in Agda.Termination.CallMatrix

Methods

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

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

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

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

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

max :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a Source #

min :: CallMatrix' a -> CallMatrix' a -> CallMatrix' a Source #

(HasZero a, Show a) => Show (CallMatrix' a) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods showsPrec :: Int -> CallMatrix' a -> ShowS Source # show :: CallMatrix' a -> String Source # showList :: [CallMatrix' a] -> ShowS Source #
PartialOrd a => PartialOrd (CallMatrix' a) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods comparable :: Comparable (CallMatrix' a) Source #
NotWorse (CallMatrix' Order) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods notWorse :: CallMatrix' Order -> CallMatrix' Order -> Bool Source #
HasZero a => Diagonal (CallMatrix' a) a Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods diagonal :: CallMatrix' a -> [a] Source #

type CallMatrix = CallMatrix' Order Source #

class CallComb a where Source #

Call matrix multiplication and call combination.

Methods

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

Instances

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 Methods (>*<) :: CallMatrix -> CallMatrix -> CallMatrix 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 #
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

- augCallMatrix :: CallMatrix

  The matrix of the (composed call).

- augCallInfo :: cinfo

  Meta info, like call path.

Instances

Eq cinfo => Eq (CallMatrixAug cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods (==) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool Source # (/=) :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool Source #
Show cinfo => Show (CallMatrixAug cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods showsPrec :: Int -> CallMatrixAug cinfo -> ShowS Source # show :: CallMatrixAug cinfo -> String Source # showList :: [CallMatrixAug cinfo] -> ShowS Source #
PartialOrd (CallMatrixAug cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods comparable :: Comparable (CallMatrixAug cinfo) Source #
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 #
NotWorse (CallMatrixAug cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods notWorse :: CallMatrixAug cinfo -> CallMatrixAug cinfo -> Bool 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 #
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

- cmSet :: Favorites (CallMatrixAug cinfo)

Instances

Show cinfo => Show (CMSet cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods showsPrec :: Int -> CMSet cinfo -> ShowS Source # show :: CMSet cinfo -> String Source # showList :: [CMSet cinfo] -> ShowS Source #
Semigroup (CMSet cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods (<>) :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo Source # sconcat :: NonEmpty (CMSet cinfo) -> CMSet cinfo Source # stimes :: Integral b => b -> CMSet cinfo -> CMSet cinfo Source #
Monoid (CMSet cinfo) Source # |
Instance details Defined in Agda.Termination.CallMatrix Methods mempty :: CMSet cinfo Source # mappend :: CMSet cinfo -> CMSet cinfo -> CMSet cinfo Source # mconcat :: [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 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 #
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