--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Finite.Internal.Integral
-- Copyright   :  (C) 2015-2024 mniip
-- License     :  BSD3
-- Maintainer  :  mniip <mniip@mniip.com>
-- Stability   :  experimental
-- Portability :  portable
--------------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}
#endif
module Data.Finite.Internal.Integral
    (
        SaneIntegral(..), Limited, KnownIntegral, intVal,
        withIntegral, withLimited,
        Finite(Finite), finite, getFinite
    )
    where

#if MIN_VERSION_base(4,8,0)
import Numeric.Natural
#endif
import Control.DeepSeq
import Control.Monad
import Data.Ix
import Data.Int
import Data.Proxy
import Data.Tagged
import Data.Type.Equality
import Data.Word
import GHC.Exts
import GHC.Read
import GHC.TypeLits
import Language.Haskell.TH.Lib
import Text.ParserCombinators.ReadPrec
import Text.Read.Lex
import Unsafe.Coerce

#include "MachDeps.h"

-- | A class of datatypes that faithfully represent a sub-range of 'Integer'
-- that includes @0@. A valid instance must obey the following laws:
--
-- 'fromInteger' must be a retract of 'toInteger':
--
-- prop> fromInteger (toInteger a) == a
--
-- Restricted to the range @[0, 'Limit']@ (with 'Nothing' understood as positive
-- infinity), 'fromInteger' must be an inverse of 'toInteger':
--
-- prop> limited i ==> toInteger (fromInteger i) == i
-- where:
--
-- > limited i = case limit of
-- >     Just l -> 0 <= i && i <= l
-- >     Nothing -> 0 <= i
--
-- __WARNING__: violating the above constraint in particular breaks type safety.
--
-- The implementations of 'Ord', 'Enum', 'Num', 'Integral' must be compatible
-- with that of 'Integer', whenever all arguments and results fall within
-- @[0, 'Limit']@, for example:
--
-- prop> limited i && limited j && limited k && (i * j == k) ==> (fromInteger i * fromInteger j == fromInteger k)
--
-- Methods 'modAdd', 'modSub', and 'modMul' implement modular addition,
-- multiplication, and subtraction. The default implementation is via 'Integer',
-- but a faster implementation can be provided instead. If provided, the
-- implementation must be correct for moduli in range @[1, 'Limit']@.
--
-- __WARNING:__ a naive implementaton is prone to arithmetic overflow and may
-- produce invalid results for moduli close to 'Limit'.
class Integral a => SaneIntegral a where
    type Limit a :: Maybe Nat
    -- | Given @n > 0@, @0 <= a < n@, and @0 <= b < n@, @'modAdd' n a b@
    -- computes @(a 'Prelude.+' b) \` 'mod' \` n@.
    modAdd :: a -> a -> a -> a
    modAdd a
n a
a a
b = Integer -> a
forall a. Num a => Integer -> a
fromInteger
        (Integer -> Integer -> Integer -> Integer
forall a. SaneIntegral a => a -> a -> a -> a
modAdd (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
b) :: Integer)
    -- | Given @n > 0@, @0 <= a < n@, and @0 <= b < n@, @'modSub' n a b@
    -- computes @(a 'Prelude.-' b) \` 'mod' \` n@.
    modSub :: a -> a -> a -> a
    modSub a
n a
a a
b = Integer -> a
forall a. Num a => Integer -> a
fromInteger
        (Integer -> Integer -> Integer -> Integer
forall a. SaneIntegral a => a -> a -> a -> a
modSub (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
b) :: Integer)
    -- | Given @n > 0@, @0 <= a < n@, and @0 <= b < n@, @'modMul' n a b@
    -- computes @(a 'Prelude.*' b) \` 'mod' \` n@.
    modMul :: a -> a -> a -> a
    modMul a
n a
a a
b = Integer -> a
forall a. Num a => Integer -> a
fromInteger
        (Integer -> Integer -> Integer -> Integer
forall a. SaneIntegral a => a -> a -> a -> a
modMul (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
a) (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
b) :: Integer)

    -- | Unsafely obtain evidence that @n <= Limit a@. When 'Limit' is 'Nothing'
    -- there is no evidence to obtain, and @\\_ _ k -> k@ is a valid
    -- implementation. When 'Limit' is a 'Just', the default implementation
    -- should work.
    unsafeWithLimited :: proxy1 a -> proxy2 n -> (Limited a n => r) -> r
    default unsafeWithLimited
        :: forall n r lim proxy1 proxy2. (Limit a ~ 'Just lim)
        => proxy1 a -> proxy2 n -> (Limited a n => r) -> r
    unsafeWithLimited proxy1 a
_ proxy2 n
_ Limited a n => r
k = case (Any :~: Any)
-> OrdCond (CmpNat n lim) 'True 'True 'False :~: 'True
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (n <=? lim) :~: 'True of
        OrdCond (Compare n lim) 'True 'True 'False :~: 'True
Refl -> r
Limited a n => r
k

instance SaneIntegral Integer where
    type Limit Integer = 'Nothing
    modAdd :: Integer -> Integer -> Integer -> Integer
modAdd Integer
n Integer
a Integer
b = case Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b of
        Integer
r | Integer
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
n -> Integer
r Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
n
        Integer
r -> Integer
r
    modSub :: Integer -> Integer -> Integer -> Integer
modSub Integer
n Integer
a Integer
b = if Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
b then Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b else Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
a
    modMul :: Integer -> Integer -> Integer -> Integer
modMul Integer
n Integer
a Integer
b = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
b) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
n
    unsafeWithLimited :: forall (proxy1 :: * -> *) (proxy2 :: Natural -> *) (n :: Natural)
       r.
proxy1 Integer -> proxy2 n -> (Limited Integer n => r) -> r
unsafeWithLimited proxy1 Integer
_ proxy2 n
_ Limited Integer n => r
k = r
Limited Integer n => r
k

#if MIN_VERSION_base(4,8,0)
instance SaneIntegral Natural where
    type Limit Natural = 'Nothing
    modAdd :: Natural -> Natural -> Natural -> Natural
modAdd Natural
n Natural
a Natural
b = case Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
b of
        Natural
r | Natural
r Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
n -> Natural
r Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
n
        Natural
r -> Natural
r
    modSub :: Natural -> Natural -> Natural -> Natural
modSub Natural
n Natural
a Natural
b = if Natural
a Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
b then Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
b else Natural
n Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
b Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
a
    modMul :: Natural -> Natural -> Natural -> Natural
modMul Natural
n Natural
a Natural
b = (Natural
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Natural
b) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
n
    unsafeWithLimited :: forall (proxy1 :: * -> *) (proxy2 :: Natural -> *) (n :: Natural)
       r.
proxy1 Natural -> proxy2 n -> (Limited Natural n => r) -> r
unsafeWithLimited proxy1 Natural
_ proxy2 n
_ Limited Natural n => r
k = r
Limited Natural n => r
k
#endif

instance SaneIntegral Word where
    type Limit Word = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word))

    modAdd :: Word -> Word -> Word -> Word
modAdd (W# Word#
n) (W# Word#
a) (W# Word#
b) = Word# -> Word
W# (case Word# -> Word# -> (# Word#, Word# #)
plusWord2# Word#
a Word#
b of
        (# Word#
0##, Word#
r #) | Int# -> Bool
isTrue# (Word# -> Word# -> Int#
ltWord# Word#
r Word#
n) -> Word#
r
        (# Word#
_, Word#
r #) -> Word# -> Word# -> Word#
minusWord# Word#
r Word#
n)

    modSub :: Word -> Word -> Word -> Word
modSub (W# Word#
n) (W# Word#
a) (W# Word#
b) = Word# -> Word
W# (if Int# -> Bool
isTrue# (Word# -> Word# -> Int#
leWord# Word#
b Word#
a)
        then Word# -> Word# -> Word#
minusWord# Word#
a Word#
b
        else Word# -> Word# -> Word#
plusWord# (Word# -> Word# -> Word#
minusWord# Word#
n Word#
b) Word#
a)

    modMul :: Word -> Word -> Word -> Word
modMul (W# Word#
n) (W# Word#
a) (W# Word#
b) = Word# -> Word
W# (case Word#
n of
        Word#
0## -> [Char] -> Word#
forall a. HasCallStack => [Char] -> a
error [Char]
"modMul: division by zero"
        Word#
_ -> case Word# -> Word# -> (# Word#, Word# #)
timesWord2# Word#
a Word#
b of
            (# Word#
h, Word#
l #) -> case Word# -> Word# -> Word# -> (# Word#, Word# #)
quotRemWord2# Word#
h Word#
l Word#
n of
                (# Word#
_, Word#
r #) -> Word#
r)

modAddViaWord :: (Num a, Integral a) => a -> a -> a -> a
modAddViaWord :: forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord a
n a
a a
b = Word -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    (Word -> Word -> Word -> Word
forall a. SaneIntegral a => a -> a -> a -> a
modAdd (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n) (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
b) :: Word)

modSubViaWord :: (Num a, Integral a) => a -> a -> a -> a
modSubViaWord :: forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord a
n a
a a
b = Word -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    (Word -> Word -> Word -> Word
forall a. SaneIntegral a => a -> a -> a -> a
modSub (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n) (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
b) :: Word)

modMulViaWord :: (Num a, Integral a) => a -> a -> a -> a
modMulViaWord :: forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord a
n a
a a
b = Word -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral
    (Word -> Word -> Word -> Word
forall a. SaneIntegral a => a -> a -> a -> a
modMul (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n) (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (a -> Word
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
b) :: Word)

instance SaneIntegral Int where
    type Limit Int = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int))
    modAdd :: Int -> Int -> Int -> Int
modAdd = Int -> Int -> Int -> Int
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Int -> Int -> Int -> Int
modSub = Int -> Int -> Int -> Int
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Int -> Int -> Int -> Int
modMul = Int -> Int -> Int -> Int
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord

instance SaneIntegral Word8 where
    type Limit Word8
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word8))
    modAdd :: Word8 -> Word8 -> Word8 -> Word8
modAdd = Word8 -> Word8 -> Word8 -> Word8
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Word8 -> Word8 -> Word8 -> Word8
modSub = Word8 -> Word8 -> Word8 -> Word8
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Word8 -> Word8 -> Word8 -> Word8
modMul = Word8 -> Word8 -> Word8 -> Word8
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord

instance SaneIntegral Int8 where
    type Limit Int8
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int8))
    modAdd :: Int8 -> Int8 -> Int8 -> Int8
modAdd = Int8 -> Int8 -> Int8 -> Int8
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Int8 -> Int8 -> Int8 -> Int8
modSub = Int8 -> Int8 -> Int8 -> Int8
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Int8 -> Int8 -> Int8 -> Int8
modMul = Int8 -> Int8 -> Int8 -> Int8
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord

instance SaneIntegral Word16 where
    type Limit Word16
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word16))
    modAdd :: Word16 -> Word16 -> Word16 -> Word16
modAdd = Word16 -> Word16 -> Word16 -> Word16
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Word16 -> Word16 -> Word16 -> Word16
modSub = Word16 -> Word16 -> Word16 -> Word16
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Word16 -> Word16 -> Word16 -> Word16
modMul = Word16 -> Word16 -> Word16 -> Word16
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord

instance SaneIntegral Int16 where
    type Limit Int16
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int16))
    modAdd :: Int16 -> Int16 -> Int16 -> Int16
modAdd = Int16 -> Int16 -> Int16 -> Int16
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Int16 -> Int16 -> Int16 -> Int16
modSub = Int16 -> Int16 -> Int16 -> Int16
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Int16 -> Int16 -> Int16 -> Int16
modMul = Int16 -> Int16 -> Int16 -> Int16
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord

instance SaneIntegral Word32 where
    type Limit Word32
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word32))
#if WORD_SIZE_IN_BITS >= 32
    modAdd :: Word32 -> Word32 -> Word32 -> Word32
modAdd = Word32 -> Word32 -> Word32 -> Word32
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Word32 -> Word32 -> Word32 -> Word32
modSub = Word32 -> Word32 -> Word32 -> Word32
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Word32 -> Word32 -> Word32 -> Word32
modMul = Word32 -> Word32 -> Word32 -> Word32
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord
#endif

instance SaneIntegral Int32 where
    type Limit Int32
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int32))
#if WORD_SIZE_IN_BITS >= 32
    modAdd :: Int32 -> Int32 -> Int32 -> Int32
modAdd = Int32 -> Int32 -> Int32 -> Int32
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Int32 -> Int32 -> Int32 -> Int32
modSub = Int32 -> Int32 -> Int32 -> Int32
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Int32 -> Int32 -> Int32 -> Int32
modMul = Int32 -> Int32 -> Int32 -> Int32
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord
#endif

instance SaneIntegral Word64 where
    type Limit Word64
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Word64))
#if WORD_SIZE_IN_BITS >= 64
    modAdd :: Word64 -> Word64 -> Word64 -> Word64
modAdd = Word64 -> Word64 -> Word64 -> Word64
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Word64 -> Word64 -> Word64 -> Word64
modSub = Word64 -> Word64 -> Word64 -> Word64
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Word64 -> Word64 -> Word64 -> Word64
modMul = Word64 -> Word64 -> Word64 -> Word64
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord
#endif

instance SaneIntegral Int64 where
    type Limit Int64
        = 'Just $(litT $ numTyLit $ toInteger (maxBound :: Int64))
#if WORD_SIZE_IN_BITS >= 64
    modAdd :: Int64 -> Int64 -> Int64 -> Int64
modAdd = Int64 -> Int64 -> Int64 -> Int64
forall a. (Num a, Integral a) => a -> a -> a -> a
modAddViaWord
    modSub :: Int64 -> Int64 -> Int64 -> Int64
modSub = Int64 -> Int64 -> Int64 -> Int64
forall a. (Num a, Integral a) => a -> a -> a -> a
modSubViaWord
    modMul :: Int64 -> Int64 -> Int64 -> Int64
modMul = Int64 -> Int64 -> Int64 -> Int64
forall a. (Num a, Integral a) => a -> a -> a -> a
modMulViaWord
#endif

class LeqMaybe (n :: Nat) (c :: Maybe Nat)
instance LeqMaybe n 'Nothing
instance n <= m => LeqMaybe n ('Just m)

-- | Ensures that the value of @n@ is representable in type @a@ (which should be
-- a 'SaneIntegral').
type Limited a (n :: Nat) = LeqMaybe n (Limit a)

-- | This class asserts that the value of @n@ is known at runtime, and that it
-- is representable in type @a@ (which should be a 'SaneIntegral').
--
-- At runtime it acts like an implicit parameter of type @a@, much like
-- 'KnownNat' is an implicit parameter of type 'Integer'.
class KnownIntegral a (n :: Nat) where
    intVal_ :: Tagged n a

instance (SaneIntegral a, Limited a n, KnownNat n) => KnownIntegral a n where
    intVal_ :: Tagged n a
intVal_ = a -> Tagged n a
forall {k} (s :: k) b. b -> Tagged s b
Tagged (a -> Tagged n a) -> a -> Tagged n a
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> Integer -> a
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

-- | Reflect a type-level number into a term.
intVal :: forall n a proxy. KnownIntegral a n => proxy n -> a
intVal :: forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal proxy n
_ = Tagged n a -> a
forall {k} (s :: k) b. Tagged s b -> b
unTagged (Tagged n a
forall a (n :: Natural). KnownIntegral a n => Tagged n a
intVal_ :: Tagged n a)
{-# INLINABLE intVal #-}

-- | Recover a 'KnownNat' constraint from a 'KnownIntegral' constraint.
withIntegral
    :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)
    => proxy1 a -> proxy2 n -> (KnownNat n => r) -> r
withIntegral :: forall a (n :: Natural) r (proxy1 :: * -> *)
       (proxy2 :: Natural -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy1 a -> proxy2 n -> (KnownNat n => r) -> r
withIntegral proxy1 a
_ proxy2 n
_ KnownNat n => r
k = case Integer -> Maybe SomeNat
someNatVal Integer
n of
    Maybe SomeNat
Nothing -> [Char] -> r
forall a. HasCallStack => [Char] -> a
error ([Char] -> r) -> [Char] -> r
forall a b. (a -> b) -> a -> b
$ [Char]
"withIntegral: got KnownIntegral instance dictionary "
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for which toInteger returns " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n
    Just (SomeNat (Proxy n
_ :: Proxy m)) -> case (Any :~: Any) -> n :~: n
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: n :~: m of
        n :~: n
Refl -> r
KnownNat n => r
k
    where n :: Integer
n = Tagged n a -> Integer
forall a. Integral a => a -> Integer
toInteger (Tagged n a -> Integer) -> Tagged n a -> Integer
forall a b. (a -> b) -> a -> b
$ (Tagged n a
forall a (n :: Natural). KnownIntegral a n => Tagged n a
intVal_  :: Tagged n a)
{-# INLINABLE withIntegral #-}

-- | Recover a 'Limited' constraint from a 'KnownIntegral' constraint.
withLimited
    :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n)
    => proxy1 a -> proxy2 n -> (Limited a n => r) -> r
withLimited :: forall a (n :: Natural) r (proxy1 :: * -> *)
       (proxy2 :: Natural -> *).
(SaneIntegral a, KnownIntegral a n) =>
proxy1 a -> proxy2 n -> (Limited a n => r) -> r
withLimited = proxy1 a -> proxy2 n -> (Limited a n => r) -> r
forall a (proxy1 :: * -> *) (proxy2 :: Natural -> *) (n :: Natural)
       r.
SaneIntegral a =>
proxy1 a -> proxy2 n -> (Limited a n => r) -> r
forall (proxy1 :: * -> *) (proxy2 :: Natural -> *) (n :: Natural)
       r.
proxy1 a -> proxy2 n -> (Limited a n => r) -> r
unsafeWithLimited
  where _n :: Tagged n a
_n = Tagged n a
forall a (n :: Natural). KnownIntegral a n => Tagged n a
intVal_ :: Tagged n a
{-# INLINABLE withLimited #-}

-- | Finite number type. The type @'Finite' a n@ is inhabited by exactly @n@
-- values from type @a@, in the range @[0, n)@ including @0@ but excluding @n@.
-- @a@ must be an instance of 'SaneIntegral' to use this type. Invariants:
--
-- prop> getFinite x < intVal x
-- prop> getFinite x >= 0
newtype Finite a (n :: Nat) = Finite a
    deriving (Finite a n -> Finite a n -> Bool
(Finite a n -> Finite a n -> Bool)
-> (Finite a n -> Finite a n -> Bool) -> Eq (Finite a n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a (n :: Natural). Eq a => Finite a n -> Finite a n -> Bool
$c== :: forall a (n :: Natural). Eq a => Finite a n -> Finite a n -> Bool
== :: Finite a n -> Finite a n -> Bool
$c/= :: forall a (n :: Natural). Eq a => Finite a n -> Finite a n -> Bool
/= :: Finite a n -> Finite a n -> Bool
Eq, Eq (Finite a n)
Eq (Finite a n) =>
(Finite a n -> Finite a n -> Ordering)
-> (Finite a n -> Finite a n -> Bool)
-> (Finite a n -> Finite a n -> Bool)
-> (Finite a n -> Finite a n -> Bool)
-> (Finite a n -> Finite a n -> Bool)
-> (Finite a n -> Finite a n -> Finite a n)
-> (Finite a n -> Finite a n -> Finite a n)
-> Ord (Finite a n)
Finite a n -> Finite a n -> Bool
Finite a n -> Finite a n -> Ordering
Finite a n -> Finite a n -> Finite a n
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
forall a (n :: Natural). Ord a => Eq (Finite a n)
forall a (n :: Natural). Ord a => Finite a n -> Finite a n -> Bool
forall a (n :: Natural).
Ord a =>
Finite a n -> Finite a n -> Ordering
forall a (n :: Natural).
Ord a =>
Finite a n -> Finite a n -> Finite a n
$ccompare :: forall a (n :: Natural).
Ord a =>
Finite a n -> Finite a n -> Ordering
compare :: Finite a n -> Finite a n -> Ordering
$c< :: forall a (n :: Natural). Ord a => Finite a n -> Finite a n -> Bool
< :: Finite a n -> Finite a n -> Bool
$c<= :: forall a (n :: Natural). Ord a => Finite a n -> Finite a n -> Bool
<= :: Finite a n -> Finite a n -> Bool
$c> :: forall a (n :: Natural). Ord a => Finite a n -> Finite a n -> Bool
> :: Finite a n -> Finite a n -> Bool
$c>= :: forall a (n :: Natural). Ord a => Finite a n -> Finite a n -> Bool
>= :: Finite a n -> Finite a n -> Bool
$cmax :: forall a (n :: Natural).
Ord a =>
Finite a n -> Finite a n -> Finite a n
max :: Finite a n -> Finite a n -> Finite a n
$cmin :: forall a (n :: Natural).
Ord a =>
Finite a n -> Finite a n -> Finite a n
min :: Finite a n -> Finite a n -> Finite a n
Ord, Ord (Finite a n)
Ord (Finite a n) =>
((Finite a n, Finite a n) -> [Finite a n])
-> ((Finite a n, Finite a n) -> Finite a n -> Int)
-> ((Finite a n, Finite a n) -> Finite a n -> Int)
-> ((Finite a n, Finite a n) -> Finite a n -> Bool)
-> ((Finite a n, Finite a n) -> Int)
-> ((Finite a n, Finite a n) -> Int)
-> Ix (Finite a n)
(Finite a n, Finite a n) -> Int
(Finite a n, Finite a n) -> [Finite a n]
(Finite a n, Finite a n) -> Finite a n -> Bool
(Finite a n, Finite a n) -> Finite a n -> Int
forall a.
Ord a =>
((a, a) -> [a])
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Int)
-> ((a, a) -> a -> Bool)
-> ((a, a) -> Int)
-> ((a, a) -> Int)
-> Ix a
forall a (n :: Natural). Ix a => Ord (Finite a n)
forall a (n :: Natural). Ix a => (Finite a n, Finite a n) -> Int
forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> [Finite a n]
forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> Finite a n -> Bool
forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> Finite a n -> Int
$crange :: forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> [Finite a n]
range :: (Finite a n, Finite a n) -> [Finite a n]
$cindex :: forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> Finite a n -> Int
index :: (Finite a n, Finite a n) -> Finite a n -> Int
$cunsafeIndex :: forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> Finite a n -> Int
unsafeIndex :: (Finite a n, Finite a n) -> Finite a n -> Int
$cinRange :: forall a (n :: Natural).
Ix a =>
(Finite a n, Finite a n) -> Finite a n -> Bool
inRange :: (Finite a n, Finite a n) -> Finite a n -> Bool
$crangeSize :: forall a (n :: Natural). Ix a => (Finite a n, Finite a n) -> Int
rangeSize :: (Finite a n, Finite a n) -> Int
$cunsafeRangeSize :: forall a (n :: Natural). Ix a => (Finite a n, Finite a n) -> Int
unsafeRangeSize :: (Finite a n, Finite a n) -> Int
Ix)

type role Finite nominal nominal

-- | Convert an @a@ into a @'Finite' a@, throwing an error if the input is out
-- of bounds.
finite :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Finite a n
finite :: forall (n :: Natural) a.
(SaneIntegral a, KnownIntegral a n) =>
a -> Finite a n
finite a
x
    | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
x
    | Bool
otherwise = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Finite a n) -> [Char] -> Finite a n
forall a b. (a -> b) -> a -> b
$ [Char]
"finite: Integral " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x)
        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not representable in Finite _ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
    where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# INLINABLE finite #-}

-- | Convert a @'Finite' a@ into the corresponding @a@.
getFinite :: forall n a. Finite a n -> a
getFinite :: forall (n :: Natural) a. Finite a n -> a
getFinite (Finite a
x) = a
x
{-# INLINABLE getFinite #-}

-- | Throws an error for @'Finite' _ 0@
instance (SaneIntegral a, KnownIntegral a n) => Bounded (Finite a n) where
    {-# SPECIALIZE instance KnownNat n => Bounded (Finite Integer n) #-}
#if MIN_VERSION_base(4,8,0)
    {-# SPECIALIZE instance KnownNat n => Bounded (Finite Natural n) #-}
#endif
    {-# SPECIALIZE instance KnownIntegral Word n => Bounded (Finite Word n) #-}
    {-# SPECIALIZE instance KnownIntegral Int n => Bounded (Finite Int n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word8 n => Bounded (Finite Word8 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int8 n => Bounded (Finite Int8 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word16 n => Bounded (Finite Word16 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int16 n => Bounded (Finite Int16 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word32 n => Bounded (Finite Word32 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int32 n => Bounded (Finite Int32 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word64 n => Bounded (Finite Word64 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int64 n => Bounded (Finite Int64 n) #-}
    maxBound :: Finite a n
maxBound
        | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1
        | Bool
otherwise = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error [Char]
"maxBound: Finite _ 0 is uninhabited"
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) :: a
    minBound :: Finite a n
minBound
        | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
0 = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
0
        | Bool
otherwise = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error [Char]
"minBound: Finite _ 0 is uninhabited"
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) :: a

instance (SaneIntegral a, KnownIntegral a n) => Enum (Finite a n) where
    {-# SPECIALIZE instance KnownNat n => Enum (Finite Integer n) #-}
#if MIN_VERSION_base(4,8,0)
    {-# SPECIALIZE instance KnownNat n => Enum (Finite Natural n) #-}
#endif
    {-# SPECIALIZE instance KnownIntegral Word n => Enum (Finite Word n) #-}
    {-# SPECIALIZE instance KnownIntegral Int n => Enum (Finite Int n) #-}
    {-# SPECIALIZE instance KnownIntegral Word8 n => Enum (Finite Word8 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int8 n => Enum (Finite Int8 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word16 n => Enum (Finite Word16 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int16 n => Enum (Finite Int16 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word32 n => Enum (Finite Word32 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int32 n => Enum (Finite Int32 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word64 n => Enum (Finite Word64 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int64 n => Enum (Finite Int64 n) #-}
    succ :: Finite a n -> Finite a n
succ (Finite a
x)
        | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1 = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error [Char]
"succ: bad argument"
        | Bool
otherwise = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
succ a
x
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    pred :: Finite a n -> Finite a n
pred (Finite a
x)
        | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error [Char]
"pred: bad argument"
        | Bool
otherwise = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Enum a => a -> a
pred a
x
    fromEnum :: Finite a n -> Int
fromEnum = a -> Int
forall a. Enum a => a -> Int
fromEnum (a -> Int) -> (Finite a n -> a) -> Finite a n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite a n -> a
forall (n :: Natural) a. Finite a n -> a
getFinite
    toEnum :: Int -> Finite a n
toEnum Int
x
        | Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
x
        | Bool
otherwise = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Finite a n) -> [Char] -> Finite a n
forall a b. (a -> b) -> a -> b
$ [Char]
"toEnum: Int " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
x
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not representable in Finite _ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) :: a
    enumFrom :: Finite a n -> [Finite a n]
enumFrom Finite a n
x = Finite a n -> Finite a n -> [Finite a n]
forall a. Enum a => a -> a -> [a]
enumFromTo Finite a n
x Finite a n
forall a. Bounded a => a
maxBound
    enumFromTo :: Finite a n -> Finite a n -> [Finite a n]
enumFromTo (Finite a
x) (Finite a
y) = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> [a] -> [Finite a n]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` a -> a -> [a]
forall a. Enum a => a -> a -> [a]
enumFromTo a
x a
y
    enumFromThen :: Finite a n -> Finite a n -> [Finite a n]
