{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}

-- | This module provides a type for the positive integers, together
--   with conversion functions and other operations.
--
--   When an operation is partial (for example, subtraction), the result
--   has a 'Maybe' type, letting the user handle such case, without the
--   need for handling exceptions during evaluation.
--   As a result, 'PositiveInteger' is not an instance of the 'Num' class
--   or any of its subclasses. Functions are provided that offer similar
--   functionality.
--
--   It is recommended that you import this module qualified, as some of
--   the function names clash with those from the Prelude.
module Numeric.PositiveInteger
  ( PositiveInteger
  , one
    -- * Conversions
    -- ** To @PositiveInteger@
  , fromNatural
  , fromIntegral
    -- ** From @PositiveInteger@
  , toNatural
  , toNum
    -- ** Type-level conversions
  , fromTypeNat
  , withTypeNat
  , fromTypeNat1
  , withTypeNat1
    -- * Operations
  , next
  , add
  , sub
  , mul
  , div
    -- * Positive lengths
  , length
    -- * Non-empty lists
  , take
  , replicate
  , replicateM
    ) where

import Prelude hiding (fromIntegral, div, length, take, replicate)
import Prelude qualified
import Numeric.Natural (Natural)
import Text.Read (readPrec)
import Control.Monad qualified as Monad
import GHC.TypeNats (KnownNat, SomeNat (..), someNatVal, natVal, cmpNat, type (+))
import Data.Type.Ord (type (>), OrderingI (..))
import Data.Proxy (Proxy (..))

#if MIN_VERSION_base(4,18,0)
import Data.Foldable1 (Foldable1)
#else
import Control.Applicative (liftA2)
#endif

import Data.List.NonEmpty (NonEmpty)
import Data.List.NonEmpty qualified as NonEmpty

-- | Unbounded positive integers.
--
--   No 'Num' instance is provided, as no negative integers are available.
newtype PositiveInteger = PositiveInteger Natural deriving (PositiveInteger -> PositiveInteger -> Bool
(PositiveInteger -> PositiveInteger -> Bool)
-> (PositiveInteger -> PositiveInteger -> Bool)
-> Eq PositiveInteger
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PositiveInteger -> PositiveInteger -> Bool
== :: PositiveInteger -> PositiveInteger -> Bool
$c/= :: PositiveInteger -> PositiveInteger -> Bool
/= :: PositiveInteger -> PositiveInteger -> Bool
Eq, Eq PositiveInteger
Eq PositiveInteger =>
(PositiveInteger -> PositiveInteger -> Ordering)
-> (PositiveInteger -> PositiveInteger -> Bool)
-> (PositiveInteger -> PositiveInteger -> Bool)
-> (PositiveInteger -> PositiveInteger -> Bool)
-> (PositiveInteger -> PositiveInteger -> Bool)
-> (PositiveInteger -> PositiveInteger -> PositiveInteger)
-> (PositiveInteger -> PositiveInteger -> PositiveInteger)
-> Ord PositiveInteger
PositiveInteger -> PositiveInteger -> Bool
PositiveInteger -> PositiveInteger -> Ordering
PositiveInteger -> PositiveInteger -> PositiveInteger
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
$ccompare :: PositiveInteger -> PositiveInteger -> Ordering
compare :: PositiveInteger -> PositiveInteger -> Ordering
$c< :: PositiveInteger -> PositiveInteger -> Bool
< :: PositiveInteger -> PositiveInteger -> Bool
$c<= :: PositiveInteger -> PositiveInteger -> Bool
<= :: PositiveInteger -> PositiveInteger -> Bool
$c> :: PositiveInteger -> PositiveInteger -> Bool
> :: PositiveInteger -> PositiveInteger -> Bool
$c>= :: PositiveInteger -> PositiveInteger -> Bool
>= :: PositiveInteger -> PositiveInteger -> Bool
$cmax :: PositiveInteger -> PositiveInteger -> PositiveInteger
max :: PositiveInteger -> PositiveInteger -> PositiveInteger
$cmin :: PositiveInteger -> PositiveInteger -> PositiveInteger
min :: PositiveInteger -> PositiveInteger -> PositiveInteger
Ord)

-- | The number 1.
one :: PositiveInteger
{-# INLINE one #-}
one :: PositiveInteger
one = Natural -> PositiveInteger
PositiveInteger Natural
1

instance Show PositiveInteger where
  show :: PositiveInteger -> String
show (PositiveInteger Natural
n) = Natural -> String
forall a. Show a => a -> String
show Natural
n

instance Read PositiveInteger where
  readPrec :: ReadPrec PositiveInteger
readPrec = do
    Natural
n <- ReadPrec Natural
forall a. Read a => ReadPrec a
readPrec
    Bool -> ReadPrec ()
forall (f :: * -> *). Alternative f => Bool -> f ()
Monad.guard (Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
/= Natural
0)
    PositiveInteger -> ReadPrec PositiveInteger
forall a. a -> ReadPrec a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PositiveInteger -> ReadPrec PositiveInteger)
-> PositiveInteger -> ReadPrec PositiveInteger
forall a b. (a -> b) -> a -> b
$ Natural -> PositiveInteger
PositiveInteger Natural
n

