{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Algebra.Basic.Class where

import           Data.Bool                        (bool)
import           Data.Kind                        (Type)
import           GHC.Natural                      (naturalFromInteger)
import           Numeric.Natural                  (Natural)
import           Prelude                          hiding (Num (..), div, divMod, length, mod, negate, product,
                                                   replicate, sum, (/), (^))
import qualified Prelude                          as Haskell

import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Prelude                   (length, replicate)

infixl 7 *, /
infixl 6 +, -, -!

{- | Every algebraic structure has a handful of "constant types" related
with it: natural numbers, integers, field of constants etc. This typeclass
captures this relation.
-}
class FromConstant a b where
    -- | Builds an element of an algebraic structure from a constant.
    --
    -- @fromConstant@ should preserve algebraic structure, e.g. if both the
    -- structure and the type of constants are additive monoids, the following
    -- should hold:
    --
    -- [Homomorphism] @fromConstant (c + d) == fromConstant c + fromConstant d@
    fromConstant :: a -> b

instance FromConstant a a where
    fromConstant :: a -> a
fromConstant = a -> a
forall a. a -> a
id

class ToConstant a b where
    toConstant :: a -> b

instance ToConstant a a where
    toConstant :: a -> a
toConstant = a -> a
forall a. a -> a
id

--------------------------------------------------------------------------------

{- | A class of types with a binary associative operation with a multiplicative
feel to it. Not necessarily commutative.
-}
class MultiplicativeSemigroup a where
    -- | A binary associative operation. The following should hold:
    --
    -- [Associativity] @x * (y * z) == (x * y) * z@
    (*) :: a -> a -> a

product1 :: (Foldable t, MultiplicativeSemigroup a) => t a -> a
product1 :: forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeSemigroup a) =>
t a -> a
product1 = (a -> a -> a) -> t a -> a
forall a. (a -> a -> a) -> t a -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*)

{- | A class for semigroup (and monoid) actions on types where exponential
notation is the most natural (including an exponentiation itself).
-}
class MultiplicativeSemigroup b => Exponent a b where
    -- | A right semigroup action on a type. The following should hold:
    --
    -- [Compatibility] @a ^ (m * n) == (a ^ m) ^ n@
    --
    -- If exponents form a monoid, the following should also hold:
    --
    -- [Right identity] @a ^ one == a@
    --
    -- NOTE, however, that even if exponents form a semigroup, left
    -- distributivity (that @a ^ (m + n) == (a ^ m) * (a ^ n)@) is desirable but
    -- not required: otherwise instance for Bool as exponent could not be made
    -- lawful.
    (^) :: a -> b -> a

{- | A class of types with a binary associative operation with a multiplicative
feel to it and an identity element. Not necessarily commutative.

While exponentiation by a natural is specified as a constraint, a default
implementation is provided as a @'natPow'@ function. You can provide a faster
alternative, but do not forget to check that it satisfies the following
(in addition to the properties already stated in @'Exponent'@ documentation):

[Left identity] @one ^ n == one@
[Absorption] @a ^ 0 == one@
[Left distributivity] @a ^ (m + n) == (a ^ m) * (a ^ n)@

Finally, if the base monoid operation is commutative, power should
distribute over @('*')@:

[Right distributivity] @(a * b) ^ n == (a ^ n) * (b ^ n)@
-}
class (MultiplicativeSemigroup a, Exponent a Natural) => MultiplicativeMonoid a where
    -- | An identity with respect to multiplication:
    --
    -- [Left identity] @one * x == x@
    -- [Right identity] @x * one == x@
    one :: a

natPow :: MultiplicativeMonoid a => a -> Natural -> a
-- | A default implementation for natural exponentiation. Uses only @('*')@ and
-- @'one'@ so doesn't loop via an @'Exponent' Natural a@ instance.
natPow :: forall a. MultiplicativeMonoid a => a -> Natural -> a
natPow a
a Natural
n = [a] -> a
forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeMonoid a) =>
t a -> a
product ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Natural -> a -> a) -> [Natural] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Natural -> a -> a
forall {a} {a}.
(Eq a, Num a, MultiplicativeMonoid a) =>
a -> a -> a
f (Natural -> [Natural]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion Natural
n) ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (\a
x -> a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
x) a
a)
  where
    f :: a -> a -> a
