{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE Safe #-}
#if __GLASGOW_HASKELL__ < 710
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
#endif
module Data.Nat (
Nat(..),
toNatural,
fromNatural,
cata,
explicitShow,
explicitShowsPrec,
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
data Nat = Z | S Nat deriving (Nat -> Nat -> Bool
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
Nat -> DataType
Nat -> Constr
(forall b. Data b => b -> b) -> Nat -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable @(* -> * -> *) t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable @(* -> *) t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data)
#if __GLASGOW_HASKELL__ < 710
deriving instance Typeable 'Z
deriving instance Typeable 'S
#endif
instance Show Nat where
showsPrec :: Int -> Nat -> ShowS
showsPrec Int
d = forall a. Show a => Int -> a -> ShowS
showsPrec Int
d 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) = forall a. Ord a => a -> a -> Ordering
compare Nat
n Nat
m
Nat
Z <= :: Nat -> Nat -> Bool
<= Nat
_ = Bool
True
S Nat
_ <= Nat
Z = Bool
False
S Nat
n <= S Nat
m = Nat
n forall a. Ord a => a -> a -> Bool
<= Nat
m
Nat
n < :: Nat -> Nat -> Bool
< Nat
m = Bool -> Bool
not (Nat
m forall a. Ord a => a -> a -> Bool
<= Nat
n)
Nat
n > :: Nat -> Nat -> Bool
> Nat
m = Bool -> Bool
not (Nat
n forall a. Ord a => a -> a -> Bool
<= Nat
m)
Nat
n >= :: Nat -> Nat -> Bool
>= Nat
m = Nat
m forall a. Ord a => a -> a -> Bool
<= Nat
n
min :: Nat -> Nat -> Nat
min Nat
Z Nat
_ = Nat
Z
min (S Nat
_) Nat
Z = Nat
Z
min (S Nat
n) (S Nat
m) = Nat -> Nat
S (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 (forall a. Ord a => a -> a -> a
max Nat
n Nat
m)
instance Num Nat where
fromInteger :: Integer -> Nat
fromInteger = Natural -> Nat
fromNatural forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Num a => a -> a -> a
+ Nat
m)
Nat
Z * :: Nat -> Nat -> Nat
* Nat
_ = Nat
Z
S Nat
n * Nat
m = (Nat
n forall a. Num a => a -> a -> a
* Nat
m) forall a. Num a => a -> a -> a
+ Nat
m
abs :: Nat -> Nat
abs = 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
_ = forall a. HasCallStack => String -> a
error String
"negate @Nat"
instance Real Nat where
toRational :: Nat -> Rational
toRational = forall a. Real a => a -> Rational
toRational forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
instance Integral Nat where
toInteger :: Nat -> Integer
toInteger = forall a. a -> (a -> a) -> Nat -> a
cata Integer
0 forall a. Enum a => a -> a
succ
quotRem :: Nat -> Nat -> (Nat, Nat)
quotRem Nat
_ Nat
Z = forall a e. Exception e => e -> a
throw ArithException
DivideByZero
quotRem Nat
_ Nat
_ = forall a. HasCallStack => String -> a
error String
"quotRam @Nat un-implemented"
instance Enum Nat where
toEnum :: Int -> Nat
toEnum Int
n
| Int
n forall a. Ord a => a -> a -> Bool
< Int
0 = forall a e. Exception e => e -> a
throw ArithException
Underflow
| Bool
otherwise = forall a. (a -> a) -> a -> [a]
iterate Nat -> Nat
S Nat
Z forall a. [a] -> Int -> a
!! Int
n
fromEnum :: Nat -> Int
fromEnum = forall a. a -> (a -> a) -> Nat -> a
cata Int
0 forall a. Enum a => a -> a
succ
succ :: Nat -> Nat
succ = Nat -> Nat
S
pred :: Nat -> Nat
pred Nat
Z = 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) = forall a. NFData a => a -> ()
rnf Nat
n
instance Hashable Nat where
hashWithSalt :: Int -> Nat -> Int
hashWithSalt Int
salt = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
instance QC.Arbitrary Nat where
arbitrary :: Gen Nat
arbitrary = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Natural -> Nat
fromNatural forall a. Integral a => Gen a
QC.arbitrarySizedNatural
shrink :: Nat -> [Nat]
shrink Nat
Z = []
shrink (S Nat
n) = Nat
n forall a. a -> [a] -> [a]
: forall a. Arbitrary a => a -> [a]
QC.shrink Nat
n
instance QC.CoArbitrary Nat where
coarbitrary :: forall b. Nat -> Gen b -> Gen b
coarbitrary Nat
Z = forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
0 :: Int)
coarbitrary (S Nat
n) = forall n a. Integral n => n -> Gen a -> Gen a
QC.variant (Int
1 :: Int) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary Nat
n
instance QC.Function Nat where
function :: forall b. (Nat -> b) -> Nat :-> b
function = forall a b. Integral a => (a -> b) -> a :-> b
QC.functionIntegral
instance U.Universe Nat where
universe :: [Nat]
universe = Nat -> [Nat]
go Nat
Z where
go :: Nat -> [Nat]
go Nat
n = Nat
n forall a. a -> [a] -> [a]
: Nat -> [Nat]
go (Nat -> Nat
S Nat
n)
explicitShow :: Nat -> String
explicitShow :: Nat -> String
explicitShow Nat
n = Int -> Nat -> ShowS
explicitShowsPrec Int
0 Nat
n String
""
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 forall a. Ord a => a -> a -> Bool
> Int
10)
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"S "
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ShowS
explicitShowsPrec Int
11 Nat
n
cata :: a -> (a -> a) -> Nat -> a
cata :: forall a. 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)
toNatural :: Nat -> Natural
toNatural :: Nat -> Natural
toNatural Nat
Z = Natural
0
toNatural (S Nat
n) = forall a. Enum a => a -> a
succ (Nat -> Natural
toNatural Nat
n)
fromNatural :: Natural -> Nat
fromNatural :: Natural -> Nat
fromNatural Natural
0 = Nat
Z
fromNatural Natural
n = Nat -> Nat
S (Natural -> Nat
fromNatural (forall a. Enum a => a -> a
pred Natural
n))
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