-- | Convert from a 'Natural' number, returning 'Nothing' if the input
--   is 0.
fromNatural :: Natural -> Maybe PositiveInteger
{-# INLINE fromNatural #-}
fromNatural :: Natural -> Maybe PositiveInteger
fromNatural Natural
n = if Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 then Maybe PositiveInteger
forall a. Maybe a
Nothing else PositiveInteger -> Maybe PositiveInteger
forall a. a -> Maybe a
Just (Natural -> PositiveInteger
PositiveInteger Natural
n)

-- | Convert from a type that's instance of 'Integral'.
--   Similar to Prelude's 'Prelude.fromIntegral', but the result is
--   a 'Maybe', since the input might not be positive.
fromIntegral :: Integral a => a -> Maybe PositiveInteger
{-# INLINE fromIntegral #-}
fromIntegral :: forall a. Integral a => a -> Maybe PositiveInteger
fromIntegral a
n =
  if a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0
     then PositiveInteger -> Maybe PositiveInteger
forall a. a -> Maybe a
Just (Natural -> PositiveInteger
PositiveInteger (Natural -> PositiveInteger) -> Natural -> PositiveInteger
forall a b. (a -> b) -> a -> b
$ a -> Natural
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral a
n)
     else Maybe PositiveInteger
forall a. Maybe a
Nothing

-- | Cast a positive integer to a natural number.
toNatural :: PositiveInteger -> Natural
{-# INLINE toNatural #-}
toNatural :: PositiveInteger -> Natural
toNatural (PositiveInteger Natural
n) = Natural
n

-- | Convert a positive integer to any type instance of 'Num'.
--   This is equivalent to Prelude's 'Prelude.fromIntegral' when the input
--   type is 'PositiveInteger'.
toNum :: Num a => PositiveInteger -> a
{-# INLINE toNum #-}
toNum :: forall a. Num a => PositiveInteger -> a
toNum (PositiveInteger Natural
n) = Natural -> a
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral Natural
n

-- | Convert a type-level natural to a positive integer.
--   Equivalent to 'natVal' for positive integers.
--
-- @since 0.1.1.0
fromTypeNat :: (KnownNat n, n > 0) => proxy n -> PositiveInteger
{-# INLINE fromTypeNat #-}
fromTypeNat :: forall (n :: Natural) (proxy :: Natural -> *).
(KnownNat n, n > 0) =>
proxy n -> PositiveInteger
fromTypeNat = Natural -> PositiveInteger
PositiveInteger (Natural -> PositiveInteger)
-> (proxy n -> Natural) -> proxy n -> PositiveInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal

-- | Convert a positive integer to a type-level natural and apply
--   a function to it.
--
-- @since 0.1.1.0
withTypeNat :: PositiveInteger -> (forall proxy n . (KnownNat n, n > 0) => proxy n -> a) -> a
{-# INLINE withTypeNat #-}
withTypeNat :: forall a.
PositiveInteger
-> (forall (proxy :: Natural -> *) (n :: Natural).
    (KnownNat n, n > 0) =>
    proxy n -> a)
-> a
withTypeNat (PositiveInteger Natural
n) forall (proxy :: Natural -> *) (n :: Natural).
(KnownNat n, n > 0) =>
proxy n -> a
f =
  case Natural -> SomeNat
someNatVal Natural
n of
    SomeNat Proxy n
proxy ->
      case Proxy n -> Proxy 0 -> OrderingI n 0
forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat Proxy n
proxy (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @0) of
        OrderingI n 0
GTI -> Proxy n -> a
forall (proxy :: Natural -> *) (n :: Natural).
(KnownNat n, n > 0) =>
proxy n -> a
f Proxy n
proxy
        -- This case should be impossible.
        OrderingI n 0
_ -> String -> a
forall a. HasCallStack => String -> a
error String
"Positive integer is not positive!"

-- | Convert a type-level natural in @n + 1@ form to a positive integer.
--
-- @since 0.1.2.0
fromTypeNat1 :: forall proxy n . KnownNat n => proxy (1+n) -> PositiveInteger
fromTypeNat1 :: forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy (1 + n) -> PositiveInteger
fromTypeNat1 proxy (1 + n)
_ = Natural -> PositiveInteger
PositiveInteger (Natural -> PositiveInteger) -> Natural -> PositiveInteger
forall a b. (a -> b) -> a -> b
$ Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)

-- | Convert a positive integer to a type-level natural in @n + 1@ form
--   and apply a function to it.
--
-- @since 0.1.2.0
withTypeNat1 :: PositiveInteger -> (forall proxy n . KnownNat n => proxy (1 + n) -> a) -> a
withTypeNat1 :: forall a.
PositiveInteger
-> (forall (proxy :: Natural -> *) (n :: Natural).
    KnownNat n =>
    proxy (1 + n) -> a)
-> a
withTypeNat1 (PositiveInteger Natural
n) forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy (1 + n) -> a
f =
  case Natural -> SomeNat
someNatVal (Natural -> SomeNat) -> Natural -> SomeNat
forall a b. (a -> b) -> a -> b
$ Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 of
    SomeNat (Proxy n
_ :: Proxy n) -> Proxy (1 + n) -> a
forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy (1 + n) -> a
f (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(1 + n))

-- | Return the next positive integer.
next :: PositiveInteger -> PositiveInteger
{-# INLINE next #-}
next :: PositiveInteger -> PositiveInteger
next (PositiveInteger Natural
n) = Natural -> PositiveInteger
PositiveInteger (Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
1)

-- | Add two positive integers.
add :: PositiveInteger -> PositiveInteger -> PositiveInteger
{-# INLINE add #-}
add :: PositiveInteger -> PositiveInteger -> PositiveInteger
add (PositiveInteger Natural
n) (PositiveInteger Natural
m) = Natural -> PositiveInteger
PositiveInteger (Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
+Natural
m)

-- | Multiply two positive integers.
mul :: PositiveInteger -> PositiveInteger -> PositiveInteger
{-# INLINE mul #-}
mul :: PositiveInteger -> PositiveInteger -> PositiveInteger
mul (PositiveInteger Natural
n) (PositiveInteger Natural
m) = Natural -> PositiveInteger
PositiveInteger (Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
*Natural
m)

-- | Subtract two positive integers. If the result wouldn't be positive,
--   'Nothing' is returned.
sub :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
{-# INLINE sub #-}
sub :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
sub (PositiveInteger Natural
n) (PositiveInteger Natural
m) =
  if Natural
n Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
m then PositiveInteger -> Maybe PositiveInteger
forall a. a -> Maybe a
Just (PositiveInteger -> Maybe PositiveInteger)
-> PositiveInteger -> Maybe PositiveInteger
forall a b. (a -> b) -> a -> b
$ Natural -> PositiveInteger
PositiveInteger (Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
m) else Maybe PositiveInteger
forall a. Maybe a
Nothing

-- | Divide a positive integer by another. If the divisor is larger than
--   the dividend, 'Nothing' is returned.
div :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
{-# INLINE div #-}
div :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
div (PositiveInteger Natural
n) (PositiveInteger Natural
m) =
  if Natural
m Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
n then PositiveInteger -> Maybe PositiveInteger
forall a. a -> Maybe a
Just (Natural -> PositiveInteger
PositiveInteger (Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
Prelude.div Natural
n Natural
m)) else Maybe PositiveInteger
forall a. Maybe a
Nothing

{-

Starting on base-4.18.0.0, the type class Foldable1 becomes available.
This allows us to generalize the type of length.

-}

#if MIN_VERSION_base(4,18,0)
-- | Length of a non-empty data structure.
length :: Foldable1 t => t a -> PositiveInteger
#else
-- | Lenght of a non-empty list.
length :: NonEmpty a -> PositiveInteger
#endif
{-# INLINE length #-}
length :: forall (t :: * -> *) a. Foldable1 t => t a -> PositiveInteger
length = Natural -> PositiveInteger
PositiveInteger (Natural -> PositiveInteger)
-> (t a -> Natural) -> t a -> PositiveInteger
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Int -> Natural) -> (t a -> Int) -> t a -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
Prelude.length

-- | Take a positive number of elements from a non-empty list.
take :: PositiveInteger -> NonEmpty a -> NonEmpty a
take :: forall a. PositiveInteger -> NonEmpty a -> NonEmpty a
take (PositiveInteger Natural
n) (a
x NonEmpty.:| [a]
xs) =
  a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
NonEmpty.:| Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
Prelude.take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) [a]
xs

-- | Produce a non-empty list with the same value repeated a given number of
--   times.
replicate :: PositiveInteger -> a -> NonEmpty a
{-# INLINE replicate #-}
replicate :: forall a. PositiveInteger -> a -> NonEmpty a
replicate (PositiveInteger Natural
n) a
x =
  a
x a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
NonEmpty.:| Int -> a -> [a]
forall a. Int -> a -> [a]
Prelude.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) a
x

-- | Repeat an action a given number of times and collect the
--   results in a non-empty list.
replicateM :: Applicative f => PositiveInteger -> f a -> f (NonEmpty a)
{-# INLINE replicateM #-}
replicateM :: forall (f :: * -> *) a.
Applicative f =>
PositiveInteger -> f a -> f (NonEmpty a)
replicateM (PositiveInteger Natural
n) f a
x =
  (a -> [a] -> NonEmpty a) -> f a -> f [a] -> f (NonEmpty a)
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
(NonEmpty.:|) f a
x (f [a] -> f (NonEmpty a)) -> f [a] -> f (NonEmpty a)
forall a b. (a -> b) -> a -> b
$ Int -> f a -> f [a]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
Monad.replicateM (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
Prelude.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) f a
x