f a
0 a
_ = a
forall a. MultiplicativeMonoid a => a
one
    f a
1 a
x = a
x
    f a
_ a
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"^: This should never happen."

product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
product :: forall (t :: Type -> Type) a.
(Foldable t, MultiplicativeMonoid a) =>
t a -> a
product = (a -> a -> a) -> a -> t a -> a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) a
forall a. MultiplicativeMonoid a => a
one

multiExp :: (MultiplicativeMonoid a, Exponent a b, Foldable t) => a -> t b -> a
multiExp :: forall a b (t :: Type -> Type).
(MultiplicativeMonoid a, Exponent a b, Foldable t) =>
a -> t b -> a
multiExp a
a = (a -> b -> a) -> a -> t b -> a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\a
x b
y -> a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* (a
a a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
y)) a
forall a. MultiplicativeMonoid a => a
one

{- | A class for monoid actions where multiplicative notation is the most
natural (including multiplication by constant itself).
-}
class MultiplicativeMonoid b => Scale b a where
    -- | A left monoid action on a type. Should satisfy the following:
    --
    -- [Compatibility] @scale (c * d) a == scale c (scale d a)@
    -- [Left identity] @scale one a == a@
    --
    -- If, in addition, a cast from constant is defined, they should agree:
    --
    -- [Scale agrees] @scale c a == fromConstant c * a@
    -- [Cast agrees] @fromConstant c == scale c one@
    --
    -- If the action is on an abelian structure, scaling should respect it:
    --
    -- [Left distributivity] @scale c (a + b) == scale c a + scale c b@
    -- [Right absorption] @scale c zero == zero@
    --
    -- If, in addition, the scaling itself is abelian, this structure should
    -- propagate:
    --
    -- [Right distributivity] @scale (c + d) a == scale c a + scale d a@
    -- [Left absorption] @scale zero a == zero@
    --
    -- The default implementation is the multiplication by a constant.
    scale :: b -> a -> a
    default scale :: (FromConstant b a, MultiplicativeSemigroup a) => b -> a -> a
    scale = a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (a -> a -> a) -> (b -> a) -> b -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance MultiplicativeMonoid a => Scale a a

instance {-# OVERLAPPABLE #-} (Scale b a, Functor f) => Scale b (f a) where
    scale :: b -> f a -> f a
scale = (a -> a) -> f a -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a) -> f a -> f a) -> (b -> a -> a) -> b -> f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a -> a
forall b a. Scale b a => b -> a -> a
scale

