-- | 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 p :: Int
p n :: 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
    x :: Natural
x == :: Natural -> Natural -> Bool
== y :: 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
    Z   compare :: Natural -> Natural -> Ordering
`compare` Z    =  Ordering
EQ
    Z   `compare` S _  =  Ordering
LT
    S _ `compare` Z    =  Ordering
GT
    S x :: Natural
x `compare` S y :: 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 -> Bool
>= Z = Bool
True
    Z >= S _ = Bool
False
    S a :: Natural
a >= S b :: 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 x :: Natural
x max :: Natural -> Natural -> Natural
`max` S y :: Natural
y = Natural -> Natural
S (Natural
x Natural -> Natural -> Natural
forall a. Ord a => a -> a -> a
`max` Natural
y)
    x :: Natural
x   `max` y :: Natural
y   = Natural
x Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
y

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

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

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

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

    Z   * :: Natural -> Natural -> Natural
* y :: Natural
y  =  Natural
Z
    S x :: Natural
x * y :: 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 x :: Natural
x = Natural
x
    signum :: Natural -> Natural
signum Z = Natural
Z
    signum (S _) = Natural -> Natural
S Natural
Z

    fromInteger :: Integer -> Natural
fromInteger x :: Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = String -> Natural
forall a. HasCallStack => String -> a
error "Natural: fromInteger"
    fromInteger 0 = Natural
Z
    fromInteger x :: 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
-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 x :: Natural
x y :: Natural
y =
        if Natural
x Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
y then
            (0, Natural
x)
        else
            let (q :: Natural
q, r :: 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  (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 Z = 0
    toInteger (S x :: Natural
x) = 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 Z = String -> Natural
forall a. HasCallStack => String -> a
error "Natural: pred 0"
    pred (S a :: 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 from :: Natural
from thn :: Natural
thn to :: 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 from :: Natural
from Nothing      = []
      go from :: Natural
from (Just count :: 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 from :: Natural
from thn :: Natural
thn to :: 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 from :: 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 a :: 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 a :: Natural
a b :: 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 a :: Natural
a c :: 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