{-# 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

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 = \case
  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 (negate 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
  }