--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Finite.Internal
-- Copyright   :  (C) 2015-2022 mniip
-- License     :  BSD3
-- Maintainer  :  mniip <mniip@mniip.com>
-- Stability   :  experimental
-- Portability :  portable
--------------------------------------------------------------------------------
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE KindSignatures #-}
module Data.Finite.Internal
    (
        Finite(Finite),
        finite,
        getFinite
    )
    where

import Control.DeepSeq
import Control.Monad
import Data.Ratio
import GHC.Generics
import GHC.Read
import GHC.TypeLits
import Text.ParserCombinators.ReadPrec
import Text.Read.Lex

-- | Finite number type. @'Finite' n@ is inhabited by exactly @n@ values
-- the range @[0, n)@ including @0@ but excluding @n@. Invariants:
--
-- prop> getFinite x < natVal x
-- prop> getFinite x >= 0
newtype Finite (n :: Nat) = Finite Integer
                          deriving (Finite n -> Finite n -> Bool
(Finite n -> Finite n -> Bool)
-> (Finite n -> Finite n -> Bool) -> Eq (Finite n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: Nat). Finite n -> Finite n -> Bool
/= :: Finite n -> Finite n -> Bool
$c/= :: forall (n :: Nat). Finite n -> Finite n -> Bool
== :: Finite n -> Finite n -> Bool
$c== :: forall (n :: Nat). Finite n -> Finite n -> Bool
Eq, Eq (Finite n)
Eq (Finite n)
-> (Finite n -> Finite n -> Ordering)
-> (Finite n -> Finite n -> Bool)
-> (Finite n -> Finite n -> Bool)
-> (Finite n -> Finite n -> Bool)
-> (Finite n -> Finite n -> Bool)
-> (Finite n -> Finite n -> Finite n)
-> (Finite n -> Finite n -> Finite n)
-> Ord (Finite n)
Finite n -> Finite n -> Bool
Finite n -> Finite n -> Ordering
Finite n -> Finite n -> Finite 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 (n :: Nat). Eq (Finite n)
forall (n :: Nat). Finite n -> Finite n -> Bool
forall (n :: Nat). Finite n -> Finite n -> Ordering
forall (n :: Nat). Finite n -> Finite n -> Finite n
min :: Finite n -> Finite n -> Finite n
$cmin :: forall (n :: Nat). Finite n -> Finite n -> Finite n
max :: Finite n -> Finite n -> Finite n
$cmax :: forall (n :: Nat). Finite n -> Finite n -> Finite n
>= :: Finite n -> Finite n -> Bool
$c>= :: forall (n :: Nat). Finite n -> Finite n -> Bool
> :: Finite n -> Finite n -> Bool
$c> :: forall (n :: Nat). Finite n -> Finite n -> Bool
<= :: Finite n -> Finite n -> Bool
$c<= :: forall (n :: Nat). Finite n -> Finite n -> Bool
< :: Finite n -> Finite n -> Bool
$c< :: forall (n :: Nat). Finite n -> Finite n -> Bool
compare :: Finite n -> Finite n -> Ordering
$ccompare :: forall (n :: Nat). Finite n -> Finite n -> Ordering
$cp1Ord :: forall (n :: Nat). Eq (Finite n)
Ord, (forall x. Finite n -> Rep (Finite n) x)
-> (forall x. Rep (Finite n) x -> Finite n) -> Generic (Finite n)
forall x. Rep (Finite n) x -> Finite n
forall x. Finite n -> Rep (Finite n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (Finite n) x -> Finite n
forall (n :: Nat) x. Finite n -> Rep (Finite n) x
$cto :: forall (n :: Nat) x. Rep (Finite n) x -> Finite n
$cfrom :: forall (n :: Nat) x. Finite n -> Rep (Finite n) x
Generic)

-- | Convert an 'Integer' into a 'Finite', throwing an error if the input is out
-- of bounds.
finite :: KnownNat n => Integer -> Finite n
finite :: Integer -> Finite n
finite Integer
x = Finite n
result
    where
        result :: Finite n
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
            then Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
            else [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Finite n) -> [Char] -> Finite n
forall a b. (a -> b) -> a -> b
$ [Char]
"finite: 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 (Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result)

-- | Convert a 'Finite' into the corresponding 'Integer'.
getFinite :: Finite n -> Integer
getFinite :: Finite n -> Integer
getFinite (Finite Integer
x) = Integer
x

-- | Throws an error for @'Finite' 0@
instance KnownNat n => Bounded (Finite n) where
    maxBound :: Finite n
maxBound = Finite n
result
        where
            result :: Finite n
result = if Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
                then Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
                else [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error [Char]
"maxBound: Finite 0 is uninhabited"
    minBound :: Finite n
minBound = Finite n
result
        where
            result :: Finite n
result = if Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0
                then Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
0
                else [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error [Char]
"minBound: Finite 0 is uninhabited"

instance KnownNat n => Enum (Finite n) where
    succ :: Finite n -> Finite n
succ fx :: Finite n
fx@(Finite Integer
x) = if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
        then [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error [Char]
"succ: bad argument"
        else Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Enum a => a -> a
succ Integer
x
    pred :: Finite n -> Finite n
pred (Finite Integer
x) = if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
        then [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error [Char]
"pred: bad argument"
        else Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer -> Integer
forall a. Enum a => a -> a
pred Integer
x
    fromEnum :: Finite n -> Int
fromEnum = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (Integer -> Int) -> (Finite n -> Integer) -> Finite n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite
    toEnum :: Int -> Finite n
toEnum = Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
finite (Integer -> Finite n) -> (Int -> Integer) -> Int -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Enum a => Int -> a
toEnum
    enumFrom :: Finite n -> [Finite n]
enumFrom Finite n
x = Finite n -> Finite n -> [Finite n]
forall a. Enum a => a -> a -> [a]
enumFromTo Finite n
x Finite n
forall a. Bounded a => a
maxBound
    enumFromTo :: Finite n -> Finite n -> [Finite n]
enumFromTo (Finite Integer
x) (Finite Integer
y) = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> [Integer] -> [Finite n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Integer -> Integer -> [Integer]
forall a. Enum a => a -> a -> [a]
enumFromTo Integer
x Integer
y
    enumFromThen :: Finite n -> Finite n -> [Finite n]
enumFromThen Finite n
x Finite n
y = Finite n -> Finite n -> Finite n -> [Finite n]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Finite n
x Finite n
y (if Finite n
x Finite n -> Finite n -> Bool
forall a. Ord a => a -> a -> Bool
>= Finite n
y then Finite n
forall a. Bounded a => a
minBound else Finite n
forall a. Bounded a => a
maxBound)
    enumFromThenTo :: Finite n -> Finite n -> Finite n -> [Finite n]
enumFromThenTo (Finite Integer
x) (Finite Integer
y) (Finite Integer
z) = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> [Integer] -> [Finite n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Integer -> Integer -> Integer -> [Integer]
forall a. Enum a => a -> a -> a -> [a]
enumFromThenTo Integer
x Integer
y Integer
z

instance Show (Finite n) where
    showsPrec :: Int -> Finite n -> [Char] -> [Char]
showsPrec Int
d (Finite Integer
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 -> Integer -> [Char] -> [Char]
forall a. Show a => Int -> a -> [Char] -> [Char]
showsPrec Int
10 Integer
x

instance KnownNat n => Read (Finite n) where
    readPrec :: ReadPrec (Finite n)
readPrec = ReadPrec (Finite n) -> ReadPrec (Finite n)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (Finite n) -> ReadPrec (Finite n))
-> ReadPrec (Finite n) -> ReadPrec (Finite n)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (Finite n) -> ReadPrec (Finite n)
forall a. Int -> ReadPrec a -> ReadPrec a
Text.ParserCombinators.ReadPrec.prec Int
10 (ReadPrec (Finite n) -> ReadPrec (Finite n))
-> ReadPrec (Finite n) -> ReadPrec (Finite n)
forall a b. (a -> b) -> a -> b
$ do
                 Lexeme -> ReadPrec ()
expectP ([Char] -> Lexeme
Ident [Char]
"finite")
                 Integer
x <- ReadPrec Integer
forall a. Read a => ReadPrec a
readPrec
                 let result :: Finite n
result = Integer -> Finite n
forall (n :: Nat). KnownNat n => Integer -> Finite n
finite Integer
x
                 Bool -> ReadPrec ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result)
                 Finite n -> ReadPrec (Finite n)
forall (m :: * -> *) a. Monad m => a -> m a
return Finite n
result

-- | 'Prelude.+', 'Prelude.-', and 'Prelude.*' implement arithmetic modulo @n@.
-- The 'fromInteger' function raises an error for inputs outside of bounds.
instance KnownNat n => Num (Finite n) where
    fx :: Finite n
fx@(Finite Integer
x) + :: Finite n -> Finite n -> Finite n
+ Finite Integer
y = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx
    fx :: Finite n
fx@(Finite Integer
x) - :: Finite n -> Finite n -> Finite n
- Finite Integer
y = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx
    fx :: Finite n
fx@(Finite Integer
x) * :: Finite n -> Finite n -> Finite n
* Finite Integer
y = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
fx
    abs :: Finite n -> Finite n
abs Finite n
fx = Finite n
fx
    signum :: Finite n -> Finite n
signum (Finite Integer
x) = Integer -> Finite n
forall a. Num a => Integer -> a
fromInteger (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ if Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer
0 else Integer
1
    fromInteger :: Integer -> Finite n
fromInteger Integer
x = Finite n
result
        where
            result :: Finite n
result = if Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
                then Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite Integer
x
                else [Char] -> Finite n
forall a. HasCallStack => [Char] -> a
error ([Char] -> Finite n) -> [Char] -> Finite 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 (Finite n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal Finite n
result)

instance KnownNat n => Real (Finite n) where
    toRational :: Finite n -> Rational
toRational (Finite Integer
x) = Integer
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

-- | 'quot' and 'rem' are the same as 'div' and 'mod' and they implement regular
-- division of numbers in the range @[0, n)@, __not__ modular arithmetic.
instance KnownNat n => Integral (Finite n) where
    quotRem :: Finite n -> Finite n -> (Finite n, Finite n)
quotRem (Finite Integer
x) (Finite Integer
y) = (Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y, Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Finite (Integer -> Finite n) -> Integer -> Finite n
forall a b. (a -> b) -> a -> b
$ Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)
    toInteger :: Finite n -> Integer
toInteger (Finite Integer
x) = Integer
x

instance NFData (Finite n)