-- | Lazy natural numbers.
-- Addition and multiplication recurses over the first argument, i.e.,
-- @1 + n@ is the way to write the constant time successor function.
--
-- Note that (+) and (*) are not commutative for lazy natural numbers
-- when considering bottom.
module Data.Number.Natural(Natural, infinity) where

import Data.Maybe

data Natural = Z | S Natural

instance Show Natural where
    showsPrec :: Int -> Natural -> ShowS
showsPrec Int
p Natural
n = Int -> Integer -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n)

instance Eq Natural where
    Natural
x == :: Natural -> Natural -> Bool
== Natural
y  =  Natural
x Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Natural
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord Natural where
    Natural
Z   compare :: Natural -> Natural -> Ordering
`compare` Natural
Z    =  Ordering
EQ
    Natural
Z   `compare` S Natural
_  =  Ordering
LT
    S Natural
_ `compare` Natural
Z    =  Ordering
GT
    S Natural
x `compare` S Natural
y  =  Natural
x Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` Natural
y

    -- (_|_) `compare` Z == _|_, but (_|_) >= Z = True
    -- so for maximum laziness, we need a specialized version of (>=) and (<=)
    Natural
_ >= :: Natural -> Natural -> Bool
>= Natural
Z = Bool
True
    Natural
Z >= S Natural
_ = Bool
False
    S Natural
a >= S Natural
b = Natural
a Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
b

    <= :: Natural -> Natural -> Bool
(<=) = (Natural -> Natural -> Bool) -> Natural -> Natural -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
(>=)

    S Natural
x max :: Natural -> Natural -> Natural
`max` S Natural
y = Natural -> Natural
S (Natural
x Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
`max` Natural
y)
    Natural
x   `max` Natural
y   = Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
y

    S Natural
x min :: Natural -> Natural -> Natural
`min` S Natural
y = Natural -> Natural
S (Natural
x Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
`min` Natural
y)
    Natural
_   `min` Natural
_   = Natural
Z

maybeSubtract :: Natural -> Natural -> Maybe Natural
Natural
a   maybeSubtract :: Natural -> Natural -> Maybe Natural
`maybeSubtract` Natural
Z   = Natural -> Maybe Natural
forall a. a -> Maybe a
Just Natural
a
S Natural
a `maybeSubtract` S Natural
b = Natural
a Natural -> Natural -> Maybe Natural
`maybeSubtract` Natural
b
Natural
_   `maybeSubtract` Natural
_   = Maybe Natural
forall a. Maybe a
Nothing

instance Num Natural where
    Natural
Z   + :: Natural -> Natural -> Natural
+ Natural
y  =  Natural
y
    S Natural
x + Natural
y  =  Natural -> Natural
S (Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
y)

    Natural
x   - :: Natural -> Natural -> Natural
- Natural
y  = Natural -> Maybe Natural -> Natural
forall a. a -> Maybe a -> a
fromMaybe (String -> Natural
forall a. HasCallStack => String -> a
error String
"Natural: (-)") (Natural
x Natural -> Natural -> Maybe Natural
`maybeSubtract` Natural
y)

    Natural
Z   * :: Natural -> Natural -> Natural
* Natural
y  =  Natural
Z
    S Natural
x * Natural
y  =  Natural
y Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
y

    abs :: Natural -> Natural
abs Natural
x = Natural
x
    signum :: Natural -> Natural
signum Natural
Z = Natural
Z
    signum (S Natural
_) = Natural -> Natural
S Natural
Z

    fromInteger :: Integer -> Natural
fromInteger Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = String -> Natural
forall a. HasCallStack => String -> a
error String
"Natural: fromInteger"
    fromInteger Integer
0 = Natural
Z
    fromInteger Integer
x = Natural -> Natural
S (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer
xInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))

instance Integral Natural where
    -- Not the most efficient version, but efficiency isn't the point of this module. :)
    quotRem :: Natural -> Natural -> (Natural, Natural)
quotRem Natural
x Natural
y =
        if Natural
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
y then
            (Natural
0, Natural
x)
        else
            let (Natural
q, Natural
r) = Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
quotRem (Natural
xNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
y) Natural
y
            in  (Natural
1Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
q, Natural
r)
    div :: Natural -> Natural -> Natural
div = Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
quot
    mod :: Natural -> Natural -> Natural
mod = Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
rem
    toInteger :: Natural -> Integer
toInteger Natural
Z = Integer
0
    toInteger (S Natural
x) = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
x

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

instance Enum Natural where
    succ :: Natural -> Natural
succ = Natural -> Natural
S
    pred :: Natural -> Natural
pred Natural
Z = String -> Natural
forall a. HasCallStack => String -> a
error String
"Natural: pred 0"
    pred (S Natural
a) = Natural
a
    toEnum :: Int -> Natural
toEnum = Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    fromEnum :: Natural -> Int
fromEnum = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    enumFromThenTo :: Natural -> Natural -> Natural -> [Natural]
enumFromThenTo Natural
from Natural
thn Natural
to | Natural
from Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
thn = Natural -> Maybe Natural -> [Natural]
go Natural
from (Natural
to Natural -> Natural -> Maybe Natural
`maybeSubtract` Natural
from) where
      go :: Natural -> Maybe Natural -> [Natural]
go Natural
from Maybe Natural
Nothing      = []
      go Natural
from (Just Natural
count) = Natural
fromNatural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
:Natural -> Maybe Natural -> [Natural]
go (Natural
step Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
from) (Natural
count Natural -> Natural -> Maybe Natural
`maybeSubtract` Natural
step)
      step :: Natural
step = Natural
thn Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
from
    enumFromThenTo Natural
from Natural
thn Natural
to | Bool
otherwise = Natural -> [Natural]
go (Natural
from Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
step) where
      go :: Natural -> [Natural]
go Natural
from | Natural
from Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
to Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
step = let next :: Natural
next = Natural
from Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
step in Natural
nextNatural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
:Natural -> [Natural]
go Natural
next
              | Bool
otherwise         = []
      step :: Natural
step = Natural
from Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
thn
    enumFrom :: Natural -> [Natural]
enumFrom Natural
a       = Natural -> Natural -> Natural -> [Natural]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Natural
a (Natural -> Natural
S Natural
a) Natural
infinity
    enumFromThen :: Natural -> Natural -> [Natural]
enumFromThen Natural
a Natural
b = Natural -> Natural -> Natural -> [Natural]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Natural
a Natural
b Natural
infinity
    enumFromTo :: Natural -> Natural -> [Natural]
enumFromTo Natural
a Natural
c   = Natural -> Natural -> Natural -> [Natural]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Natural
a (Natural -> Natural
S Natural
a) Natural
c

-- | The infinite natural number.
infinity :: Natural
infinity :: Natural
infinity = Natural -> Natural
S Natural
infinity