{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

module Natural (
  Natural
, HasNatural(..)
, AsNatural(..)
, ProductNatural(..)
, MaxNatural(..)
, MinNatural(..)
, zero
, zero'
, successor
, successor'
, plus
, multiply
, square
, zeroOr
, length
, replicate
, take
, drop
, splitAt
, (!!)
, findIndices
, findIndex
, elemIndices
, elemIndex
, minus
, list
, Positive
, HasPositive(..)
, AsPositive(..)
, SumPositive(..)
, MaxPositive(..)
, MinPositive(..)
, naturalPositive
, one
, one'
, successor1
, successor1'
, successorW
, plus1
, multiply1
, square1
, oneOr
, notZero
, length1
, replicate1
, take1
, drop1
, splitAt1
, (!!!)
, findIndices1
, findIndex1
, elemIndices1
, elemIndex1
, minus1
, list1
, plusone
, minusone
) where

import Control.Applicative(Const)
import Control.Category((.), id)
import Control.Lens(Wrapped(_Wrapped', Unwrapped), Rewrapped, Prism', Lens', Iso', (^?), ( # ), (^.), _Wrapped, prism', iso)
import Control.Monad((>>=))
import Data.Bool(Bool)
import Data.Eq(Eq((==)))
import Data.Foldable(Foldable(foldl))
import Data.Function(const)
import Data.Functor.Identity(Identity)
import Data.Int(Int)
import Data.List(iterate, zip, filter, map, repeat)
import Data.List.NonEmpty(NonEmpty((:|)))
import qualified Data.List.NonEmpty as NonEmpty(iterate, zip, filter)
import Data.Maybe(listToMaybe, Maybe(Just, Nothing), fromMaybe)
import Data.Monoid(Monoid(mappend, mempty))
import Data.Ord(Ord((<)), min, max)
import Data.Semigroup(Semigroup((<>)))
import Data.Semigroup.Foldable(Foldable1(foldMap1))
import Data.Tuple(fst, snd)
import Data.Word(Word)
import Prelude(Show, Integral, Integer, (-), (+), (*), (^), fromIntegral)

newtype Natural =
  Natural
    Integer
  deriving (Natural -> Natural -> Bool
(Natural -> Natural -> Bool)
-> (Natural -> Natural -> Bool) -> Eq Natural
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Natural -> Natural -> Bool
$c/= :: Natural -> Natural -> Bool
== :: Natural -> Natural -> Bool
$c== :: Natural -> Natural -> Bool
Eq, Eq Natural
Eq Natural
-> (Natural -> Natural -> Ordering)
-> (Natural -> Natural -> Bool)
-> (Natural -> Natural -> Bool)
-> (Natural -> Natural -> Bool)
-> (Natural -> Natural -> Bool)
-> (Natural -> Natural -> Natural)
-> (Natural -> Natural -> Natural)
-> Ord Natural
Natural -> Natural -> Bool
Natural -> Natural -> Ordering
Natural -> Natural -> Natural
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 :: Natural -> Natural -> Natural
$cmin :: Natural -> Natural -> Natural
max :: Natural -> Natural -> Natural
$cmax :: Natural -> Natural -> Natural
>= :: Natural -> Natural -> Bool
$c>= :: Natural -> Natural -> Bool
> :: Natural -> Natural -> Bool
$c> :: Natural -> Natural -> Bool
<= :: Natural -> Natural -> Bool
$c<= :: Natural -> Natural -> Bool
< :: Natural -> Natural -> Bool
$c< :: Natural -> Natural -> Bool
compare :: Natural -> Natural -> Ordering
$ccompare :: Natural -> Natural -> Ordering
$cp1Ord :: Eq Natural
Ord, Int -> Natural -> ShowS
[Natural] -> ShowS
Natural -> String
(Int -> Natural -> ShowS)
-> (Natural -> String) -> ([Natural] -> ShowS) -> Show Natural
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Natural] -> ShowS
$cshowList :: [Natural] -> ShowS
show :: Natural -> String
$cshow :: Natural -> String
showsPrec :: Int -> Natural -> ShowS
$cshowsPrec :: Int -> Natural -> ShowS
Show)

instance Semigroup Natural where
  Natural Integer
x <> :: Natural -> Natural -> Natural
<> Natural Integer
y =
    Integer -> Natural
Natural (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)

instance Monoid Natural where
  mappend :: Natural -> Natural -> Natural
mappend =
    Natural -> Natural -> Natural
forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: Natural
mempty =
    Integer -> Natural
Natural Integer
0

class HasNatural a where
  natural ::
    Lens'
      a
      Natural

instance HasNatural Natural where
  natural :: (Natural -> f Natural) -> Natural -> f Natural
natural =
    (Natural -> f Natural) -> Natural -> f Natural
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

class AsNatural a where
  _Natural ::
    Prism'
      a
      Natural

instance AsNatural Natural where
  _Natural :: p Natural (f Natural) -> p Natural (f Natural)
_Natural =
    p Natural (f Natural) -> p Natural (f Natural)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

integralPrism ::
  Integral a =>
  Prism'
    a
    Natural
integralPrism :: Prism' a Natural
integralPrism =
  (Natural -> a) -> (a -> Maybe Natural) -> Prism' a Natural
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\(Natural Integer
n) -> Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
    (\a
n -> if a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 then Maybe Natural
forall a. Maybe a
Nothing else Natural -> Maybe Natural
forall a. a -> Maybe a
Just (Integer -> Natural
Natural (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n)))

instance AsNatural Int where
  _Natural :: p Natural (f Natural) -> p Int (f Int)
_Natural =
    p Natural (f Natural) -> p Int (f Int)
forall a. Integral a => Prism' a Natural
integralPrism

instance AsNatural Integer where
  _Natural :: p Natural (f Natural) -> p Integer (f Integer)
_Natural =
    p Natural (f Natural) -> p Integer (f Integer)
forall a. Integral a => Prism' a Natural
integralPrism

instance AsNatural Word where
  _Natural :: p Natural (f Natural) -> p Word (f Word)
_Natural =
    p Natural (f Natural) -> p Word (f Word)
forall a. Integral a => Prism' a Natural
integralPrism

instance Integral a => AsNatural (Const a b) where
  _Natural :: p Natural (f Natural) -> p (Const a b) (f (Const a b))
_Natural =
    p Natural (f Natural) -> p (Const a b) (f (Const a b))
forall a. Integral a => Prism' a Natural
integralPrism

instance Integral a => AsNatural (Identity a) where
  _Natural :: p Natural (f Natural) -> p (Identity a) (f (Identity a))
_Natural =
    p Natural (f Natural) -> p (Identity a) (f (Identity a))
forall a. Integral a => Prism' a Natural
integralPrism

newtype ProductNatural =
  ProductNatural
    Natural
  deriving (ProductNatural -> ProductNatural -> Bool
(ProductNatural -> ProductNatural -> Bool)
-> (ProductNatural -> ProductNatural -> Bool) -> Eq ProductNatural
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProductNatural -> ProductNatural -> Bool
$c/= :: ProductNatural -> ProductNatural -> Bool
== :: ProductNatural -> ProductNatural -> Bool
$c== :: ProductNatural -> ProductNatural -> Bool
Eq, Eq ProductNatural
Eq ProductNatural
-> (ProductNatural -> ProductNatural -> Ordering)
-> (ProductNatural -> ProductNatural -> Bool)
-> (ProductNatural -> ProductNatural -> Bool)
-> (ProductNatural -> ProductNatural -> Bool)
-> (ProductNatural -> ProductNatural -> Bool)
-> (ProductNatural -> ProductNatural -> ProductNatural)
-> (ProductNatural -> ProductNatural -> ProductNatural)
-> Ord ProductNatural
ProductNatural -> ProductNatural -> Bool
ProductNatural -> ProductNatural -> Ordering
ProductNatural -> ProductNatural -> ProductNatural
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 :: ProductNatural -> ProductNatural -> ProductNatural
$cmin :: ProductNatural -> ProductNatural -> ProductNatural
max :: ProductNatural -> ProductNatural -> ProductNatural
$cmax :: ProductNatural -> ProductNatural -> ProductNatural
>= :: ProductNatural -> ProductNatural -> Bool
$c>= :: ProductNatural -> ProductNatural -> Bool
> :: ProductNatural -> ProductNatural -> Bool
$c> :: ProductNatural -> ProductNatural -> Bool
<= :: ProductNatural -> ProductNatural -> Bool
$c<= :: ProductNatural -> ProductNatural -> Bool
< :: ProductNatural -> ProductNatural -> Bool
$c< :: ProductNatural -> ProductNatural -> Bool
compare :: ProductNatural -> ProductNatural -> Ordering
$ccompare :: ProductNatural -> ProductNatural -> Ordering
$cp1Ord :: Eq ProductNatural
Ord, Int -> ProductNatural -> ShowS
[ProductNatural] -> ShowS
ProductNatural -> String
(Int -> ProductNatural -> ShowS)
-> (ProductNatural -> String)
-> ([ProductNatural] -> ShowS)
-> Show ProductNatural
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProductNatural] -> ShowS
$cshowList :: [ProductNatural] -> ShowS
show :: ProductNatural -> String
$cshow :: ProductNatural -> String
showsPrec :: Int -> ProductNatural -> ShowS
$cshowsPrec :: Int -> ProductNatural -> ShowS
Show)

instance HasNatural ProductNatural where
  natural :: (Natural -> f Natural) -> ProductNatural -> f ProductNatural
natural =
    (Natural -> f Natural) -> ProductNatural -> f ProductNatural
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Natural -> f Natural) -> ProductNatural -> f ProductNatural)
-> ((Natural -> f Natural) -> Natural -> f Natural)
-> (Natural -> f Natural)
-> ProductNatural
-> f ProductNatural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Natural -> f Natural) -> Natural -> f Natural
forall a. HasNatural a => Lens' a Natural
natural

