1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy Fri May 31 18:00:35 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy Fri May 31 18:05:20 2013 +0200
1.3 @@ -355,18 +355,7 @@
1.4
1.5 argumentns "a b d M P g p" named according to [1] p.93 *)
1.6 fun try_new_prime_up a b d M P g p =
1.7 -(writeln ("try_new_prime_up: a = " ^ PolyML.makestring a ^
1.8 -", b = " ^ PolyML.makestring b ^
1.9 -", d = " ^ PolyML.makestring d ^
1.10 -", M = " ^ PolyML.makestring M ^
1.11 -", P = " ^ PolyML.makestring P ^
1.12 -", g = " ^ PolyML.makestring g ^
1.13 -", p = " ^ PolyML.makestring p);
1.14 - if P > M then
1.15 -(writeln ("try_new_prime_up 1 -----> " ^ PolyML.makestring g);
1.16 - g
1.17 -)
1.18 - else
1.19 + if P > M then g else
1.20 let
1.21 val p = p next_prime_not_dvd d
1.22 val g_p = centr_up ( ( (normalise (mod_up_gcd a b p) p)
1.23 @@ -376,11 +365,7 @@
1.24 in
1.25 if deg_up g_p < deg_up g
1.26 then
1.27 - if (deg_up g_p) = 0 then
1.28 -(writeln ("try_new_prime_up 2 -----> " ^ PolyML.makestring [1]);
1.29 - [1]: unipoly
1.30 -)
1.31 - else try_new_prime_up a b d M p g_p p
1.32 + if (deg_up g_p) = 0 then [1]: unipoly else try_new_prime_up a b d M p g_p p
1.33 else
1.34 if deg_up g_p <> deg_up g then try_new_prime_up a b d M P g p else
1.35 let
1.36 @@ -388,7 +373,7 @@
1.37 val g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P
1.38 in try_new_prime_up a b d M P g p end
1.39 end
1.40 -)
1.41 +
1.42 (* HENSEL_lifting_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
1.43 HENSEL_lifting_up p1 p2 d M p = gcd
1.44 assumes d = gcd (lcoeff_up p1, lcoeff_up p2) \<and>
1.45 @@ -398,32 +383,19 @@
1.46
1.47 argumentns "a b d M p" named according to [1] p.93 *)
1.48 fun HENSEL_lifting_up a b d M p =
1.49 -(writeln ("HENSEL_lifting_up: a = " ^ PolyML.makestring a ^
1.50 -", b = " ^ PolyML.makestring b ^
1.51 -", d = " ^ PolyML.makestring d ^
1.52 -", M = " ^ PolyML.makestring M ^
1.53 -", p = " ^ PolyML.makestring p);
1.54 let
1.55 val p = p next_prime_not_dvd d
1.56 val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p
1.57 (*.. nesting of functions see above*)
1.58 in
1.59 - if deg_up g_p = 0 then
1.60 -(writeln ("HENSEL_lifting_up 1 ----> " ^ PolyML.makestring [1]);
1.61 - [1]
1.62 -)
1.63 - else
1.64 + if deg_up g_p = 0 then [1] else
1.65 let
1.66 val g = primitive_up (try_new_prime_up a b d M p g_p p)
1.67 in
1.68 - if (g %|% a) andalso (g %|% b) then
1.69 -(writeln ("HENSEL_lifting_up 2 -----> " ^ PolyML.makestring g);
1.70 - g:unipoly
1.71 -)
1.72 - else HENSEL_lifting_up a b d M p
1.73 + if (g %|% a) andalso (g %|% b) then g:unipoly else HENSEL_lifting_up a b d M p
1.74 end
1.75 end
1.76 -)
1.77 +
1.78 (* gcd_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> unipoly
1.79 gcd_up a b = c
1.80 assumes not (a = [] \<or> a = [0]) \<and> not (b = []\<or> b = [0]) \<and>
2.1 --- a/test/Tools/isac/Test_Some2.thy Fri May 31 18:00:35 2013 +0200
2.2 +++ b/test/Tools/isac/Test_Some2.thy Fri May 31 18:05:20 2013 +0200
2.3 @@ -6,37 +6,6 @@
2.4 begin
2.5 ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly.sml"
2.6
2.7 -(*test codegen*)
2.8 -(*
2.9 -export_code "try_new_prime_up" in SML
2.10 -module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
2.11 -*)
2.12 -ML_file "/home/neuper/devel/isac/codegen/try_new_prime_up.ML" (*automat. generated *)
2.13 -ML_file "/home/neuper/devel/isac/codegen/try_new_prime_up.sml" (*included test:
2.14 -ML error (line 769 of "/home/neuper/devel/isac/codegen/try_new_prime_up.sml"):
2.15 -Type error in function application.
2.16 - Function: GCD_Univariate.try_new_prime_up :
2.17 - GCD_Univariate.inta list ->
2.18 - GCD_Univariate.inta list -> GCD_Univariate.nat -> GCD_Univariate.nat -> GCD_Univariate.nat ->
2.19 - GCD_Univariate.inta list -> GCD_Univariate.nat -> GCD_Univariate.inta list
2.20 - Argument: a : int list Reason: Can't unify GCD_Univariate.inta with int (*In Basis*)
2.21 - (Different type constructors)
2.22 -*)
2.23 -
2.24 -(*ML_file "/home/neuper/devel/isac/codegen/gcd_univariate-error1-swapf.sml" errors*)
2.25 -(*ML_file "/home/neuper/devel/isac/codegen/gcd_univariate-error2-div2.sml" errors*)
2.26 -(*
2.27 -export_code "gcd_up" in SML
2.28 -module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
2.29 -*)
2.30 -export_code "gcd_up" in SML (*WITHOUT IMPORT: Not a constant: gcd_up*)
2.31 -module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
2.32 -
2.33 -ML_file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML" (*automat. generated *)
2.34 -(*ML error (line 915 of "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"):
2.35 -Type error in function application. Function: div2 : inta -> inta -> inta
2.36 - Argument: (swapf1, m) : (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd
2.37 - Reason: Can't unify inta to (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd (Incompatible types)*)
2.38 ML {*
2.39 *}
2.40 ML {*
2.41 @@ -46,28 +15,6 @@
2.42 ML {*
2.43 *}
2.44 ML {*
2.45 -if gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] then ()
2.46 -else error "gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] changed";
2.47 -*}
2.48 -ML {*
2.49 -
2.50 -(* gcd (1 + x^2) (x + x^2) = (1 + x) *)
2.51 -if gcd_up [~1, 0 ,1] [0, 1, 1] = [1, 1]
2.52 - then () else error "gcd_up [~1, 0 ,1] ... changed";
2.53 -*}
2.54 -ML {*
2.55 -val (a, b, d, M, P, g, p) =
2.56 - ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
2.57 - 2, 10240, 3, [~1, 1, ~1], 3);
2.58 -if try_new_prime_up a b d M P g p = [~1, 1, ~1]
2.59 - then () else error "try_new_prime_up changed";
2.60 -*}
2.61 -ML {*
2.62 -val (a, b, d, M, P, g, p) =
2.63 - ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
2.64 - 2, 10240, 5, [2, 2, 2, 2], 5);
2.65 -if try_new_prime_up a b d M P g p = [~4, ~2, 2]
2.66 - then () else error "try_new_prime_up changed";
2.67 *}
2.68 ML {*
2.69 *}