    -- |
    -- 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))