{-# 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
  , (.*.)
  , 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 {-# 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, 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 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
 | 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

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


-- | 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)
  | 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 @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
  (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.
--   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
  (Decr k, Decr l)       -> Decr (min k l) -- cut off not needed, within borders
  (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
  }