{-# 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

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 (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 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 :: 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
    -- Matrix-shaped orders are no longer supported
    (Mat{}  , Order
_      ) -> PartialOrdering
forall a. HasCallStack => a
__IMPOSSIBLE__
    (Order
_      , Mat{}  ) -> PartialOrdering
forall a. HasCallStack => a
__IMPOSSIBLE__
    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
  -- Matrix-shaped orders are no longer supported
  Mat Matrix Int Order
m   `notWorse` Order
o       = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
  Order
o       `notWorse` Mat Matrix Int Order
m   = Bool
forall a. HasCallStack => a
__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
  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 ?
  Mat Matrix Int Order
m    -> Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ (Order -> Order) -> Matrix Int Order -> Matrix Int Order
forall a b. (a -> b) -> Matrix Int a -> Matrix Int b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Order -> Order
increase Int
i) Matrix Int Order
m

-- | 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
  Mat{}    -> 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

-- | Smart constructor for matrix shaped orders, avoiding empty and singleton matrices.
orderMat :: Matrix Int Order -> Order
orderMat :: Matrix Int Order -> Order
orderMat Matrix Int Order
m
 | Matrix Int Order -> Bool
forall i b. (Num i, Ix i) => Matrix i b -> Bool
Matrix.isEmpty Matrix Int Order
m        = Order
le     -- 0x0 Matrix = neutral element
 | Just Order
o <- Matrix Int Order -> Maybe Order
forall i b. (Eq i, Num i, HasZero b) => Matrix i b -> Maybe b
isSingleton Matrix Int Order
m = Order
o      -- 1x1 Matrix
 | Bool
otherwise               = Matrix Int Order -> Order
Mat Matrix Int Order
m  -- nxn Matrix

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
isOrder (Mat Matrix Int Order
m)    = Bool
False  -- TODO: extend to matrices

-- | @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 (Mat Matrix Int Order
m) = (Order -> Bool) -> [Order] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Order -> Bool
isDecr ([Order] -> Bool) -> [Order] -> Bool
forall a b. (a -> b) -> a -> b
$ Matrix Int Order -> [Order]
forall m e. Diagonal m e => m -> [e]
diagonal Matrix Int Order
m
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
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
"?"
  pretty (Mat Matrix Int Order
m)    = Doc
"Mat" Doc -> Doc -> Doc
<+> Matrix Int Order -> Doc
forall a. Pretty a => a -> Doc
pretty Matrix Int Order
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
Order
Unknown    .*. :: (?cutoff::CutOff) => Order -> Order -> Order
.*. Order
_           = Order
Unknown
(Mat Matrix Int Order
m)    .*. Order
Unknown     = 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
(Decr Bool
_ Int
0) .*. (Mat Matrix Int Order
m)     = Matrix Int Order -> Order
Mat Matrix Int Order
m
(Decr Bool
u Int
k) .*. (Mat Matrix Int Order
m)     = (Bool -> Int -> Order
Decr Bool
u Int
k) (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*. ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m)
(Mat Matrix Int Order
m1)   .*. (Mat Matrix Int Order
m2)
  | Matrix Int Order -> Matrix Int Order -> Bool
okM Matrix Int Order
m1 Matrix Int Order
m2              = Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ Semiring Order
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
(Ix i, Eq a) =>
Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
mul Semiring Order
(?cutoff::CutOff) => Semiring Order
orderSemiring Matrix Int Order
m1 Matrix Int Order
m2
  | Bool
otherwise              = ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*. ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m2)
(Mat Matrix Int Order
m)   .*. (Decr Bool
_ Int
0)   = Matrix Int Order -> Order
Mat Matrix Int Order
m
(Mat Matrix Int Order
m)   .*. (Decr Bool
u Int
k)   = ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m) (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
.*. (Bool -> Int -> Order
Decr Bool
u Int
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 :: (?cutoff::CutOff) => Matrix Int Order -> Order
collapse Matrix Int Order
m = case Matrix Int Order -> [[Order]]
forall i b. (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists (Matrix Int Order -> [[Order]]) -> Matrix Int Order -> [[Order]]
forall a b. (a -> b) -> a -> b
$ Matrix Int Order -> Matrix Int Order
forall a. Transpose a => a -> a
Matrix.transpose Matrix Int Order
m of
  [] -> Order
forall a. HasCallStack => a
__IMPOSSIBLE__   -- This can never happen if order matrices are generated by the smart constructor
  [[Order]]
m' -> (Order -> Order -> Order) -> [Order] -> Order
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
(.*.) ([Order] -> Order) -> [Order] -> Order
forall a b. (a -> b) -> a -> b
$ ([Order] -> Order) -> [[Order]] -> [Order]
forall a b. (a -> b) -> [a] -> [b]
map ((Order -> Order -> Order) -> [Order] -> Order
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
maxO) [[Order]]
m'

collapseO :: (?cutoff :: CutOff) => Order -> Order
collapseO :: (?cutoff::CutOff) => Order -> Order
collapseO (Mat Matrix Int Order
m) = (?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m
collapseO Order
o       = Order
o

-- | Can two matrices be multplied together?
okM :: Matrix Int Order -> Matrix Int Order -> Bool
okM :: Matrix Int Order -> Matrix Int Order -> Bool
okM Matrix Int Order
m1 Matrix Int Order
m2 = Size Int -> Int
forall i. Size i -> i
rows (Matrix Int Order -> Size Int
forall i b. Matrix i b -> Size i
size Matrix Int Order
m2) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Size Int -> Int
forall i. Size i -> i
cols (Matrix Int Order -> Size Int
forall i b. Matrix i b -> Size i
size Matrix Int Order
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 :: (?cutoff::CutOff) => [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 (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
maxO Order
Unknown

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

maxO :: (?cutoff :: CutOff) => Order -> Order -> Order
maxO :: (?cutoff::CutOff) => 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
  (Mat Matrix Int Order
m1, Mat Matrix Int Order
m2) -> Matrix Int Order -> Order
Mat ((Order -> Order -> Order)
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
(Ord i, HasZero a) =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
Matrix.add (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
maxO Matrix Int Order
m1 Matrix Int Order
m2)
  (Mat Matrix Int Order
m, Order
_)       -> (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
maxO ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m) Order
o2
  (Order
_, Mat Matrix Int Order
m)       -> (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
maxO Order
o1 ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
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 :: (?cutoff::CutOff) => [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' (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
minO Order
o [Order]
l
infimum []    = Order
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Pick the worst information.
minO :: (?cutoff :: CutOff) => Order -> Order -> Order
minO :: (?cutoff::CutOff) => 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)
  (Mat Matrix Int Order
m1, Mat Matrix Int Order
m2)
    | Matrix Int Order -> Size Int
forall i b. Matrix i b -> Size i
size Matrix Int Order
m1 Size Int -> Size Int -> Bool
forall a. Eq a => a -> a -> Bool
== Matrix Int Order -> Size Int
forall i b. Matrix i b -> Size i
size Matrix Int Order
m2 -> Matrix Int Order -> Order
Mat (Matrix Int Order -> Order) -> Matrix Int Order -> Order
forall a b. (a -> b) -> a -> b
$ (Order -> Order -> Order)
-> Matrix Int Order -> Matrix Int Order -> Matrix Int Order
forall i a.
Ord i =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
Matrix.intersectWith (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
minO Matrix Int Order
m1 Matrix Int Order
m2
    | Bool
otherwise          -> (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
minO ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m2)
  (Mat Matrix Int Order
m1, Order
_)            -> (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
minO ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m1) Order
o2
  (Order
_, Mat Matrix Int Order
m2)            -> (?cutoff::CutOff) => Order -> Order -> Order
Order -> Order -> Order
minO Order
o1 ((?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
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 :: (?cutoff::CutOff) => Semiring Order
orderSemiring = Semiring.Semiring
  { add :: Order -> Order -> Order
Semiring.add  = (?cutoff::CutOff) => Order -> Order -> Order
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
  }