instance AsNatural ProductNatural where
  _Natural :: p Natural (f Natural) -> p ProductNatural (f ProductNatural)
_Natural =
    p Natural (f Natural) -> p ProductNatural (f ProductNatural)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (p Natural (f Natural) -> p ProductNatural (f ProductNatural))
-> (p Natural (f Natural) -> p Natural (f Natural))
-> p Natural (f Natural)
-> p ProductNatural (f ProductNatural)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p Natural (f Natural) -> p Natural (f Natural)
forall a. AsNatural a => Prism' a Natural
_Natural

instance ProductNatural ~ a =>
  Rewrapped ProductNatural a
  
instance Wrapped ProductNatural where
  type Unwrapped ProductNatural = Natural
  _Wrapped' :: p (Unwrapped ProductNatural) (f (Unwrapped ProductNatural))
-> p ProductNatural (f ProductNatural)
_Wrapped' =
    (ProductNatural -> Natural)
-> (Natural -> ProductNatural)
-> Iso ProductNatural ProductNatural Natural Natural
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
      (\(ProductNatural Natural
x) -> Natural
x)
      Natural -> ProductNatural
ProductNatural

instance Semigroup ProductNatural where
  ProductNatural (Natural Integer
x) <> :: ProductNatural -> ProductNatural -> ProductNatural
<> ProductNatural (Natural Integer
y) =
    Natural -> ProductNatural
ProductNatural (Integer -> Natural
Natural (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y))

instance Monoid ProductNatural where
  mappend :: ProductNatural -> ProductNatural -> ProductNatural
mappend =
    ProductNatural -> ProductNatural -> ProductNatural
forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: ProductNatural
mempty =
    Natural -> ProductNatural
ProductNatural (Integer -> Natural
Natural Integer
1)

newtype MaxNatural =
  MaxNatural
    Natural
  deriving (MaxNatural -> MaxNatural -> Bool
(MaxNatural -> MaxNatural -> Bool)
-> (MaxNatural -> MaxNatural -> Bool) -> Eq MaxNatural
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MaxNatural -> MaxNatural -> Bool
$c/= :: MaxNatural -> MaxNatural -> Bool
== :: MaxNatural -> MaxNatural -> Bool
$c== :: MaxNatural -> MaxNatural -> Bool
Eq, Eq MaxNatural
Eq MaxNatural
-> (MaxNatural -> MaxNatural -> Ordering)
-> (MaxNatural -> MaxNatural -> Bool)
-> (MaxNatural -> MaxNatural -> Bool)
-> (MaxNatural -> MaxNatural -> Bool)
-> (MaxNatural -> MaxNatural -> Bool)
-> (MaxNatural -> MaxNatural -> MaxNatural)
-> (MaxNatural -> MaxNatural -> MaxNatural)
-> Ord MaxNatural
MaxNatural -> MaxNatural -> Bool
MaxNatural -> MaxNatural -> Ordering
MaxNatural -> MaxNatural -> MaxNatural
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 :: MaxNatural -> MaxNatural -> MaxNatural
$cmin :: MaxNatural -> MaxNatural -> MaxNatural
max :: MaxNatural -> MaxNatural -> MaxNatural
$cmax :: MaxNatural -> MaxNatural -> MaxNatural
>= :: MaxNatural -> MaxNatural -> Bool
$c>= :: MaxNatural -> MaxNatural -> Bool
> :: MaxNatural -> MaxNatural -> Bool
$c> :: MaxNatural -> MaxNatural -> Bool
<= :: MaxNatural -> MaxNatural -> Bool
$c<= :: MaxNatural -> MaxNatural -> Bool
< :: MaxNatural -> MaxNatural -> Bool
$c< :: MaxNatural -> MaxNatural -> Bool
compare :: MaxNatural -> MaxNatural -> Ordering
$ccompare :: MaxNatural -> MaxNatural -> Ordering
$cp1Ord :: Eq MaxNatural
Ord, Int -> MaxNatural -> ShowS
[MaxNatural] -> ShowS
MaxNatural -> String
(Int -> MaxNatural -> ShowS)
-> (MaxNatural -> String)
-> ([MaxNatural] -> ShowS)
-> Show MaxNatural
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MaxNatural] -> ShowS
$cshowList :: [MaxNatural] -> ShowS
show :: MaxNatural -> String
$cshow :: MaxNatural -> String
showsPrec :: Int -> MaxNatural -> ShowS
$cshowsPrec :: Int -> MaxNatural -> ShowS
Show)

instance HasNatural MaxNatural where
  natural :: (Natural -> f Natural) -> MaxNatural -> f MaxNatural
natural =
    (Natural -> f Natural) -> MaxNatural -> f MaxNatural
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Natural -> f Natural) -> MaxNatural -> f MaxNatural)
-> ((Natural -> f Natural) -> Natural -> f Natural)
-> (Natural -> f Natural)
-> MaxNatural
-> f MaxNatural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Natural -> f Natural) -> Natural -> f Natural
forall a. HasNatural a => Lens' a Natural
natural

instance AsNatural MaxNatural where
  _Natural :: p Natural (f Natural) -> p MaxNatural (f MaxNatural)
_Natural =
    p Natural (f Natural) -> p MaxNatural (f MaxNatural)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (p Natural (f Natural) -> p MaxNatural (f MaxNatural))
