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 #  
Arbitrary Order Source #  
Arbitrary CallMatrix #  
CoArbitrary Order Source #  
Pretty Order Source #  
Pretty CallMatrix 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). 
HasZero Order 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.
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.