-- |
-- Module      : Basement.Block
-- License     : BSD-style
-- Maintainer  : Haskell Foundation
--
-- Types to represent ℤ/nℤ.
--
-- ℤ/nℤ is a finite field and is defined as the set of natural number:
-- {0, 1, ..., n − 1}.
--
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
module Basement.Bounded
    ( Zn64
    , unZn64
    , Zn
    , unZn
    , zn64
    , zn
    , zn64Nat
    , znNat
    ) where

import           GHC.TypeLits
import           Data.Word
import           Basement.Compat.Base
import           Basement.Compat.Natural
import           Basement.Numerical.Number
import           Data.Proxy
import           Basement.Nat
import qualified Prelude

-- | A type level bounded natural backed by a Word64
newtype Zn64 (n :: Nat) = Zn64 { forall (n :: Nat). Zn64 n -> Word64
unZn64 :: Word64 }
    deriving (Int -> Zn64 n -> ShowS
[Zn64 n] -> ShowS
Zn64 n -> String
(Int -> Zn64 n -> ShowS)
-> (Zn64 n -> String) -> ([Zn64 n] -> ShowS) -> Show (Zn64 n)
forall (n :: Nat). Int -> Zn64 n -> ShowS
forall (n :: Nat). [Zn64 n] -> ShowS
forall (n :: Nat). Zn64 n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat). Int -> Zn64 n -> ShowS
showsPrec :: Int -> Zn64 n -> ShowS
$cshow :: forall (n :: Nat). Zn64 n -> String
show :: Zn64 n -> String
$cshowList :: forall (n :: Nat). [Zn64 n] -> ShowS
showList :: [Zn64 n] -> ShowS
Show,Zn64 n -> Zn64 n -> Bool
(Zn64 n -> Zn64 n -> Bool)
-> (Zn64 n -> Zn64 n -> Bool) -> Eq (Zn64 n)
forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
== :: Zn64 n -> Zn64 n -> Bool
$c/= :: forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
/= :: Zn64 n -> Zn64 n -> Bool
Eq,Eq (Zn64 n)
Eq (Zn64 n) =>
(Zn64 n -> Zn64 n -> Ordering)
-> (Zn64 n -> Zn64 n -> Bool)
-> (Zn64 n -> Zn64 n -> Bool)
-> (Zn64 n -> Zn64 n -> Bool)
-> (Zn64 n -> Zn64 n -> Bool)
-> (Zn64 n -> Zn64 n -> Zn64 n)
-> (Zn64 n -> Zn64 n -> Zn64 n)
-> Ord (Zn64 n)
Zn64 n -> Zn64 n -> Bool
Zn64 n -> Zn64 n -> Ordering
Zn64 n -> Zn64 n -> Zn64 n
forall (n :: Nat). Eq (Zn64 n)
forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
forall (n :: Nat). Zn64 n -> Zn64 n -> Ordering
forall (n :: Nat). Zn64 n -> Zn64 n -> Zn64 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
$ccompare :: forall (n :: Nat). Zn64 n -> Zn64 n -> Ordering
compare :: Zn64 n -> Zn64 n -> Ordering
$c< :: forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
< :: Zn64 n -> Zn64 n -> Bool
$c<= :: forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
<= :: Zn64 n -> Zn64 n -> Bool
$c> :: forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
> :: Zn64 n -> Zn64 n -> Bool
$c>= :: forall (n :: Nat). Zn64 n -> Zn64 n -> Bool
>= :: Zn64 n -> Zn64 n -> Bool
$cmax :: forall (n :: Nat). Zn64 n -> Zn64 n -> Zn64 n
max :: Zn64 n -> Zn64 n -> Zn64 n
$cmin :: forall (n :: Nat). Zn64 n -> Zn64 n -> Zn64 n
min :: Zn64 n -> Zn64 n -> Zn64 n
Ord)

instance (KnownNat n, NatWithinBound Word64 n) => Prelude.Num (Zn64 n) where
    fromInteger :: Integer -> Zn64 n
fromInteger = Word64 -> Zn64 n
forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Word64 -> Zn64 n
zn64 (Word64 -> Zn64 n) -> (Integer -> Word64) -> Integer -> Zn64 n
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Word64
forall a. Num a => Integer -> a
Prelude.fromInteger
    + :: Zn64 n -> Zn64 n -> Zn64 n