-> (p Natural (f Natural) -> p Natural (f Natural))
-> p Natural (f Natural)
-> p MaxNatural (f MaxNatural)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p Natural (f Natural) -> p Natural (f Natural)
forall a. AsNatural a => Prism' a Natural
_Natural

instance MaxNatural ~ a =>
  Rewrapped MaxNatural a
  
instance Wrapped MaxNatural where
  type Unwrapped MaxNatural = Natural
  _Wrapped' :: p (Unwrapped MaxNatural) (f (Unwrapped MaxNatural))
-> p MaxNatural (f MaxNatural)
_Wrapped' =
    (MaxNatural -> Natural)
-> (Natural -> MaxNatural)
-> Iso MaxNatural MaxNatural Natural Natural
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
      (\(MaxNatural Natural
x) -> Natural
x)
      Natural -> MaxNatural
MaxNatural

instance Semigroup MaxNatural where
  MaxNatural (Natural Integer
x) <> :: MaxNatural -> MaxNatural -> MaxNatural
<> MaxNatural (Natural Integer
y) =
    Natural -> MaxNatural
MaxNatural (Integer -> Natural
Natural (Integer
x Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`max` Integer
y))

newtype MinNatural =
  MinNatural
    Natural
  deriving (MinNatural -> MinNatural -> Bool
(MinNatural -> MinNatural -> Bool)
-> (MinNatural -> MinNatural -> Bool) -> Eq MinNatural
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MinNatural -> MinNatural -> Bool
$c/= :: MinNatural -> MinNatural -> Bool
== :: MinNatural -> MinNatural -> Bool
$c== :: MinNatural -> MinNatural -> Bool
Eq, Eq MinNatural
Eq MinNatural
-> (MinNatural -> MinNatural -> Ordering)
-> (MinNatural -> MinNatural -> Bool)
-> (MinNatural -> MinNatural -> Bool)
-> (MinNatural -> MinNatural -> Bool)
-> (MinNatural -> MinNatural -> Bool)
-> (MinNatural -> MinNatural -> MinNatural)
-> (MinNatural -> MinNatural -> MinNatural)
-> Ord MinNatural
MinNatural -> MinNatural -> Bool
MinNatural -> MinNatural -> Ordering
MinNatural -> MinNatural -> MinNatural
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 :: MinNatural -> MinNatural -> MinNatural
$cmin :: MinNatural -> MinNatural -> MinNatural
max :: MinNatural -> MinNatural -> MinNatural
$cmax :: MinNatural -> MinNatural -> MinNatural
>= :: MinNatural -> MinNatural -> Bool
$c>= :: MinNatural -> MinNatural -> Bool
> :: MinNatural -> MinNatural -> Bool
$c> :: MinNatural -> MinNatural -> Bool
<= :: MinNatural -> MinNatural -> Bool
$c<= :: MinNatural -> MinNatural -> Bool
< :: MinNatural -> MinNatural -> Bool
$c< :: MinNatural -> MinNatural -> Bool
compare :: MinNatural -> MinNatural -> Ordering
$ccompare :: MinNatural -> MinNatural -> Ordering
$cp1Ord :: Eq MinNatural
Ord, Int -> MinNatural -> ShowS
[MinNatural] -> ShowS
MinNatural -> String
(Int -> MinNatural -> ShowS)
-> (MinNatural -> String)
-> ([MinNatural] -> ShowS)
-> Show MinNatural
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MinNatural] -> ShowS
$cshowList :: [MinNatural] -> ShowS
show :: MinNatural -> String
$cshow :: MinNatural -> String
showsPrec :: Int -> MinNatural -> ShowS
$cshowsPrec :: Int -> MinNatural -> ShowS
Show)

instance HasNatural MinNatural where
  natural :: (Natural -> f Natural) -> MinNatural -> f MinNatural
natural =
    (Natural -> f Natural) -> MinNatural -> f MinNatural
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Natural -> f Natural) -> MinNatural -> f MinNatural)
-> ((Natural -> f Natural) -> Natural -> f Natural)
-> (Natural -> f Natural)
-> MinNatural
-> f MinNatural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Natural -> f Natural) -> Natural -> f Natural
forall a. HasNatural a => Lens' a Natural
natural

instance AsNatural MinNatural where
  _Natural :: p Natural (f Natural) -> p MinNatural (f MinNatural)
_Natural =
    p Natural (f Natural) -> p MinNatural (f MinNatural)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (p Natural (f Natural) -> p MinNatural (f MinNatural))
-> (p Natural (f Natural) -> p Natural (f Natural))
-> p Natural (f Natural)
-> p MinNatural (f MinNatural)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p Natural (f Natural) -> p Natural (f Natural)
forall a. AsNatural a => Prism' a Natural
_Natural

instance MinNatural ~ a =>
  Rewrapped MinNatural a
  
instance Wrapped MinNatural where
  type Unwrapped MinNatural = Natural
  _Wrapped' :: p (Unwrapped MinNatural) (f (Unwrapped MinNatural))
-> p MinNatural (f MinNatural)
_Wrapped' =
    (MinNatural -> Natural)
-> (Natural -> MinNatural)
-> Iso MinNatural MinNatural Natural Natural
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
      (\(MinNatural Natural
x) -> Natural
x)
      Natural -> MinNatural
MinNatural

instance Semigroup MinNatural where
  MinNatural (Natural Integer
x) <> :: MinNatural -> MinNatural -> MinNatural
<> MinNatural (Natural Integer
y) =
    Natural -> MinNatural
MinNatural (Integer -> Natural
Natural (Integer
x Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`min` Integer
y))

zero ::
  Prism'
    Natural
    ()
zero :: p () (f ()) -> p Natural (f Natural)
zero =
  (() -> Natural)
-> (Natural -> Maybe ()) -> Prism Natural Natural () ()
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\() -> Integer -> Natural
Natural Integer
0)
    (\(Natural Integer
n) -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)

zero' ::
  Natural
zero' :: Natural
zero' =
  Tagged () (Identity ()) -> Tagged Natural (Identity Natural)
Prism Natural Natural () ()
zero (Tagged () (Identity ()) -> Tagged Natural (Identity Natural))
-> () -> Natural
forall t b. AReview t b -> b -> t
# ()

successor ::
  Prism'
    Natural
    Natural
successor :: p Natural (f Natural) -> p Natural (f Natural)
successor =
  (Natural -> Natural)
