-- TODO: merge with the Posta version. And release them as a standalone package
{-# LANGUAGE CPP, DeriveDataTypeable #-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2015.12.17
-- |
-- Module      :  Data.Number.Nat
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  Haskell98 + CPP
--
-- A data type for natural numbers (aka non-negative integers).
----------------------------------------------------------------
module Data.Number.Nat
    ( Nat()
    , fromNat
    , toNat
    , unsafeNat
    , MaxNat(..)
    ) where

#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (Monoid(..))
#endif

#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup
#endif

import Data.Data (Data, Typeable)

----------------------------------------------------------------
----------------------------------------------------------------
-- | Natural numbers, with fixed-width à la 'Int'. N.B., the 'Num'
-- instance will throw errors on subtraction, negation, and
-- 'fromInteger' when the result is not a natural number.
newtype Nat = Nat Int
    deriving (Nat -> Nat -> Bool
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c== :: Nat -> Nat -> Bool
Eq, Eq Nat
Eq Nat
-> (Nat -> Nat -> Ordering)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> Ord Nat
Nat -> Nat -> Bool
Nat -> Nat -> Ordering
Nat -> Nat -> Nat
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 :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmax :: Nat -> Nat -> Nat
>= :: Nat -> Nat -> Bool
$c>= :: Nat -> Nat -> Bool
> :: Nat -> Nat -> Bool
$c> :: Nat -> Nat -> Bool
<= :: Nat -> Nat -> Bool
$c<= :: Nat -> Nat -> Bool
< :: Nat -> Nat -> Bool
$c< :: Nat -> Nat -> Bool
compare :: Nat -> Nat -> Ordering
$ccompare :: Nat -> Nat -> Ordering
$cp1Ord :: Eq Nat
Ord, Int -> Nat -> ShowS
[Nat] -> ShowS
Nat -> String
(Int -> Nat -> ShowS)
-> (Nat -> String) -> ([Nat] -> ShowS) -> Show Nat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Nat] -> ShowS
$cshowList :: [Nat] -> ShowS
show :: Nat -> String
$cshow :: Nat -> String
showsPrec :: Int -> Nat -> ShowS
$cshowsPrec :: Int -> Nat -> ShowS
Show, Typeable Nat
DataType
Constr
Typeable Nat
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Nat -> c Nat)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Nat)
-> (Nat -> Constr)
-> (Nat -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Nat))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat))
-> ((forall b. Data b => b -> b) -> Nat -> Nat)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r)
-> (forall u. (forall d. Data d => d -> u) -> Nat -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Nat -> m Nat)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Nat -> m Nat)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Nat -> m Nat)
-> Data Nat
Nat -> DataType
Nat -> Constr
(forall b. Data b => b -> b) -> Nat -> Nat
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
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) -> Nat -> u
forall u. (forall d. Data d => d -> u) -> Nat -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cNat :: Constr
$tNat :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapMp :: (forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapM :: (forall d. Data d => d -> m d) -> Nat -> m Nat
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapQi :: Int -> (forall d. Data d => d -> u) -> Nat -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
gmapQ :: (forall d. Data d => d -> u) -> Nat -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
$cgmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Nat)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
dataTypeOf :: Nat -> DataType
$cdataTypeOf :: Nat -> DataType
toConstr :: Nat -> Constr
$ctoConstr :: Nat -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
$cp1Data :: Typeable Nat
Data, Typeable)

-- TODO: should we define our own Show instance, in order to just
-- show the Int itself, relying on our 'fromInteger' definition to
-- preserve cut&paste-ability? If so, then we should ensure that
-- the Read instance is optional in whether the \"Nat\" is there
-- or not.

-- N.B., we cannot derive Read, since that would inject invalid numbers!
instance Read Nat where
    readsPrec :: Int -> ReadS Nat
readsPrec Int
d =
        Bool -> ReadS Nat -> ReadS Nat
forall a. Bool -> ReadS a -> ReadS a
readParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ReadS Nat -> ReadS Nat) -> ReadS Nat -> ReadS Nat
forall a b. (a -> b) -> a -> b
$ \String
s0 -> do
            (String
"Nat", String
s1) <- ReadS String
lex String
s0
            (Int
i,     String
s2) <- Int -> ReadS Int
forall a. Read a => Int -> ReadS a
readsPrec Int
11 String
s1
            [(Nat, String)]
