{-# LANGUAGE CPP                #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE Safe               #-}

#if __GLASGOW_HASKELL__ < 710
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE StandaloneDeriving #-}
#endif
-- | 'Nat' numbers.
--
-- This module is designed to be imported qualified.
--
module Data.Nat (
    -- * Natural, Nat numbers
    Nat(..),
    toNatural,
    fromNatural,
    cata,
    -- * Showing
    explicitShow,
    explicitShowsPrec,
    -- * Aliases
    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,
    ) where

import Control.DeepSeq (NFData (..))
import Data.Data       (Data)
import Data.Hashable   (Hashable (..))
import Data.Typeable   (Typeable)
import GHC.Exception   (ArithException (..), throw)
import Numeric.Natural (Natural)

import qualified Data.Universe.Class as U
import qualified Test.QuickCheck     as QC

-- $setup

-------------------------------------------------------------------------------
-- Nat
-------------------------------------------------------------------------------

-- | Nat natural numbers.
--
-- Better than GHC's built-in 'GHC.TypeLits.Nat' for some use cases.
--
data Nat = Z | S Nat 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, Typeable, 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)
$cS :: Constr
$cZ :: 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)

#if __GLASGOW_HASKELL__ < 710
deriving instance Typeable 'Z
deriving instance Typeable 'S
#endif

-- | 'Nat' is printed as 'Natural'.
--
-- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'
--
instance Show Nat where
    showsPrec :: Int -> Nat -> ShowS
showsPrec Int
d = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Natural -> ShowS) -> (Nat -> Natural) -> Nat -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Natural
toNatural

instance Ord Nat where
    compare :: Nat -> Nat -> Ordering
compare Nat
Z     Nat
Z     = Ordering
EQ
    compare Nat
Z     (S Nat
_) = Ordering
LT
    compare (S Nat
_) Nat
Z     = Ordering
GT
    compare (S Nat
n) (S Nat
m) = Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Nat
n Nat
m

    Nat
Z   < :: Nat -> Nat -> Bool
< Nat
Z   = Bool
False
    Nat
Z   < S Nat
_ = Bool
True
    S Nat
_ < Nat
Z   = Bool
False
    S Nat
n < S Nat
m = Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
m

    Nat
Z   <= :: Nat -> Nat -> Bool
<= Nat
Z   = Bool
True
    Nat
Z   <= S Nat
_ = Bool
True
    S Nat
_ <= Nat
Z   = Bool
False
    S Nat
n <= S Nat
m = Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
m

    min :: Nat -> Nat -> Nat
min Nat
Z     Nat
Z     = Nat
Z
    min Nat
Z     (S Nat
_) = Nat
Z
    min (S Nat
_) Nat
Z     = Nat
Z
    min (S Nat
n) (S Nat
m) = Nat -> Nat
S (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
min Nat
n Nat
m)

    max :: Nat -> Nat -> Nat
max Nat
Z       Nat
Z       = Nat
Z
    max Nat
Z       m :: Nat
m@(S Nat
_) = Nat
m
    max n :: Nat
n@(S Nat
_) Nat
Z       = Nat
n
    max (S Nat
n)   (S Nat
m)   = Nat -> Nat
S (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max Nat
n Nat
m)

instance Num Nat where
    fromInteger :: Integer -> Nat
fromInteger = Natural -> Nat
fromNatural (Natural -> Nat) -> (Integer -> Natural) -> Integer -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Natural
forall a. Num a => Integer -> a
fromInteger

    Nat
Z   + :: Nat -> Nat -> Nat
+ Nat
m = Nat
m
    S Nat
n + Nat
m = Nat -> Nat
S (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m)

    Nat
Z   * :: Nat -> Nat -> Nat
* Nat
_ = Nat
Z
    S Nat
n * Nat
m = (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* Nat
m) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
m

    abs :: Nat -> Nat
abs = Nat -> Nat
forall a. a -> a
id

    signum :: Nat -> Nat
signum Nat
Z     = Nat
Z
    signum (S Nat
_) = Nat -> Nat
S Nat
Z

    negate :: Nat -> Nat
negate Nat
_ = String -> Nat
forall a. HasCallStack => String -> a
error String
"negate @Nat"

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

instance Integral Nat where
    toInteger :: Nat -> Integer
toInteger = Integer -> (Integer -> Integer) -> Nat -> Integer
forall a. a -> (a -> a) -> Nat -> a
cata Integer
0 Integer -> Integer
forall a. Enum a => a -> a
succ

    quotRem :: Nat -> Nat -> (Nat, Nat)
quotRem Nat
_ Nat
Z = ArithException -> (Nat, Nat)
forall a e. Exception e => e -> a
throw ArithException
DivideByZero
    quotRem Nat
_ Nat
_ = String -> (Nat, Nat)
forall a. HasCallStack => String -> a
error String
"quotRam @Nat un-implemented"

{- TODO: make <= with witness
instance Ix Nat where
    range = _

    inRange = _
-}

instance Enum Nat where
    toEnum :: Int -> Nat
toEnum Int
n
        | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = ArithException -> Nat
forall a e. Exception e => e -> a
throw ArithException
Underflow
        | Bool
otherwise = (Nat -> Nat) -> Nat -> [Nat]
forall a. (a -> a) -> a -> [a]
iterate Nat -> Nat
S Nat
Z [Nat] -> Int -> Nat
forall a. [a] -> Int -> a
!! Int
n

    fromEnum :: Nat -> Int
fromEnum = Int -> (Int -> Int) -> Nat -> Int
forall a. a -> (a -> a) -> Nat -> a
cata Int
0 Int -> Int
forall a. Enum a => a -> a
succ

    succ :: Nat -> Nat
succ       = Nat -> Nat
S
    pred :: Nat -> Nat
