{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE ImplicitParams #-}
module Agda.Termination.Order
(
Order(..), decr
, increase, decrease, setUsability
, (.*.)
, supremum, infimum
, orderSemiring
, le, lt, unknown, orderMat, collapseO
, nonIncreasing, decreasing, isDecr
, NotWorse(..)
, isOrder
) where
import qualified Data.Foldable as Fold
import qualified Data.List as List
import Agda.Termination.CutOff
import Agda.Termination.SparseMatrix as Matrix
import Agda.Termination.Semiring (HasZero(..), Semiring)
import qualified Agda.Termination.Semiring as Semiring
import Agda.Utils.PartialOrd
import Agda.Syntax.Common.Pretty
import Agda.Utils.Impossible
data Order
= Decr !Bool {-# UNPACK #-} !Int
| Unknown
| Mat {-# UNPACK #-} !(Matrix Int Order)
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
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
(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
class NotWorse a where
notWorse :: a -> a -> Bool
instance NotWorse Order where
Order
o notWorse :: Order -> Order -> Bool
`notWorse` Order
Unknown = Bool
True
Order
Unknown `notWorse` Decr Bool
_ Int
k = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
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
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')
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__
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
onlym :: p -> Bool
onlym p
o = Bool
True
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
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
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
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
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
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
| 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
| Bool
otherwise = Matrix Int Order -> Order
Mat Matrix Int Order
m
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
le :: Order
le :: Order
le = Bool -> Int -> Order
Decr Bool
False Int
0
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 :: 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
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
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
"?"
pretty (Mat Matrix Int Order
m) = Doc
"Mat" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Matrix Int Order -> Doc
forall a. Pretty a => a -> Doc
pretty Matrix Int Order
m
(.*.) :: (?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)
(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 :: (?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__
[[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
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)
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
maxO :: (?cutoff :: CutOff) => Order -> Order -> Order
maxO :: (?cutoff::CutOff) => Order -> Order -> Order
maxO Order
o1 Order
o2 = case (Order
o1,Order
o2) of
(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)
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__
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
(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
(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)
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
}