1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Sun Sep 01 15:54:48 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Sun Sep 01 16:50:51 2013 +0200
     1.3 @@ -661,19 +661,20 @@
     1.4    (* naming of n, M, m, r, ...  follows Winkler p. 95 
     1.5      n: amount of variables 
     1.6      r: *)
     1.7 -  fun gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
     1.8 -    if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
     1.9 -      if n > 1
    1.10 -      then
    1.11 -        let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); 
    1.12 -        in try_new_r a b n M r [] [] end
    1.13 -      else 
    1.14 -        let val (a', b') = (multi_to_uni a, multi_to_uni b)
    1.15 -        in
    1.16 -          (* a b are made primitive and this is compensated by multiplying with gcd of divisors *)
    1.17 -          uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %* 
    1.18 -                        (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))
    1.19 -        end
    1.20 +  fun gcd_poly' [(c1, es1)] [(c2, es2)] _ _ = [(Integer.gcd c1 c2, map2 Integer.min es1 es2)]
    1.21 +    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
    1.22 +      if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
    1.23 +        if n > 1
    1.24 +        then
    1.25 +          let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); 
    1.26 +          in try_new_r a b n M r [] [] end
    1.27 +        else 
    1.28 +          let val (a', b') = (multi_to_uni a, multi_to_uni b)
    1.29 +          in
    1.30 +            (* a b are made primitive and this is compensated by multiplying with gcd of divisors *)
    1.31 +            uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %* 
    1.32 +                          (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))
    1.33 +          end
    1.34  
    1.35    (* fn: poly -> poly -> int -> 
    1.36                        int -> int -> int list -> poly list -> poly*)

     2.1 --- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml	Sun Sep 01 15:54:48 2013 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml	Sun Sep 01 16:50:51 2013 +0200
     2.3 @@ -804,10 +804,16 @@
     2.4  if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_poly mail changed";
     2.5  (* \<forall>c'. (c' dvd\<^isub>p  a \<and> c' dvd\<^isub>p b) \<longrightarrow> c' \<le>\<^isub>p c) can NOT be checked this way, of course *)
     2.6  
     2.7 +(* regression test for --- fun gcd_poly downto division by zero ---*)
     2.8 +val a = [(9, [5, 2, 4])]: poly
     2.9 +val b = [(15, [6, 3, 1])]: poly
    2.10 +val ((a', b'), c) = gcd_poly a b;
    2.11 +if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "regression test changed";
    2.12 +
    2.13  "----------- fun gcd_poly downto division by zero -------";
    2.14  "----------- fun gcd_poly downto division by zero -------";
    2.15  "----------- fun gcd_poly downto division by zero -------";
    2.16 -"-------- example 187a: exception Div raised...";
    2.17 +"-------- example 187a: exception Div raised...  REGRSSION TEST FOR REMOVAL OF THIS BUG IS ABOVE";
    2.18  val a = [(12, [1, 1])]: poly
    2.19  val b = [(8, [0, 2])]: poly;
    2.20  (*            val ((a', b'), c) = gcd_poly a b