content: {-# OPTIONS_GHC -Wunused-imports #-}
  
  {-# 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.Syntax.Common.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
    }
  