-> (Natural -> Maybe Natural) -> Prism' Natural Natural
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\(Natural Integer
n) -> Integer -> Natural
Natural (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1))
    (\(Natural Integer
n) -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Maybe Natural
forall a. Maybe a
Nothing else Natural -> Maybe Natural
forall a. a -> Maybe a
Just (Integer -> Natural
Natural (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))

successor' ::
  Natural
  -> Natural
successor' :: Natural -> Natural
successor' =
  (Tagged Natural (Identity Natural)
-> Tagged Natural (Identity Natural)
Prism' Natural Natural
successor (Tagged Natural (Identity Natural)
 -> Tagged Natural (Identity Natural))
-> Natural -> Natural
forall t b. AReview t b -> b -> t
#)

plus ::
  Natural
  -> Natural
  -> Natural
plus :: Natural -> Natural -> Natural
plus =
  Natural -> Natural -> Natural
forall a. Semigroup a => a -> a -> a
(<>)

multiply ::
  Natural
  -> Natural
  -> Natural
multiply :: Natural -> Natural -> Natural
multiply Natural
x Natural
y =
  (Tagged Natural (Identity Natural)
-> Tagged ProductNatural (Identity ProductNatural)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (Tagged Natural (Identity Natural)
 -> Tagged ProductNatural (Identity ProductNatural))
-> Natural -> ProductNatural
forall t b. AReview t b -> b -> t
# Natural
x ProductNatural -> ProductNatural -> ProductNatural
forall a. Semigroup a => a -> a -> a
<> (Tagged Natural (Identity Natural)
-> Tagged ProductNatural (Identity ProductNatural)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (Tagged Natural (Identity Natural)
 -> Tagged ProductNatural (Identity ProductNatural))
-> Natural -> ProductNatural
forall t b. AReview t b -> b -> t
# Natural
y :: ProductNatural)) ProductNatural -> Getting Natural ProductNatural Natural -> Natural
forall s a. s -> Getting a s a -> a
^. Getting Natural ProductNatural Natural
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped

square ::
  Natural
  -> Natural
  -> Natural
square :: Natural -> Natural -> Natural
square (Natural Integer
x) (Natural Integer
y) =
  Integer -> Natural
Natural (Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y)

zeroOr ::
  AsNatural a =>
  a
  -> Natural
zeroOr :: a -> Natural
zeroOr a
n =
  Natural -> Maybe Natural -> Natural
forall a. a -> Maybe a -> a
fromMaybe Natural
zero' (a
n a -> Getting (First Natural) a Natural -> Maybe Natural
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Natural) a Natural
forall a. AsNatural a => Prism' a Natural
_Natural)

length ::
  Foldable f =>
  f a
  -> Natural
length :: f a -> Natural
length =
  (Natural -> a -> Natural) -> Natural -> f a -> Natural
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Natural -> a -> Natural
forall a b. a -> b -> a
const (Natural -> a -> Natural)
-> (Natural -> Natural) -> Natural -> a -> Natural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Natural -> Natural
successor') Natural
zero'

replicate ::
  Natural
  -> a
  -> [a]
replicate :: Natural -> a -> [a]
replicate Natural
n =
  Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
take Natural
n ([a] -> [a]) -> (a -> [a]) -> a -> [a]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> [a]
forall a. a -> [a]
repeat

take ::
  Natural
  -> [a]
  -> [a]
take :: Natural -> [a] -> [a]
take Natural
_ [] =
  []
take Natural
n (a
h:[a]
t) =
  case Natural
n Natural -> Getting (First Natural) Natural Natural -> Maybe Natural
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Natural) Natural Natural
Prism' Natural Natural
successor of
    Maybe Natural
Nothing ->
      []
    Just Natural
p ->
      a
h a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
take Natural
p [a]
t

drop ::
  Natural
  -> [a]
  -> [a]
drop :: Natural -> [a] -> [a]
drop Natural
_ [] =
  []
drop Natural
n (a
h:[a]
t) =
  case Natural
n Natural -> Getting (First Natural) Natural Natural -> Maybe Natural
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Natural) Natural Natural
Prism' Natural Natural
successor of
    Maybe Natural
Nothing ->
      a
ha -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
t
    Just Natural
p ->
      Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
drop Natural
p [a]
t

splitAt ::
  Natural
  -> [a]
  -> ([a], [a])
splitAt :: Natural -> [a] -> ([a], [a])
splitAt Natural
n [a]
x =
  (Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
take Natural
n [a]
x, Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
drop Natural
n [a]
x)

(!!) ::
  [a]
  -> Natural
  -> Maybe a
[] !! :: [a] -> Natural -> Maybe a
!! Natural
_ =
  Maybe a
forall a. Maybe a
Nothing
(a
_:[a]
t) !! Natural
n =
  (Natural
n Natural -> Getting (First Natural) Natural Natural -> Maybe Natural
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Natural) Natural Natural
Prism' Natural Natural
successor) Maybe Natural -> (Natural -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([a]
t [a] -> Natural -> Maybe a
forall a. [a] -> Natural -> Maybe a
!!)

findIndices ::
  (a -> Bool)
  -> [a]
  -> [Natural]
findIndices :: (a -> Bool) -> [a] -> [Natural]
findIndices a -> Bool
p [a]
x =
  ((a, Natural) -> Natural) -> [(a, Natural)] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
map (a, Natural) -> Natural
forall a b. (a, b) -> b
snd (((a, Natural) -> Bool) -> [(a, Natural)] -> [(a, Natural)]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> Bool
p (a -> Bool) -> ((a, Natural) -> a) -> (a, Natural) -> Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a, Natural) -> a
forall a b. (a, b) -> a
fst) ([a] -> [Natural] -> [(a, Natural)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
x ((Natural -> Natural) -> Natural -> [Natural]
forall a. (a -> a) -> a -> [a]
iterate Natural -> Natural
successor' Natural
zero')))

findIndex ::
  (a -> Bool)
  -> [a]
  -> Maybe Natural
findIndex :: (a -> Bool) -> [a] -> Maybe Natural
findIndex a -> Bool
p =
  [Natural] -> Maybe Natural
forall a. [a] -> Maybe a
listToMaybe ([Natural] -> Maybe Natural)
-> ([a] -> [Natural]) -> [a] -> Maybe Natural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Bool) -> [a] -> [Natural]
forall a. (a -> Bool) -> [a] -> [Natural]
findIndices a -> Bool
p

elemIndices ::
  Eq a =>
  a
  -> [a]
  -> [Natural]
elemIndices :: a -> [a] -> [Natural]
elemIndices =
  (a -> Bool) -> [a] -> [Natural]
forall a. (a -> Bool) -> [a] -> [Natural]
findIndices ((a -> Bool) -> [a] -> [Natural])
-> (a -> a -> Bool) -> a -> [a] -> [Natural]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

elemIndex ::
  Eq a =>
  a
  -> [a]
  -> Maybe Natural
elemIndex :: a -> [a] -> Maybe Natural
elemIndex =
  (a -> Bool) -> [a] -> Maybe Natural
forall a. (a -> Bool) -> [a] -> Maybe Natural
findIndex ((a -> Bool) -> [a] -> Maybe Natural)
-> (a -> a -> Bool) -> a -> [a] -> Maybe Natural
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

minus ::
  Natural
  -> Natural
  -> Natural
minus :: Natural -> Natural -> Natural
minus (Natural Integer
x) (Natural Integer
y) =
  Integer -> Natural
Natural (if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
y then Integer
0 else Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)

list ::
  Iso'
    Natural
    [()]
list :: p [()] (f [()]) -> p Natural (f Natural)
list =
  (Natural -> [()])
-> ([()] -> Natural) -> Iso Natural Natural [()] [()]
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
    (\Natural
n -> Natural -> () -> [()]
forall a. Natural -> a -> [a]
replicate Natural
n ())
    [()] -> Natural
forall (f :: * -> *) a. Foldable f => f a -> Natural
length

----

newtype Positive =
  Positive
    Integer
  deriving (Positive -> Positive -> Bool
(Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool) -> Eq Positive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Positive -> Positive -> Bool
$c/= :: Positive -> Positive -> Bool
== :: Positive -> Positive -> Bool
$c== :: Positive -> Positive -> Bool
Eq, Eq Positive
Eq Positive
-> (Positive -> Positive -> Ordering)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Bool)
-> (Positive -> Positive -> Positive)
-> (Positive -> Positive -> Positive)
-> Ord Positive
Positive -> Positive -> Bool
Positive -> Positive -> Ordering
Positive -> Positive -> Positive
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 :: Positive -> Positive -> Positive
$cmin :: Positive -> Positive -> Positive
max :: Positive -> Positive -> Positive
$cmax :: Positive -> Positive -> Positive
>= :: Positive -> Positive -> Bool
$c>= :: Positive -> Positive -> Bool
> :: Positive -> Positive -> Bool
$c> :: Positive -> Positive -> Bool
<= :: Positive -> Positive -> Bool
$c<= :: Positive -> Positive -> Bool
< :: Positive -> Positive -> Bool
$c< :: Positive -> Positive -> Bool
compare :: Positive -> Positive -> Ordering
$ccompare :: Positive -> Positive -> Ordering
$cp1Ord :: Eq Positive
Ord, Int -> Positive -> ShowS
[Positive] -> ShowS
Positive -> String
(Int -> Positive -> ShowS)
-> (Positive -> String) -> ([Positive] -> ShowS) -> Show Positive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Positive] -> ShowS
$cshowList :: [Positive] -> ShowS
show :: Positive -> String
$cshow :: Positive -> String
showsPrec :: Int -> Positive -> ShowS
$cshowsPrec :: Int -> Positive -> ShowS
Show)

