-- | See 'Peano'.

module Data.Peano ( Peano (Zero, Succ), infinity ) where

import Data.Data       ( Data, Typeable )
import Data.Ix         ( Ix( index, inRange, range, rangeSize ) )

-- | The natural numbers in (lazy) unary notation.
data Peano
  = Zero
  | Succ Peano
  deriving (Peano -> Peano -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Peano -> Peano -> Bool
$c/= :: Peano -> Peano -> Bool
== :: Peano -> Peano -> Bool
$c== :: Peano -> Peano -> Bool
Eq, Eq Peano
Peano -> Peano -> Bool
Peano -> Peano -> Ordering
Peano -> Peano -> Peano
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 :: Peano -> Peano -> Peano
$cmin :: Peano -> Peano -> Peano
max :: Peano -> Peano -> Peano
$cmax :: Peano -> Peano -> Peano
>= :: Peano -> Peano -> Bool
$c>= :: Peano -> Peano -> Bool
> :: Peano -> Peano -> Bool
$c> :: Peano -> Peano -> Bool
<= :: Peano -> Peano -> Bool
$c<= :: Peano -> Peano -> Bool
< :: Peano -> Peano -> Bool
$c< :: Peano -> Peano -> Bool
compare :: Peano -> Peano -> Ordering
$ccompare :: Peano -> Peano -> Ordering
Ord, Typeable, Typeable Peano
Peano -> DataType
Peano -> Constr
(forall b. Data b => b -> b) -> Peano -> Peano
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u
forall u. (forall d. Data d => d -> u) -> Peano -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Peano
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Peano -> c Peano
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Peano)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Peano -> m Peano
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Peano -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Peano -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Peano -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r
gmapT :: (forall b. Data b => b -> b) -> Peano -> Peano
$cgmapT :: (forall b. Data b => b -> b) -> Peano -> Peano
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Peano)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Peano)
dataTypeOf :: Peano -> DataType
$cdataTypeOf :: Peano -> DataType
toConstr :: Peano -> Constr
$ctoConstr :: Peano -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Peano
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Peano
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Peano -> c Peano
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Peano -> c Peano
Data, ReadPrec [Peano]
ReadPrec Peano
Int -> ReadS Peano
ReadS [Peano]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Peano]
$creadListPrec :: ReadPrec [Peano]
readPrec :: ReadPrec Peano
$creadPrec :: ReadPrec Peano
readList :: ReadS [Peano]
$creadList :: ReadS [Peano]
readsPrec :: Int -> ReadS Peano
$creadsPrec :: Int -> ReadS Peano
Read, Int -> Peano -> ShowS
[Peano] -> ShowS
Peano -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Peano] -> ShowS
$cshowList :: [Peano] -> ShowS
show :: Peano -> String
$cshow :: Peano -> String
showsPrec :: Int -> Peano -> ShowS
$cshowsPrec :: Int -> Peano -> ShowS
Show)

instance Enum Peano where
    succ :: Peano -> Peano
succ = Peano -> Peano
Succ

    pred :: Peano -> Peano
pred (Succ Peano
n) = Peano
n
    pred Peano
Zero     = forall a. HasCallStack => String -> a
error String
"Data.Peano.pred Zero"

    toEnum :: Int -> Peano
toEnum   = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum

    fromEnum :: Peano -> Int
fromEnum = forall a. Enum a => a -> Int
fromEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance Bounded Peano where
    minBound :: Peano
minBound = Peano
Zero
    maxBound :: Peano
maxBound = Peano
infinity

instance Ix Peano where
    range :: (Peano, Peano) -> [Peano]
range            = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. Enum a => a -> a -> [a]
enumFromTo
    index :: (Peano, Peano) -> Peano -> Int
index (Peano
l, Peano
_) Peano
n   = forall a. Enum a => a -> Int
fromEnum (Peano
n forall a. Num a => a -> a -> a
- Peano
l)
    inRange :: (Peano, Peano) -> Peano -> Bool
inRange (Peano
l, Peano
u) Peano
n = Peano
l forall a. Ord a => a -> a -> Bool
<= Peano
n Bool -> Bool -> Bool
&& Peano
u forall a. Ord a => a -> a -> Bool
>= Peano
n
    rangeSize :: (Peano, Peano) -> Int
rangeSize (Peano
l, Peano
u) = forall a. Enum a => a -> Int
fromEnum (Peano -> Peano
Succ Peano
u forall a. Num a => a -> a -> a
- Peano
l)

instance Num Peano where
    Peano
Zero   + :: Peano -> Peano -> Peano
+ Peano
n = Peano
n
    Succ Peano
m + Peano
n = Peano -> Peano
Succ (Peano
m forall a. Num a => a -> a -> a
+ Peano
n)

    Peano
m      - :: Peano -> Peano -> Peano
- Peano
Zero   = Peano
m
    Succ Peano
m - Succ Peano
n = Peano
m forall a. Num a => a -> a -> a
- Peano
n
    Peano
Zero   - Peano
_      = forall a. HasCallStack => String -> a
error String
"Data.Peano.(-): underflow (negative)"

    Peano
Zero   * :: Peano -> Peano -> Peano
* Peano
_ = Peano
Zero
    Succ Peano
m * Peano
n = Peano
n forall a. Num a => a -> a -> a
+ Peano
m forall a. Num a => a -> a -> a
* Peano
n

    abs :: Peano -> Peano
abs = forall a. a -> a
id

    signum :: Peano -> Peano
signum Peano
Zero = Peano
Zero
    signum Peano
_    = Peano -> Peano
Succ Peano
Zero

    fromInteger :: Integer -> Peano
fromInteger Integer
n =
      case forall a. Ord a => a -> a -> Ordering
compare Integer
n Integer
0 of
        Ordering
LT -> forall a. HasCallStack => String -> a
error String
"fromInteger n | n < 0"
        Ordering
EQ -> Peano
Zero
        Ordering
GT -> Peano -> Peano
Succ (forall a. Num a => Integer -> a
fromInteger (Integer
n forall a. Num a => a -> a -> a
- Integer
1))

instance Real Peano where
    toRational :: Peano -> Rational
toRational = forall a. Real a => a -> Rational
toRational forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

instance Integral Peano where
    toInteger :: Peano -> Integer
toInteger Peano
Zero     = Integer
0
    toInteger (Succ Peano
n) = forall a. Integral a => a -> Integer
toInteger Peano
n forall a. Num a => a -> a -> a
+ Integer
1

    Peano
Zero quotRem :: Peano -> Peano -> (Peano, Peano)
`quotRem` Peano
Zero   = forall a. HasCallStack => String -> a
error String
"Data.Peano.quotRem: zero divided by zero"
    Peano
m    `quotRem` Peano
n      =
      case forall a. Ord a => a -> a -> Ordering
compare Peano
m Peano
n of
        Ordering
LT -> (Peano
Zero, Peano
m)
        Ordering
_  -> let (Peano
q, Peano
r) = forall a. Integral a => a -> a -> (a, a)
quotRem (Peano
m forall a. Num a => a -> a -> a
- Peano
n) Peano
n in (Peano -> Peano
Succ Peano
q, Peano
r)

    divMod :: Peano -> Peano -> (Peano, Peano)
divMod = forall a. Integral a => a -> a -> (a, a)
quotRem

-- | The infinite number (ω).
infinity :: Peano
infinity :: Peano
infinity = Peano -> Peano
Succ Peano
infinity