{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Provides the 'ModN' type for modular arithmetic.
--
-- @since 0.1
module Numeric.Data.ModN
  ( -- * Type
    ModN (MkModN),

    -- * Creation
    Internal.mkModN,
    mkModNTH,
    Internal.unsafeModN,
    Internal.reallyUnsafeModN,

    -- * Elimination
    unModN,

    -- * Optics
    -- $optics
    _MkModN,
    rmatching,
  )
where

import Data.Bounds (MaybeUpperBounded)
import Data.Typeable (Typeable)
import GHC.TypeNats (KnownNat)
import Language.Haskell.TH.Syntax (Code, Lift, Q)
import Numeric.Algebra (MEuclidean)
import Numeric.Convert.Integer (FromInteger, ToInteger)
import Numeric.Data.Internal.Utils (rmatching)
import Numeric.Data.Internal.Utils qualified as Utils
import Numeric.Data.ModN.Internal (ModN (MkModN, UnsafeModN))
import Numeric.Data.ModN.Internal qualified as Internal
import Optics.Core (ReversedPrism', prism, re)

-- $setup
-- >>> :set -XTemplateHaskell
-- >>> import Data.Int (Int8)
-- >>> import Numeric.Data.ModN.Internal (mkModN)

-- | @since 0.1
unModN :: ModN n a -> a
unModN :: forall (n :: Nat) a. ModN n a -> a
unModN (UnsafeModN a
x) = a
x
{-# INLINE unModN #-}

-- | Template haskell for creating a 'ModN' at compile-time.
--
-- ==== __Examples__
-- >>> $$(mkModNTH @11 7)
-- MkModN 7 (mod 11)
--
-- @since 0.1
mkModNTH ::
  forall n a.
  ( FromInteger a,
    Lift a,
    ToInteger a,
    KnownNat n,
    MaybeUpperBounded a,
    MEuclidean a,
    Typeable a
  ) =>
  a ->
  Code Q (ModN n a)
mkModNTH :: forall (n :: Nat) a.
(FromInteger a, Lift a, ToInteger a, KnownNat n,
 MaybeUpperBounded a, MEuclidean a, Typeable a) =>
a -> Code Q (ModN n a)
mkModNTH = Either String (ModN n a) -> Code Q (ModN n a)
forall a. Lift a => Either String a -> Code Q a
Utils.liftErrorTH (Either String (ModN n a) -> Code Q (ModN n a))
-> (a -> Either String (ModN n a)) -> a -> Code Q (ModN n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either String (ModN n a)
forall (n :: Nat) a.
(FromInteger a, ToInteger a, KnownNat n, MaybeUpperBounded a,
 MEuclidean a, Typeable a) =>
a -> Either String (ModN n a)
Internal.mkModN
{-# INLINEABLE mkModNTH #-}

-- $optics
-- We provide a 'ReversedPrism'' '_MkModN' that allows for total
-- elimination and partial construction, along with a 'Optics.Core.LabelOptic' 'Optics.Core.Getter'
-- for @#unModN@.
--
-- ==== __Examples__
--
-- >>> :set -XOverloadedLabels
-- >>> import Optics.Core (view)
-- >>> let n = $$(mkModNTH @7 9)
-- >>> view #unModN n
-- 2

-- | 'ReversedPrism'' that enables total elimination and partial construction.
--
-- ==== __Examples__
-- >>> import Optics.Core (view)
-- >>> n = $$(mkModNTH @7 9)
-- >>> view _MkModN n
-- 2
--
-- >>> rmatching (_MkModN @7) 9
-- Right (MkModN 2 (mod 7))
--
-- >>> rmatching (_MkModN @128) (9 :: Int8)
-- Left 9
--
-- @since 0.1
_MkModN ::
  forall n a.
  ( FromInteger a,
    ToInteger a,
    KnownNat n,
    MaybeUpperBounded a,
    MEuclidean a,
    Typeable a
  ) =>
  ReversedPrism' (ModN n a) a
_MkModN :: forall (n :: Nat) a.
(FromInteger a, ToInteger a, KnownNat n, MaybeUpperBounded a,
 MEuclidean a, Typeable a) =>
ReversedPrism' (ModN n a) a
_MkModN = Optic A_Prism NoIx a a (ModN n a) (ModN n a)
-> Optic (ReversedOptic A_Prism) NoIx (ModN n a) (ModN n a) a a
forall (is :: IxList) s t a b.
AcceptsEmptyIndices "re" is =>
Optic A_Prism is s t a b
-> Optic (ReversedOptic A_Prism) is b a t s
forall k (is :: IxList) s t a b.
(ReversibleOptic k, AcceptsEmptyIndices "re" is) =>
Optic k is s t a b -> Optic (ReversedOptic k) is b a t s
re ((ModN n a -> a)
-> (a -> Either a (ModN n a))
-> Optic A_Prism NoIx a a (ModN n a) (ModN n a)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism ModN n a -> a
forall (n :: Nat) a. ModN n a -> a
unModN a -> Either a (ModN n a)
forall {a} {n :: Nat}.
(FromInteger a, ToInteger a, KnownNat n, MaybeUpperBounded a,
 MEuclidean a, Typeable a) =>
a -> Either a (ModN n a)
g)
  where
    g :: a -> Either a (ModN n a)
g a
x = case a -> Either String (ModN n a)
forall (n :: Nat) a.
(FromInteger a, ToInteger a, KnownNat n, MaybeUpperBounded a,
 MEuclidean a, Typeable a) =>
a -> Either String (ModN n a)
Internal.mkModN a
x of
      Left String
_ -> a -> Either a (ModN n a)
forall a b. a -> Either a b
Left a
x
      Right ModN n a
x' -> ModN n a -> Either a (ModN n a)
forall a b. b -> Either a b
Right ModN n a
x'
{-# INLINEABLE _MkModN #-}