-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A library of constructive algebra.
--   
--   A library of algebra focusing mainly on commutative ring theory from a
--   constructive point of view.
--   
--   Classical structures are implemented without Noetherian assumptions.
--   This means that it is not assumed that all ideals are finitely
--   generated. For example, instead of principal ideal domains one gets
--   Bezout domains which are integral domains in which all finitely
--   generated ideals are principal (and not necessarily that all ideals
--   are principal). This give a good framework for implementing many
--   interesting algorithms.
@package constructive-algebra
@version 0.3.0


-- | Type level characters. Used for representing the variable name in
--   univariate polynomials.
module Algebra.TypeChar.Char
data A_
data B_
data C_
data D_
data E_
data F_
data G_
data H_
data I_
data J_
data K_
data L_
data M_
data N_
data O_
data P_
data Q_
data R_
data S_
data T_
data U_
data V_
data W_
data X_
data Y_
data Z_
data A
data B
data C
data D
data E
data F
data G
data H
data I
data J
data K
data L
data M
data N
data O
data P
data Q
data R
data S
data T
data U
data V
data W
data X
data Y
data Z
instance Show Z
instance Show Y
instance Show X
instance Show W
instance Show V
instance Show U
instance Show T
instance Show S
instance Show R
instance Show Q
instance Show P
instance Show O
instance Show N
instance Show M
instance Show L
instance Show K
instance Show J
instance Show I
instance Show H
instance Show G
instance Show F
instance Show E
instance Show D
instance Show C
instance Show B
instance Show A
instance Show Z_
instance Show Y_
instance Show X_
instance Show W_
instance Show V_
instance Show U_
instance Show T_
instance Show S_
instance Show R_
instance Show Q_
instance Show P_
instance Show O_
instance Show N_
instance Show M_
instance Show L_
instance Show K_
instance Show J_
instance Show I_
instance Show H_
instance Show G_
instance Show F_
instance Show E_
instance Show D_
instance Show C_
instance Show B_
instance Show A_


-- | The representation of the ring structure.
module Algebra.Structures.Ring

-- | Definition of rings.
class Ring a
(<+>) :: Ring a => a -> a -> a
(<*>) :: Ring a => a -> a -> a
neg :: Ring a => a -> a
zero :: Ring a => a
one :: Ring a => a

-- | Addition is associative.
propAddAssoc :: (Ring a, Eq a) => a -> a -> a -> (Bool, String)

-- | Zero is the additive identity.
propAddIdentity :: (Ring a, Eq a) => a -> (Bool, String)

-- | Negation give the additive inverse.
propAddInv :: (Ring a, Eq a) => a -> (Bool, String)

-- | Addition is commutative.
propAddComm :: (Ring a, Eq a) => a -> a -> (Bool, String)

-- | Multiplication is associative.
propMulAssoc :: (Ring a, Eq a) => a -> a -> a -> (Bool, String)

-- | One is the multiplicative identity.
propMulIdentity :: (Ring a, Eq a) => a -> (Bool, String)

-- | Multiplication is right-distributive over addition.
propRightDist :: (Ring a, Eq a) => a -> a -> a -> (Bool, String)

-- | Multiplication is left-ditributive over addition.
propLeftDist :: (Ring a, Eq a) => a -> a -> a -> (Bool, String)

-- | Specification of rings. Test that the arguments satisfy the ring
--   axioms.
propRing :: (Ring a, Eq a) => a -> a -> a -> Property

-- | Subtraction
(<->) :: Ring a => a -> a -> a

-- | Exponentiation
(<^>) :: Ring a => a -> Integer -> a

-- | Summation
sumRing :: Ring a => [a] -> a

-- | Product
productRing :: Ring a => [a] -> a


-- | Structure for commutative rings.
module Algebra.Structures.CommutativeRing

-- | Definition of commutative rings.
class Ring a => CommutativeRing a
propMulComm :: (CommutativeRing a, Eq a) => a -> a -> Bool

-- | Specification of commutative rings. Test that multiplication is
--   commutative and that it satisfies the ring axioms.
propCommutativeRing :: (CommutativeRing a, Eq a) => a -> a -> a -> Property

