module Agda.Termination.Order
(
Order(..), decr
, increase, decrease
, (.*.)
, 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
data Order
= Decr !Int
| Unknown
| Mat !(Matrix Int Order)
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
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
(Mat{} , _ ) -> __IMPOSSIBLE__
(_ , Mat{} ) -> __IMPOSSIBLE__
class NotWorse a where
notWorse :: a -> a -> Bool
instance NotWorse Order where
o `notWorse` Unknown = True
Unknown `notWorse` Decr k = k < 0
Decr l `notWorse` Decr k = k < 0 || l >= k
Mat m `notWorse` o = __IMPOSSIBLE__
o `notWorse` Mat m = __IMPOSSIBLE__
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
onlym o = True
onlyn o = zeroElement `notWorse` o
both = notWorse
trivial = id
increase :: Int -> Order -> Order
increase i o = case o of
Unknown -> Unknown
Decr k -> Decr $ k i
Mat m -> Mat $ fmap (increase i) m
decrease :: Int -> Order -> Order
decrease i o = increase (i) o
decr :: (?cutoff :: CutOff) => Int -> Order
decr k = case ?cutoff of
CutOff c | k < c -> Unknown
| k > c -> Decr $ c + 1
_ -> Decr k
orderMat :: Matrix Int Order -> Order
orderMat m
| Matrix.isEmpty m = Decr 0
| Just o <- isSingleton m = o
| otherwise = Mat m
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
prop_decr :: (?cutoff :: CutOff) => Int -> Bool
prop_decr = isOrder . decr
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
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
(.*.) :: (?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)
| okM m1 m2 = Mat $ mul orderSemiring m1 m2
| otherwise = (collapse m1) .*. (collapse m2)
(Mat m) .*. (Decr 0) = Mat m
(Mat m) .*. (Decr k) = (collapse m) .*. (Decr k)
collapse :: (?cutoff :: CutOff) => Matrix Int Order -> Order
collapse m = case toLists $ Matrix.transpose m of
[] -> __IMPOSSIBLE__
m' -> foldl1 (.*.) $ map (foldl1 maxO) 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)
supremum :: (?cutoff :: CutOff) => [Order] -> Order
supremum = foldr maxO Unknown
maxO :: (?cutoff :: CutOff) => Order -> Order -> Order
maxO o1 o2 = case (o1,o2) of
(Decr k, Decr l) -> Decr (max k l)
(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)
infimum :: (?cutoff :: CutOff) => [Order] -> Order
infimum (o:l) = List.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)
(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)
orderSemiring :: (?cutoff :: CutOff) => Semiring Order
orderSemiring = Semiring.Semiring
{ Semiring.add = maxO
, Semiring.mul = (.*.)
, Semiring.zero = Unknown
}