{-# 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Order -> Order -> Bool
$c/= :: Order -> Order -> Bool
== :: Order -> Order -> Bool
$c== :: Order -> Order -> Bool
Eq, Eq 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
min :: Order -> Order -> Order
$cmin :: Order -> Order -> Order
max :: Order -> Order -> Order
$cmax :: Order -> Order -> Order
>= :: Order -> Order -> Bool
$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
compare :: Order -> Order -> Ordering
$ccompare :: Order -> Order -> Ordering
Ord, Int -> Order -> ShowS
[Order] -> ShowS
Order -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Order] -> ShowS
$cshowList :: [Order] -> ShowS
show :: Order -> String
$cshow :: Order -> String
showsPrec :: Int -> Order -> ShowS
$cshowsPrec :: Int -> 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` forall a. Ord a => Comparable a
comparableOrd Int
k Int
l
    -- Matrix-shaped orders are no longer supported
    (Mat{}  , Order
_      ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    (Order
_      , Mat{}  ) -> forall a. HasCallStack => a
__IMPOSSIBLE__
    where
    comparableBool :: Bool -> Bool -> PartialOrdering
comparableBool = forall a b c. ((a, b) -> c) -> a -> b -> c
curry 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 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 forall a. Ord a => a -> a -> Bool
< Int
0   -- we are increasing or
    Bool -> Bool -> Bool
|| Int
l 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       = forall a. HasCallStack => a
__IMPOSSIBLE__
  Order
o       `notWorse` Mat Matrix Int Order
m   = 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
    | forall i b. Matrix i b -> Size i
size Matrix i o
m forall a. Eq a => a -> a -> Bool
/= forall i b. Matrix i b -> Size i
size Matrix i o
n = forall a. HasCallStack => a
__IMPOSSIBLE__
    | Bool
otherwise        = forall (t :: * -> *). Foldable t => t Bool -> Bool
Fold.and forall a b. (a -> b) -> a -> b
$ 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 forall {p}. p -> Bool
onlym forall {a}. (NotWorse a, HasZero a) => a -> Bool
onlyn o -> o -> Bool
both 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 = forall a. HasZero a => a
zeroElement forall a. NotWorse a => a -> a -> Bool
`notWorse` a
o
    both :: o -> o -> Bool
both    = forall a. NotWorse a => a -> a -> Bool
notWorse
    trivial :: a -> a
trivial = 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 forall a b. (a -> b) -> a -> b
$ Int
k 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 forall a b. (a -> b) -> a -> 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 of
  CutOff Int
c | Int
k forall a. Ord a => a -> a -> Bool
< -Int
c -> Order
Unknown
           | Int
k forall a. Ord a => a -> a -> Bool
> Int
c  -> Bool -> Int -> Order
Decr Bool
u forall a b. (a -> b) -> a -> b
$ Int
c 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
 | 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 <- 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 of
  CutOff
DontCutOff -> Bool
True
  CutOff Int
c   -> Int
k forall a. Ord a => a -> a -> Bool
>= -Int
c Bool -> Bool -> Bool
&& Int
k forall a. Ord a => a -> a -> Bool
<= Int
c 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
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 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 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Order -> Bool
isDecr forall a b. (a -> b) -> a -> b
$ 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) forall a b. (a -> b) -> a -> b
$ String -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show (forall a. Num a => a -> a
negate Int
k)
  pretty Order
Unknown    = Doc
"?"
  pretty (Mat Matrix Int Order
m)    = Doc
"Mat" Doc -> Doc -> 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
decr (Bool
u Bool -> Bool -> Bool
|| Bool
u') (Int
k 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
.*. ((?cutoff::CutOff) => 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 forall a b. (a -> b) -> a -> b
$ forall i a.
(Ix i, Eq a) =>
Semiring a -> Matrix i a -> Matrix i a -> Matrix i a
mul (?cutoff::CutOff) => Semiring Order
orderSemiring Matrix Int Order
m1 Matrix Int Order
m2
  | Bool
otherwise              = ((?cutoff::CutOff) => Matrix Int Order -> Order
collapse Matrix Int Order
m1) (?cutoff::CutOff) => Order -> Order -> Order
.*. ((?cutoff::CutOff) => 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
collapse Matrix Int Order
m) (?cutoff::CutOff) => 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 forall i b. (Integral i, HasZero b) => Matrix i b -> [[b]]
toLists forall a b. (a -> b) -> a -> b
$ forall a. Transpose a => a -> a
Matrix.transpose Matrix Int Order
m of
  [] -> forall a. HasCallStack => a
__IMPOSSIBLE__   -- This can never happen if order matrices are generated by the smart constructor
  [[Order]]
m' -> forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::CutOff) => Order -> Order -> Order
(.*.) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (?cutoff::CutOff) => 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
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 = forall i. Size i -> i
rows (forall i b. Matrix i b -> Size i
size Matrix Int Order
m2) forall a. Eq a => a -> a -> Bool
== forall i. Size i -> i
cols (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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (?cutoff::CutOff) => 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 forall a. Ord a => a -> a -> Bool
> Int
0 -> Order
o2
  (Decr Bool
True  Int
k, Decr Bool
False Int
_) | Int
k forall a. Ord a => a -> a -> Bool
> Int
0 -> Order
o1
  (Decr Bool
u Int
k, Decr Bool
u' Int
l) -> if Int
l 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 (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
maxO Matrix Int Order
m1 Matrix Int Order
m2)
  (Mat Matrix Int Order
m, Order
_)       -> (?cutoff::CutOff) => Order -> Order -> Order
maxO ((?cutoff::CutOff) => Matrix Int Order -> Order
collapse Matrix Int Order
m) Order
o2
  (Order
_, Mat Matrix Int Order
m)       -> (?cutoff::CutOff) => Order -> Order -> Order
maxO Order
o1 ((?cutoff::CutOff) => 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) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (?cutoff::CutOff) => Order -> Order -> Order
minO Order
o [Order]
l
infimum []    = 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 forall a. Ord a => a -> a -> Bool
<= Int
0 Bool -> Bool -> Bool
|| Int
k 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 forall a. Ord a => a -> a -> Bool
<= Int
0 Bool -> Bool -> Bool
|| Int
l 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 (forall a. Ord a => a -> a -> a
min Int
k Int
l)
  (Mat Matrix Int Order
m1, Mat Matrix Int Order
m2)
    | forall i b. Matrix i b -> Size i
size Matrix Int Order
m1 forall a. Eq a => a -> a -> Bool
== forall i b. Matrix i b -> Size i
size Matrix Int Order
m2 -> Matrix Int Order -> Order
Mat forall a b. (a -> b) -> a -> b
$ forall i a.
Ord i =>
(a -> a -> a) -> Matrix i a -> Matrix i a -> Matrix i a
Matrix.intersectWith (?cutoff::CutOff) => Order -> Order -> Order
minO Matrix Int Order
m1 Matrix Int Order
m2
    | Bool
otherwise          -> (?cutoff::CutOff) => Order -> Order -> Order
minO ((?cutoff::CutOff) => Matrix Int Order -> Order
collapse Matrix Int Order
m1) ((?cutoff::CutOff) => Matrix Int Order -> Order
collapse Matrix Int Order
m2)
  (Mat Matrix Int Order
m1, Order
_)            -> (?cutoff::CutOff) => Order -> Order -> Order
minO ((?cutoff::CutOff) => Matrix Int Order -> Order
collapse Matrix Int Order
m1) Order
o2
  (Order
_, Mat Matrix Int Order
m2)            -> (?cutoff::CutOff) => Order -> Order -> Order
minO Order
o1 ((?cutoff::CutOff) => 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
maxO
  , mul :: Order -> Order -> Order
Semiring.mul  = (?cutoff::CutOff) => Order -> Order -> Order
(.*.)
  , zero :: Order
Semiring.zero = Order
Unknown
  -- , Semiring.one  = Le
  }