module Algebra.Structures.Group
class Group a
(<+>) :: Group a => a -> a -> a
zero :: Group a => a
neg :: Group a => a -> a
propAssoc :: (Group a, Eq a) => a -> a -> a -> Bool
propId :: (Group a, Eq a) => a -> Bool
propInv :: (Group a, Eq a) => a -> Bool
propGroup :: (Group a, Eq a) => a -> a -> a -> Property

-- | Abelian groups:
class Group a => AbelianGroup a
propComm :: (AbelianGroup a, Eq a) => a -> a -> Bool
propAbelianGroup :: (AbelianGroup a, Eq a) => a -> a -> a -> Property
sumGroup :: AbelianGroup a => [a] -> a
instance (Group a, Ring a) => AbelianGroup a
instance Ring a => Group a
instance (Group a, Group b) => Group (a, b)


-- | Finitely generated ideals in commutative rings.
module Algebra.Ideal

-- | Ideals characterized by their list of generators.
data CommutativeRing a => Ideal a
Id :: [a] -> Ideal a

-- | The zero ideal.
zeroIdeal :: CommutativeRing a => Ideal a

-- | Test if an ideal is principal.
isPrincipal :: CommutativeRing a => Ideal a -> Bool
fromId :: CommutativeRing a => Ideal a -> [a]

-- | Evaluate the ideal at a certain point.
eval :: CommutativeRing a => a -> Ideal a -> a

