{-# LANGUAGE CPP #-}
{-# LANGUAGE ImplicitParams #-}
-- | 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.
module Agda.Termination.Order
( -- * Structural orderings
Order(..), decr
, increase, decrease, setUsability
, (.*.)
, supremum, infimum
, orderSemiring
, le, lt, unknown, orderMat, collapseO
, nonIncreasing, decreasing, isDecr
, NotWorse(..)
, isOrder
) where
import qualified Data.Foldable as Fold
import qualified Data.List as List
import Agda.Termination.CutOff
import Agda.Termination.SparseMatrix as Matrix
import Agda.Termination.Semiring (HasZero(..), Semiring)
import qualified Agda.Termination.Semiring as Semiring
import Agda.Utils.PartialOrd
import Agda.Utils.Pretty
#include "undefined.h"
import Agda.Utils.Impossible
------------------------------------------------------------------------
-- Structural orderings
-- | 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.
data Order
= Decr !Bool {-# UNPACK #-} !Int
-- ^ Decrease of callee argument wrt. caller parameter.
--
-- The @Bool@ indicates whether the decrease (if any) is usable.
-- In any chain, there needs to be one usable decrease.
-- Unusable decreases come from SIZELT constraints which are
-- not in inductive pattern match or a coinductive copattern match.
-- See issue #2331.
--
-- UPDATE: Andreas, 2017-07-26:
-- 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 {-# UNPACK #-} !(Matrix Int Order)
-- ^ Matrix-shaped order, currently UNUSED.
deriving (Eq, Ord, Show)
-- instance Show Order where
-- show (Decr u k) = if u then show (- k) else "(" ++ show (-k) ++ ")"
-- show Unknown = "."
-- show (Mat m) = "Mat " ++ show m
instance HasZero Order where
zeroElement = Unknown
-- | 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).
instance PartialOrd Order where
comparable o o' = case (o, o') of
(Unknown, Unknown) -> POEQ
(Unknown, _ ) -> POLT
(_ , Unknown) -> POGT
(Decr u k, Decr u' l) -> comparableBool u u' `orPO` comparableOrd k l
-- Matrix-shaped orders are no longer supported
(Mat{} , _ ) -> __IMPOSSIBLE__
(_ , Mat{} ) -> __IMPOSSIBLE__
where
comparableBool = curry $ \case
(False, True) -> POLT
(True, False) -> POGT
_ -> POEQ
-- | A partial order, aimed at deciding whether a call graph gets
-- worse during the completion.
--
class NotWorse a where
notWorse :: a -> a -> Bool
-- | It does not get worse then ``increase''.
-- If we are still decreasing, it can get worse: less decreasing.
instance NotWorse Order where
o `notWorse` Unknown = True -- we are unboundedly increasing
Unknown `notWorse` Decr _ k = k < 0 -- we are increasing
Decr u l `notWorse` Decr u' k = k < 0 -- we are increasing or
|| l >= k && (u || not u') -- we are decreasing, but not less, and not less usable
-- Matrix-shaped orders are no longer supported
Mat m `notWorse` o = __IMPOSSIBLE__
o `notWorse` Mat m = __IMPOSSIBLE__
{-
Mat m `notWorse` Mat n = m `notWorse` n -- matrices are compared pointwise
o `notWorse` Mat n = o `notWorse` collapse n -- or collapsed (sound?)
Mat m `notWorse` o = collapse m `notWorse` o
-}
-- | We assume the matrices have the same dimension.
instance (Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) where
m `notWorse` n
| size m /= size n = __IMPOSSIBLE__
| otherwise = Fold.and $ zipMatrices onlym onlyn both trivial m n
where
-- If an element is only in @m@, then its 'Unknown' in @n@
-- so it gotten better at best, in any case, not worse.
onlym o = True -- @== o `notWorse` Unknown@
onlyn o = zeroElement `notWorse` o
both = notWorse
trivial = id -- @True@ counts as zero as it is neutral for @and@
-- | Raw increase which does not cut off.
increase :: Int -> Order -> Order
increase i o = case o of
Unknown -> Unknown
Decr u k -> Decr u $ k - i -- TODO: should we set u to False if k - i < 0 ?
Mat m -> Mat $ fmap (increase i) m
-- | Raw decrease which does not cut off.
decrease :: Int -> Order -> Order
decrease i o = increase (-i) o
setUsability :: Bool -> Order -> Order
setUsability u o = case o of
Decr _ k -> Decr u k
Unknown -> o
Mat{} -> o
-- | Smart constructor for @Decr k :: Order@ which cuts off too big values.
--
-- Possible values for @k@: @- ?cutoff '<=' k '<=' ?cutoff + 1@.
decr :: (?cutoff :: CutOff) => Bool -> Int -> Order
decr u k = case ?cutoff of
CutOff c | k < -c -> Unknown
| k > c -> Decr u $ c + 1
_ -> Decr u k
-- | Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.
orderMat :: Matrix Int Order -> Order
orderMat m
| Matrix.isEmpty m = le -- 0x0 Matrix = neutral element
| Just o <- isSingleton m = o -- 1x1 Matrix
| otherwise = Mat m -- nxn Matrix
withinCutOff :: (?cutoff :: CutOff) => Int -> Bool
withinCutOff k = case ?cutoff of
DontCutOff -> True
CutOff c -> k >= -c && k <= c + 1
isOrder :: (?cutoff :: CutOff) => Order -> Bool
isOrder (Decr _ k) = withinCutOff k
isOrder Unknown = True
isOrder (Mat m) = False -- TODO: extend to matrices
-- | @le@, @lt@, @decreasing@, @unknown@: for backwards compatibility, and for external use.
le :: Order
le = Decr False 0
-- | Usable decrease.
lt :: Order
lt = Decr True 1
unknown :: Order
unknown = Unknown
nonIncreasing :: Order -> Bool
nonIncreasing (Decr _ k) = k >= 0
nonIncreasing _ = False
-- | Decreasing and usable?
decreasing :: Order -> Bool
decreasing (Decr u k) = u && k > 0
decreasing _ = False
-- | Matrix-shaped order is decreasing if any diagonal element is decreasing.
isDecr :: Order -> Bool
isDecr (Mat m) = any isDecr $ diagonal m
isDecr o = decreasing o
instance Pretty Order where
pretty (Decr u 0) = "="
pretty (Decr u k) = mparens (not u) $ text $ show (0 - k)
pretty Unknown = "?"
pretty (Mat m) = "Mat" <+> pretty m
-- | Multiplication of 'Order's.
-- (Corresponds to sequential composition.)
-- I think this funny pattern matching is because overlapping patterns
-- are producing a warning and thus an error (strict compilation settings)
(.*.) :: (?cutoff :: CutOff) => Order -> Order -> Order
Unknown .*. _ = Unknown
(Mat m) .*. Unknown = Unknown
(Decr _ k) .*. Unknown = Unknown
(Decr u k) .*. (Decr u' l) = decr (u || u') (k + l) -- if one is usable, so is the composition
(Decr _ 0) .*. (Mat m) = Mat m
(Decr u k) .*. (Mat m) = (Decr u k) .*. (collapse m)
(Mat m1) .*. (Mat m2)
| okM m1 m2 = Mat $ mul orderSemiring m1 m2
| otherwise = (collapse m1) .*. (collapse m2)
(Mat m) .*. (Decr _ 0) = Mat m
(Mat m) .*. (Decr u k) = (collapse m) .*. (Decr u k)
-- | collapse @m@
--
-- We assume that @m@ codes a permutation: each row has at most one column
-- that is not @Unknown@.
--
-- To collapse a matrix into a single value, we take the best value of
-- each column and multiply them. That means if one column is all @Unknown@,
-- i.e., no argument relates to that parameter, then the collapsed value
-- is also @Unknown@.
--
-- This makes order multiplication associative.
collapse :: (?cutoff :: CutOff) => Matrix Int Order -> Order
collapse m = case toLists $ Matrix.transpose m of
[] -> __IMPOSSIBLE__ -- This can never happen if order matrices are generated by the smart constructor
m' -> foldl1 (.*.) $ map (foldl1 maxO) m'
collapseO :: (?cutoff :: CutOff) => Order -> Order
collapseO (Mat m) = collapse m
collapseO o = o
-- | Can two matrices be multplied together?
okM :: Matrix Int Order -> Matrix Int Order -> Bool
okM m1 m2 = (rows $ size m2) == (cols $ size m1)
-- | The supremum of a (possibly empty) list of 'Order's.
-- More information (i.e., more decrease) is bigger.
-- 'Unknown' is no information, thus, smallest.
supremum :: (?cutoff :: CutOff) => [Order] -> Order
supremum = foldr maxO Unknown
-- | @('Order', 'maxO', '.*.')@ forms a semiring,
-- with 'Unknown' as zero and 'Le' as one.
maxO :: (?cutoff :: CutOff) => Order -> Order -> Order
maxO o1 o2 = case (o1,o2) of
-- NOTE: strictly speaking the maximum does not exists
-- which is better, an unusable decrease by 2 or a usable decrease by 1?
-- We give the usable information priority if it is a decrease.
(Decr False _, Decr True l) | l > 0 -> o2
(Decr True k, Decr False _) | k > 0 -> o1
(Decr u k, Decr u' l) -> if l > k then o2 else o1
(Unknown, _) -> o2
(_, Unknown) -> o1
(Mat m1, Mat m2) -> Mat (Matrix.add maxO m1 m2)
(Mat m, _) -> maxO (collapse m) o2
(_, Mat m) -> maxO o1 (collapse m)
-- | The infimum of a (non empty) list of 'Order's.
-- Gets the worst information.
-- 'Unknown' is the least element, thus, dominant.
infimum :: (?cutoff :: CutOff) => [Order] -> Order
infimum (o:l) = List.foldl' minO o l
infimum [] = __IMPOSSIBLE__
-- | Pick the worst information.
minO :: (?cutoff :: CutOff) => Order -> Order -> Order
minO o1 o2 = case (o1,o2) of
(Unknown, _) -> Unknown
(_, Unknown) -> Unknown
-- different usability:
-- We pick the unusable one if it is not a decrease or
-- decreases not more than the usable one.
(Decr False k, Decr True l) -> if k <= 0 || k <= l then o1 else o2
(Decr True k, Decr False l) -> if l <= 0 || l <= k then o2 else o1
-- same usability:
(Decr u k, Decr _ l) -> Decr u (min k l)
(Mat m1, Mat m2)
| size m1 == size m2 -> Mat $ Matrix.intersectWith minO m1 m2
| otherwise -> minO (collapse m1) (collapse m2)
(Mat m1, _) -> minO (collapse m1) o2
(_, Mat m2) -> minO o1 (collapse m2)
-- | 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@.
orderSemiring :: (?cutoff :: CutOff) => Semiring Order
orderSemiring = Semiring.Semiring
{ Semiring.add = maxO
, Semiring.mul = (.*.)
, Semiring.zero = Unknown
-- , Semiring.one = Le
}