{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE Safe #-}
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
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
/= :: Nat -> Nat -> Bool
Eq, Typeable, Typeable @(*) Nat
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 -> Constr
Nat -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Nat -> c Nat
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Nat
$ctoConstr :: Nat -> Constr
toConstr :: Nat -> Constr
$cdataTypeOf :: Nat -> DataType
dataTypeOf :: Nat -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable @(* -> *) t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable @(* -> *) t =>
(forall d. Data d => c (t d)) -> Maybe (c Nat)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable @(* -> * -> *) t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable @(* -> * -> *) t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Nat)
$cgmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
gmapT :: (forall b. Data b => b -> b) -> Nat -> Nat
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Nat -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Nat -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Nat -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Nat -> m Nat
Data)
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
_ = 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
n < :: Nat -> Nat -> Bool
< Nat
m = Bool -> Bool
not (Nat
m Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
n)
Nat
n > :: Nat -> Nat -> Bool
> Nat
m = Bool -> Bool
not (Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
m)
Nat
n >= :: Nat -> Nat -> Bool
>= Nat
m = Nat
m Nat -> Nat -> Bool
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 (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"
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. HasCallStack => [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
instance QC.Arbitrary Nat where
arbitrary :: Gen Nat
arbitrary = (Natural -> Nat) -> Gen Natural -> Gen Nat
forall a b. (a -> b) -> Gen a -> Gen b
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 :: forall b. 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
forall b. Nat -> Gen b -> Gen b
QC.coarbitrary Nat
n
instance QC.Function Nat where
function :: forall b. (Nat -> b) -> Nat :-> b
function = (Nat -> b) -> Nat :-> b
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 Nat -> [Nat] -> [Nat]
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 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
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) = Natural -> Natural
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 (Natural -> Natural
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