-- | Addition of ideals.
addId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Multiplication of ideals.
mulId :: (CommutativeRing a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Test if an operations compute the correct ideal. The operation should
--   give a witness that the comuted ideal contains the same elements.
--   
--   If [ x_1, ..., x_n ] `op` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]
--   
--   Then the witness should give that
--   
--   z_k = a_k1 * x_1 + ... + a_kn * x_n = b_k1 * y_1 + ... + b_km * y_m
--   
--   This is used to check that the intersection computed is correct.
isSameIdeal :: (CommutativeRing a, Eq a) => (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Ideal a -> Ideal a -> Bool

-- | Compute witnesses for two lists for the zero ideal. This is used when
--   computing the intersection of two ideals.
zeroIdealWitnesses :: CommutativeRing a => [a] -> [a] -> (Ideal a, [[a]], [[a]])
instance (CommutativeRing a, Arbitrary a, Eq a) => Arbitrary (Ideal a)
instance (CommutativeRing a, Show a) => Show (Ideal a)

module Algebra.Structures.StronglyDiscrete

-- | Strongly discrete rings
--   
--   A ring is called strongly discrete if ideal membership is decidable.
--   Nothing correspond to that x is not in the ideal and Just is the
--   witness. Examples include all Bezout domains and polynomial rings.
class Ring a => StronglyDiscrete a
member :: StronglyDiscrete a => a -> Ideal a -> Maybe [a]

-- | Test that the witness is actually a witness that the element is in the
--   ideal.
propStronglyDiscrete :: (CommutativeRing a, StronglyDiscrete a, Eq a) => a -> Ideal a -> Bool

module Algebra.Structures.IntegralDomain

-- | Definition of integral domains.
class CommutativeRing a => IntegralDomain a
propZeroDivisors :: (IntegralDomain a, Eq a) => a -> a -> Bool

-- | Specification of integral domains. Test that there are no
--   zero-divisors and that it satisfies the axioms of commutative rings.
propIntegralDomain :: (IntegralDomain a, Eq a) => a -> a -> a -> Property


-- | Representation of Euclidean domains. That is integral domains with an
--   Euclidean functions and decidable division.
module Algebra.Structures.EuclideanDomain

-- | Euclidean domains
--   
--   Given a and b compute (q,r) such that a = bq + r and r = 0 || norm r
--   &lt; norm b. Where norm is the Euclidean function.
class IntegralDomain a => EuclideanDomain a
norm :: EuclideanDomain a => a -> Integer
quotientRemainder :: EuclideanDomain a => a -> a -> (a, a)

-- | Check both that |a| <a>= |ab| and |a| </a>= 0 for all a,b.
propNorm :: (EuclideanDomain a, Eq a) => a -> a -> Bool
propQuotRem :: (EuclideanDomain a, Eq a) => a -> a -> Bool
propEuclideanDomain :: (EuclideanDomain a, Eq a) => a -> a -> a -> Property
modulo :: EuclideanDomain a => a -> a -> a
quotient :: EuclideanDomain a => a -> a -> a
divides :: (EuclideanDomain a, Eq a) => a -> a -> Bool

-- | The Euclidean algorithm for calculating the GCD of a and b.
euclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> a

-- | Generalized Euclidean algorithm to compute GCD of a list of elements.
genEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> a

-- | Lowest common multiple, (a*b)/gcd(a,b).
lcmE :: (EuclideanDomain a, Eq a) => a -> a -> a

-- | Generalized lowest common multiple to compute lcm of a list of
--   elements.
genLcmE :: (EuclideanDomain a, Eq a) => [a] -> a

-- | The extended Euclidean algorithm.
--   
--   Computes x and y in ax + by = gcd(a,b).
extendedEuclidAlg :: (EuclideanDomain a, Eq a) => a -> a -> (a, a)

-- | Generalized extended Euclidean algorithm.
--   
--   Solves a_1 x_1 + ... + a_n x_n = gcd (a_1,...,a_n)
genExtendedEuclidAlg :: (EuclideanDomain a, Eq a) => [a] -> [a]


-- | Structure for fields.
module Algebra.Structures.Field

-- | Definition of fields.
class IntegralDomain a => Field a
inv :: Field a => a -> a
propMulInv :: (Field a, Eq a) => a -> Bool

-- | Specification of fields. Test that the multiplicative inverses behave
--   as expected and that it satisfies the axioms of integral domains.
propField :: (Field a, Eq a) => a -> a -> a -> Property

-- | Division
(</>) :: Field a => a -> a -> a


-- | A small simple matrix library.
module Algebra.Matrix

-- | Row vectors
newtype Vector r
Vec :: [r] -> Vector r
unVec :: Vector r -> [r]
lengthVec :: Vector r -> Int

-- | Matrices
newtype Matrix r
M :: [Vector r] -> Matrix r

-- | Construct a mxn matrix.
matrix :: [[r]] -> Matrix r
matrixToVector :: Matrix r -> Vector r
vectorToMatrix :: Vector r -> Matrix r
unMVec :: Matrix r -> [[r]]
unM :: Matrix r -> [Vector r]
(!!!) :: Matrix a -> (Int, Int) -> a

-- | Construct a nxn identity matrix.
identity :: IntegralDomain r => Int -> Matrix r
propLeftIdentity :: (IntegralDomain r, Eq r) => Matrix r -> Bool
propRightIdentity :: (IntegralDomain r, Eq r) => Matrix r -> Bool

-- | Matrix multiplication.
mulM :: Ring r => Matrix r -> Matrix r -> Matrix r

-- | Matrix addition.
addM :: Ring r => Matrix r -> Matrix r -> Matrix r

-- | Transpose a matrix.
transpose :: Matrix r -> Matrix r
isSquareMatrix :: Matrix r -> Bool

-- | Compute the dimension of a matrix.
dimension :: Matrix r -> (Int, Int)

-- | Scale a row in a matrix.
scale :: CommutativeRing a => Matrix a -> Int -> a -> Matrix a

-- | Swap two rows of a matrix.
swap :: Matrix a -> Int -> Int -> Matrix a
pivot :: CommutativeRing a => Matrix a -> a -> Int -> Int -> Matrix a
addRow :: CommutativeRing a => Matrix a -> Vector a -> Int -> Matrix a
subRow :: CommutativeRing a => Matrix a -> Vector a -> Int -> Matrix a
addCol :: CommutativeRing a => Matrix a -> Vector a -> Int -> Matrix a
subCol :: CommutativeRing a => Matrix a -> Vector a -> Int -> Matrix a
findPivot :: (CommutativeRing a, Eq a) => Matrix a -> (Int, Int) -> Maybe (a, Int)

-- | Compute row echelon form of a system Ax=b.
forwardElim :: (Field a, Eq a) => (Matrix a, Vector a) -> (Matrix a, Vector a)

-- | Gauss-Jordan elimination: Given A and B solve Ax=B.
gaussElim :: (Field a, Eq a, Show a) => (Matrix a, Vector a) -> (Matrix a, Vector a)
gaussElimCorrect :: (Field a, Eq a, Arbitrary a, Show a) => (Matrix a, Vector a) -> Property
instance Eq r => Eq (Vector r)
instance Eq r => Eq (Matrix r)
instance Functor Matrix
instance Arbitrary r => Arbitrary (Matrix r)
instance Show r => Show (Matrix r)
instance Functor Vector
instance Arbitrary r => Arbitrary (Vector r)
instance Show r => Show (Vector r)


-- | Representation of coherent rings. Traditionally a ring is coherent if
--   every finitely generated ideal is finitely presented. This means that
--   it is possible to solve homogenous linear equations in them.
module Algebra.Structures.Coherent

-- | Definition of coherent rings.
--   
--   We say that R is coherent iff for any M, we can find L such that ML=0
--   and
--   
--   MX=0 &lt;-&gt; exists Y. X=LY
--   
--   that is, iff we can generate the solutions of any linear homogeous
--   system of equations.
--   
--   The main point here is that ML=0, it is not clear how to represent the
--   equivalence in Haskell. This would probably be possible in type
--   theory.
class IntegralDomain a => Coherent a
solve :: Coherent a => Vector a -> Matrix a
propCoherent :: (Coherent a, Eq a) => Vector a -> Bool

-- | Test that the second matrix is a solution to the first.
isSolution :: (CommutativeRing a, Eq a) => Matrix a -> Matrix a -> Bool

-- | Solves a system of equations.
solveMxN :: (Coherent a, Eq a) => Matrix a -> Matrix a

-- | Test that the solution of an MxN system is in fact a solution of the
--   system
propSolveMxN :: (Coherent a, Eq a) => Matrix a -> Bool

-- | Intersection computable -&gt; Coherence.
--   
--   Proof that if there is an algorithm to compute a f.g. set of
--   generators for the intersection of two f.g. ideals then the ring is
--   coherent.
--   
--   Takes the vector to solve, [x1,...,xn], and a function (int) that
--   computes the intersection of two ideals.
--   
--   If [ x_1, ..., x_n ] `int` [ y_1, ..., y_m ] = [ z_1, ..., z_l ]
--   
--   then int should give witnesses us and vs such that:
--   
--   z_k = n_k1 * x_1 + ... + u_kn * x_n = u_k1 * y_1 + ... + n_km * y_m
solveWithIntersection :: (IntegralDomain a, Eq a) => Vector a -> (Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])) -> Matrix a