instance Semigroup Positive where
  Positive Integer
x <> :: Positive -> Positive -> Positive
<> Positive Integer
y =
    Integer -> Positive
Positive (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y)

instance Monoid Positive where
  mappend :: Positive -> Positive -> Positive
mappend =
    Positive -> Positive -> Positive
forall a. Semigroup a => a -> a -> a
(<>)
  mempty :: Positive
mempty =
    Integer -> Positive
Positive Integer
0

class HasPositive a where
  positive ::
    Lens'
      a
      Positive

instance HasPositive Positive where
  positive :: (Positive -> f Positive) -> Positive -> f Positive
positive =
    (Positive -> f Positive) -> Positive -> f Positive
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

class AsPositive a where
  _Positive ::
    Prism'
      a
      Positive

instance AsPositive Positive where
  _Positive :: p Positive (f Positive) -> p Positive (f Positive)
_Positive =
    p Positive (f Positive) -> p Positive (f Positive)
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

integralPrism1 ::
  Integral a =>
  Prism'
    a
    Positive
integralPrism1 :: Prism' a Positive
integralPrism1 =
  (Positive -> a) -> (a -> Maybe Positive) -> Prism' a Positive
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\(Positive Integer
n) -> Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n)
    (\a
n -> if a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
1 then Maybe Positive
forall a. Maybe a
Nothing else Positive -> Maybe Positive
forall a. a -> Maybe a
Just (Integer -> Positive
Positive (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n)))

instance AsPositive Int where
  _Positive :: p Positive (f Positive) -> p Int (f Int)
_Positive =
    p Positive (f Positive) -> p Int (f Int)
forall a. Integral a => Prism' a Positive
integralPrism1

instance AsPositive Integer where
  _Positive :: p Positive (f Positive) -> p Integer (f Integer)
_Positive =
    p Positive (f Positive) -> p Integer (f Integer)
forall a. Integral a => Prism' a Positive
integralPrism1

instance AsPositive Word where
  _Positive :: p Positive (f Positive) -> p Word (f Word)
_Positive =
    p Positive (f Positive) -> p Word (f Word)
forall a. Integral a => Prism' a Positive
integralPrism1

instance Integral a => AsPositive (Const a b) where
  _Positive :: p Positive (f Positive) -> p (Const a b) (f (Const a b))
_Positive =
    p Positive (f Positive) -> p (Const a b) (f (Const a b))
forall a. Integral a => Prism' a Positive
integralPrism1

instance Integral a => AsPositive (Identity a) where
  _Positive :: p Positive (f Positive) -> p (Identity a) (f (Identity a))
_Positive =
    p Positive (f Positive) -> p (Identity a) (f (Identity a))
forall a. Integral a => Prism' a Positive
integralPrism1

newtype SumPositive =
  SumPositive
    Positive
  deriving (SumPositive -> SumPositive -> Bool
(SumPositive -> SumPositive -> Bool)
-> (SumPositive -> SumPositive -> Bool) -> Eq SumPositive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SumPositive -> SumPositive -> Bool
$c/= :: SumPositive -> SumPositive -> Bool
== :: SumPositive -> SumPositive -> Bool
$c== :: SumPositive -> SumPositive -> Bool
Eq, Eq SumPositive
Eq SumPositive
-> (SumPositive -> SumPositive -> Ordering)
-> (SumPositive -> SumPositive -> Bool)
-> (SumPositive -> SumPositive -> Bool)
-> (SumPositive -> SumPositive -> Bool)
-> (SumPositive -> SumPositive -> Bool)
-> (SumPositive -> SumPositive -> SumPositive)
-> (SumPositive -> SumPositive -> SumPositive)
-> Ord SumPositive
SumPositive -> SumPositive -> Bool
SumPositive -> SumPositive -> Ordering
SumPositive -> SumPositive -> SumPositive
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 :: SumPositive -> SumPositive -> SumPositive
$cmin :: SumPositive -> SumPositive -> SumPositive
max :: SumPositive -> SumPositive -> SumPositive
$cmax :: SumPositive -> SumPositive -> SumPositive
>= :: SumPositive -> SumPositive -> Bool
$c>= :: SumPositive -> SumPositive -> Bool
> :: SumPositive -> SumPositive -> Bool
$c> :: SumPositive -> SumPositive -> Bool
<= :: SumPositive -> SumPositive -> Bool
$c<= :: SumPositive -> SumPositive -> Bool
< :: SumPositive -> SumPositive -> Bool
$c< :: SumPositive -> SumPositive -> Bool
compare :: SumPositive -> SumPositive -> Ordering
$ccompare :: SumPositive -> SumPositive -> Ordering
$cp1Ord :: Eq SumPositive
Ord, Int -> SumPositive -> ShowS
[SumPositive] -> ShowS
SumPositive -> String
(Int -> SumPositive -> ShowS)
-> (SumPositive -> String)
-> ([SumPositive] -> ShowS)
-> Show SumPositive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SumPositive] -> ShowS
$cshowList :: [SumPositive] -> ShowS
show :: SumPositive -> String
$cshow :: SumPositive -> String
showsPrec :: Int -> SumPositive -> ShowS
$cshowsPrec :: Int -> SumPositive -> ShowS
Show)

instance HasPositive SumPositive where
  positive :: (Positive -> f Positive) -> SumPositive -> f SumPositive
positive =
    (Positive -> f Positive) -> SumPositive -> f SumPositive
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Positive -> f Positive) -> SumPositive -> f SumPositive)
-> ((Positive -> f Positive) -> Positive -> f Positive)
-> (Positive -> f Positive)
-> SumPositive
-> f SumPositive
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Positive -> f Positive) -> Positive -> f Positive
forall a. HasPositive a => Lens' a Positive
positive

instance AsPositive SumPositive where
  _Positive :: p Positive (f Positive) -> p SumPositive (f SumPositive)
_Positive =
    p Positive (f Positive) -> p SumPositive (f SumPositive)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (p Positive (f Positive) -> p SumPositive (f SumPositive))
-> (p Positive (f Positive) -> p Positive (f Positive))
-> p Positive (f Positive)
-> p SumPositive (f SumPositive)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p Positive (f Positive) -> p Positive (f Positive)
forall a. AsPositive a => Prism' a Positive
_Positive

instance SumPositive ~ a =>
  Rewrapped SumPositive a
  
instance Wrapped SumPositive where
  type Unwrapped SumPositive = Positive
  _Wrapped' :: p (Unwrapped SumPositive) (f (Unwrapped SumPositive))
-> p SumPositive (f SumPositive)
_Wrapped' =
    (SumPositive -> Positive)
-> (Positive -> SumPositive)
-> Iso SumPositive SumPositive Positive Positive
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
      (\(SumPositive Positive
x) -> Positive
x)
      Positive -> SumPositive
SumPositive

