{-# OPTIONS_GHC -Wunused-imports #-}

-- | More monoids.

module Agda.Utils.Monoid
  ( MaxNat(..)
  , Fwd, pattern Fwd, appFwd
  )
  where

import Data.Monoid (Endo(..), Dual(..))

-- | 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
  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

-- | Function composition in the diagrammatic order.

newtype Fwd a = MkFwd (Dual (Endo a))
  deriving (NonEmpty (Fwd a) -> Fwd a
Fwd a -> Fwd a -> Fwd a
(Fwd a -> Fwd a -> Fwd a)
-> (NonEmpty (Fwd a) -> Fwd a)
-> (forall b. Integral b => b -> Fwd a -> Fwd a)
-> Semigroup (Fwd a)
forall b. Integral b => b -> Fwd a -> Fwd a
forall a. NonEmpty (Fwd a) -> Fwd a
forall a. Fwd a -> Fwd a -> Fwd a
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall a b. Integral b => b -> Fwd a -> Fwd a
$c<> :: forall a. Fwd a -> Fwd a -> Fwd a
<> :: Fwd a -> Fwd a -> Fwd a
$csconcat :: forall a. NonEmpty (Fwd a) -> Fwd a
sconcat :: NonEmpty (Fwd a) -> Fwd a
$cstimes :: forall a b. Integral b => b -> Fwd a -> Fwd a
stimes :: forall b. Integral b => b -> Fwd a -> Fwd a
Semigroup, Semigroup (Fwd a)
Fwd a
Semigroup (Fwd a) =>
Fwd a
-> (Fwd a -> Fwd a -> Fwd a)
-> ([Fwd a] -> Fwd a)
-> Monoid (Fwd a)
[Fwd a] -> Fwd a
Fwd a -> Fwd a -> Fwd a
forall a. Semigroup (Fwd a)
forall a. Fwd a
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall a. [Fwd a] -> Fwd a
forall a. Fwd a -> Fwd a -> Fwd a
$cmempty :: forall a. Fwd a
mempty :: Fwd a
$cmappend :: forall a. Fwd a -> Fwd a -> Fwd a
mappend :: Fwd a -> Fwd a -> Fwd a
$cmconcat :: forall a. [Fwd a] -> Fwd a
mconcat :: [Fwd a] -> Fwd a
Monoid)

pattern Fwd :: (a -> a) -> Fwd a
pattern $mFwd :: forall {r} {a}. Fwd a -> ((a -> a) -> r) -> ((# #) -> r) -> r
$bFwd :: forall a. (a -> a) -> Fwd a
Fwd f = MkFwd (Dual (Endo f))

appFwd :: Fwd a -> (a -> a)
appFwd :: forall a. Fwd a -> a -> a
appFwd (MkFwd (Dual (Endo a -> a
f))) = a -> a
f