-- | Strongly discrete coherent rings.
--   
--   If the ring is strongly discrete and coherent then we can solve
--   arbitrary equations of the type AX=b.
solveGeneralEquation :: (Coherent a, StronglyDiscrete a) => Vector a -> a -> Maybe (Matrix a)
propSolveGeneralEquation :: (Coherent a, StronglyDiscrete a, Eq a) => Vector a -> a -> Bool

-- | Solves general linear systems of the kind AX = B.
--   
--   A is given as a matrix and B is given as a row vector (it should be
--   column vector).
solveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Maybe (Matrix a, Matrix a)
propSolveGeneral :: (Coherent a, StronglyDiscrete a, Eq a) => Matrix a -> Vector a -> Property


-- | Representation of Bezout domains. That is non-Noetherian analogues of
--   principal ideal domains. This means that all finitely generated ideals
--   are principal.
module Algebra.Structures.BezoutDomain

-- | Bezout domains
--   
--   Has a Bezout function which given a and b give g, a1, b1, x and y such
--   that:
--   
--   <ul>
--   <li>g = gcd(a,b)</li>
--   <li>a = g * a1 and b = g * b1</li>
--   <li>g = a * x + b * y</li>
--   </ul>
class IntegralDomain a => BezoutDomain a
bezout :: BezoutDomain a => a -> a -> (a, a, a, a, a)
propBezoutDomain :: (BezoutDomain a, Eq a) => a -> a -> Property