{- | A class of groups in a multiplicative notation.

While exponentiation by an integer is specified in a constraint, a default
implementation is provided as an @'intPow'@ function. You can provide a faster
alternative yourself, but do not forget to check that your implementation
computes the same results on all inputs.
-}
class (MultiplicativeMonoid a, Exponent a Integer) => MultiplicativeGroup a where
    {-# MINIMAL (invert | (/)) #-}

    -- | Division in a group. The following should hold:
    --
    -- [Division] @x / x == one@
    -- [Cancellation] @(y / x) * x == y@
    -- [Agreement] @x / y == x * invert y@
    (/) :: a -> a -> a
    a
x / a
y = a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a -> a
forall a. MultiplicativeGroup a => a -> a
invert a
y

    -- | Inverse in a group. The following should hold:
    --
    -- [Left inverse] @invert x * x == one@
    -- [Right inverse] @x * invert x == one@
    -- [Agreement] @invert x == one / x@
    invert :: a -> a
    invert a
x = a
forall a. MultiplicativeMonoid a => a
one a -> a -> a
forall a. MultiplicativeGroup a => a -> a -> a
/ a
x

intPow :: MultiplicativeGroup a => a -> Integer -> a
-- | A default implementation for integer exponentiation. Uses only natural
-- exponentiation and @'invert'@ so doesn't loop via an @'Exponent' Integer a@
-- instance.
intPow :: forall a. MultiplicativeGroup a => a -> Integer -> a
intPow a
a Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = a -> a
forall a. MultiplicativeGroup a => a -> a
invert a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger (-Integer
n)
           | Bool
otherwise = a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger Integer
n

--------------------------------------------------------------------------------

-- | A class of types with a binary associative, commutative operation.
class AdditiveSemigroup a where
    -- | A binary associative commutative operation. The following should hold:
    --
    -- [Associativity] @x + (y + z) == (x + y) + z@
    -- [Commutativity] @x + y == y + x@
    (+) :: a -> a -> a

{- | A class of types with a binary associative, commutative operation and with
an identity element.

While scaling by a natural is specified as a constraint, a default
implementation is provided as a @'natScale'@ function.
-}
class (AdditiveSemigroup a, Scale Natural a) => AdditiveMonoid a where
    -- | An identity with respect to addition:
    --
    -- [Identity] @x + zero == x@
    zero :: a

natScale :: AdditiveMonoid a => Natural -> a -> a
-- | A default implementation for natural scaling. Uses only @('+')@ and
-- @'zero'@ so doesn't loop via a @'Scale' Natural a@ instance.
natScale :: forall a. AdditiveMonoid a => Natural -> a -> a
natScale Natural
n a
a = [a] -> a
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Natural -> a -> a) -> [Natural] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Natural -> a -> a
forall {a} {a}. (Eq a, Num a, AdditiveMonoid a) => a -> a -> a
f (Natural -> [Natural]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion Natural
n) ((a -> a) -> a -> [a]
forall a. (a -> a) -> a -> [a]
iterate (\a
x -> a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
x) a
a)
  where
    f :: a -> a -> a
f a
0 a
_ = a
forall a. AdditiveMonoid a => a
zero
    f a
1 a
x = a
x
    f a
_ a
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"scale: This should never happen."

sum :: (Foldable t, AdditiveMonoid a) => t a -> a
sum :: forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum = (a -> a -> a) -> a -> t a -> a
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
(+) a
forall a. AdditiveMonoid a => a
zero

