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