    {-# 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
    /= :: Order -> Order -> Bool
    $c/= :: Order -> Order -> Bool
    == :: Order -> Order -> Bool
    $c== :: 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
    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
    (Int -> Order -> ShowS)
    -> (Order -> String) -> ([Order] -> ShowS) -> Show Order
    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` 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 (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 (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 (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 (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 (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 :: forall a. (a -> a -> a) -> (a -> a -> a) -> a -> Semiring a
    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
      }