instance Semigroup SumPositive where
  SumPositive (Positive Integer
x) <> :: SumPositive -> SumPositive -> SumPositive
<> SumPositive (Positive Integer
y) =
    Positive -> SumPositive
SumPositive (Integer -> Positive
Positive (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y))

newtype MaxPositive =
  MaxPositive
    Positive
  deriving (MaxPositive -> MaxPositive -> Bool
(MaxPositive -> MaxPositive -> Bool)
-> (MaxPositive -> MaxPositive -> Bool) -> Eq MaxPositive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MaxPositive -> MaxPositive -> Bool
$c/= :: MaxPositive -> MaxPositive -> Bool
== :: MaxPositive -> MaxPositive -> Bool
$c== :: MaxPositive -> MaxPositive -> Bool
Eq, Eq MaxPositive
Eq MaxPositive
-> (MaxPositive -> MaxPositive -> Ordering)
-> (MaxPositive -> MaxPositive -> Bool)
-> (MaxPositive -> MaxPositive -> Bool)
-> (MaxPositive -> MaxPositive -> Bool)
-> (MaxPositive -> MaxPositive -> Bool)
-> (MaxPositive -> MaxPositive -> MaxPositive)
-> (MaxPositive -> MaxPositive -> MaxPositive)
-> Ord MaxPositive
MaxPositive -> MaxPositive -> Bool
MaxPositive -> MaxPositive -> Ordering
MaxPositive -> MaxPositive -> MaxPositive
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 :: MaxPositive -> MaxPositive -> MaxPositive
$cmin :: MaxPositive -> MaxPositive -> MaxPositive
max :: MaxPositive -> MaxPositive -> MaxPositive
$cmax :: MaxPositive -> MaxPositive -> MaxPositive
>= :: MaxPositive -> MaxPositive -> Bool
$c>= :: MaxPositive -> MaxPositive -> Bool
> :: MaxPositive -> MaxPositive -> Bool
$c> :: MaxPositive -> MaxPositive -> Bool
<= :: MaxPositive -> MaxPositive -> Bool
$c<= :: MaxPositive -> MaxPositive -> Bool
< :: MaxPositive -> MaxPositive -> Bool
$c< :: MaxPositive -> MaxPositive -> Bool
compare :: MaxPositive -> MaxPositive -> Ordering
$ccompare :: MaxPositive -> MaxPositive -> Ordering
$cp1Ord :: Eq MaxPositive
Ord, Int -> MaxPositive -> ShowS
[MaxPositive] -> ShowS
MaxPositive -> String
(Int -> MaxPositive -> ShowS)
-> (MaxPositive -> String)
-> ([MaxPositive] -> ShowS)
-> Show MaxPositive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MaxPositive] -> ShowS
$cshowList :: [MaxPositive] -> ShowS
show :: MaxPositive -> String
$cshow :: MaxPositive -> String
showsPrec :: Int -> MaxPositive -> ShowS
$cshowsPrec :: Int -> MaxPositive -> ShowS
Show)

instance HasPositive MaxPositive where
  positive :: (Positive -> f Positive) -> MaxPositive -> f MaxPositive
positive =
    (Positive -> f Positive) -> MaxPositive -> f MaxPositive
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Positive -> f Positive) -> MaxPositive -> f MaxPositive)
-> ((Positive -> f Positive) -> Positive -> f Positive)
-> (Positive -> f Positive)
-> MaxPositive
-> f MaxPositive
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Positive -> f Positive) -> Positive -> f Positive
forall a. HasPositive a => Lens' a Positive
positive

instance AsPositive MaxPositive where
  _Positive :: p Positive (f Positive) -> p MaxPositive (f MaxPositive)
_Positive =
    p Positive (f Positive) -> p MaxPositive (f MaxPositive)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (p Positive (f Positive) -> p MaxPositive (f MaxPositive))
-> (p Positive (f Positive) -> p Positive (f Positive))
-> p Positive (f Positive)
-> p MaxPositive (f MaxPositive)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p Positive (f Positive) -> p Positive (f Positive)
forall a. AsPositive a => Prism' a Positive
_Positive

instance MaxPositive ~ a =>
  Rewrapped MaxPositive a
  
instance Wrapped MaxPositive where
  type Unwrapped MaxPositive = Positive
  _Wrapped' :: p (Unwrapped MaxPositive) (f (Unwrapped MaxPositive))
-> p MaxPositive (f MaxPositive)
_Wrapped' =
    (MaxPositive -> Positive)
-> (Positive -> MaxPositive)
-> Iso MaxPositive MaxPositive Positive Positive
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
      (\(MaxPositive Positive
x) -> Positive
x)
      Positive -> MaxPositive
MaxPositive

instance Semigroup MaxPositive where
  MaxPositive (Positive Integer
x) <> :: MaxPositive -> MaxPositive -> MaxPositive
<> MaxPositive (Positive Integer
y) =
    Positive -> MaxPositive
MaxPositive (Integer -> Positive
Positive (Integer
x Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`max` Integer
y))

newtype MinPositive =
  MinPositive
    Positive
  deriving (MinPositive -> MinPositive -> Bool
(MinPositive -> MinPositive -> Bool)
-> (MinPositive -> MinPositive -> Bool) -> Eq MinPositive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MinPositive -> MinPositive -> Bool
$c/= :: MinPositive -> MinPositive -> Bool
== :: MinPositive -> MinPositive -> Bool
$c== :: MinPositive -> MinPositive -> Bool
Eq, Eq MinPositive
Eq MinPositive
-> (MinPositive -> MinPositive -> Ordering)
-> (MinPositive -> MinPositive -> Bool)
-> (MinPositive -> MinPositive -> Bool)
-> (MinPositive -> MinPositive -> Bool)
-> (MinPositive -> MinPositive -> Bool)
-> (MinPositive -> MinPositive -> MinPositive)
-> (MinPositive -> MinPositive -> MinPositive)
-> Ord MinPositive
MinPositive -> MinPositive -> Bool
MinPositive -> MinPositive -> Ordering
MinPositive -> MinPositive -> MinPositive
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 :: MinPositive -> MinPositive -> MinPositive
$cmin :: MinPositive -> MinPositive -> MinPositive
max :: MinPositive -> MinPositive -> MinPositive
$cmax :: MinPositive -> MinPositive -> MinPositive
>= :: MinPositive -> MinPositive -> Bool
$c>= :: MinPositive -> MinPositive -> Bool
> :: MinPositive -> MinPositive -> Bool
$c> :: MinPositive -> MinPositive -> Bool
<= :: MinPositive -> MinPositive -> Bool
$c<= :: MinPositive -> MinPositive -> Bool
< :: MinPositive -> MinPositive -> Bool
$c< :: MinPositive -> MinPositive -> Bool
compare :: MinPositive -> MinPositive -> Ordering
$ccompare :: MinPositive -> MinPositive -> Ordering
$cp1Ord :: Eq MinPositive
Ord, Int -> MinPositive -> ShowS
[MinPositive] -> ShowS
MinPositive -> String
(Int -> MinPositive -> ShowS)
-> (MinPositive -> String)
-> ([MinPositive] -> ShowS)
-> Show MinPositive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MinPositive] -> ShowS
$cshowList :: [MinPositive] -> ShowS
show :: MinPositive -> String
$cshow :: MinPositive -> String
showsPrec :: Int -> MinPositive -> ShowS
$cshowsPrec :: Int -> MinPositive -> ShowS
Show)

instance HasPositive MinPositive where
  positive :: (Positive -> f Positive) -> MinPositive -> f MinPositive
