{-# LANGUAGE CPP  #-}

-- | More monoids.

module Agda.Utils.Monoid where

#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup (Semigroup(..))
#endif


-- | Maximum of on-negative (small) natural numbers.

newtype MaxNat = MaxNat { MaxNat -> Int
getMaxNat :: Int }
  deriving (Integer -> MaxNat
MaxNat -> MaxNat
MaxNat -> MaxNat -> MaxNat
(MaxNat -> MaxNat -> MaxNat)
-> (MaxNat -> MaxNat -> MaxNat)
-> (MaxNat -> MaxNat -> MaxNat)
-> (MaxNat -> MaxNat)
-> (MaxNat -> MaxNat)
-> (MaxNat -> MaxNat)
-> (Integer -> MaxNat)
-> Num MaxNat
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: MaxNat -> MaxNat -> MaxNat
+ :: MaxNat -> MaxNat -> MaxNat
$c- :: MaxNat -> MaxNat -> MaxNat
- :: MaxNat -> MaxNat -> MaxNat
$c* :: MaxNat -> MaxNat -> MaxNat
* :: MaxNat -> MaxNat -> MaxNat
$cnegate :: MaxNat -> MaxNat
negate :: MaxNat -> MaxNat
$cabs :: MaxNat -> MaxNat
abs :: MaxNat -> MaxNat
$csignum :: MaxNat -> MaxNat
signum :: MaxNat -> MaxNat
$cfromInteger :: Integer -> MaxNat
fromInteger :: Integer -> MaxNat
Num, MaxNat -> MaxNat -> Bool
(MaxNat -> MaxNat -> Bool)
-> (MaxNat -> MaxNat -> Bool) -> Eq MaxNat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MaxNat -> MaxNat -> Bool
== :: MaxNat -> MaxNat -> Bool
$c/= :: MaxNat -> MaxNat -> Bool
/= :: MaxNat -> MaxNat -> Bool
Eq, Eq MaxNat
Eq MaxNat
-> (MaxNat -> MaxNat -> Ordering)
-> (MaxNat -> MaxNat -> Bool)
-> (MaxNat -> MaxNat -> Bool)
-> (MaxNat -> MaxNat -> Bool)
-> (MaxNat -> MaxNat -> Bool)
-> (MaxNat -> MaxNat -> MaxNat)
-> (MaxNat -> MaxNat -> MaxNat)
-> Ord MaxNat
MaxNat -> MaxNat -> Bool
MaxNat -> MaxNat -> Ordering
MaxNat -> MaxNat -> MaxNat
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 :: MaxNat -> MaxNat -> Ordering
compare :: MaxNat -> MaxNat -> Ordering
$c< :: MaxNat -> MaxNat -> Bool
< :: MaxNat -> MaxNat -> Bool
$c<= :: MaxNat -> MaxNat -> Bool
<= :: MaxNat -> MaxNat -> Bool
$c> :: MaxNat -> MaxNat -> Bool
> :: MaxNat -> MaxNat -> Bool
$c>= :: MaxNat -> MaxNat -> Bool
>= :: MaxNat -> MaxNat -> Bool
$cmax :: MaxNat -> MaxNat -> MaxNat
max :: MaxNat -> MaxNat -> MaxNat
$cmin :: MaxNat -> MaxNat -> MaxNat
min :: MaxNat -> MaxNat -> MaxNat
Ord, Int -> MaxNat -> ShowS
[MaxNat] -> ShowS
MaxNat -> String
(Int -> MaxNat -> ShowS)
-> (MaxNat -> String) -> ([MaxNat] -> ShowS) -> Show MaxNat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MaxNat -> ShowS
showsPrec :: Int -> MaxNat -> ShowS
$cshow :: MaxNat -> String
show :: MaxNat -> String
$cshowList :: [MaxNat] -> ShowS
showList :: [MaxNat] -> ShowS
Show, Int -> MaxNat
MaxNat -> Int
MaxNat -> [MaxNat]
MaxNat -> MaxNat
MaxNat -> MaxNat -> [MaxNat]
MaxNat -> MaxNat -> MaxNat -> [MaxNat]
(MaxNat -> MaxNat)
-> (MaxNat -> MaxNat)
-> (Int -> MaxNat)
-> (MaxNat -> Int)
-> (MaxNat -> [MaxNat])
-> (MaxNat -> MaxNat -> [MaxNat])
-> (MaxNat -> MaxNat -> [MaxNat])
-> (MaxNat -> MaxNat -> MaxNat -> [MaxNat])
-> Enum MaxNat
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: MaxNat -> MaxNat
succ :: MaxNat -> MaxNat
$cpred :: MaxNat -> MaxNat
pred :: MaxNat -> MaxNat
$ctoEnum :: Int -> MaxNat
toEnum :: Int -> MaxNat
$cfromEnum :: MaxNat -> Int
fromEnum :: MaxNat -> Int
$cenumFrom :: MaxNat -> [MaxNat]
enumFrom :: MaxNat -> [MaxNat]
$cenumFromThen :: MaxNat -> MaxNat -> [MaxNat]
enumFromThen :: MaxNat -> MaxNat -> [MaxNat]
$cenumFromTo :: MaxNat -> MaxNat -> [MaxNat]
enumFromTo :: MaxNat -> MaxNat -> [MaxNat]
$cenumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat]
enumFromThenTo :: MaxNat -> MaxNat -> MaxNat -> [MaxNat]
Enum)

instance Semigroup MaxNat where
  <> :: MaxNat -> MaxNat -> MaxNat
(<>) = MaxNat -> MaxNat -> MaxNat
forall a. Ord a => a -> a -> a
max

instance Monoid MaxNat where
  mempty :: MaxNat
mempty     = MaxNat
0
#if !(MIN_VERSION_base(4,11,0))
  mappend    = (<>)
#endif
  mconcat :: [MaxNat] -> MaxNat
mconcat [] = MaxNat
0
  mconcat [MaxNat]
ms = [MaxNat] -> MaxNat
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [MaxNat]
ms