656 in (order p', new_vals, steps) end |
656 in (order p', new_vals, steps) end |
657 *} |
657 *} |
658 |
658 |
659 subsection {* gcd_poly algorithm, code for [1] p.95 *} |
659 subsection {* gcd_poly algorithm, code for [1] p.95 *} |
660 ML {* |
660 ML {* |
661 fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2) |
661 fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2) |
662 |
662 |
663 (* naming of n, M, m, r, ... follows Winkler p. 95 |
663 (* naming of n, M, m, r, ... follows Winkler p. 95 |
664 assumes: n = length es1 = length es2 |
664 assumes: n = length es1 = length es2 |
665 r: *) |
665 r: *) |
666 fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom] |
666 fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom] |
667 | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom] |
667 | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom] |
668 | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = |
668 | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = |
669 if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else |
669 if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else |
670 if n > 1 |
670 if n > 1 |
671 then |
671 then |
672 let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); |
672 let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); |
673 in try_new_r a b n M r [] [] end |
673 in try_new_r a b n M r [] [] end |