Agda.Termination.Order

An Abstract domain of relative sizes, i.e., differences between size of formal function parameter and function argument in recursive call; used in the termination checker.

Structural orderings

data Order

In the paper referred to above, there is an order R with Unknown <= Le <= Lt.

This is generalized to Unknown <= 'Decr k' where Decr 1 replaces Lt and Decr 0 replaces Le. A negative decrease means an increase. The generalization allows the termination checker to record an increase by 1 which can be compensated by a following decrease by 2 which results in an overall decrease.

However, the termination checker of the paper itself terminates because there are only finitely many different call-matrices. To maintain termination of the terminator we set a cutoff point which determines how high the termination checker can count. This value should be set by a global or file-wise option.

See Call for more information.

TODO: document orders which are call-matrices themselves.

Constructors

Decr !Int

Decrease of callee argument wrt. caller parameter.

Unknown

No relation, infinite increase, or increase beyond termination depth.

Mat !(Matrix Int Order)

Matrix-shaped order, currently UNUSED.

Instances

Eq Order

Methods

(==) :: Order -> Order -> Bool

(/=) :: Order -> Order -> Bool

Ord Order

Methods

compare :: Order -> Order -> Ordering

(<) :: Order -> Order -> Bool

(<=) :: Order -> Order -> Bool

(>) :: Order -> Order -> Bool

(>=) :: Order -> Order -> Bool

max :: Order -> Order -> Order

min :: Order -> Order -> Order

Show Order

Methods

showsPrec :: Int -> Order -> ShowS

show :: Order -> String

showList :: [Order] -> ShowS

Pretty Order

Methods

pretty :: Order -> Doc

prettyPrec :: Int -> Order -> Doc

Pretty CallMatrix

Methods

pretty :: CallMatrix -> Doc

prettyPrec :: Int -> CallMatrix -> Doc

PartialOrd Order

Information order: Unknown is least information. The more we decrease, the more information we have.

When having comparable call-matrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information).

Methods

comparable :: Comparable Order

HasZero Order

Methods

zeroElement :: Order

NotWorse Order

It does not get worse then `increase'. If we are still decreasing, it can get worse: less decreasing.

Methods

notWorse :: Order -> Order -> Bool

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

Methods

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

NotWorse (CallMatrix' Order)

Methods

notWorse :: CallMatrix' Order -> CallMatrix' Order -> Bool

Diagonal (CallMatrixAug cinfo) Order

Methods

diagonal :: CallMatrixAug cinfo -> [Order]

decr :: (?cutoff :: CutOff) => Int -> Order

Smart constructor for Decr k :: Order which cuts off too big values.

Possible values for k: - ?cutoff <= k <= ?cutoff + 1.

increase :: Int -> Order -> Order

Raw increase which does not cut off.

decrease :: Int -> Order -> Order

Raw decrease which does not cut off.

(.*.) :: (?cutoff :: CutOff) => Order -> Order -> Order

Multiplication of Orders. (Corresponds to sequential composition.)

supremum :: (?cutoff :: CutOff) => [Order] -> Order

The supremum of a (possibly empty) list of Orders. More information (i.e., more decrease) is bigger. Unknown is no information, thus, smallest.

infimum :: (?cutoff :: CutOff) => [Order] -> Order

The infimum of a (non empty) list of Orders. Gets the worst information. Unknown is the least element, thus, dominant.

orderSemiring :: (?cutoff :: CutOff) => Semiring Order

We use a record for semiring instead of a type class since implicit arguments cannot occur in instance constraints, like instance (?cutoff :: Int) => SemiRing Order.

le :: Order

le, lt, decreasing, unknown: for backwards compatibility, and for external use.

lt :: Order

unknown :: Order

orderMat :: Matrix Int Order -> Order

Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.

collapseO :: (?cutoff :: CutOff) => Order -> Order

nonIncreasing :: Order -> Bool

decreasing :: Order -> Bool

isDecr :: Order -> Bool

Matrix-shaped order is decreasing if any diagonal element is decreasing.

class NotWorse a where

A partial order, aimed at deciding whether a call graph gets worse during the completion.

Minimal complete definition

notWorse

Methods

notWorse :: a -> a -> Bool

Instances

NotWorse Order

It does not get worse then `increase'. If we are still decreasing, it can get worse: less decreasing.

Methods

notWorse :: Order -> Order -> Bool

NotWorse (CallMatrixAug cinfo)

Methods

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

NotWorse (CallMatrix' Order)

Methods

notWorse :: CallMatrix' Order -> CallMatrix' Order -> Bool

(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o)

We assume the matrices have the same dimension.

Methods

notWorse :: Matrix i o -> Matrix i o -> Bool

isOrder :: (?cutoff :: CutOff) => Order -> Bool