{- | A class of abelian groups.

While scaling by an integer is specified in a constraint, a default
implementation is provided as an @'intScale'@ function.
-}
class (AdditiveMonoid a, Scale Integer a) => AdditiveGroup a where
    {-# MINIMAL (negate | (-)) #-}

    -- | Subtraction in an abelian group. The following should hold:
    --
    -- [Subtraction] @x - x == zero@
    -- [Agreement] @x - y == x + negate y@
    (-) :: a -> a -> a
    a
x - a
y = a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a -> a
forall a. AdditiveGroup a => a -> a
negate a
y

    -- | Inverse in an abelian group. The following should hold:
    --
    -- [Negative] @x + negate x == zero@
    -- [Agreement] @negate x == zero - x@
    negate :: a -> a
    negate a
x = a
forall a. AdditiveMonoid a => a
zero a -> a -> a
forall a. AdditiveGroup a => a -> a -> a
- a
x

intScale :: AdditiveGroup a => Integer -> a -> a
-- | A default implementation for integer scaling. Uses only natural scaling and
-- @'negate'@ so doesn't loop via a @'Scale' Integer a@ instance.
intScale :: forall a. AdditiveGroup a => Integer -> a -> a
intScale Integer
n a
a | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = Integer -> Natural
naturalFromInteger (-Integer
n) Natural -> a -> a
forall b a. Scale b a => b -> a -> a
`scale` a -> a
forall a. AdditiveGroup a => a -> a
negate a
a
             | Bool
otherwise = Integer -> Natural
naturalFromInteger Integer
n Natural -> a -> a
forall b a. Scale b a => b -> a -> a
`scale` a
a

--------------------------------------------------------------------------------

{- | Class of semirings with both 0 and 1. The following should hold:

[Left distributivity] @a * (b + c) == a * b + a * c@
[Right distributivity] @(a + b) * c == a * c + b * c@
-}
class (AdditiveMonoid a, MultiplicativeMonoid a, FromConstant Natural a) => Semiring a

{- | A Euclidean domain @R@ is an integral domain which can be endowed
with at least one function @f : R\{0} -> R+@ s.t.
If @a@ and @b@ are in @R@ and @b@ is nonzero, then there exist @q@ and @r@ in @R@ such that
@a = bq + r@ and either @r = 0@ or @f(r) < f(b)@.

@q@ and @r@ are called respectively a quotient and a remainder of the division (or Euclidean division) of @a@ by @b@.

The function @divMod@ associated with this class produces @q@ and @r@ given @a@ and @b@.
-}
class Semiring a => EuclideanDomain a where
    {-# MINIMAL divMod #-}

    divMod :: a -> a -> (a, a)

    div :: a -> a -> a
    div a
n a
d = (a, a) -> a
forall a b. (a, b) -> a
Haskell.fst ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> (a, a)
forall a. EuclideanDomain a => a -> a -> (a, a)
divMod a
n a
d

    mod :: a -> a -> a
    mod a
n a
d = (a, a) -> a
forall a b. (a, b) -> b
Haskell.snd ((a, a) -> a) -> (a, a) -> a
forall a b. (a -> b) -> a -> b
$ a -> a -> (a, a)
forall a. EuclideanDomain a => a -> a -> (a, a)
divMod a
n a
d


{- | Class of rings with both 0, 1 and additive inverses. The following should hold:

[Left distributivity] @a * (b - c) == a * b - a * c@
[Right distributivity] @(a - b) * c == a * c - b * c@
-}
class (Semiring a, AdditiveGroup a, FromConstant Integer a) => Ring a

{- | Type of modules/algebras over the base type of constants @b@. As all the
required laws are implied by the constraints, this is simply an alias rather
than a typeclass in its own right.

Note the following useful facts:

* every 'Ring' is an algebra over natural numbers and over integers;
* every 'Ring' is an algebra over itself. However, due to the possible
overlapping instances of @Scale a a@ and @FromConstant a a@ you might
need to defer the resolution of these constraints until @a@ is specified.
-}
type Algebra b a = (Ring a, Scale b a, FromConstant b a)

{- | Class of fields. As a ring, each field is commutative, that is:

[Commutativity] @x * y == y * x@

While exponentiation by an integer is specified in a constraint, a default
implementation is provided as an @'intPowF'@ function. You can provide a faster
alternative yourself, but do not forget to check that your implementation
computes the same results on all inputs.
-}
class (Ring a, Exponent a Integer) => Field a where
    {-# MINIMAL (finv | (//)) #-}

    -- | Division in a field. The following should hold:
    --
    -- [Division] If @x /= 0@, @x // x == one@
    -- [Div by 0] @x // zero == zero@
    -- [Agreement] @x // y == x * finv y@
    (//) :: a -> a -> a
    a
x // a
y = a
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a -> a
forall a. Field a => a -> a
finv a
y

    -- | Inverse in a field. The following should hold:
    --
    -- [Inverse] If @x /= 0@, @x * inverse x == one@
    -- [Inv of 0] @inverse zero == zero@
    -- [Agreement] @finv x == one // x@
    finv :: a -> a
    finv a
x = a
forall a. MultiplicativeMonoid a => a
one a -> a -> a
forall a. Field a => a -> a -> a
// a
x

    -- | @rootOfUnity n@ is an element of a characteristic @2^n@, that is,
    --
    -- [Root of 0] @rootOfUnity 0 == Just one@
    -- [Root property] If @rootOfUnity n == Just x@, @x ^ (2 ^ n) == one@
    -- [Smallest root] If @rootOfUnity n == Just x@ and @m < n@, @x ^ (2 ^ m) /= one@
    -- [All roots] If @rootOfUnity n == Just x@ and @m < n@, @rootOfUnity m /= Nothing@
    rootOfUnity :: Natural -> Maybe a
    rootOfUnity Natural
0 = a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. MultiplicativeMonoid a => a
one
    rootOfUnity Natural
_ = Maybe a
forall a. Maybe a
Nothing

intPowF :: Field a => a -> Integer -> a
-- | A default implementation for integer exponentiation. Uses only natural
-- exponentiation and @'finv'@ so doesn't loop via an @'Exponent' Integer a@
-- instance.
intPowF :: forall a. Field a => a -> Integer -> a
intPowF a
a Integer
n | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0     = a -> a
forall a. Field a => a -> a
finv a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger (-Integer
n)
            | Bool
otherwise = a
a a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ Integer -> Natural
naturalFromInteger Integer
n

{- | Class of finite structures. @Order a@ should be the actual number of
elements in the type, identified up to the associated equality relation.
-}
class (KnownNat (Order a), KnownNat (NumberOfBits a)) => Finite (a :: Type) where
    type Order a :: Natural

order :: forall a . Finite a => Natural
order :: forall a. Finite a => Natural
order = forall (n :: Natural). KnownNat n => Natural
value @(Order a)

type NumberOfBits a = Log2 (Order a - 1) + 1

numberOfBits :: forall a . KnownNat (NumberOfBits a) => Natural
numberOfBits :: forall a. KnownNat (NumberOfBits a) => Natural
numberOfBits = forall (n :: Natural). KnownNat n => Natural
value @(NumberOfBits a)

type FiniteAdditiveGroup a = (Finite a, AdditiveGroup a)

type FiniteMultiplicativeGroup a = (Finite a, MultiplicativeGroup a)

type FiniteField a = (Finite a, Field a)

type PrimeField a = (FiniteField a, Prime (Order a))

{- | A field is a commutative ring in which an element is
invertible if and only if it is nonzero.
In a discrete field an element is invertible xor it equals zero.
That is equivalent in classical logic but stronger in constructive logic.
Every element is either 0 or invertible, and 0 ≠ 1.

We represent a discrete field as a field with an
internal equality function which returns `one`
for equal field elements and `zero` for distinct field elements.
-}
class Field a => DiscreteField' a where
    equal :: a -> a -> a
    default equal :: Eq a => a -> a -> a
    equal a
a a
b = a -> a -> Bool -> a
forall a. a -> a -> Bool -> a
bool a
forall a. AdditiveMonoid a => a
zero a
forall a. MultiplicativeMonoid a => a
one (a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b)

{- | An ordering of a field is usually required to have compatibility laws with
respect to addition and multiplication. However, we can drop that requirement and
define a trichotomy field as one with an internal total ordering.
We represent a trichotomy field as a discrete field with an internal comparison of
field elements returning `negate` `one` for <, `zero` for =, and `one`
for >. The law of trichotomy is that for any two field elements, exactly one
of the relations <, =, or > holds. Thus we require that -1, 0 and 1 are distinct
field elements.

prop> equal a b = one - (trichotomy a b)^2
-}
class DiscreteField' a => TrichotomyField a where
    trichotomy :: a -> a -> a
    default trichotomy :: Ord a => a -> a -> a
    trichotomy a
a a
b = case a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
a a
b of
        Ordering
LT -> a -> a
forall a. AdditiveGroup a => a -> a
negate a
forall a. MultiplicativeMonoid a => a
one
        Ordering
EQ -> a
forall a. AdditiveMonoid a => a
zero
        Ordering
GT -> a
forall a. MultiplicativeMonoid a => a
one

--------------------------------------------------------------------------------

{- | Class of semirings where a binary expansion of elements can be computed.
Note: numbers should convert to Little-endian bit representation.

The following should hold:

* @fromBinary . binaryExpansion == id@
* @fromBinary xs == foldr (\x y -> x + y + y) zero xs@
-}
class Semiring a => BinaryExpansion a where
    binaryExpansion :: a -> [a]

    fromBinary :: [a] -> a
    fromBinary = (a -> a -> a) -> a -> [a] -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x a
y -> a
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
y a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ a
y) a
forall a. AdditiveMonoid a => a
zero

padBits :: forall a . BinaryExpansion a => Natural -> [a] -> [a]
padBits :: forall a. BinaryExpansion a => Natural -> [a] -> [a]
padBits Natural
n [a]
xs = [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Natural -> a -> [a]
forall a. Natural -> a -> [a]
replicate (Natural
n Natural -> Natural -> Natural
-! [a] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [a]
xs) a
forall a. AdditiveMonoid a => a
zero

castBits :: (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits :: forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits []     = []
castBits (a
x:[a]
xs)
    | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero = b
forall a. AdditiveMonoid a => a
zero b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [b]
forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits [a]
xs
    | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. MultiplicativeMonoid a => a
one  = b
forall a. MultiplicativeMonoid a => a
one  b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [a] -> [b]
forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits [a]
xs
    | Bool
otherwise = [Char] -> [b]
forall a. HasCallStack => [Char] -> a
error [Char]
"castBits: impossible bit value"

--------------------------------------------------------------------------------

-- | A multiplicative subgroup of nonzero elements of a field.
-- TODO: hide constructor
newtype NonZero a = NonZero a
    deriving newtype (NonZero a -> NonZero a -> NonZero a
(NonZero a -> NonZero a -> NonZero a)
-> MultiplicativeSemigroup (NonZero a)
forall a.
MultiplicativeSemigroup a =>
NonZero a -> NonZero a -> NonZero a
forall a. (a -> a -> a) -> MultiplicativeSemigroup a
$c* :: forall a.
MultiplicativeSemigroup a =>
NonZero a -> NonZero a -> NonZero a
* :: NonZero a -> NonZero a -> NonZero a
MultiplicativeSemigroup, NonZero a
Exponent (NonZero a) Natural
MultiplicativeSemigroup (NonZero a)
(MultiplicativeSemigroup (NonZero a),
 Exponent (NonZero a) Natural) =>
NonZero a -> MultiplicativeMonoid (NonZero a)
forall a. MultiplicativeMonoid a => NonZero a
forall a. MultiplicativeMonoid a => Exponent (NonZero a) Natural
forall a.
MultiplicativeMonoid a =>
MultiplicativeSemigroup (NonZero a)
forall a.
(MultiplicativeSemigroup a, Exponent a Natural) =>
a -> MultiplicativeMonoid a
$cone :: forall a. MultiplicativeMonoid a => NonZero a
one :: NonZero a
MultiplicativeMonoid)

instance Exponent a b => Exponent (NonZero a) b where
    NonZero a
a ^ :: NonZero a -> b -> NonZero a
^ b
b = a -> NonZero a
forall a. a -> NonZero a
NonZero (a
a a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
b)

instance Field a => MultiplicativeGroup (NonZero a) where
    invert :: NonZero a -> NonZero a
invert (NonZero a
x) = a -> NonZero a
forall a. a -> NonZero a
NonZero (a -> a
forall a. Field a => a -> a
finv a
x)
    NonZero a
x / :: NonZero a -> NonZero a -> NonZero a
/ NonZero a
y = a -> NonZero a
forall a. a -> NonZero a
NonZero (a
x a -> a -> a
forall a. Field a => a -> a -> a
// a
y)

instance (KnownNat (Order (NonZero a)), KnownNat (NumberOfBits (NonZero a)))
    => Finite (NonZero a) where
    type Order (NonZero a) = Order a - 1

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup Natural where
    * :: Natural -> Natural -> Natural
(*) = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Haskell.*)

instance Exponent Natural Natural where
    ^ :: Natural -> Natural -> Natural
(^) = Natural -> Natural -> Natural
forall a b. (Num a, Integral b) => a -> b -> a
(Haskell.^)

instance MultiplicativeMonoid Natural where
    one :: Natural
one = Natural
1

instance AdditiveSemigroup Natural where
    + :: Natural -> Natural -> Natural
(+) = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Haskell.+)

instance AdditiveMonoid Natural where
    zero :: Natural
zero = Natural
0

instance Semiring Natural

instance EuclideanDomain Natural where
    divMod :: Natural -> Natural -> (Natural, Natural)
divMod = Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
Haskell.divMod

instance BinaryExpansion Natural where
    binaryExpansion :: Natural -> [Natural]
binaryExpansion Natural
0 = []
    binaryExpansion Natural
x = (Natural
x Natural -> Natural -> Natural
forall a. EuclideanDomain a => a -> a -> a
`mod` Natural
2) Natural -> [Natural] -> [Natural]
forall a. a -> [a] -> [a]
: Natural -> [Natural]
forall a. BinaryExpansion a => a -> [a]
binaryExpansion (Natural
x Natural -> Natural -> Natural
forall a. EuclideanDomain a => a -> a -> a
`div` Natural
2)

(-!) :: Natural -> Natural -> Natural
-! :: Natural -> Natural -> Natural
(-!) = Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
(Haskell.-)

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup Integer where
    * :: Integer -> Integer -> Integer
(*) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(Haskell.*)

instance Exponent Integer Natural where
    ^ :: Integer -> Natural -> Integer
(^) = Integer -> Natural -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
(Haskell.^)

instance MultiplicativeMonoid Integer where
    one :: Integer
one = Integer
1

instance AdditiveSemigroup Integer where
    + :: Integer -> Integer -> Integer
(+) = Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(Haskell.+)

instance Scale Natural Integer

instance AdditiveMonoid Integer where
    zero :: Integer
zero = Integer
0

instance AdditiveGroup Integer where
    negate :: Integer -> Integer
negate = Integer -> Integer
forall a. Num a => a -> a
Haskell.negate

instance FromConstant Natural Integer where
    fromConstant :: Natural -> Integer
fromConstant = Natural -> Integer
forall a b. (Integral a, Num b) => a -> b
Haskell.fromIntegral

instance Semiring Integer

instance EuclideanDomain Integer where
    divMod :: Integer -> Integer -> (Integer, Integer)
divMod = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
Haskell.divMod

instance Ring Integer

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup Bool where
    * :: Bool -> Bool -> Bool
(*) = Bool -> Bool -> Bool
(&&)

instance (Semiring a, Eq a) => Exponent Bool a where
    Bool
x ^ :: Bool -> a -> Bool
^ a
p | a
p a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. AdditiveMonoid a => a
zero = Bool
forall a. MultiplicativeMonoid a => a
one
          | Bool
otherwise = Bool
x

instance MultiplicativeMonoid Bool where
    one :: Bool
one = Bool
True

instance MultiplicativeGroup Bool where
    invert :: Bool -> Bool
invert = Bool -> Bool
forall a. a -> a
id

instance AdditiveSemigroup Bool where
    + :: Bool -> Bool -> Bool
(+) = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=)

instance Scale Natural Bool

instance AdditiveMonoid Bool where
    zero :: Bool
zero = Bool
False

instance Scale Integer Bool

instance AdditiveGroup Bool where
    negate :: Bool -> Bool
negate = Bool -> Bool
forall a. a -> a
id

instance FromConstant Natural Bool where
    fromConstant :: Natural -> Bool
fromConstant = Natural -> Bool
forall a. Integral a => a -> Bool
odd

instance Semiring Bool

instance FromConstant Integer Bool where
    fromConstant :: Integer -> Bool
fromConstant = Integer -> Bool
forall a. Integral a => a -> Bool
odd

instance Ring Bool

instance BinaryExpansion Bool where
    binaryExpansion :: Bool -> [Bool]
binaryExpansion = (Bool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:[])

    fromBinary :: [Bool] -> Bool
fromBinary []  = Bool
False
    fromBinary [Bool
x] = Bool
x
    fromBinary [Bool]
_   = [Char] -> Bool
forall a. HasCallStack => [Char] -> a
error [Char]
"fromBits: This should never happen."

instance MultiplicativeMonoid a => Exponent a Bool where
    a
_ ^ :: a -> Bool -> a
^ Bool
False = a
forall a. MultiplicativeMonoid a => a
one
    a
x ^ Bool
True  = a
x

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup a => MultiplicativeSemigroup [a] where
    * :: [a] -> [a] -> [a]
(*) = (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
(*)

instance Exponent a b => Exponent [a] b where
    [a]
x ^ :: [a] -> b -> [a]
^ b
p = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
p) [a]
x

instance MultiplicativeMonoid a => MultiplicativeMonoid [a] where
    one :: [a]
one = a -> [a]
forall a. a -> [a]
repeat a
forall a. MultiplicativeMonoid a => a
one

instance MultiplicativeGroup a => MultiplicativeGroup [a] where
    invert :: [a] -> [a]
invert = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. MultiplicativeGroup a => a -> a
invert

instance AdditiveSemigroup a => AdditiveSemigroup [a] where
    + :: [a] -> [a] -> [a]
(+) = (a -> a -> a) -> [a] -> [a] -> [a]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
(+)

instance AdditiveMonoid a => AdditiveMonoid [a] where
    zero :: [a]
zero = a -> [a]
forall a. a -> [a]
repeat a
forall a. AdditiveMonoid a => a
zero

instance AdditiveGroup a => AdditiveGroup [a] where
    negate :: [a] -> [a]
negate = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map a -> a
forall a. AdditiveGroup a => a -> a
negate

instance FromConstant b a => FromConstant b [a] where
    fromConstant :: b -> [a]
fromConstant = a -> [a]
forall a. a -> [a]
repeat (a -> [a]) -> (b -> a) -> b -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance Semiring a => Semiring [a]

instance Ring a => Ring [a]

--------------------------------------------------------------------------------

instance MultiplicativeSemigroup a => MultiplicativeSemigroup (p -> a) where
    p -> a
p1 * :: (p -> a) -> (p -> a) -> p -> a
* p -> a
p2 = \p
x -> p -> a
p1 p
x a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* p -> a
p2 p
x

instance Exponent a b => Exponent (p -> a) b where
    p -> a
f ^ :: (p -> a) -> b -> p -> a
^ b
p = \p
x -> p -> a
f p
x a -> b -> a
forall a b. Exponent a b => a -> b -> a
^ b
p

instance MultiplicativeMonoid a => MultiplicativeMonoid (p -> a) where
    one :: p -> a
one = a -> p -> a
forall a b. a -> b -> a
const a
forall a. MultiplicativeMonoid a => a
one

instance MultiplicativeGroup a => MultiplicativeGroup (p -> a) where
    invert :: (p -> a) -> p -> a
invert = (a -> a) -> (p -> a) -> p -> a
forall a b. (a -> b) -> (p -> a) -> p -> b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. MultiplicativeGroup a => a -> a
invert

instance AdditiveSemigroup a => AdditiveSemigroup (p -> a) where
    p -> a
p1 + :: (p -> a) -> (p -> a) -> p -> a
+ p -> a
p2 = \p
x -> p -> a
p1 p
x a -> a -> a
forall a. AdditiveSemigroup a => a -> a -> a
+ p -> a
p2 p
x

instance AdditiveMonoid a => AdditiveMonoid (p -> a) where
    zero :: p -> a
zero = a -> p -> a
forall a b. a -> b -> a
const a
forall a. AdditiveMonoid a => a
zero

instance AdditiveGroup a => AdditiveGroup (p -> a) where
    negate :: (p -> a) -> p -> a
negate = (a -> a) -> (p -> a) -> p -> a
forall a b. (a -> b) -> (p -> a) -> p -> b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. AdditiveGroup a => a -> a
negate

instance FromConstant b a => FromConstant b (p -> a) where
    fromConstant :: b -> p -> a
fromConstant = a -> p -> a
forall a b. a -> b -> a
const (a -> p -> a) -> (b -> a) -> b -> p -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
forall a b. FromConstant a b => a -> b
fromConstant

instance Semiring a => Semiring (p -> a)

instance Ring a => Ring (p -> a)