(+) = Zn64 n -> Zn64 n -> Zn64 n
forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Zn64 n -> Zn64 n -> Zn64 n
add64
    (-) = Zn64 n -> Zn64 n -> Zn64 n
forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Zn64 n -> Zn64 n -> Zn64 n
sub64
    * :: Zn64 n -> Zn64 n -> Zn64 n
(*) = Zn64 n -> Zn64 n -> Zn64 n
forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Zn64 n -> Zn64 n -> Zn64 n
mul64
    abs :: Zn64 n -> Zn64 n
abs Zn64 n
a = Zn64 n
a
    negate :: Zn64 n -> Zn64 n
negate Zn64 n
_ = String -> Zn64 n
forall a. HasCallStack => String -> a
error String
"cannot negate Zn64: use Foundation Numerical hierarchy for this function to not be exposed to Zn64"
    signum :: Zn64 n -> Zn64 n
signum (Zn64 Word64
a) = Word64 -> Zn64 n
forall (n :: Nat). Word64 -> Zn64 n
Zn64 (Word64 -> Word64
forall a. Num a => a -> a
Prelude.signum Word64
a)

type instance NatNumMaxBound (Zn64 n) = n

instance (KnownNat n, NatWithinBound Word64 n) => Integral (Zn64 n) where
    fromInteger :: Integer -> Zn64 n
fromInteger = Word64 -> Zn64 n
forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Word64 -> Zn64 n
zn64 (Word64 -> Zn64 n) -> (Integer -> Word64) -> Integer -> Zn64 n
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Word64
forall a. Num a => Integer -> a
Prelude.fromInteger
instance (KnownNat n, NatWithinBound Word64 n) => IsIntegral (Zn64 n) where
    toInteger :: Zn64 n -> Integer
toInteger (Zn64 Word64
n) = Word64 -> Integer
forall a. IsIntegral a => a -> Integer
toInteger Word64
n
instance (KnownNat n, NatWithinBound Word64 n) => IsNatural (Zn64 (n :: Nat)) where
    toNatural :: Zn64 n -> Nat
toNatural (Zn64 Word64
n) = Word64 -> Nat
forall a. IsNatural a => a -> Nat
toNatural Word64
n

