{-# 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.Utils.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
/= :: 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
$cp1Ord :: Eq 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
showList :: [Order] -> ShowS
$cshowList :: [Order] -> ShowS
show :: Order -> String
$cshow :: Order -> String
showsPrec :: Int -> Order -> ShowS
$cshowsPrec :: Int -> Order -> ShowS
Show)
instance HasZero Order where
zeroElement :: Order
zeroElement = Order
Unknown
instance PartialOrd Order where
comparable :: Comparable Order
comparable o :: Order
o o' :: Order
o' = case (Order
o, Order
o') of
(Unknown, Unknown) -> PartialOrdering
POEQ
(Unknown, _ ) -> PartialOrdering
POLT
(_ , Unknown) -> PartialOrdering
POGT
(Decr u :: Bool
u k :: Int
k, Decr u' :: Bool
u' l :: 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{} , _ ) -> PartialOrdering
forall a. HasCallStack => a
__IMPOSSIBLE__
(_ , 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
(False, True) -> PartialOrdering
POLT
(True, False) -> PartialOrdering
POGT
_ -> PartialOrdering
POEQ
class NotWorse a where
notWorse :: a -> a -> Bool
instance NotWorse Order where
o :: Order
o notWorse :: Order -> Order -> Bool
`notWorse` Unknown = Bool
True
Unknown `notWorse` Decr _ k :: Int
k = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0
Decr u :: Bool
u l :: Int
l `notWorse` Decr u' :: Bool
u' k :: Int
k = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 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 m :: Matrix Int Order
m `notWorse` o :: Order
o = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
o :: Order
o `notWorse` Mat m :: Matrix Int Order
m = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
instance (Ord i, HasZero o, NotWorse o) => NotWorse (Matrix i o) where
m :: Matrix i o
m notWorse :: Matrix i o -> Matrix i o -> Bool
`notWorse` n :: 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 o :: p
o = Bool
True
onlyn :: a -> Bool
onlyn o :: 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 i :: Int
i o :: Order
o = case Order
o of
Unknown -> Order
Unknown
Decr u :: Bool
u k :: 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 m :: 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
decrease :: Int -> Order -> Order
decrease :: Int -> Order -> Order
decrease i :: Int
i o :: Order
o = Int -> Order -> Order
increase (-Int
i) Order
o
setUsability :: Bool -> Order -> Order
setUsability :: Bool -> Order -> Order
setUsability u :: Bool
u o :: Order
o = case Order
o of
Decr _ k :: Int
k -> Bool -> Int -> Order
Decr Bool
u Int
k
Unknown -> Order
o
Mat{} -> Order
o
decr :: (?cutoff :: CutOff) => Bool -> Int -> Order
decr :: Bool -> Int -> Order
decr u :: Bool
u k :: Int
k = case ?cutoff::CutOff
CutOff
?cutoff of
CutOff c :: 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
+ 1
_ -> Bool -> Int -> Order
Decr Bool
u Int
k
orderMat :: Matrix Int Order -> Order
orderMat :: Matrix Int Order -> Order
orderMat m :: 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 o :: 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 :: Int -> Bool
withinCutOff k :: Int
k = case ?cutoff::CutOff
CutOff
?cutoff of
DontCutOff -> Bool
True
CutOff c :: 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
+ 1
isOrder :: (?cutoff :: CutOff) => Order -> Bool
isOrder :: Order -> Bool
isOrder (Decr _ k :: Int
k) = (?cutoff::CutOff) => Int -> Bool
Int -> Bool
withinCutOff Int
k
isOrder Unknown = Bool
True
isOrder (Mat m :: Matrix Int Order
m) = Bool
False
le :: Order
le :: Order
le = Bool -> Int -> Order
Decr Bool
False 0
lt :: Order
lt :: Order
lt = Bool -> Int -> Order
Decr Bool
True 1
unknown :: Order
unknown :: Order
unknown = Order
Unknown
nonIncreasing :: Order -> Bool
nonIncreasing :: Order -> Bool
nonIncreasing (Decr _ k :: Int
k) = Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0
nonIncreasing _ = Bool
False
decreasing :: Order -> Bool
decreasing :: Order -> Bool
decreasing (Decr u :: Bool
u k :: Int
k) = Bool
u Bool -> Bool -> Bool
&& Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0
decreasing _ = Bool
False
isDecr :: Order -> Bool
isDecr :: Order -> Bool
isDecr (Mat m :: 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 o :: Order
o = Order -> Bool
decreasing Order
o
instance Pretty Order where
pretty :: Order -> Doc
pretty (Decr u :: Bool
u 0) = "="
pretty (Decr u :: Bool
u k :: 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 (0 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
pretty Unknown = "?"
pretty (Mat m :: Matrix Int Order
m) = "Mat" Doc -> Doc -> Doc
<+> Matrix Int Order -> Doc
forall a. Pretty a => a -> Doc
pretty Matrix Int Order
m
(.*.) :: (?cutoff :: CutOff) => Order -> Order -> Order
Unknown .*. :: Order -> Order -> Order
.*. _ = Order
Unknown
(Mat m :: Matrix Int Order
m) .*. Unknown = Order
Unknown
(Decr _ k :: Int
k) .*. Unknown = Order
Unknown
(Decr u :: Bool
u k :: Int
k) .*. (Decr u' :: Bool
u' l :: 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 _ 0) .*. (Mat m :: Matrix Int Order
m) = Matrix Int Order -> Order
Mat Matrix Int Order
m
(Decr u :: Bool
u k :: Int
k) .*. (Mat m :: 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 m1 :: Matrix Int Order
m1) .*. (Mat m2 :: 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 m :: Matrix Int Order
m) .*. (Decr _ 0) = Matrix Int Order -> Order
Mat Matrix Int Order
m
(Mat m :: Matrix Int Order
m) .*. (Decr u :: Bool
u k :: 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 :: Matrix Int Order -> Order
collapse m :: 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__
m' :: [[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 :: Order -> Order
collapseO (Mat m :: Matrix Int Order
m) = (?cutoff::CutOff) => Matrix Int Order -> Order
Matrix Int Order -> Order
collapse Matrix Int Order
m
collapseO o :: Order
o = Order
o
okM :: Matrix Int Order -> Matrix Int Order -> Bool
okM :: Matrix Int Order -> Matrix Int Order -> Bool
okM m1 :: Matrix Int Order
m1 m2 :: Matrix Int Order
m2 = (Size Int -> Int
forall i. Size i -> i
rows (Size Int -> Int) -> Size Int -> Int
forall a b. (a -> b) -> a -> b
$ 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 (Size Int -> Int) -> Size Int -> Int
forall a b. (a -> b) -> a -> b
$ Matrix Int Order -> Size Int
forall i b. Matrix i b -> Size i
size Matrix Int Order
m1)
supremum :: (?cutoff :: CutOff) => [Order] -> Order
supremum :: [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
maxO :: (?cutoff :: CutOff) => Order -> Order -> Order
maxO :: Order -> Order -> Order
maxO o1 :: Order
o1 o2 :: Order
o2 = case (Order
o1,Order
o2) of
(Decr False _, Decr True l :: Int
l) | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> Order
o2
(Decr True k :: Int
k, Decr False _) | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> Order
o1
(Decr u :: Bool
u k :: Int
k, Decr u' :: Bool
u' l :: Int
l) -> if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
k then Order
o2 else Order
o1
(Unknown, _) -> Order
o2
(_, Unknown) -> Order
o1
(Mat m1 :: Matrix Int Order
m1, Mat m2 :: 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 m :: Matrix Int Order
m, _) -> (?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
(_, Mat m :: 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 :: [Order] -> Order
infimum (o :: Order
o:l :: [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__
minO :: (?cutoff :: CutOff) => Order -> Order -> Order
minO :: Order -> Order -> Order
minO o1 :: Order
o1 o2 :: Order
o2 = case (Order
o1,Order
o2) of
(Unknown, _) -> Order
Unknown
(_, Unknown) -> Order
Unknown
(Decr False k :: Int
k, Decr True l :: Int
l) -> if Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 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 True k :: Int
k, Decr False l :: Int
l) -> if Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 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 u :: Bool
u k :: Int
k, Decr _ l :: Int
l) -> Bool -> Int -> Order
Decr Bool
u (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
k Int
l)
(Mat m1 :: Matrix Int Order
m1, Mat m2 :: 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 m1 :: Matrix Int Order
m1, _) -> (?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
(_, Mat m2 :: 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 :: 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
}