-- | Compute a principal ideal from another ideal. Also give witness that
--   the principal ideal is equal to the first ideal.
--   
--   toPrincipal &lt;a_1,...,a_n&gt; = (&lt;a&gt;,u_i,v_i) where
--   
--   sum (u_i * a_i) = a
--   
--   a_i = v_i * a
toPrincipal :: BezoutDomain a => Ideal a -> (Ideal a, [a], [a])

-- | Test that the generated ideal is principal.
propToPrincipal :: (BezoutDomain a, Eq a) => Ideal a -> Bool

-- | Test that the generated ideal generate the same elements as the given.
propIsSameIdeal :: (BezoutDomain a, Eq a) => Ideal a -> Bool
gcdB :: BezoutDomain a => a -> a -> a

-- | Intersection without witness.
intersectionB :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Intersection of ideals with witness.
--   
--   If one of the ideals is the zero ideal then the intersection is the
--   zero ideal.
intersectionBWitness :: (BezoutDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])

-- | Coherence of Bezout domains.
solveB :: (BezoutDomain a, Eq a) => Vector a -> Matrix a

-- | Chinese remainder theorem
--   
--   Given a_1,...,a_n and m_1,...,m_n such that gcd(m_i,m_j) = 1. Let m =
--   m_1*...*m_n compute a such that:
--   
--   <ol>
--   <li>a = a_i (mod m_i)</li>
--   <li>If b is such that b = a_i (mod m_i) then a = b (mod m)</li>
--   </ol>
--   
--   The function return (a,m).
crt :: (BezoutDomain a, Eq a) => [a] -> [a] -> (a, a)
instance (BezoutDomain a, Eq a) => StronglyDiscrete a
instance (EuclideanDomain a, Eq a) => BezoutDomain a


-- | Greatest common divisor (GCD) domains.
--   
--   GCD domains are integral domains in which every pair of nonzero
--   elements have a greatest common divisor. They can also be
--   characterized as non-Noetherian analogues of unique factorization
--   domains.
module Algebra.Structures.GCDDomain

-- | GCD domains
class IntegralDomain a => GCDDomain a
gcd' :: GCDDomain a => a -> a -> (a, a, a)
propGCD :: (GCDDomain a, Eq a) => a -> a -> Bool

-- | Specification of GCD domains. They are integral domains in which every
--   pair of nonzero elements have a greatest common divisor.
propGCDDomain :: (Eq a, GCDDomain a, Arbitrary a, Show a) => a -> a -> a -> Property
ggcd :: GCDDomain a => [a] -> a
instance BezoutDomain a => GCDDomain a


-- | Structure of rings with explicit units.
module Algebra.Structures.ExplicitUnits

-- | A ring has explicit units if there is a function that can test if an
--   element is invertible and if this is the case give the inverse.
class IntegralDomain a => ExplicitUnits a
unit :: ExplicitUnits a => a -> Maybe a
propUnit :: (ExplicitUnits a, Eq a) => a -> Bool

-- | An element is a unit if it is invertible.
isUnit :: ExplicitUnits a => a -> Bool

-- | Decidable units is sufficient to decide divisibility in GCD domains.
(%|) :: (ExplicitUnits a, GCDDomain a) => a -> a -> Bool

-- | Test for associatedness, i.e. a ~ b iff a | b /\ b | a.
(~=) :: (ExplicitUnits a, GCDDomain a) => a -> a -> Bool


-- | The field of fractions over a GCD domain. The reason that it is an GCD
--   domain is that we only want to work over reduced quotients.
module Algebra.Structures.FieldOfFractions

-- | Field of fractions
newtype GCDDomain a => FieldOfFractions a
F :: (a, a) -> FieldOfFractions a
numerator :: GCDDomain a => FieldOfFractions a -> a
denominator :: GCDDomain a => FieldOfFractions a -> a

-- | Embed a value in the field of fractions.
toFieldOfFractions :: GCDDomain a => a -> FieldOfFractions a

-- | Extract a value from the field of fractions. This is only possible if
--   the divisor is one.
fromFieldOfFractions :: (GCDDomain a, Eq a) => FieldOfFractions a -> a