positive =
    (Positive -> f Positive) -> MinPositive -> f MinPositive
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((Positive -> f Positive) -> MinPositive -> f MinPositive)
-> ((Positive -> f Positive) -> Positive -> f Positive)
-> (Positive -> f Positive)
-> MinPositive
-> f MinPositive
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Positive -> f Positive) -> Positive -> f Positive
forall a. HasPositive a => Lens' a Positive
positive

instance AsPositive MinPositive where
  _Positive :: p Positive (f Positive) -> p MinPositive (f MinPositive)
_Positive =
    p Positive (f Positive) -> p MinPositive (f MinPositive)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (p Positive (f Positive) -> p MinPositive (f MinPositive))
-> (p Positive (f Positive) -> p Positive (f Positive))
-> p Positive (f Positive)
-> p MinPositive (f MinPositive)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. p Positive (f Positive) -> p Positive (f Positive)
forall a. AsPositive a => Prism' a Positive
_Positive

instance MinPositive ~ a =>
  Rewrapped MinPositive a
  
instance Wrapped MinPositive where
  type Unwrapped MinPositive = Positive
  _Wrapped' :: p (Unwrapped MinPositive) (f (Unwrapped MinPositive))
-> p MinPositive (f MinPositive)
_Wrapped' =
    (MinPositive -> Positive)
-> (Positive -> MinPositive)
-> Iso MinPositive MinPositive Positive Positive
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
      (\(MinPositive Positive
x) -> Positive
x)
      Positive -> MinPositive
MinPositive

instance Semigroup MinPositive where
  MinPositive (Positive Integer
x) <> :: MinPositive -> MinPositive -> MinPositive
<> MinPositive (Positive Integer
y) =
    Positive -> MinPositive
MinPositive (Integer -> Positive
Positive (Integer
x Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
`min` Integer
y))

naturalPositive ::
  Iso' Natural (Maybe Positive)
naturalPositive :: p (Maybe Positive) (f (Maybe Positive)) -> p Natural (f Natural)
naturalPositive =
  (Natural -> Maybe Positive)
-> (Maybe Positive -> Natural)
-> Iso Natural Natural (Maybe Positive) (Maybe Positive)
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
    (\(Natural Integer
n) ->
        if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Maybe Positive
forall a. Maybe a
Nothing else Positive -> Maybe Positive
forall a. a -> Maybe a
Just (Integer -> Positive
Positive Integer
n))
    (\Maybe Positive
x ->  Integer -> Natural
Natural (
              case Maybe Positive
x of
                Maybe Positive
Nothing ->
                  Integer
0
                Just (Positive Integer
n) ->
                  Integer
n)
            )

instance AsPositive Natural where
  _Positive :: p Positive (f Positive) -> p Natural (f Natural)
_Positive =
    (Positive -> Natural)
-> (Natural -> Maybe Positive) -> Prism' Natural Positive
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
      (\(Positive Integer
n) -> Integer -> Natural
Natural Integer
n)
      (\(Natural Integer
n) -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Maybe Positive
forall a. Maybe a
Nothing else Positive -> Maybe Positive
forall a. a -> Maybe a
Just (Integer -> Positive
Positive Integer
n))

one ::
  Prism'
    Positive
    ()
one :: p () (f ()) -> p Positive (f Positive)
one =
  (() -> Positive)
-> (Positive -> Maybe ()) -> Prism Positive Positive () ()
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\() -> Integer -> Positive
Positive Integer
1)
    (\(Positive Integer
n) -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing)

one' ::
  Positive
one' :: Positive
one' =
  Tagged () (Identity ()) -> Tagged Positive (Identity Positive)
Prism Positive Positive () ()
one (Tagged () (Identity ()) -> Tagged Positive (Identity Positive))
-> () -> Positive
forall t b. AReview t b -> b -> t
# ()

successor1 ::
  Prism'
    Positive
    Positive
successor1 :: p Positive (f Positive) -> p Positive (f Positive)
successor1 =
  (Positive -> Positive)
-> (Positive -> Maybe Positive) -> Prism' Positive Positive
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\(Positive Integer
n) -> Integer -> Positive
Positive (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1))
    (\(Positive Integer
n) -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1 then Maybe Positive
forall a. Maybe a
Nothing else Positive -> Maybe Positive
forall a. a -> Maybe a
Just (Integer -> Positive
Positive (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)))

successor1' ::
  Positive
  -> Positive
successor1' :: Positive -> Positive
successor1' =
  (Tagged Positive (Identity Positive)
-> Tagged Positive (Identity Positive)
Prism' Positive Positive
successor1 (Tagged Positive (Identity Positive)
 -> Tagged Positive (Identity Positive))
-> Positive -> Positive
forall t b. AReview t b -> b -> t
#)

successorW ::
  Iso'
    Natural
    Positive
successorW :: p Positive (f Positive) -> p Natural (f Natural)
successorW =
  (Natural -> Positive)
-> (Positive -> Natural) -> Iso Natural Natural Positive Positive
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
    (\(Natural Integer
n) -> Integer -> Positive
Positive (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1))
    (\(Positive Integer
n) -> Integer -> Natural
Natural (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1))

plus1 ::
  Positive
  -> Positive
  -> Positive
plus1 :: Positive -> Positive -> Positive
plus1 Positive
x Positive
y =
  (Tagged Positive (Identity Positive)
-> Tagged SumPositive (Identity SumPositive)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (Tagged Positive (Identity Positive)
 -> Tagged SumPositive (Identity SumPositive))
-> Positive -> SumPositive
forall t b. AReview t b -> b -> t
# Positive
x SumPositive -> SumPositive -> SumPositive
forall a. Semigroup a => a -> a -> a
<> (Tagged Positive (Identity Positive)
-> Tagged SumPositive (Identity SumPositive)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (Tagged Positive (Identity Positive)
 -> Tagged SumPositive (Identity SumPositive))
-> Positive -> SumPositive
forall t b. AReview t b -> b -> t
# Positive
y :: SumPositive)) SumPositive -> Getting Positive SumPositive Positive -> Positive
forall s a. s -> Getting a s a -> a
^. Getting Positive SumPositive Positive
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped

multiply1 ::
  Positive
  -> Positive
  -> Positive
multiply1 :: Positive -> Positive -> Positive
multiply1 =
  Positive -> Positive -> Positive
forall a. Semigroup a => a -> a -> a
(<>)

square1 ::
  Positive
  -> Positive
  -> Positive
square1 :: Positive -> Positive -> Positive
square1 (Positive Integer
x) (Positive Integer
y) =
  Integer -> Positive
Positive (Integer
x Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
y)

oneOr ::
  AsPositive a =>
  a
  -> Positive
oneOr :: a -> Positive
oneOr a
n =
  Positive -> Maybe Positive -> Positive
forall a. a -> Maybe a -> a
fromMaybe Positive
one' (a
n a -> Getting (First Positive) a Positive -> Maybe Positive
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First Positive) a Positive
forall a. AsPositive a => Prism' a Positive
_Positive)

notZero ::
  Prism'
    Natural
    Positive
notZero :: p Positive (f Positive) -> p Natural (f Natural)
notZero =
  (Positive -> Natural)
