{-# 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 Mikan.Termination.Order
  ( -- * Structural orderings
    Order(..), decr
  , increase, decrease, setUsability
  , (.*.)
  , supremum, infimum
  , orderSemiring
  , le, lt, unknown
  , nonIncreasing, decreasing, isDecr
  , NotWorse(..)
  , isOrder
  ) where

import Data.Foldable qualified as Fold
import Data.List qualified as List

import Mikan.Termination.CutOff
import Mikan.Termination.SparseMatrix as Matrix
import Mikan.Termination.Semiring (HasZero(..), Semiring)
import Mikan.Termination.Semiring qualified as Semiring

import Mikan.Utils.PartialOrd
import Mikan.Syntax.Common.Pretty

import Mikan.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.
    --
    --   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.
  deriving (Order -> Order -> Bool
(Order -> Order -> Bool) -> (Order -> Order -> Bool) -> Eq Order
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Order -> Order -> Bool
== :: Order -> Order -> Bool
$c/= :: Order -> Order -> Bool
/= :: Order -> Order -> Bool
Eq, Eq Order
Eq Order =>
(Order -> Order -> Ordering)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Bool)
-> (Order -> Order -> Order)
-> (Order -> Order -> Order)
-> Ord Order
Order -> Order -> Bool
Order -> Order -> Ordering
Order -> Order -> Order
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Order -> Order -> Ordering
compare :: Order -> Order -> Ordering
$c< :: Order -> Order -> Bool
< :: Order -> Order -> Bool
$c<= :: Order -> Order -> Bool
<= :: Order -> Order -> Bool
$c> :: Order -> Order -> Bool
> :: Order -> Order -> Bool
$c>= :: Order -> Order -> Bool
>= :: Order -> Order -> Bool
$cmax :: Order -> Order -> Order
max :: Order -> Order -> Order
$cmin :: Order -> Order -> Order
min :: Order -> Order -> Order
Ord, Int -> Order -> ShowS
[Order] -> ShowS
Order -> String
(Int -> Order -> ShowS)
-> (Order -> String) -> ([Order] -> ShowS) -> Show Order
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Order -> ShowS
showsPrec :: Int -> Order -> ShowS
$cshow :: Order -> String
show :: Order -> String
$cshowList :: [Order] -> ShowS
showList :: [Order] -> ShowS
Show)

instance HasZero Order where
  zeroElement :: Order
zeroElement = Order
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 :: Comparable Order
comparable Order
o Order
o' = case (Order
o, Order
o') of
    (Order
Unknown, Order
Unknown) -> PartialOrdering
POEQ
    (Order
Unknown, Order
_      ) -> PartialOrdering
POLT
    (Order
_      , Order
Unknown) -> PartialOrdering
POGT
    (Decr Bool
u Int
k, Decr Bool
u' Int
l) -> Bool -> Bool -> PartialOrdering
comparableBool Bool
u Bool
u' PartialOrdering -> PartialOrdering -> PartialOrdering
`orPO` Comparable Int
forall a. Ord a => Comparable a
comparableOrd Int
k Int
l
    where
    comparableBool :: Bool -> Bool -> PartialOrdering
comparableBool = ((Bool, Bool) -> PartialOrdering)
-> Bool -> Bool -> PartialOrdering
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((Bool, Bool) -> PartialOrdering)
 -> Bool -> Bool -> PartialOrdering)
-> ((Bool, Bool) -> PartialOrdering)
-> Bool
-> Bool
-> PartialOrdering
forall a b. (a -> b) -> a -> b
$ \case
      (Bool
False, Bool
True) -> PartialOrdering
POLT
      (Bool
True, Bool
False) -> PartialOrdering
POGT
      (Bool, Bool)
_ -> PartialOrdering
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
  Order
o        notWorse :: Order -> Order -> Bool
`notWorse` Order
Unknown  = Bool
True            -- we are unboundedly increasing
  Order
Unknown  `notWorse` Decr Bool
_ Int
k = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0           -- we are increasing
  Decr Bool
u Int
l `notWorse` Decr Bool
u' Int
k = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0   -- we are increasing or
    Bool -> Bool -> Bool
|| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k Bool -> Bool -> Bool
&& (Bool
u Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
u')            -- we are decreasing, but not less, and not less usable

-- | We assume the matrices have the same dimension.
instance (Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) where
  Matrix i o
m notWorse :: Matrix i o -> Matrix i o -> Bool
`notWorse` Matrix i o
n
    | Matrix i o -> Size i
forall i b. Matrix i b -> Size i
size Matrix i o
m Size i -> Size i -> Bool
forall a. Eq a => a -> a -> Bool
/= Matrix i o -> Size i
forall i b. Matrix i b -> Size i
size Matrix i o
n = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
    | Bool
otherwise        = Matrix i Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
Fold.and (Matrix i Bool -> Bool) -> Matrix i Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (o -> Bool)
-> (o -> Bool)
-> (o -> o -> Bool)
-> (Bool -> Bool)
-> Matrix i o
-> Matrix i o
-> Matrix i Bool
forall a b c i.
Ord i =>
(a -> c)
-> (b -> c)
-> (a -> b -> c)
-> (c -> Bool)
-> Matrix i a
-> Matrix i b
-> Matrix i c
zipMatrices o -> Bool
forall {p}. p -> Bool
onlym o -> Bool
forall {a}. (NotWorse a, HasZero a) => a -> Bool
onlyn o -> o -> Bool
both Bool -> Bool
forall {a}. a -> a
trivial Matrix i o
m Matrix i o
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 :: p -> Bool
onlym p
o = Bool
True     -- @== o `notWorse` Unknown@
    onlyn :: a -> Bool
onlyn a
o = a
forall a. HasZero a => a
zeroElement a -> a -> Bool
forall a. NotWorse a => a -> a -> Bool
`notWorse` a
o
    both :: o -> o -> Bool
both    = o -> o -> Bool
forall a. NotWorse a => a -> a -> Bool
notWorse
    trivial :: a -> a
trivial = a -> a
forall {a}. a -> a
id  -- @True@ counts as zero as it is neutral for @and@

-- | Raw increase which does not cut off.
increase :: Int -> Order -> Order
increase :: Int -> Order -> Order
increase Int
i = \case
  Order
Unknown  -> Order
Unknown
  Decr Bool
u Int
k -> Bool -> Int -> Order
Decr Bool
u (Int -> Order) -> Int -> Order
forall a b. (a -> b) -> a -> b
$ Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i   -- TODO: should we set u to False if k - i < 0 ?

-- | Raw decrease which does not cut off.
decrease :: Int -> Order -> Order
decrease :: Int -> Order -> Order
decrease Int
i Order
o = Int -> Order -> Order
increase (-Int
i) Order
o

setUsability :: Bool -> Order -> Order
setUsability :: Bool -> Order -> Order
setUsability Bool
u Order
o = case Order
o of
  Decr Bool
_ Int
k -> Bool -> Int -> Order
Decr Bool
u Int
k
  Order
Unknown  -> Order
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 :: (?cutoff::CutOff) => Bool -> Int -> Order
decr Bool
u Int
k = case ?cutoff::CutOff
CutOff
?cutoff of
  CutOff Int
c | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< -Int
c -> Order
Unknown
           | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
c  -> Bool -> Int -> Order
Decr Bool
u (Int -> Order) -> Int -> Order
forall a b. (a -> b) -> a -> b
$ Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  CutOff
_                 -> Bool -> Int -> Order
Decr Bool
u Int
k

withinCutOff :: (?cutoff :: CutOff) => Int -> Bool
withinCutOff :: (?cutoff::CutOff) => Int -> Bool
withinCutOff Int
k = case ?cutoff::CutOff
CutOff
?cutoff of
  CutOff
DontCutOff -> Bool
True
  CutOff Int
c   -> Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= -Int
c Bool -> Bool -> Bool
&& Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

isOrder :: (?cutoff :: CutOff) => Order -> Bool
isOrder :: (?cutoff::CutOff) => Order -> Bool
isOrder (Decr Bool
_ Int
k) = (?cutoff::CutOff) => Int -> Bool
Int -> Bool
withinCutOff Int
k
isOrder Order
Unknown    = Bool
True

-- | @le@, @lt@, @decreasing@, @unknown@: for backwards compatibility, and for external use.
le :: Order
le :: Order
le = Bool -> Int -> Order
Decr Bool
False Int
0

-- | Usable decrease.
lt :: Order
lt :: Order
lt = Bool -> Int -> Order
Decr Bool
True Int
1

unknown :: Order
unknown :: Order
unknown = Order
Unknown

nonIncreasing :: Order -> Bool
nonIncreasing :: Order -> Bool
nonIncreasing (Decr Bool
_ Int
k) = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0
nonIncreasing Order
_          = Bool
False

-- | Decreasing and usable?
decreasing :: Order -> Bool
decreasing :: Order -> Bool
decreasing (Decr Bool
u Int
k) = Bool
u Bool -> Bool -> Bool
&& Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
decreasing Order
_ = Bool
False

-- | Matrix-shaped order is decreasing if any diagonal element is decreasing.
isDecr :: Order -> Bool
isDecr :: Order -> Bool
isDecr Order
o = Order -> Bool
decreasing Order
o

instance Pretty Order where
  pretty :: Order -> Doc
pretty (Decr Bool
u Int
0) = Doc
"="
  pretty (Decr Bool
u Int
k) = Bool -> Doc -> Doc
mparens (Bool -> Bool
not Bool
u) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show (Int -> Int
forall a. Num a => a -> a
negate Int
k)
  pretty Order
Unknown    = Doc
"?"


-- | 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
Order
Unknown    .*. :: (?cutoff::CutOff) => Order -> Order -> Order
.*. Order
_           = Order
Unknown
(Decr Bool
_ Int
k) .*. Order
Unknown     = Order
Unknown
(Decr Bool
u Int
k) .*. (Decr Bool
u' Int
l) = (?cutoff::CutOff) => Bool -> Int -> Order
Bool -> Int -> Order
decr (Bool
u Bool -> Bool -> Bool
|| Bool
u') (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
l)  -- if one is usable, so is the composition

-- | 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 :: [Order] -> Order
supremum :: [Order] -> Order
supremum = (Order -> Order -> Order) -> Order -> [Order] -> Order
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Order -> Order -> Order
maxO Order
Unknown

-- | @('Order', 'maxO', '.*.')@ forms a semiring,
--   with 'Unknown' as zero and 'Le' as one.

maxO :: Order -> Order -> Order
maxO :: Order -> Order -> Order
maxO Order
o1 Order
o2 = case (Order
o1,Order
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 Bool
False Int
_, Decr Bool
True  Int
l) | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Order
o2
  (Decr Bool
True  Int
k, Decr Bool
False Int
_) | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Order
o1
  (Decr Bool
u Int
k, Decr Bool
u' Int
l) -> if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
k then Order
o2 else Order
o1
  (Order
Unknown, Order
_)     -> Order
o2
  (Order
_, Order
Unknown)     -> Order
o1

-- | The infimum of a (non empty) list of 'Order's.
--   Gets the worst information.
--  'Unknown' is the least element, thus, dominant.
infimum :: [Order] -> Order
infimum :: [Order] -> Order
infimum (Order
o:[Order]
l) = (Order -> Order -> Order) -> Order -> [Order] -> Order
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Order -> Order -> Order
minO Order
o [Order]
l
infimum []    = Order
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Pick the worst information.
minO :: Order -> Order -> Order
minO :: Order -> Order -> Order
minO Order
o1 Order
o2 = case (Order
o1,Order
o2) of
  (Order
Unknown, Order
_)           -> Order
Unknown
  (Order
_, Order
Unknown)           -> Order
Unknown
  -- different usability:
  -- We pick the unusable one if it is not a decrease or
  -- decreases not more than the usable one.
  (Decr Bool
False Int
k, Decr Bool
True  Int
l) -> if Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 Bool -> Bool -> Bool
|| Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
l then Order
o1 else Order
o2
  (Decr Bool
True  Int
k, Decr Bool
False Int
l) -> if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 Bool -> Bool -> Bool
|| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
k then Order
o2 else Order
o1
  -- same usability:
  (Decr Bool
u Int
k, Decr Bool
_ Int
l) -> Bool -> Int -> Order
Decr Bool
u (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
k Int
l)


-- | 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 :: (?cutoff::CutOff) => Semiring Order
orderSemiring = Semiring.Semiring
  { add :: Order -> Order -> Order
Semiring.add  = Order -> Order -> Order
maxO
  , mul :: Order -> Order -> Order
Semiring.mul  = (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
(.*.)
  , zero :: Order
Semiring.zero = Order
Unknown
  -- , Semiring.one  = Le
  }