enumFromThen Finite a n
x Finite a n
y
        = Finite a n -> Finite a n -> Finite a n -> [Finite a n]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Finite a n
x Finite a n
y (if Finite a n
x Finite a n -> Finite a n -> Bool
forall a. Ord a => a -> a -> Bool
>= Finite a n
y then Finite a n
forall a. Bounded a => a
minBound else Finite a n
forall a. Bounded a => a
maxBound)
    enumFromThenTo :: Finite a n -> Finite a n -> Finite a n -> [Finite a n]
enumFromThenTo (Finite a
x) (Finite a
y) (Finite a
z)
        = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> [a] -> [Finite a n]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` a -> a -> a -> [a]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo a
x a
y a
z

instance Show a => Show (Finite a n) where
    showsPrec :: Int -> Finite a n -> [Char] -> [Char]
showsPrec Int
d (Finite a
x)
        = Bool -> ([Char] -> [Char]) -> [Char] -> [Char]
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (([Char] -> [Char]) -> [Char] -> [Char])
-> ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
showString [Char]
"finite " ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
10 a
x

instance (Read a, SaneIntegral a, KnownIntegral a n) => Read (Finite a n) where
    readPrec :: ReadPrec (Finite a n)
readPrec = ReadPrec (Finite a n) -> ReadPrec (Finite a n)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (Finite a n) -> ReadPrec (Finite a n))
-> ReadPrec (Finite a n) -> ReadPrec (Finite a n)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (Finite a n) -> ReadPrec (Finite a n)
forall a. Int -> ReadPrec a -> ReadPrec a
Text.ParserCombinators.ReadPrec.prec Int
10 (ReadPrec (Finite a n) -> ReadPrec (Finite a n))
-> ReadPrec (Finite a n) -> ReadPrec (Finite a n)
forall a b. (a -> b) -> a -> b
$ do
        Lexeme -> ReadPrec ()
expectP ([Char] -> Lexeme
Ident [Char]
"finite")
        a
x <- ReadPrec a
forall a. Read a => ReadPrec a
readPrec
        Bool -> ReadPrec ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
n)
        Finite a n -> ReadPrec (Finite a n)
forall a. a -> ReadPrec a
forall (m :: * -> *) a. Monad m => a -> m a
return (Finite a n -> ReadPrec (Finite a n))
-> Finite a n -> ReadPrec (Finite a n)
forall a b. (a -> b) -> a -> b
$ a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
x
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)

-- | 'Prelude.+', 'Prelude.-', and 'Prelude.*' implement arithmetic modulo @n@.
-- The 'fromInteger' function raises an error for inputs outside of bounds.
instance (SaneIntegral a, KnownIntegral a n) => Num (Finite a n) where
    {-# SPECIALIZE instance KnownNat n => Num (Finite Integer n) #-}
#if MIN_VERSION_base(4,8,0)
    {-# SPECIALIZE instance KnownNat n => Num (Finite Natural n) #-}
#endif
    {-# SPECIALIZE instance KnownIntegral Word n => Num (Finite Word n) #-}
    {-# SPECIALIZE instance KnownIntegral Int n => Num (Finite Int n) #-}
    {-# SPECIALIZE instance KnownIntegral Word8 n => Num (Finite Word8 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int8 n => Num (Finite Int8 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word16 n => Num (Finite Word16 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int16 n => Num (Finite Int16 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word32 n => Num (Finite Word32 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int32 n => Num (Finite Int32 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word64 n => Num (Finite Word64 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int64 n => Num (Finite Int64 n) #-}
    Finite a
x + :: Finite a n -> Finite a n -> Finite a n
+ Finite a
y = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. SaneIntegral a => a -> a -> a -> a
modAdd a
n a
x a
y
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    Finite a
x - :: Finite a n -> Finite a n -> Finite a n
- Finite a
y = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. SaneIntegral a => a -> a -> a -> a
modSub a
n a
x a
y
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    Finite a
x * :: Finite a n -> Finite a n -> Finite a n
* Finite a
y = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. SaneIntegral a => a -> a -> a -> a
modMul a
n a
x a
y
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    abs :: Finite a n -> Finite a n
abs Finite a n
fx = Finite a n
fx
    signum :: Finite a n -> Finite a n
signum (Finite a
x) = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ if a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 then a
0 else a
1
    fromInteger :: Integer -> Finite a n
fromInteger Integer
x
        | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
x
        | Bool
otherwise = [Char] -> Finite a n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Finite a n) -> [Char] -> Finite a n
forall a b. (a -> b) -> a -> b
$ [Char]
"fromInteger: Integer " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
x
            [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not representable in Finite _ " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Integer -> [Char]
forall a. Show a => a -> [Char]
show (a -> Integer
forall a. Integral a => a -> Integer
toInteger a
n)
        where n :: a
n = Proxy n -> a
forall (n :: Natural) a (proxy :: Natural -> *).
KnownIntegral a n =>
proxy n -> a
intVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) :: a

instance (SaneIntegral a, KnownIntegral a n) => Real (Finite a n) where
    {-# SPECIALIZE instance KnownNat n => Real (Finite Integer n) #-}
#if MIN_VERSION_base(4,8,0)
    {-# SPECIALIZE instance KnownNat n => Real (Finite Natural n) #-}
#endif
    {-# SPECIALIZE instance KnownIntegral Word n => Real (Finite Word n) #-}
    {-# SPECIALIZE instance KnownIntegral Int n => Real (Finite Int n) #-}
    {-# SPECIALIZE instance KnownIntegral Word8 n => Real (Finite Word8 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int8 n => Real (Finite Int8 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word16 n => Real (Finite Word16 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int16 n => Real (Finite Int16 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word32 n => Real (Finite Word32 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int32 n => Real (Finite Int32 n) #-}
    {-# SPECIALIZE instance KnownIntegral Word64 n => Real (Finite Word64 n) #-}
    {-# SPECIALIZE instance KnownIntegral Int64 n => Real (Finite Int64 n) #-}
    toRational :: Finite a n -> Rational
toRational (Finite a
x) = a -> Rational
forall a. Real a => a -> Rational
toRational a
x

-- | 'quot' and 'rem' are the same as 'div' and 'mod' and they implement regular
-- division of numbers in the range @[0, n)@, __not__ modular inverses.
instance (SaneIntegral a, KnownIntegral a n) => Integral (Finite a n) where
    {-# SPECIALIZE instance KnownNat n => Integral (Finite Integer n) #-}
#if MIN_VERSION_base(4,8,0)
    {-# SPECIALIZE instance KnownNat n => Integral (Finite Natural n) #-}
#endif
    {-# SPECIALIZE instance KnownIntegral Word n => Integral (Finite Word n) #-}
    {-# SPECIALIZE instance KnownIntegral Int n => Integral (Finite Int n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word8 n => Integral (Finite Word8 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int8 n => Integral (Finite Int8 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word16 n => Integral (Finite Word16 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int16 n => Integral (Finite Int16 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word32 n => Integral (Finite Word32 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int32 n => Integral (Finite Int32 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Word64 n => Integral (Finite Word64 n) #-}
    {-# SPECIALIZE instance
        KnownIntegral Int64 n => Integral (Finite Int64 n) #-}
    quot :: Finite a n -> Finite a n -> Finite a n
quot (Finite a
x) (Finite a
y) = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Integral a => a -> a -> a
quot a
x a
y
    rem :: Finite a n -> Finite a n -> Finite a n
rem (Finite a
x) (Finite a
y) = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Integral a => a -> a -> a
rem a
x a
y
    quotRem :: Finite a n -> Finite a n -> (Finite a n, Finite a n)
quotRem (Finite a
x) (Finite a
y) = case a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
quotRem a
x a
y of
        (a
q, a
r) -> (a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
q, a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
r)
    div :: Finite a n -> Finite a n -> Finite a n
div (Finite a
x) (Finite a
y) = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Integral a => a -> a -> a
div a
x a
y
    mod :: Finite a n -> Finite a n -> Finite a n
mod (Finite a
x) (Finite a
y) = a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite (a -> Finite a n) -> a -> Finite a n
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. Integral a => a -> a -> a
mod a
x a
y
    divMod :: Finite a n -> Finite a n -> (Finite a n, Finite a n)
divMod (Finite a
x) (Finite a
y) = case a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
divMod a
x a
y of
        (a
q, a
r) -> (a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
q, a -> Finite a n
forall a (n :: Natural). a -> Finite a n
Finite a
r)
    toInteger :: Finite a n -> Integer
toInteger (Finite a
x) = a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x

instance NFData a => NFData (Finite a n) where
    rnf :: Finite a n -> ()
rnf (Finite a
x) = a -> ()
forall a. NFData a => a -> ()
rnf a
x