-- | Reduce an element.
reduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> FieldOfFractions a
propReduce :: (GCDDomain a, Eq a) => FieldOfFractions a -> Property
instance (GCDDomain a, Eq a) => Field (FieldOfFractions a)
instance (GCDDomain a, Eq a) => IntegralDomain (FieldOfFractions a)
instance (GCDDomain a, Eq a) => CommutativeRing (FieldOfFractions a)
instance (GCDDomain a, Eq a) => Ring (FieldOfFractions a)
instance (GCDDomain a, Eq a) => Eq (FieldOfFractions a)
instance (GCDDomain a, Eq a, Arbitrary a) => Arbitrary (FieldOfFractions a)
instance (GCDDomain a, Show a, Eq a) => Show (FieldOfFractions a)


-- | Prufer domains are non-Noetherian analogues of Dedekind domains. That
--   is integral domains in which every finitely generated ideal is
--   invertible. This implementation is mainly based on:
--   
--   http://hlombardi.free.fr/liens/salouThesis.pdf
module Algebra.Structures.PruferDomain

-- | Given a and b it computes u, v and we such that:
--   
--   <ol>
--   <li>au = bv</li>
--   <li>b(1-u) = aw</li>
--   </ol>
class IntegralDomain a => PruferDomain a
calcUVW :: PruferDomain a => a -> a -> (a, a, a)

-- | Property specifying that: au = bv and b(1-u) = aw
propCalcUVW :: (PruferDomain a, Eq a) => a -> a -> Bool
propPruferDomain :: (PruferDomain a, Eq a) => a -> a -> a -> Property

-- | Bezout domain -&gt; Prufer domain
--   
--   Proof that all Bezout domains are Prufer domains.
calcUVW_B :: (BezoutDomain a, Eq a) => a -> a -> (a, a, a)

-- | Alternative characterization of Prufer domains, given a and b compute
--   u, v, w, t such that:
--   
--   ua = vb &amp;&amp; wa = tb &amp;&amp; u+t = 1
calcUVWT :: PruferDomain a => a -> a -> (a, a, a, a)
propCalcUVWT :: (PruferDomain a, Eq a) => a -> a -> Bool

-- | Go back to the original definition.
fromUVWTtoUVW :: (a, a, a, a) -> (a, a, a)

-- | Compute a principal localization matrix for an ideal in a Prufer
--   domain.
computePLM_PD :: (PruferDomain a, Eq a) => Ideal a -> Matrix a

-- | Ideal inversion. Given I compute J such that IJ is principal. Uses the
--   principal localization matrix for the ideal.
invertIdeal :: (PruferDomain a, Eq a) => Ideal a -> Ideal a
intersectionPD :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> Ideal a

-- | Compute the intersection of I and J by:
--   
--   (I \cap J)(I + J) = IJ =&gt; (I \cap J)(I + J)(I + J)' = IJ(I + J)'
intersectionPDWitness :: (PruferDomain a, Eq a) => Ideal a -> Ideal a -> (Ideal a, [[a]], [[a]])

-- | Coherence of Prufer domains.
solvePD :: (PruferDomain a, Eq a) => Vector a -> Matrix a


-- | Specification of principal localization matrices used in the coherence
--   proof of Prufer domains.
module Algebra.PLM

-- | A principal localization matrix for an ideal (x1,...,xn) is a matrix
--   such that:
--   
--   <ul>
--   <li>The sum of the diagonal should equal 1.</li>
--   <li>For all i, j, l in {1..n}: a_lj * x_i = a_li * x_j</li>
--   </ul>
propPLM :: (CommutativeRing a, Eq a) => Ideal a -> Matrix a -> Bool

-- | Principal localization matrices for ideals are computable in Bezout
--   domains.
computePLM_B :: (BezoutDomain a, Eq a) => Ideal a -> Matrix a

module Algebra.Z

-- | Type synonym for integers.
type Z = Integer

-- | Definition of integral domains.
class CommutativeRing a => IntegralDomain a
instance PruferDomain Z
instance Coherent Z
instance EuclideanDomain Z
instance ExplicitUnits Z
instance IntegralDomain Z
instance CommutativeRing Z
instance Ring Z