-> (Natural -> Maybe Positive) -> Prism' Natural Positive
forall b s a. (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism'
    (\(Positive Integer
n) -> Integer -> Natural
Natural Integer
n)
    (\(Natural Integer
n) -> if Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Maybe Positive
forall a. Maybe a
Nothing else Positive -> Maybe Positive
forall a. a -> Maybe a
Just (Integer -> Positive
Positive Integer
n))

length1 ::
  Foldable1 f =>
  f a
  -> Positive
length1 :: f a -> Positive
length1 f a
x =
  (a -> SumPositive) -> f a -> SumPositive
forall (t :: * -> *) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1 (SumPositive -> a -> SumPositive
forall a b. a -> b -> a
const (Positive -> SumPositive
SumPositive Positive
one')) f a
x SumPositive -> Getting Positive SumPositive Positive -> Positive
forall s a. s -> Getting a s a -> a
^. Getting Positive SumPositive Positive
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped

replicate1 ::
  Positive
  -> a
  -> NonEmpty a
replicate1 :: Positive -> a -> NonEmpty a
replicate1 Positive
n a
a =
  Positive -> NonEmpty a -> NonEmpty a
forall a. Positive -> NonEmpty a -> NonEmpty a
take1 Positive
n (a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| a -> [a]
forall a. a -> [a]
repeat a
a)

take1 ::
  Positive
  -> NonEmpty a
  -> NonEmpty a
take1 :: Positive -> NonEmpty a -> NonEmpty a
take1 Positive
n (a
h:|[a]
t) =
  a
h a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
take (Tagged Positive (Identity Positive)
-> Tagged Natural (Identity Natural)
Iso Natural Natural Positive Positive
successorW (Tagged Positive (Identity Positive)
 -> Tagged Natural (Identity Natural))
-> Positive -> Natural
forall t b. AReview t b -> b -> t
# Positive
n) [a]
t

drop1 ::
  Positive
  -> NonEmpty a
  -> [a]
drop1 :: Positive -> NonEmpty a -> [a]
drop1 Positive
n (a
_:|[a]
t) =
  Natural -> [a] -> [a]
forall a. Natural -> [a] -> [a]
drop (Tagged Positive (Identity Positive)
-> Tagged Natural (Identity Natural)
Iso Natural Natural Positive Positive
successorW (Tagged Positive (Identity Positive)
 -> Tagged Natural (Identity Natural))
-> Positive -> Natural
forall t b. AReview t b -> b -> t
# Positive
n) [a]
t

splitAt1 ::
  Positive
  -> NonEmpty a
  -> (NonEmpty a, [a])
splitAt1 :: Positive -> NonEmpty a -> (NonEmpty a, [a])
splitAt1 Positive
n NonEmpty a
x =
  (Positive -> NonEmpty a -> NonEmpty a
forall a. Positive -> NonEmpty a -> NonEmpty a
take1 Positive
n NonEmpty a
x, Positive -> NonEmpty a -> [a]
forall a. Positive -> NonEmpty a -> [a]
drop1 Positive
n NonEmpty a
x)

(!!!) ::
  NonEmpty a
  -> Positive
  -> Maybe a
(a
_:|[a]
t) !!! :: NonEmpty a -> Positive -> Maybe a
!!! Positive
n =
  [a]
t [a] -> Natural -> Maybe a
forall a. [a] -> Natural -> Maybe a
!! (Tagged Positive (Identity Positive)
-> Tagged Natural (Identity Natural)
Iso Natural Natural Positive Positive
successorW (Tagged Positive (Identity Positive)
 -> Tagged Natural (Identity Natural))
-> Positive -> Natural
forall t b. AReview t b -> b -> t
# Positive
n)

findIndices1 ::
  (a -> Bool)
  -> NonEmpty a
  -> [Positive]
findIndices1 :: (a -> Bool) -> NonEmpty a -> [Positive]
findIndices1 a -> Bool
p NonEmpty a
x =
  ((a, Positive) -> Positive) -> [(a, Positive)] -> [Positive]
forall a b. (a -> b) -> [a] -> [b]
map (a, Positive) -> Positive
forall a b. (a, b) -> b
snd (((a, Positive) -> Bool)
-> NonEmpty (a, Positive) -> [(a, Positive)]
forall a. (a -> Bool) -> NonEmpty a -> [a]
NonEmpty.filter (a -> Bool
p (a -> Bool) -> ((a, Positive) -> a) -> (a, Positive) -> Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a, Positive) -> a
forall a b. (a, b) -> a
fst) (NonEmpty a -> NonEmpty Positive -> NonEmpty (a, Positive)
forall a b. NonEmpty a -> NonEmpty b -> NonEmpty (a, b)
NonEmpty.zip NonEmpty a
x ((Positive -> Positive) -> Positive -> NonEmpty Positive
forall a. (a -> a) -> a -> NonEmpty a
NonEmpty.iterate Positive -> Positive
successor1' Positive
one')))
  
findIndex1 ::
  (a -> Bool)
  -> NonEmpty a
  -> Maybe Positive
findIndex1 :: (a -> Bool) -> NonEmpty a -> Maybe Positive
findIndex1 a -> Bool
p =
  [Positive] -> Maybe Positive
forall a. [a] -> Maybe a
listToMaybe ([Positive] -> Maybe Positive)
-> (NonEmpty a -> [Positive]) -> NonEmpty a -> Maybe Positive
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (a -> Bool) -> NonEmpty a -> [Positive]
forall a. (a -> Bool) -> NonEmpty a -> [Positive]
findIndices1 a -> Bool
p

elemIndices1 ::
  Eq a =>
  a
  -> NonEmpty a
  -> [Positive]
elemIndices1 :: a -> NonEmpty a -> [Positive]
elemIndices1 =
  (a -> Bool) -> NonEmpty a -> [Positive]
forall a. (a -> Bool) -> NonEmpty a -> [Positive]
findIndices1 ((a -> Bool) -> NonEmpty a -> [Positive])
-> (a -> a -> Bool) -> a -> NonEmpty a -> [Positive]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

elemIndex1 ::
  Eq a =>
  a
  -> NonEmpty a
  -> Maybe Positive
elemIndex1 :: a -> NonEmpty a -> Maybe Positive
elemIndex1 =
  (a -> Bool) -> NonEmpty a -> Maybe Positive
forall a. (a -> Bool) -> NonEmpty a -> Maybe Positive
findIndex1 ((a -> Bool) -> NonEmpty a -> Maybe Positive)
-> (a -> a -> Bool) -> a -> NonEmpty a -> Maybe Positive
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

minus1 ::
  Positive
  -> Positive
  -> Positive
minus1 :: Positive -> Positive -> Positive
minus1 (Positive Integer
x) (Positive Integer
y) =
  Integer -> Positive
Positive (if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
y then Integer
1 else Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)

list1 ::
  Iso'
    Positive
    (NonEmpty ())
list1 :: p (NonEmpty ()) (f (NonEmpty ())) -> p Positive (f Positive)
list1 =
  (Positive -> NonEmpty ())
-> (NonEmpty () -> Positive)
-> Iso Positive Positive (NonEmpty ()) (NonEmpty ())
forall s a b t. (s -> a) -> (b -> t) -> Iso s t a b
iso
    (\Positive
n -> Positive -> () -> NonEmpty ()
forall a. Positive -> a -> NonEmpty a
replicate1 Positive
n ())
    NonEmpty () -> Positive
forall (f :: * -> *) a. Foldable1 f => f a -> Positive
length1

plusone ::
  Natural
  -> Positive
plusone :: Natural -> Positive
plusone =
  (Natural -> Getting Positive Natural Positive -> Positive
forall s a. s -> Getting a s a -> a
^. Getting Positive Natural Positive
Iso Natural Natural Positive Positive
successorW)

minusone ::
  Positive
  -> Natural
minusone :: Positive -> Natural
minusone =
  (Tagged Positive (Identity Positive)
-> Tagged Natural (Identity Natural)
Iso Natural Natural Positive Positive
successorW (Tagged Positive (Identity Positive)
 -> Tagged Natural (Identity Natural))
-> Positive -> Natural
forall t b. AReview t b -> b -> t
#)