-> (Nat -> [(Nat, String)]) -> Maybe Nat -> [(Nat, String)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Nat
n -> [(Nat
n,String
s2)]) (Int -> Maybe Nat
toNat Int
i)


-- | Safely convert a natural number to an integer.
fromNat :: Nat -> Int
fromNat :: Nat -> Int
fromNat (Nat Int
i) = Int
i
{-# INLINE fromNat #-}


-- | Safely convert an integer to a natural number. Returns @Nothing@
-- if the integer is negative.
toNat :: Int -> Maybe Nat
toNat :: Int -> Maybe Nat
toNat Int
x
    | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = Maybe Nat
forall a. Maybe a
Nothing
    | Bool
otherwise = Nat -> Maybe Nat
forall a. a -> Maybe a
Just (Int -> Nat
Nat Int
x)
{-# INLINE toNat #-}


-- | Unsafely convert an integer to a natural number. Throws an
-- error if the integer is negative.
unsafeNat :: Int -> Nat
unsafeNat :: Int -> Nat
unsafeNat Int
x
    | Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_unsafeNat
    | Bool
otherwise = Int -> Nat
Nat Int
x
{-# INLINE unsafeNat #-}


instance Num Nat where
    Nat Int
i + :: Nat -> Nat -> Nat
+ Nat Int
j   = Int -> Nat
Nat (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)
    Nat Int
i * :: Nat -> Nat -> Nat
* Nat Int
j   = Int -> Nat
Nat (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
j)
    Nat Int
i - :: Nat -> Nat -> Nat
- Nat Int
j
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
j    = Int -> Nat
Nat (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j)
        | Bool
otherwise = String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_subtraction
    negate :: Nat -> Nat
negate Nat
_        = String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_negate
    abs :: Nat -> Nat
abs Nat
n           = Nat
n
    signum :: Nat -> Nat
signum Nat
_        = Int -> Nat
Nat Int
1
    fromInteger :: Integer -> Nat
fromInteger Integer
i
        | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = Int -> Nat
Nat Int
n
        | Bool
otherwise = String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_fromInteger
        where
        n :: Int
        n :: Int
n = Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i
    {-# INLINE (+) #-}
    {-# INLINE (*) #-}
    {-# INLINE (-) #-}
    {-# INLINE negate #-}
    {-# INLINE abs #-}
    {-# INLINE signum #-}
    {-# INLINE fromInteger #-}

instance Enum Nat where
    succ :: Nat -> Nat
succ (Nat Int
i) = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
forall a. Bounded a => a
maxBound then Int -> Nat
Nat (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) else String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_succ
    pred :: Nat -> Nat
pred (Nat Int
i) = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0        then Int -> Nat
Nat (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) else String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_pred
    toEnum :: Int -> Nat
toEnum Int
n     = if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0        then Int -> Nat
Nat Int
n     else String -> Nat
forall a. HasCallStack => String -> a
error String
_errmsg_toEnum
    fromEnum :: Nat -> Int
fromEnum (Nat Int
i) = Int
i

    enumFrom :: Nat -> [Nat]
enumFrom       (Nat Int
i)                 = (Int -> Nat) -> [Int] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Nat
Nat (Int -> [Int]
forall a. Enum a => a -> [a]
enumFrom       Int
i)
    enumFromThen :: Nat -> Nat -> [Nat]
enumFromThen   (Nat Int
i) (Nat Int
j)         = (Int -> Nat) -> [Int] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Nat
Nat (Int -> Int -> [Int]
forall a. Enum a => a -> a -> [a]
enumFromThen   Int
i Int
j)
    enumFromTo :: Nat -> Nat -> [Nat]
enumFromTo     (Nat Int
i)         (Nat Int
k) = (Int -> Nat) -> [Int] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Nat
Nat (Int -> Int -> [Int]
forall a. Enum a => a -> a -> [a]
enumFromTo     Int
i   Int
k)
    enumFromThenTo :: Nat -> Nat -> Nat -> [Nat]
enumFromThenTo (Nat Int
i) (Nat Int
j) (Nat Int
k) = (Int -> Nat) -> [Int] -> [Nat]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Nat
Nat (Int -> Int -> Int -> [Int]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Int
i Int
j Int
k)
    {-# INLINE succ #-}
    {-# INLINE pred #-}
    {-# INLINE toEnum #-}
    {-# INLINE fromEnum #-}
    {-# INLINE enumFrom #-}
    {-# INLINE enumFromThen #-}
    {-# INLINE enumFromTo #-}
    {-# INLINE enumFromThenTo #-}

instance Real Nat where
    toRational :: Nat -> Rational
toRational (Nat Int
i) = Int -> Rational
forall a. Real a => a -> Rational
toRational Int
i
    {-# INLINE toRational #-}

instance Integral Nat where
    quot :: Nat -> Nat -> Nat
quot    (Nat Int
i) (Nat Int
j) = Int -> Nat
Nat (Int -> Int -> Int
forall a. Integral a => a -> a -> a
quot Int
i Int
j)
    rem :: Nat -> Nat -> Nat
rem     (Nat Int
i) (Nat Int
j) = Int -> Nat
Nat (Int -> Int -> Int
forall a. Integral a => a -> a -> a
rem  Int
i Int
j)
    quotRem :: Nat -> Nat -> (Nat, Nat)
quotRem (Nat Int
i) (Nat Int
j) = case Int -> Int -> (Int, Int)
forall a. Integral a => a -> a -> (a, a)
quotRem Int
i Int
j of (Int
q,Int
r) -> (Int -> Nat
Nat Int
q, Int -> Nat
Nat Int
r)
    div :: Nat -> Nat -> Nat
div    = Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
quot
    mod :: Nat -> Nat -> Nat
mod    = Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
rem
    divMod :: Nat -> Nat -> (Nat, Nat)
divMod = Nat -> Nat -> (Nat, Nat)
forall a. Integral a => a -> a -> (a, a)
quotRem
    toInteger :: Nat -> Integer
toInteger (Nat Int
i) = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i
    {-# INLINE quot #-}
    {-# INLINE rem #-}
    {-# INLINE div #-}
    {-# INLINE mod #-}
    {-# INLINE quotRem #-}
    {-# INLINE divMod #-}
    {-# INLINE toInteger #-}


----------------------------------------------------------------
newtype MaxNat = MaxNat { MaxNat -> Nat
unMaxNat :: Nat }

instance Semigroup MaxNat where
    MaxNat Nat
m <> :: MaxNat -> MaxNat -> MaxNat
<> MaxNat Nat
n = Nat -> MaxNat
MaxNat (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
m Nat
n)

instance Monoid MaxNat where
    mempty :: MaxNat
mempty  = Nat -> MaxNat
MaxNat Nat
0
#if !(MIN_VERSION_base(4,11,0))
    mappend = (<>)
#endif

----------------------------------------------------------------
_errmsg_unsafeNat, _errmsg_subtraction, _errmsg_negate, _errmsg_fromInteger, _errmsg_succ, _errmsg_pred, _errmsg_toEnum
    :: String
_errmsg_unsafeNat :: String
_errmsg_unsafeNat   = String
"unsafeNat: negative input"
_errmsg_subtraction :: String
_errmsg_subtraction = String
"(-)@Nat: Num is a bad abstraction"
_errmsg_negate :: String
_errmsg_negate      = String
"negate@Nat: Num is a bad abstraction"
_errmsg_fromInteger :: String
_errmsg_fromInteger = String
"fromInteger@Nat: Num is a bad abstraction"
_errmsg_succ :: String
_errmsg_succ        = String
"succ@Nat: No successor of the maxBound"
_errmsg_pred :: String
_errmsg_pred        = String
"pred@Nat: No predecessor of zero"
_errmsg_toEnum :: String
_errmsg_toEnum      = String
"toEnum@Nat: negative input"
{-# NOINLINE _errmsg_unsafeNat #-}
{-# NOINLINE _errmsg_subtraction #-}
{-# NOINLINE _errmsg_negate #-}
{-# NOINLINE _errmsg_fromInteger #-}
{-# NOINLINE _errmsg_succ #-}
{-# NOINLINE _errmsg_pred #-}
{-# NOINLINE _errmsg_toEnum #-}

----------------------------------------------------------------
----------------------------------------------------------- fin.