-- | Create an element of ℤ/nℤ from a Word64
--
-- If the value is greater than n, then the value is normalized by using the
-- integer modulus n
zn64 :: forall n . (KnownNat n, NatWithinBound Word64 n) => Word64 -> Zn64 n
zn64 :: forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Word64 -> Zn64 n
zn64 Word64
v = Word64 -> Zn64 n
forall (n :: Nat). Word64 -> Zn64 n
Zn64 (Word64
v Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Word64
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Word64 n) =>
proxy n -> Word64
natValWord64 (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | Create an element of ℤ/nℤ from a type level Nat
zn64Nat :: forall m n . (KnownNat m, KnownNat n, NatWithinBound Word64 m, NatWithinBound Word64 n, CmpNat m n ~ 'LT)
        => Proxy m
        -> Zn64 n
zn64Nat :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n, NatWithinBound Word64 m,
 NatWithinBound Word64 n, CmpNat m n ~ 'LT) =>
Proxy m -> Zn64 n
zn64Nat Proxy m
p = Word64 -> Zn64 n
forall (n :: Nat). Word64 -> Zn64 n
Zn64 (Proxy m -> Word64
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Word64 n) =>
proxy n -> Word64
natValWord64 Proxy m
p)

-- | Add 2 Zn64
add64 :: forall n . (KnownNat n, NatWithinBound Word64 n) => Zn64 n -> Zn64 n -> Zn64 n
add64 :: forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Zn64 n -> Zn64 n -> Zn64 n
add64 (Zn64 Word64
a) (Zn64 Word64
b) = Word64 -> Zn64 n
forall (n :: Nat). Word64 -> Zn64 n
Zn64 ((Word64
a Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
Prelude.+ Word64
b) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Word64
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Word64 n) =>
proxy n -> Word64
natValWord64 (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | subtract 2 Zn64
sub64 :: forall n . (KnownNat n, NatWithinBound Word64 n) => Zn64 n -> Zn64 n -> Zn64 n
sub64 :: forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Zn64 n -> Zn64 n -> Zn64 n
sub64 (Zn64 Word64
a) (Zn64 Word64
b) = Word64 -> Zn64 n
forall (n :: Nat). Word64 -> Zn64 n
Zn64 ((Word64
a Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
Prelude.- Word64
b) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Word64
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Word64 n) =>
proxy n -> Word64
natValWord64 (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | Multiply 2 Zn64
mul64 :: forall n . (KnownNat n, NatWithinBound Word64 n) => Zn64 n -> Zn64 n -> Zn64 n
mul64 :: forall (n :: Nat).
(KnownNat n, NatWithinBound Word64 n) =>
Zn64 n -> Zn64 n -> Zn64 n
mul64 (Zn64 Word64
a) (Zn64 Word64
b) = Word64 -> Zn64 n
forall (n :: Nat). Word64 -> Zn64 n
Zn64 ((Word64
a Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
Prelude.* Word64
b) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Word64
forall (n :: Nat) (proxy :: Nat -> *).
(KnownNat n, NatWithinBound Word64 n) =>
proxy n -> Word64
natValWord64 (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | A type level bounded natural
newtype Zn (n :: Nat) = Zn { forall (n :: Nat). Zn n -> Nat
unZn :: Natural }
    deriving (Int -> Zn n -> ShowS
[Zn n] -> ShowS
Zn n -> String
(Int -> Zn n -> ShowS)
-> (Zn n -> String) -> ([Zn n] -> ShowS) -> Show (Zn n)
forall (n :: Nat). Int -> Zn n -> ShowS
forall (n :: Nat). [Zn n] -> ShowS
forall (n :: Nat). Zn n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Nat). Int -> Zn n -> ShowS
showsPrec :: Int -> Zn n -> ShowS
$cshow :: forall (n :: Nat). Zn n -> String
show :: Zn n -> String
$cshowList :: forall (n :: Nat). [Zn n] -> ShowS
showList :: [Zn n] -> ShowS
Show,Zn n -> Zn n -> Bool
(Zn n -> Zn n -> Bool) -> (Zn n -> Zn n -> Bool) -> Eq (Zn n)
forall (n :: Nat). Zn n -> Zn n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). Zn n -> Zn n -> Bool
== :: Zn n -> Zn n -> Bool
$c/= :: forall (n :: Nat). Zn n -> Zn n -> Bool
/= :: Zn n -> Zn n -> Bool
Eq,Eq (Zn n)
Eq (Zn n) =>
(Zn n -> Zn n -> Ordering)
-> (Zn n -> Zn n -> Bool)
-> (Zn n -> Zn n -> Bool)
-> (Zn n -> Zn n -> Bool)
-> (Zn n -> Zn n -> Bool)
-> (Zn n -> Zn n -> Zn n)
-> (Zn n -> Zn n -> Zn n)
-> Ord (Zn n)
Zn n -> Zn n -> Bool
Zn n -> Zn n -> Ordering
Zn n -> Zn n -> Zn n
forall (n :: Nat). Eq (Zn n)
forall (n :: Nat). Zn n -> Zn n -> Bool
forall (n :: Nat). Zn n -> Zn n -> Ordering
forall (n :: Nat). Zn n -> Zn n -> Zn 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
$ccompare :: forall (n :: Nat). Zn n -> Zn n -> Ordering
compare :: Zn n -> Zn n -> Ordering
$c< :: forall (n :: Nat). Zn n -> Zn n -> Bool
< :: Zn n -> Zn n -> Bool
$c<= :: forall (n :: Nat). Zn n -> Zn n -> Bool
<= :: Zn n -> Zn n -> Bool
$c> :: forall (n :: Nat). Zn n -> Zn n -> Bool
> :: Zn n -> Zn n -> Bool
$c>= :: forall (n :: Nat). Zn n -> Zn n -> Bool
>= :: Zn n -> Zn n -> Bool
$cmax :: forall (n :: Nat). Zn n -> Zn n -> Zn n
max :: Zn n -> Zn n -> Zn n
$cmin :: forall (n :: Nat). Zn n -> Zn n -> Zn n
min :: Zn n -> Zn n -> Zn n
Ord)

instance KnownNat n => Prelude.Num (Zn n) where
    fromInteger :: Integer -> Zn n
fromInteger = Nat -> Zn n
forall (n :: Nat). KnownNat n => Nat -> Zn n
zn (Nat -> Zn n) -> (Integer -> Nat) -> Integer -> Zn n
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Nat
forall a. Num a => Integer -> a
Prelude.fromInteger
    + :: Zn n -> Zn n -> Zn n
(+) = Zn n -> Zn n -> Zn n
forall (n :: Nat). KnownNat n => Zn n -> Zn n -> Zn n
add
    (-) = Zn n -> Zn n -> Zn n
forall (n :: Nat). KnownNat n => Zn n -> Zn n -> Zn n
sub
    * :: Zn n -> Zn n -> Zn n
(*) = Zn n -> Zn n -> Zn n
forall (n :: Nat). KnownNat n => Zn n -> Zn n -> Zn n
mul
    abs :: Zn n -> Zn n
abs Zn n
a = Zn n
a
    negate :: Zn n -> Zn n
negate Zn n
_ = String -> Zn n
forall a. HasCallStack => String -> a
error String
"cannot negate Zn: use Foundation Numerical hierarchy for this function to not be exposed to Zn"
    signum :: Zn n -> Zn n
signum = Nat -> Zn n
forall (n :: Nat). Nat -> Zn n
Zn (Nat -> Zn n) -> (Zn n -> Nat) -> Zn n -> Zn n
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Nat -> Nat
forall a. Num a => a -> a
Prelude.signum (Nat -> Nat) -> (Zn n -> Nat) -> Zn n -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Zn n -> Nat
forall (n :: Nat). Zn n -> Nat
unZn

type instance NatNumMaxBound (Zn n) = n

instance KnownNat n => Integral (Zn n) where
    fromInteger :: Integer -> Zn n
fromInteger = Nat -> Zn n
forall (n :: Nat). KnownNat n => Nat -> Zn n
zn (Nat -> Zn n) -> (Integer -> Nat) -> Integer -> Zn n
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Integer -> Nat
forall a. Num a => Integer -> a
Prelude.fromInteger
instance KnownNat n => IsIntegral (Zn n) where
    toInteger :: Zn n -> Integer
toInteger (Zn Nat
n) = Nat -> Integer
forall a. IsIntegral a => a -> Integer
toInteger Nat
n
instance KnownNat n => IsNatural (Zn n) where
    toNatural :: Zn n -> Nat
toNatural Zn n
i = Zn n -> Nat
forall (n :: Nat). Zn n -> Nat
unZn Zn n
i

-- | Create an element of ℤ/nℤ from a Natural.
--
-- If the value is greater than n, then the value is normalized by using the
-- integer modulus n
zn :: forall n . KnownNat n => Natural -> Zn n
zn :: forall (n :: Nat). KnownNat n => Nat -> Zn n
zn Nat
v = Nat -> Zn n
forall (n :: Nat). Nat -> Zn n
Zn (Nat
v Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natValNatural (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | Create an element of ℤ/nℤ from a type level Nat
znNat :: forall m n . (KnownNat m, KnownNat n, CmpNat m n ~ 'LT) => Proxy m -> Zn n
znNat :: forall (m :: Nat) (n :: Nat).
(KnownNat m, KnownNat n, CmpNat m n ~ 'LT) =>
Proxy m -> Zn n
znNat Proxy m
m = Nat -> Zn n
forall (n :: Nat). Nat -> Zn n
Zn (Proxy m -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natValNatural Proxy m
m)

-- | Add 2 Zn
add :: forall n . KnownNat n => Zn n -> Zn n -> Zn n
add :: forall (n :: Nat). KnownNat n => Zn n -> Zn n -> Zn n
add (Zn Nat
a) (Zn Nat
b) = Nat -> Zn n
forall (n :: Nat). Nat -> Zn n
Zn ((Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
Prelude.+ Nat
b) Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natValNatural (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | subtract 2 Zn
sub :: forall n . KnownNat n => Zn n -> Zn n -> Zn n
sub :: forall (n :: Nat). KnownNat n => Zn n -> Zn n -> Zn n
sub (Zn Nat
a) (Zn Nat
b) = Nat -> Zn n
forall (n :: Nat). Nat -> Zn n
Zn ((Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
Prelude.- Nat
b) Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natValNatural (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

-- | Multiply 2 Zn
mul :: forall n . KnownNat n => Zn n -> Zn n -> Zn n
mul :: forall (n :: Nat). KnownNat n => Zn n -> Zn n -> Zn n
mul (Zn Nat
a) (Zn Nat
b) = Nat -> Zn n
forall (n :: Nat). Nat -> Zn n
Zn ((Nat
a Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
Prelude.* Nat
b) Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
`Prelude.mod` Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natValNatural (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))