-- | Integers modulo n parametrised by the n. This also has type-level
--   primality testing used for instantiating integral domain and field
--   type classes. The primality testing is very slow, but it seem to be
--   working fine for relatively small numbers.
module Algebra.Zn

-- | The phantom type n represents which modulo to work in.
newtype Zn n
Zn :: Integer -> Zn n
type Z3 = Zn D3
instance Eq (Zn n)
instance Ord (Zn n)
instance Pos x => IsZero (x :* d) False
instance IsZero D9 False
instance IsZero D8 False
instance IsZero D7 False
instance IsZero D6 False
instance IsZero D5 False
instance IsZero D4 False
instance IsZero D3 False
instance IsZero D2 False
instance IsZero D1 False
instance IsZero D0 True
instance (Pred y z, Trich z D1 r1, Mod x y rest, IsZero rest b1, Not b1 b', Prime' x z r1 b2, And b' b2 b3) => Prime' x y GT b3
instance Prime' x D1 EQ True
instance (Sqrt x y, Trich y D1 r, Prime' x y r b) => Prime x b
instance (ExpBase y D2 square, Succ y y', Trich x square r, Sqrt' x y' r sqrt) => Sqrt' x y GT sqrt
instance Pred y y' => Sqrt' x y EQ y'
instance Sub y D2 y' => Sqrt' x y LT y'
instance (Nat x, Nat sqrt, Sqrt' x D1 GT sqrt) => Sqrt x sqrt
instance (Prime n True, Nat n) => Field (Zn n)
instance (Prime n True, Nat n) => IntegralDomain (Zn n)
instance Nat n => CommutativeRing (Zn n)
instance Nat n => Ring (Zn n)
instance Nat n => Arbitrary (Zn n)
instance Nat n => Num (Zn n)
instance Show (Zn n)


-- | R-modules.
module Algebra.Structures.Module

-- | Module over a commutative ring r.
class (CommutativeRing r, AbelianGroup m) => Module r m
(*>) :: Module r m => r -> m -> m

-- | Since the ring is commutative we can turn the scalar multiplication
--   around.
(<*) :: Module r m => m -> r -> m
propScalarMul :: (Module r m, Eq m) => r -> m -> m -> Bool
propScalarAdd :: (Module r m, Eq m) => r -> r -> m -> Bool
propScalarAssoc :: (Module r m, Eq m) => r -> r -> m -> Bool
propModule :: (Module r m, Eq m) => r -> r -> m -> m -> Property
instance AbelianGroup m => Module Z m


-- | Representation of rational numbers as the field of fractions of Z.
module Algebra.Q

-- | Q is the field of fractions of Z.
type Q = FieldOfFractions Z
toQ :: Z -> Q
toZ :: Q -> Z
instance ExplicitUnits Q
instance Fractional Q
instance Num Q


-- | Univariate polynomials parametrised by the variable name.
module Algebra.UPoly

-- | Polynomials over a commutative ring, indexed by a phantom type x that
--   denote the name of the variable that the polynomial is over. For
--   example UPoly Q X_ is Q[x] and UPoly Q T_ is Q[t].
newtype CommutativeRing r => UPoly r x
UP :: [r] -> UPoly r x

-- | The degree of the polynomial.
deg :: CommutativeRing r => UPoly r x -> Integer

-- | Useful shorthand for Q[x].
type Qx = UPoly Q X_

-- | The variable x in Q[x].
x :: Qx

-- | Take a list and construct a polynomial by removing all zeroes in the
--   end.
toUPoly :: (CommutativeRing r, Eq r) => [r] -> UPoly r x

-- | Take an element of the ring and the degree of the desired monomial,
--   for example: monomial 3 7 = 3x^7
monomial :: CommutativeRing r => r -> Integer -> UPoly r x

-- | Compute the leading term of a polynomial.
lt :: CommutativeRing r => UPoly r x -> r

-- | Formal derivative of polynomials in k[x].
deriv :: CommutativeRing r => UPoly r x -> UPoly r x

-- | Compute the content of a polynomial, i.e. the gcd of the coefficients.
cont :: (GCDDomain a, Eq a) => UPoly a x -> a

-- | If all coefficients are relatively prime then the polynomial is
--   primitive.
isPrimitive :: (ExplicitUnits a, GCDDomain a, Eq a) => UPoly a x -> Bool

-- | Lemma 4.2: Given a polynomial p in K[x] where K=Quot(A) we can find c
--   in K and q primitive in A[x] such that p = cq.
toPrimitive :: (GCDDomain a, Eq a) => UPoly (FieldOfFractions a) x -> (FieldOfFractions a, UPoly a x)
propToPrimitive :: (ExplicitUnits a, GCDDomain a, Eq a) => UPoly (FieldOfFractions a) x -> Property

-- | Gauss lemma says that if p and q are polynomials over a GCD domain
--   then cont(pq) = cont(p) * cont(q).
gaussLemma :: (ExplicitUnits a, GCDDomain a, Eq a) => UPoly a x -> UPoly a x -> Property

-- | Proof that if A is a GCD domain then A[x] also is a GCD domain. This
--   also computes witnesses that the computed GCD divides the given
--   polynomials.
gcdUPolyWitness :: (GCDDomain a, Eq a) => UPoly a x -> UPoly a x -> (UPoly a x, UPoly a x, UPoly a x)

-- | Square free decomposition of a polynomial.
sqfr :: (Num k, Field k) => UPoly k x -> UPoly k x

-- | Distinct power factorization, aka square free decomposition
sqfrDec :: (Num k, Field k) => UPoly k x -> [UPoly k x]
instance Eq r => Eq (UPoly r x)
instance Ord r => Ord (UPoly r x)
instance (ExplicitUnits a, Eq a) => ExplicitUnits (UPoly a x)
instance (Field k, Eq k) => PruferDomain (UPoly k x)
instance (Field k, Eq k) => EuclideanDomain (UPoly k x)
instance (CommutativeRing r, Eq r) => IntegralDomain (UPoly r x)
instance (CommutativeRing r, Eq r) => CommutativeRing (UPoly r x)
instance (Show r, Field r, Num r, Show x) => Num (UPoly r x)
instance (CommutativeRing r, Eq r) => Ring (UPoly r x)
instance (CommutativeRing r, Eq r, Arbitrary r) => Arbitrary (UPoly r x)
instance (CommutativeRing r, Eq r, Show r, Show x) => Show (UPoly r x)


-- | The field of rational functions is the field of fractions of k[x].
module Algebra.FieldOfRationalFunctions

-- | Field of rational functions.
type FieldOfRationalFunctions k x = FieldOfFractions (UPoly k x)

-- | The field of fraction of Q[x].
type QX = FieldOfRationalFunctions Q X_
toQX :: Qx -> QX
toQx :: QX -> Qx
instance (Show k, Field k, Num k, Show x) => Num (FieldOfRationalFunctions k x)


-- | The elliptic curve y^2 = 1 - x^4 in Q[x,y].
module Algebra.EllipticCurve

-- | The elliptic curve y^2=1-x^4 over Q[x,y].
newtype EllipticCurve
C :: (Qx, Qx) -> EllipticCurve
instance Eq EllipticCurve
instance Arbitrary EllipticCurve
instance Coherent EllipticCurve
instance PruferDomain EllipticCurve
instance IntegralDomain EllipticCurve
instance CommutativeRing EllipticCurve
instance Ring EllipticCurve
instance Show EllipticCurve


-- | Proof that Z[sqrt(-5)] is a Prufer domain. This implies that it is
--   possible to solve systems of equations over Z[sqrt(-5)].
module Algebra.ZSqrt5

-- | Z[sqrt(-5)] is a pair such that (a,b) = a + b*sqrt(-5)
newtype ZSqrt5
ZSqrt5 :: (Z, Z) -> ZSqrt5
instance Eq ZSqrt5
instance Ord ZSqrt5
instance Arbitrary ZSqrt5
instance Coherent ZSqrt5
instance PruferDomain ZSqrt5
instance IntegralDomain ZSqrt5
instance CommutativeRing ZSqrt5
instance Ring ZSqrt5
instance Show ZSqrt5