{-# 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) = text "="
  pretty (Decr u k) = mparens (not u) $ text $ show (0 - k)
  pretty Unknown    = text "?"
  pretty (Mat m)    = text "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
  }