{-# 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 (Eq, Ord)

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

instance Show PositiveInteger where
  show (PositiveInteger n) = show n

instance Read PositiveInteger where
  readPrec = do
    n <- readPrec
    Monad.guard (n /= 0)
    pure $ PositiveInteger n

-- | Convert from a 'Natural' number, returning 'Nothing' if the input
--   is 0.
fromNatural :: Natural -> Maybe PositiveInteger
{-# INLINE fromNatural #-}
fromNatural n = if n == 0 then Nothing else Just (PositiveInteger 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 n =
  if n > 0
     then Just (PositiveInteger $ Prelude.fromIntegral n)
     else Nothing

-- | Cast a positive integer to a natural number.
toNatural :: PositiveInteger -> Natural
{-# INLINE toNatural #-}
toNatural (PositiveInteger n) = 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 (PositiveInteger n) = Prelude.fromIntegral 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 = PositiveInteger . 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 (PositiveInteger n) f =
  case someNatVal n of
    SomeNat proxy ->
      case cmpNat proxy (Proxy @0) of
        GTI -> f proxy
        -- This case should be impossible.
        _ -> error "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 _ = PositiveInteger $ 1 + natVal (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 (PositiveInteger n) f =
  case someNatVal $ n - 1 of
    SomeNat (_ :: Proxy n) -> f (Proxy @(1 + n))

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

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

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

-- | Subtract two positive integers. If the result wouldn't be positive,
--   'Nothing' is returned.
sub :: PositiveInteger -> PositiveInteger -> Maybe PositiveInteger
{-# INLINE sub #-}
sub (PositiveInteger n) (PositiveInteger m) =
  if n > m then Just $ PositiveInteger (n - m) else 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 n) (PositiveInteger m) =
  if m <= n then Just (PositiveInteger (Prelude.div n m)) else 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 = PositiveInteger . Prelude.fromIntegral . Prelude.length

-- | Take a positive number of elements from a non-empty list.
take :: PositiveInteger -> NonEmpty a -> NonEmpty a
take (PositiveInteger n) (x NonEmpty.:| xs) =
  x NonEmpty.:| Prelude.take (Prelude.fromIntegral $ n - 1) xs

-- | Produce a non-empty list with the same value repeated a given number of
--   times.
replicate :: PositiveInteger -> a -> NonEmpty a
{-# INLINE replicate #-}
replicate (PositiveInteger n) x =
  x NonEmpty.:| Prelude.replicate (Prelude.fromIntegral $ n - 1) 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 (PositiveInteger n) x =
  liftA2 (NonEmpty.:|) x $ Monad.replicateM (Prelude.fromIntegral $ n - 1) x