--Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd.
--All rights reserved.
--
--Redistribution and use in source and binary forms, with or without
--modification, are permitted provided that the following conditions are
--met:
--
--    - Redistributions of source code must retain the above copyright
--      notice, this list of conditions and the following disclaimer.
--
--    - Redistributions in binary form must reproduce the above copyright
--      notice, this list of conditions and the following disclaimer in
--      the documentation and/or other materials provided with the
--      distribution.
--
--    - Neither the name of The Numerical ALgorithms Group Ltd. nor the
--      names of its contributors may be used to endorse or promote products
--      derived from this software without specific prior written permission.
--
--THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
--IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
--TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
--PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
--OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
--EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
--PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
--PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
--LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
--NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
--SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

)abbrev domain MODRING ModularRing
++ Author: P.Gianni, B.Trager
++ Date Created:
++ Date Last Updated:
++ Basic Functions:
++ Related Constructors:
++ Also See:
++ AMS Classifications:
++ Keywords:
++ References:
++ Description:
++ These domains are used for the factorization and gcds
++ of univariate polynomials over the integers in order to work modulo
++ different  primes.
++ See \spadtype{EuclideanModularRing} ,\spadtype{ModularField}

ModularRing(R,Mod,reduction:(R,Mod) -> R,
               merge:(Mod,Mod) -> Union(Mod,"failed"),
                      exactQuo : (R,R,Mod) -> Union(R,"failed")) : C == T
 where
  R    :  CommutativeRing
  Mod  :  AbelianMonoid

  C == Ring with
                modulus :   %     -> Mod
			++ modulus(x) \undocumented
                coerce  :   %     -> R
			++ coerce(x) \undocumented
                reduce  : (R,Mod) -> %
			++ reduce(r,m) \undocumented
                exQuo   :  (%,%)  -> Union(%,"failed")
			++ exQuo(x,y) \undocumented
                recip   :    %    -> Union(%,"failed")
			++ recip(x) \undocumented
                inv     :    %    -> %
			++ inv(x) \undocumented

  T == add
    --representation
      Rep:= Record(val:R,modulo:Mod)
    --declarations
      x,y: %

    --define
      modulus(x)   == x.modulo
      coerce(x: %): R == x.val
      coerce(i:Integer):% == [i::R,0]$Rep
      i:Integer * x:% == (i::%)*x
      coerce(x):OutputForm == (x.val)::OutputForm
      reduce (a:R,m:Mod) == [reduction(a,m),m]$Rep

      characteristic:NonNegativeInteger == characteristic$R
      0 == [0$R,0$Mod]$Rep
      1 == [1$R,0$Mod]$Rep
      zero? x == zero? x.val
      one? x == one? x.val

      newmodulo(m1:Mod,m2:Mod) : Mod ==
        r:=merge(m1,m2)
        r case "failed" => error "incompatible moduli"
        r::Mod

      x=y ==
        x.val = y.val => true
        x.modulo = y.modulo => false
        (x-y).val = 0
      x+y == reduce((x.val +$R y.val),newmodulo(x.modulo,y.modulo))
      x-y == reduce((x.val -$R y.val),newmodulo(x.modulo,y.modulo))
      -x  == reduce ((-$R x.val),x.modulo)
      x*y == reduce((x.val *$R y.val),newmodulo(x.modulo,y.modulo))

      exQuo(x,y) ==
        xm:=x.modulo
        if xm ~=$Mod y.modulo then xm:=newmodulo(xm,y.modulo)
        r:=exactQuo(x.val,y.val,xm)
        r case "failed"=> "failed"
        [r::R,xm]$Rep

      --if R has EuclideanDomain then
      recip x ==
        r:=exactQuo(1$R,x.val,x.modulo)
        r case "failed" => "failed"
        [r,x.modulo]$Rep

      inv x ==
        if (u:=recip x) case "failed" then error("not invertible")
        else u::%

)abbrev domain EMR EuclideanModularRing
++ Description:
++ These domains are used for the factorization and gcds
++ of univariate polynomials over the integers in order to work modulo
++ different  primes.
++ See \spadtype{ModularRing}, \spadtype{ModularField}
EuclideanModularRing(S,R,Mod,reduction:(R,Mod) -> R,
                     merge:(Mod,Mod) -> Union(Mod,"failed"),
                      exactQuo : (R,R,Mod) -> Union(R,"failed")) : C == T
 where
  S    :  CommutativeRing
  R    :  UnivariatePolynomialCategory S
  Mod  :  AbelianMonoid

  C == Join(EuclideanDomain, Eltable(R,R)) with
                modulus :   %     -> Mod
			++ modulus(x) \undocumented
                coerce  :   %     -> R
			++ coerce(x) \undocumented
                reduce  : (R,Mod) -> %
			++ reduce(r,m) \undocumented
                exQuo   :  (%,%)  -> Union(%,"failed")
			++ exQuo(x,y) \undocumented
                recip   :    %    -> Union(%,"failed")
			++ recip(x) \undocumented
                inv     :    %    -> %
			++ inv(x) \undocumented

  T == ModularRing(R,Mod,reduction,merge,exactQuo) add

    --representation
      Rep:= Record(val:R,modulo:Mod)
    --declarations
      x,y,z: %

      divide(x,y) ==
        t:=merge(x.modulo,y.modulo)
        t case "failed" => error "incompatible moduli"
        xm:=t::Mod
        yv:=y.val
        invlcy:R
        if one? leadingCoefficient yv then invlcy:=1
        else
          invlcy:=(inv reduce((leadingCoefficient yv)::R,xm)).val
          yv:=reduction(invlcy*yv,xm)
        r:=monicDivide(x.val,yv)
        [reduce(invlcy*r.quotient,xm),reduce(r.remainder,xm)]

      if R has fmecg:(R,NonNegativeInteger,S,R)->R
         then x rem y  ==
           t:=merge(x.modulo,y.modulo)
           t case "failed" => error "incompatible moduli"
           xm:=t::Mod
           yv:=y.val
           invlcy:R
           if not one? leadingCoefficient yv then
             invlcy:=(inv reduce((leadingCoefficient yv)::R,xm)).val
             yv:=reduction(invlcy*yv,xm)
           dy:=degree yv
           xv:=x.val
           while (d:=degree xv - dy)>=0 repeat
                 xv:=reduction(fmecg(xv,d::NonNegativeInteger,
                                     leadingCoefficient xv,yv),xm)
                 xv = 0 => return [xv,xm]$Rep
           [xv,xm]$Rep
         else x rem y  == 
           t:=merge(x.modulo,y.modulo)
           t case "failed" => error "incompatible moduli"
           xm:=t::Mod
           yv:=y.val
           invlcy:R
           if not one? leadingCoefficient yv then
             invlcy:=(inv reduce((leadingCoefficient yv)::R,xm)).val
             yv:=reduction(invlcy*yv,xm)
           r:=monicDivide(x.val,yv)
           reduce(r.remainder,xm)

      euclideanSize x == degree x.val

      unitCanonical x ==
        zero? x => x
        degree(x.val) = 0 => 1
        one? leadingCoefficient(x.val) => x
        invlcx:%:=inv reduce((leadingCoefficient(x.val))::R,x.modulo)
        invlcx * x

      unitNormal x ==
        zero?(x) or one?(leadingCoefficient(x.val)) => [1, x, 1]
        lcx := reduce((leadingCoefficient(x.val))::R,x.modulo)
        invlcx:=inv lcx
        degree(x.val) = 0 => [lcx, 1, invlcx]
        [lcx, invlcx * x, invlcx]

      elt(x : %,s : R) : R == reduction(elt(x.val,s),x.modulo)

)abbrev domain MODFIELD ModularField
++ These domains are used for the factorization and gcds
++ of univariate polynomials over the integers in order to work modulo
++ different  primes.
++ See \spadtype{ModularRing}, \spadtype{EuclideanModularRing} 
ModularField(R,Mod,reduction:(R,Mod) -> R,
               merge:(Mod,Mod) -> Union(Mod,"failed"),
                      exactQuo : (R,R,Mod) -> Union(R,"failed")) : C == T
 where
  R    :  CommutativeRing
  Mod  :  AbelianMonoid

  C == Field with
                modulus :   %     -> Mod
			++ modulus(x) \undocumented
                coerce  :   %     -> R
			++ coerce(x) \undocumented
                reduce  : (R,Mod) -> %
			++ reduce(r,m) \undocumented
                exQuo   :  (%,%)  -> Union(%,"failed")
			++ exQuo(x,y) \undocumented

  T == ModularRing(R,Mod,reduction,merge,exactQuo)