pred Nat
Z     = ArithException -> Nat
forall a e. Exception e => e -> a
throw ArithException
Underflow
    pred (S Nat
n) = Nat
n

instance NFData Nat where
    rnf :: Nat -> ()
rnf Nat
Z     = ()
    rnf (S Nat
n) = Nat -> ()
forall a. NFData a => a -> ()
rnf Nat
n

instance Hashable Nat where
    hashWithSalt :: Int -> Nat -> Int
hashWithSalt Int
salt = Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Integer -> Int) -> (Nat -> Integer) -> Nat -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance QC.Arbitrary Nat where
    arbitrary :: Gen Nat
arbitrary = (Natural -> Nat) -> Gen Natural -> Gen Nat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Natural -> Nat
fromNatural Gen Natural
forall a. Integral a => Gen a
QC.arbitrarySizedNatural

    shrink :: Nat -> [Nat]
shrink Nat
Z     = []
    shrink (S Nat
n) = Nat
n Nat -> [Nat] -> [Nat]
forall a. a -> [a] -> [a]
: Nat -> [Nat]
forall a. Arbitrary a => a -> [a]
QC.shrink Nat
n

instance QC.CoArbitrary Nat where
    coarbitrary :: Nat -> Gen b -> Gen b
coarbitrary Nat
Z     = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
    coarbitrary (S Nat
n) = Int -> Gen b -> Gen b
forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) (Gen b -> Gen b) -> (Gen b -> Gen b) -> Gen b -> Gen b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Gen b -> Gen b
forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary Nat
n

instance QC.Function Nat where
    function :: (Nat -> b) -> Nat :-> b
function = (Nat -> b) -> Nat :-> b
forall a b. Integral a => (a -> b) -> a :-> b
QC.functionIntegral

-------------------------------------------------------------------------------
-- universe-base
-------------------------------------------------------------------------------

-- |
--
-- >>> import qualified Data.Universe.Class as U
-- >>> take 10 (U.universe :: [Nat])
-- [0,1,2,3,4,5,6,7,8,9]
--
-- @since 0.1.2
instance U.Universe Nat where
    universe :: [Nat]
universe = Nat -> [Nat]
go Nat
Z where
        go :: Nat -> [Nat]
go Nat
n = Nat
n Nat -> [Nat] -> [Nat]
forall a. a -> [a] -> [a]
: Nat -> [Nat]
go (Nat -> Nat
S Nat
n)

-------------------------------------------------------------------------------
-- Showing
-------------------------------------------------------------------------------

-- | 'show' displaying a structure of 'Nat'.
--
-- >>> explicitShow 0
-- "Z"
--
-- >>> explicitShow 2
-- "S (S Z)"
--
explicitShow :: Nat -> String
explicitShow :: Nat -> String
explicitShow Nat
n = Int -> Nat -> ShowS
explicitShowsPrec Int
0 Nat
n String
""

-- | 'showsPrec' displaying a structure of 'Nat'.
explicitShowsPrec :: Int -> Nat -> ShowS
explicitShowsPrec :: Int -> Nat -> ShowS
explicitShowsPrec Int
_ Nat
Z     = String -> ShowS
showString String
"Z"
explicitShowsPrec Int
d (S Nat
n) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10)
    (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"S "
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ShowS
explicitShowsPrec Int
11 Nat
n

-------------------------------------------------------------------------------
-- Conversions
-------------------------------------------------------------------------------

-- | Fold 'Nat'.
--
-- >>> cata [] ('x' :) 2
-- "xx"
--
cata :: a -> (a -> a) -> Nat -> a
cata :: a -> (a -> a) -> Nat -> a
cata a
z a -> a
f = Nat -> a
go where
    go :: Nat -> a
go Nat
Z     = a
z
    go (S Nat
n) = a -> a
f (Nat -> a
go Nat
n)

-- | Convert 'Nat' to 'Natural'
--
-- >>> toNatural 0
-- 0
--
-- >>> toNatural 2
-- 2
--
-- >>> toNatural $ S $ S $ Z
-- 2
--
toNatural :: Nat -> Natural
toNatural :: Nat -> Natural
toNatural Nat
Z = Natural
0
toNatural (S Nat
n) = Natural -> Natural
forall a. Enum a => a -> a
succ (Nat -> Natural
toNatural Nat
n)

-- | Convert 'Natural' to 'Nat'
--
-- >>> fromNatural 4
-- 4
--
-- >>> explicitShow (fromNatural 4)
-- "S (S (S (S Z)))"
--
fromNatural :: Natural -> Nat
fromNatural :: Natural -> Nat
fromNatural Natural
0 = Nat
Z
fromNatural Natural
n = Nat -> Nat
S (Natural -> Nat
fromNatural (Natural -> Natural
forall a. Enum a => a -> a
pred Natural
n))

-------------------------------------------------------------------------------
-- Aliases
-------------------------------------------------------------------------------

nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9 :: Nat
nat0 :: Nat
nat0 = Nat
Z
nat1 :: Nat
nat1 = Nat -> Nat
S Nat
nat0
nat2 :: Nat
nat2 = Nat -> Nat
S Nat
nat1
nat3 :: Nat
nat3 = Nat -> Nat
S Nat
nat2
nat4 :: Nat
nat4 = Nat -> Nat
S Nat
nat3
nat5 :: Nat
nat5 = Nat -> Nat
S Nat
nat4
nat6 :: Nat
nat6 = Nat -> Nat
S Nat
nat5
nat7 :: Nat
nat7 = Nat -> Nat
S Nat
nat6
nat8 :: Nat
nat8 = Nat -> Nat
S Nat
nat7
nat9 :: Nat
nat9 = Nat -> Nat
S Nat
nat8