{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# 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(Mat), decr , increase, decrease , (.*.) , supremum, infimum , orderSemiring , le, lt, unknown, orderMat, collapseO , nonIncreasing, decreasing, isDecr , NotWorse(..) , tests ) where import qualified Data.Foldable as Fold import Data.List as List hiding (union, insert) import Agda.Termination.CutOff import Agda.Termination.SparseMatrix as Matrix hiding (tests) import Agda.Termination.Semiring (HasZero(..), Semiring) import qualified Agda.Termination.Semiring as Semiring import Agda.Utils.PartialOrd hiding (tests) import Agda.Utils.Pretty import Agda.Utils.QuickCheck import Agda.Utils.TestHelpers #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 {-# UNPACK #-} !Int -- ^ Decrease of callee argument wrt. caller parameter. | Unknown -- ^ No relation, infinite increase, or increase beyond termination depth. | Mat {-# UNPACK #-} !(Matrix Int Order) -- ^ Matrix-shaped order, currently UNUSED. deriving (Eq,Ord) instance Show Order where show (Decr k) = 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 k , Decr l ) -> comparableOrd k l -- Matrix-shaped orders are no longer supported (Mat{} , _ ) -> __IMPOSSIBLE__ (_ , Mat{} ) -> __IMPOSSIBLE__ -- | 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 l `notWorse` Decr k = k < 0 || l >= k -- we are increasing or -- we are decreasing, but more -- 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) => NotWorse (Matrix i Order) where m `notWorse` n | size m /= size n = __IMPOSSIBLE__ | otherwise = Fold.all isTrue $ 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 = Unknown `notWorse` o both = notWorse isTrue = id trivial = id -- | Raw increase which does not cut off. increase :: Int -> Order -> Order increase i o = case o of Unknown -> Unknown Decr k -> Decr $ k - i Mat m -> Mat $ fmap (increase i) m -- | Raw decrease which does not cut off. decrease :: Int -> Order -> Order decrease i o = increase (-i) o -- | Smart constructor for @Decr k :: Order@ which cuts off too big values. -- -- Possible values for @k@: @- ?cutoff '<=' k '<=' ?cutoff + 1@. -- decr :: (?cutoff :: CutOff) => Int -> Order decr k = case ?cutoff of CutOff c | k < -c -> Unknown | k > c -> Decr $ c + 1 _ -> Decr k -- | Smart constructor for matrix shaped orders, avoiding empty and singleton matrices. orderMat :: Matrix Int Order -> Order orderMat m | Matrix.isEmpty m = Decr 0 -- 0x0 Matrix = neutral element | otherwise = case isSingleton m of Just o -> o -- 1x1 Matrix Nothing -> 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 prop_decr :: (?cutoff :: CutOff) => Int -> Bool prop_decr = isOrder . decr -- | @le@, @lt@, @decreasing@, @unknown@: for backwards compatibility, and for external use. le :: Order le = Decr 0 lt :: Order lt = Decr 1 unknown :: Order unknown = Unknown nonIncreasing :: Order -> Bool nonIncreasing (Decr k) = k >= 0 nonIncreasing _ = False decreasing :: Order -> Bool decreasing (Decr k) = 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 0) = text "=" pretty (Decr k) = text $ show (0 - k) pretty Unknown = text "?" pretty (Mat m) = text "Mat" <+> pretty m --instance Ord Order where -- max = maxO {- instances cannot have implicit arguments?! GHC manual says: 7.8.3.1. Implicit-parameter type constraints You can't have an implicit parameter in the context of a class or instance declaration. For example, both these declarations are illegal: class (?x::Int) => C a where ... instance (?x::a) => Foo [a] where ... Reason: exactly which implicit parameter you pick up depends on exactly where you invoke a function. But the ``invocation'' of instance declarations is done behind the scenes by the compiler, so it's hard to figure out exactly where it is done. Easiest thing is to outlaw the offending types. instance (?cutoff :: CutOff) => Arbitrary Order where arbitrary = frequency [(20, return Unknown) ,(80, elements [- ?cutoff .. ?cutoff + 1] >>= Decr) ] -- no embedded matrices generated for now. -} instance Arbitrary Order where arbitrary = frequency [(30, return Unknown) ,(70, elements [0,1] >>= return . Decr) ] -- no embedded matrices generated for now. instance CoArbitrary Order where coarbitrary (Decr k) = variant 0 coarbitrary Unknown = variant 1 coarbitrary (Mat m) = variant 2 -- | 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 k) .*. (Decr l) = decr (k + l) (Decr 0) .*. (Mat m) = Mat m (Decr k) .*. (Mat m) = (Decr k) .*. (collapse m) (Mat m1) .*. (Mat m2) = if (okM m1 m2) then Mat $ mul orderSemiring m1 m2 else (collapse m1) .*. (collapse m2) (Mat m) .*. (Decr 0) = Mat m (Mat m) .*. (Decr k) = (collapse m) .*. (Decr k) {- collapse m We assume that m codes a permutation: each row has at most one column that is not Un. 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 Un, i.e., no argument relates to that parameter, than the collapsed value is also Un. This makes order multiplication associative. -} collapse :: (?cutoff :: CutOff) => Matrix Int Order -> Order collapse m = -- if not $ Matrix.matrixInvariant m then __IMPOSSIBLE__ else 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' {- OLD CODE, does not give associative matrix multiplication: collapse :: (?cutoff :: CutOff) => Matrix Int Order -> Order collapse m = foldl (.*.) le (Data.Array.elems $ diagonal m) -} collapseO :: (?cutoff :: CutOff) => Order -> Order collapseO (Mat m) = collapse m collapseO o = o 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 (Decr k, Decr l) -> Decr (max k l) -- cut off not needed, within borders (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. -- 'Unknown' is the least element, thus, dominant. infimum :: (?cutoff :: CutOff) => [Order] -> Order infimum (o:l) = foldl' minO o l infimum [] = __IMPOSSIBLE__ minO :: (?cutoff :: CutOff) => Order -> Order -> Order minO o1 o2 = case (o1,o2) of (Unknown,_) -> Unknown (_,Unknown) -> Unknown (Decr k, Decr l) -> Decr (min k l) -- cut off not needed, within borders (Mat m1, Mat m2) -> if (size m1 == size m2) then Mat $ Matrix.intersectWith minO m1 m2 else minO (collapse m1) (collapse m2) (Mat m1,_) -> minO (collapse m1) o2 (_,Mat m2) -> minO o1 (collapse m2) {- Cannot have implicit arguments in instances. Too bad! instance Monoid Order where mempty = Unknown mappend = maxO instance (cutoff :: Int) => SemiRing Order where multiply = (.*.) -} orderSemiring :: (?cutoff :: CutOff) => Semiring Order orderSemiring = Semiring.Semiring { Semiring.add = maxO , Semiring.mul = (.*.) , Semiring.zero = Unknown -- , Semiring.one = Le } prop_orderSemiring :: (?cutoff :: CutOff) => Order -> Order -> Order -> Bool prop_orderSemiring = Semiring.semiringInvariant orderSemiring ------------------------------------------------------------------------ -- All tests tests :: IO Bool tests = runTests "Agda.Termination.Order" [ quickCheck' prop_decr , quickCheck' prop_orderSemiring ] where ?cutoff = DontCutOff -- CutOff 2 -- don't cut off in tests!