--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 package LEADCDET LeadingCoefDetermination
++ Author : P.Gianni, May 1990
++ Description:
++ Package for leading coefficient determination in the lifting step.
++ Package working for every R euclidean with property "F".
LeadingCoefDetermination(OV,E,Z,P) : C == T
 where
  OV    :   OrderedSet
  E     :   OrderedAbelianMonoidSup
  Z     :   EuclideanDomain
  BP        ==> SparseUnivariatePolynomial Z
  P         :   PolynomialCategory(Z,E,OV)
  NNI       ==> NonNegativeInteger
  LeadFact  ==> Record(polfac:List(P),correct:Z,corrfact:List(BP))
  ParFact   ==> Record(irr:P,pow:Integer)
  FinalFact ==> Record(contp:Z,factors:List(ParFact))
 
  C == with
   polCase  : (Z,NNI,List(Z)) -> Boolean
     ++ polCase(contprod, numFacts, evallcs), where contprod is the
     ++ product of the content of the leading coefficient of
     ++ the polynomial to be factored with the content of the
     ++ evaluated polynomial, numFacts is the number of factors
     ++ of the leadingCoefficient, and evallcs is the list of
     ++ the evaluated factors of the leadingCoefficient, returns
     ++ true if the factors of the leading Coefficient can be
     ++ distributed with this valuation.
   distFact : (Z,List(BP),FinalFact,List(Z),List(OV),List(Z)) ->
                                              Union(LeadFact,"failed")
     ++ distFact(contm,unilist,plead,vl,lvar,lval), where contm is
     ++ the content of the evaluated polynomial, unilist is the list
     ++ of factors of the evaluated polynomial, plead is the complete
     ++ factorization of the leading coefficient, vl is the list
     ++ of factors of the leading coefficient evaluated, lvar is the
     ++ list of variables, lval is the list of values, returns a record
     ++ giving the list of leading coefficients to impose on the univariate
     ++ factors, 
 
  T == add
    distribute: (Z,List(BP),List(P),List(Z),List(OV),List(Z)) -> LeadFact
    checkpow  : (Z,Z) -> NNI
 
    polCase(d:Z,nk:NNI,lval:List(Z)):Boolean ==
      -- d is the product of the content lc m (case polynomial)
      -- and the cont of the polynomial evaluated
      q:Z
      distlist:List(Z) := [d]
      for i in 1..nk repeat
        q := unitNormal(lval.i).canonical
        for j in 0..(i-1)::NNI repeat
          y := distlist.((i-j)::NNI)
          while not one? y  repeat
            y := gcd(y,q)
            q := q quo y
          if q=1 then return false
        distlist := append(distlist,[q])
      true
 
    checkpow(a:Z,b:Z) : NonNegativeInteger ==
      qt: Union(Z,"failed")
      for i in 0.. repeat
        qt:= b exquo a
        if qt case "failed" then return i
        b:=qt::Z
 
    distribute(contm:Z,unilist:List(BP),pl:List(P),vl:List(Z),
                              lvar:List(OV),lval:List(Z)): LeadFact ==
      d,lcp : Z
      nf:NNI:=#unilist
      for i in 1..nf repeat
          lcp := leadingCoefficient (unilist.i)
          d:= gcd(lcp,vl.i)
          pl.i := (lcp quo d)*pl.i
          d := vl.i quo d
          unilist.i := d*unilist.i
          contm := contm quo d
      if not one? contm then for i in 1..nf repeat pl.i := contm*pl.i
      [pl,contm,unilist]$LeadFact
 
    distFact(contm:Z,unilist:List(BP),plead:FinalFact,
             vl:List(Z),lvar:List(OV),lval:List(Z)):Union(LeadFact,"failed") ==
      h:NonNegativeInteger
      c,d : Z
      lpol:List(P):=[]
      lexp:List(Integer):=[]
      nf:NNI := #unilist
      vl := reverse vl --lpol and vl reversed so test from right to left
      for fpl in plead.factors repeat
       lpol:=[fpl.irr,:lpol]
       lexp:=[fpl.pow,:lexp]
      vlp:List(Z):= [1$Z for i in 1..nf]
      aux : List(P) := [1$P for i in 1..nf]
      for i in 1..nf repeat
        c := contm*leadingCoefficient unilist.i
        c=1 or c=-1  => "next i"
        for k in 1..(# lpol) repeat
          lexp.k=0 => "next factor"
          h:= checkpow(vl.k,c)
          if not zero? h then
           if h>lexp.k then return "failed"
           lexp.k:=lexp.k-h
           aux.i := aux.i*(lpol.k ** h)
           d:= vl.k**h
           vlp.i:= vlp.i*d
           c:= c quo d
        if contm=1 then vlp.i:=c
      for k in 1..(# lpol) repeat if lexp.k ~= 0 then return "failed"
      contm =1 => [[vlp.i*aux.i for i in 1..nf],1,unilist]$LeadFact
      distribute(contm,unilist,aux,vlp,lvar,lval)

