Safe Haskell  None 

Language  Haskell2010 
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.
Synopsis
 data Order
 decr :: (?cutoff :: CutOff) => Bool > Int > Order
 increase :: Int > Order > Order
 decrease :: Int > Order > Order
 setUsability :: Bool > 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
 isOrder :: (?cutoff :: CutOff) => Order > 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.
Decr !Bool !Int  Decrease of callee argument wrt. caller parameter. The UPDATE: Andreas, 20170726: Feature #2331 is unsound due to size quantification in terms. While the infrastructure for usable/unusable decrease remains in place, no unusable decreases are generated by TermCheck. 
Unknown  No relation, infinite increase, or increase beyond termination depth. 
Mat !(Matrix Int Order)  Matrixshaped order, currently UNUSED. 
Instances
Eq Order Source #  
Ord Order Source #  
Show Order Source #  
HasZero Order Source #  
Defined in Agda.Termination.Order zeroElement :: 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). 
Defined in Agda.Termination.Order  
Pretty Order Source #  
Pretty CallMatrix Source #  
Defined in Agda.Termination.CallMatrix pretty :: CallMatrix > Doc Source # prettyPrec :: Int > CallMatrix > Doc Source # prettyList :: [CallMatrix] > Doc 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:

Defined in Agda.Termination.CallMatrix (>*<) :: CallMatrix > CallMatrix > CallMatrix Source #  
NotWorse (CallMatrix' Order) Source #  
Defined in Agda.Termination.CallMatrix notWorse :: CallMatrix' Order > CallMatrix' Order > Bool Source #  
Diagonal (CallMatrixAug cinfo) Order Source #  
Defined in Agda.Termination.CallMatrix diagonal :: CallMatrixAug cinfo > [Order] Source # 
(.*.) :: (?cutoff :: CutOff) => Order > Order > Order Source #
Multiplication of Order
s.
(Corresponds to sequential composition.)
orderSemiring :: (?cutoff :: CutOff) => Semiring Order Source #
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
.
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 #
Decreasing and usable?
isDecr :: Order > Bool Source #
Matrixshaped order is decreasing if any diagonal element is decreasing.
class NotWorse a where Source #
A partial order, aimed at deciding whether a call graph gets worse during the completion.
Instances
NotWorse Order Source #  It does not get worse then ` 
NotWorse (CallMatrixAug cinfo) Source #  
Defined in Agda.Termination.CallMatrix notWorse :: CallMatrixAug cinfo > CallMatrixAug cinfo > Bool Source #  
NotWorse (CallMatrix' Order) Source #  
Defined in Agda.Termination.CallMatrix notWorse :: CallMatrix' Order > CallMatrix' Order > Bool Source #  
(Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) Source #  We assume the matrices have the same dimension. 