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

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

    fromEnum :: Peano -> Int
fromEnum = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (Integer -> Int) -> (Peano -> Integer) -> Peano -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Peano -> Integer
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            = (Peano -> Peano -> [Peano]) -> (Peano, Peano) -> [Peano]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Peano -> Peano -> [Peano]
forall a. Enum a => a -> a -> [a]
enumFromTo
    index :: (Peano, Peano) -> Peano -> Int
index (Peano
l, Peano
_) Peano
n   = Peano -> Int
forall a. Enum a => a -> Int
fromEnum (Peano
n Peano -> Peano -> Peano
forall a. Num a => a -> a -> a
- Peano
l)
    inRange :: (Peano, Peano) -> Peano -> Bool
inRange (Peano
l, Peano
u) Peano
n = Peano
l Peano -> Peano -> Bool
forall a. Ord a => a -> a -> Bool
<= Peano
n Bool -> Bool -> Bool
&& Peano
u Peano -> Peano -> Bool
forall a. Ord a => a -> a -> Bool
>= Peano
n
    rangeSize :: (Peano, Peano) -> Int
rangeSize (Peano
l, Peano
u) = Peano -> Int
forall a. Enum a => a -> Int
fromEnum (Peano -> Peano
Succ Peano
u Peano -> Peano -> Peano
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 Peano -> Peano -> Peano
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 Peano -> Peano -> Peano
forall a. Num a => a -> a -> a
- Peano
n
    Peano
Zero   - Peano
_      = String -> 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 Peano -> Peano -> Peano
forall a. Num a => a -> a -> a
+ Peano
m Peano -> Peano -> Peano
forall a. Num a => a -> a -> a
* Peano
n

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

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

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

    Peano
Zero quotRem :: Peano -> Peano -> (Peano, Peano)
`quotRem` Peano
Zero   = String -> (Peano, Peano)
forall a. HasCallStack => String -> a
error String
"Data.Peano.quotRem: zero divided by zero"
    Peano
m    `quotRem` Peano
n      =
      case Peano -> Peano -> Ordering
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) = Peano -> Peano -> (Peano, Peano)
forall a. Integral a => a -> a -> (a, a)
quotRem (Peano
m Peano -> Peano -> Peano
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 = Peano -> Peano -> (Peano, Peano)
forall a. Integral a => a -> a -> (a, a)
quotRem

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