    -- | 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