Safe Haskell | None |
---|
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
- 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 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.
Eq Order | |
Ord Order | |
Show Order | |
Arbitrary Order | |
Arbitrary CallMatrix | |
CoArbitrary Order | |
HasZero Order | |
PartialOrd Order | Information order: 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). |
Pretty Order | |
Pretty CallMatrix | |
NotWorse Order | It does not get worse then ` |
CallComb CallMatrix | Call matrix multiplication.
Note the reversed order of multiplication:
The matrix Preconditions:
Postcondition:
|
NotWorse (CallMatrix' Order) | |
Diagonal (CallMatrixAug cinfo) Order | |
Ord i => NotWorse (Matrix i Order) | We assume the matrices have the same dimension. |
(.*.) :: [cutoff :: CutOff] => Order -> Order -> OrderSource
Multiplication of Order
s. (Corresponds to sequential
composition.)
supremum :: [cutoff :: CutOff] => [Order] -> OrderSource
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] -> OrderSource
The infimum of a (non empty) list of Order
s.
Unknown
is the least element, thus, dominant.
orderSemiring :: [cutoff :: CutOff] => Semiring OrderSource
orderMat :: Matrix Int Order -> OrderSource
Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.
decreasing :: Order -> BoolSource
Matrix-shaped order is decreasing if any diagonal element is decreasing.
A partial order, aimed at deciding whether a call graph gets worse during the completion.