Safe Haskell  None 

Language  Haskell98 
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.
 data Order = Mat !(Matrix Int Order)
 decr :: (?cutoff :: CutOff) => Int > Order
 increase :: Int > Order > Order
 decrease :: Int > Order > Order
 (.*.) :: (?cutoff :: CutOff) => Order > Order > Order
 supremum :: (?cutoff :: CutOff) => [Order] > Order
 infimum :: (?cutoff :: CutOff) => [Order] > Order
 orderSemiring :: (?cutoff :: CutOff) => Semiring Order
 le :: Order
 lt :: Order
 unknown :: Order
 orderMat :: Matrix Int Order > Order
 collapseO :: (?cutoff :: CutOff) => Order > Order
 nonIncreasing :: Order > Bool
 decreasing :: Order > Bool
 isDecr :: Order > Bool
 class NotWorse a where
 tests :: IO Bool
Structural orderings
In the paper referred to above, there is an order R with
.Unknown
<=
Le
<=
Lt
This is generalized to
where
Unknown
<=
'Decr k'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 callmatrices. 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 filewise option.
See Call
for more information.
TODO: document orders which are callmatrices themselves.
Eq Order Source  
Ord Order Source  
Show Order Source  
CoArbitrary Order Source  
Arbitrary Order Source  
Arbitrary CallMatrix  
HasZero Order Source  
PartialOrd Order Source  Information order: When having comparable callmatrices, we keep the lesser one. Call graph completion works toward losing the good calls, tending towards Unknown (the least information). 
Pretty Order Source  
Pretty CallMatrix Source  
NotWorse Order Source  It does not get worse then ` 
CallComb CallMatrix Source  Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:

NotWorse (CallMatrix' Order) Source  
Diagonal (CallMatrixAug cinfo) Order Source  
Ord i => NotWorse (Matrix i Order) Source  We assume the matrices have the same dimension. 
(.*.) :: (?cutoff :: CutOff) => Order > Order > Order Source
Multiplication of Order
s. (Corresponds to sequential
composition.)
supremum :: (?cutoff :: CutOff) => [Order] > Order Source
The supremum of a (possibly empty) list of Order
s.
More information (i.e., more decrease) is bigger.
Unknown
is no information, thus, smallest.
infimum :: (?cutoff :: CutOff) => [Order] > Order Source
The infimum of a (non empty) list of Order
s.
Unknown
is the least element, thus, dominant.
orderSemiring :: (?cutoff :: CutOff) => Semiring Order Source
orderMat :: Matrix Int Order > Order Source
Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.
nonIncreasing :: Order > Bool Source
decreasing :: Order > Bool Source
isDecr :: Order > Bool Source
Matrixshaped order is decreasing if any diagonal element is decreasing.
A partial order, aimed at deciding whether a call graph gets worse during the completion.