# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1370015374 -7200
# Node ID cf55b1438731c86fd8327744cccd2b4627f09613
# Parent  5a83cf4f184aaba9c4b7e852407ec160a2fcd34b
GCD_Poly.thy with writeln for try_new_prime_up

writeln used for testing codegen

diff -r 5a83cf4f184a -r cf55b1438731 src/Tools/isac/Knowledge/GCD_Poly.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly.thy	Fri May 24 16:50:31 2013 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly.thy	Fri May 31 17:49:34 2013 +0200
@@ -355,7 +355,18 @@
 
     argumentns "a b d M P g p" named according to [1] p.93 *)
   fun try_new_prime_up a b d M P g p =
-    if P > M then g else
+(writeln ("try_new_prime_up:  a = " ^ PolyML.makestring a ^
+", b = " ^ PolyML.makestring b ^
+", d = " ^ PolyML.makestring d ^
+", M = " ^ PolyML.makestring M ^
+", P = " ^ PolyML.makestring P ^
+", g = " ^ PolyML.makestring g ^
+", p = " ^ PolyML.makestring p);
+    if P > M then
+(writeln ("try_new_prime_up 1 -----> " ^ PolyML.makestring g);
+                  g 
+)
+                    else
       let
         val p = p next_prime_not_dvd d
         val g_p = centr_up (         (    (normalise (mod_up_gcd a b p) p) 
@@ -365,7 +376,11 @@
       in
         if deg_up g_p < deg_up g
         then
-          if (deg_up g_p) = 0 then [1]: unipoly else try_new_prime_up a b d M p g_p p
+          if (deg_up g_p) = 0 then
+(writeln ("try_new_prime_up 2 -----> " ^ PolyML.makestring [1]);
+                                   [1]: unipoly
+) 
+                                                else try_new_prime_up a b d M p g_p p
         else
           if deg_up g_p <> deg_up g then try_new_prime_up a b d M P g p else
             let 
@@ -373,7 +388,7 @@
               val g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P
             in try_new_prime_up a b d M P g p end
       end
-      
+)      
   (* HENSEL_lifting_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
      HENSEL_lifting_up p1 p2 d M p = gcd
        assumes d = gcd (lcoeff_up p1, lcoeff_up p2) \<and> 
@@ -382,19 +397,33 @@
        yields  gcd | p1  \<and>  gcd | p2  \<and>  gcd is primitive
 
     argumentns "a b d M p" named according to [1] p.93 *)
-  fun HENSEL_lifting_up a b d M p = 
+  fun HENSEL_lifting_up a b d M p =
+(writeln ("HENSEL_lifting_up: a = " ^ PolyML.makestring a ^
+", b = " ^ PolyML.makestring b ^
+", d = " ^ PolyML.makestring d ^
+", M = " ^ PolyML.makestring M ^
+", p = " ^ PolyML.makestring p);
     let
       val p = p next_prime_not_dvd d 
-      val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p (*see above*)
+      val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p 
+        (*.. nesting of functions see above*)
     in
-      if deg_up g_p = 0 then [1] else
+      if deg_up g_p = 0 then 
+(writeln ("HENSEL_lifting_up 1 ----> " ^ PolyML.makestring [1]);
+                             [1] 
+)
+                                else
         let 
           val g = primitive_up (try_new_prime_up a b d M p g_p p)
         in
-          if (g %|% a) andalso (g %|% b) then g:unipoly else HENSEL_lifting_up a b d M p
+          if (g %|% a) andalso (g %|% b) then 
+(writeln ("HENSEL_lifting_up 2 -----> " ^ PolyML.makestring g);
+                                              g:unipoly
+) 
+                                                        else HENSEL_lifting_up a b d M p
         end
     end
-
+)
   (* gcd_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> unipoly
      gcd_up a b = c
      assumes not (a = [] \<or> a = [0]) \<and> not (b = []\<or> b = [0]) \<and> 
diff -r 5a83cf4f184a -r cf55b1438731 src/Tools/isac/Knowledge/GCD_Poly_FP.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri May 24 16:50:31 2013 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri May 31 17:49:34 2013 +0200
@@ -259,10 +259,9 @@
   from primes_upto_1 have "n1 < last (primes_upto (Suc n1))" by auto
   from this have                "(int n1) - (int (last (primes_upto (Suc n1)) * q))
     < (int (last (primes_upto (Suc n1)))) - (int (last (primes_upto (Suc n1)) * q))" by auto
-  from this show ?thesis sorry
+  from this show ?thesis sorry (*by (rule neg_less_iff_less)*)
 qed (*?FLORIAN : lifting nat -> int ?*)
 
-
 find_theorems "_ - _ < _ - _ = _" thm Nat.less_diff_iff
 find_theorems "_ * _ < _ * _ = _" thm Nat.Suc_mult_less_cancel1
 find_theorems "-_ < -_ = _" thm Groups.ordered_ab_group_add_class.neg_less_iff_less
@@ -439,9 +438,18 @@
 value "[5, 4, -7, 8, -1] %* 5 = [25, 20, -35, 40, -5]"
 
 (* scalar divison *)
+(*
 definition swapf :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where "swapf f a b = f b a"
+CODEGEN CAUSES ERROR:
+ML error (line 913 of "/home/neuper/devel/isac/codegen/gcd_univariate.sml"):
+Type error in function application. Function: div2 : inta -> inta -> inta
+   Argument: (swapf, m) : (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd
+   Reason: Can't unify inta to (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd (Incompatible types)
+THUS TYPE CONSTRAINED...
+*)
+definition swapf1 :: "(int \<Rightarrow> int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where "swapf1 f a b = f b a"
 definition div_ups :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "div'_ups" (* %/ error FLORIAN*) 70) where
-"p div_ups m = map (swapf op div2 m) p"
+"p div_ups m = map (swapf1 op div2 m) p"
 
 value "[4, 3, 2, 5, 6] div_ups 3 = [1, 1, 0, 1, 2]"
 value "[4, 3, 2, 0] div_ups 3    = [1, 1, 0, 0]"
@@ -561,12 +569,25 @@
 value "centr_up [1, 2, 3, 4, 5] 10    = [1, 2, 3, 4, 5]"
 value "centr_up [1, 2, 3, 4, 5] 11    = [1, 2, 3, 4, 5]"
 
+(*
+definition swapf :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where "swapf f a b = f b a"
+CODEGEN CAUSES ERROR:
+ML error (line 913 of "/home/neuper/devel/isac/codegen/gcd_univariate.sml"):
+Type error in function application. Function: div2 : inta -> inta -> inta
+   Argument: (swapf, m) : (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd
+   Reason: Can't unify inta to (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd (Incompatible types)
+THUS TYPE CONSTRAINED...
+*)
+definition swapf2 :: "(int \<Rightarrow> nat \<Rightarrow> int) \<Rightarrow> nat \<Rightarrow> int \<Rightarrow> int" where "swapf2 f a b = f b a"
+
 (* sum_lmb :: centr_up \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int
    sum_lmb [p_0, .., p_k] e = s
      assumes exp >= 0
      yields. p_0^e + p_1^e + ... + p_k^e *)
 definition sum_lmb :: "unipoly \<Rightarrow> nat \<Rightarrow> int" where
-"sum_lmb p exp = List.fold ((op +) o (swapf power exp)) p 0"
+"sum_lmb p exp = List.fold ((op +) o (swapf2 power exp)) p 0"
+
+value "power"
 
 value "sum_lmb [-1, 2, -3, 4, -5] 1 = -3"
 value "sum_lmb [-1, 2, -3, 4, -5] 2 = 55"
@@ -721,10 +742,10 @@
 
 subsection {* gcd_up, code from [1] p.93 *}
 (* try_new_prime_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly \<Rightarrow> int  \<Rightarrow> unipoly
-   try_new_prime_up p1 p2 d M P g p = new_g
-     assumes d = gcd (lcoeff_up p1, lcoeff_up p2)  \<and> 
+   try_new_prime_up a b d M P g p = new_g
+     assumes d = gcd (lcoeff_up a, lcoeff_up b)  \<and> 
              M = LANDAU_MIGNOTTE_bound  \<and>  p = prime  \<and>  p ~| d  \<and>  P \<ge> p  \<and>
-             p1 is primitive  \<and>  p2 is primitive
+             a is primitive  \<and>  b is primitive
      yields  new_g = [1] \<or> (new_g \<ge> g \<and> P > M)
 
   argumentns "a b d M P g p" named according to [1] p.93: "p" is "prime", not "poly" ! *)
@@ -760,6 +781,16 @@
 *)
 sorry
 
+value "try_new_prime_up 
+  [-18, -15, -20, 12, 20, -13, 2] 
+  [8, 28, 22, -11, -14, 1, 2]
+  (nat \<bar>gcd (lcoeff_up [-18, -15, -20, 12, 20, -13, 2]) (lcoeff_up [8, 28, 22, -11, -14, 1, 2])\<bar>)
+  ((2 * 
+    (nat \<bar>gcd (lcoeff_up [-18, -15, -20, 12, 20, -13, 2]) (lcoeff_up [8, 28, 22, -11, -14, 1, 2])\<bar>) 
+    * LANDAU_MIGNOTTE_bound [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2]))
+  (*p next_prime_not_dvd d  ...thus this function cannot be tested immediately! FLORIAN!*)
+"
+
 (* HENSEL_lifting_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
    HENSEL_lifting_up p1 p2 d M p = gcd
      assumes d = gcd (lcoeff_up p1, lcoeff_up p2) \<and> 
diff -r 5a83cf4f184a -r cf55b1438731 test/Tools/isac/Knowledge/gcd_poly.sml
--- a/test/Tools/isac/Knowledge/gcd_poly.sml	Fri May 24 16:50:31 2013 +0200
+++ b/test/Tools/isac/Knowledge/gcd_poly.sml	Fri May 31 17:49:34 2013 +0200
@@ -377,12 +377,40 @@
                                mod_up p') 
                              p'
 ;
+val (a, b, d, M, P, g, p) = (0, 0, 0, 0, 0, 0, 0) (*isolate test below*)
+
+val (a, b) = ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2])
+val d = abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))
+val M = 2 * d * LANDAU_MIGNOTTE_bound a b
+val p = 1 (*-> p in head of HENSEL_lifting_up*) next_prime_not_dvd d
+val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p (*see above*)
+val (a, b, d, M, P, g, p) = (a, b, d, M, p, g_p, p);
+
+if try_new_prime_up a b d M P g p = [~1, 1, ~1] then () else error "try_new_prime_up changed";
 
 "----------- fun gcd_up ---------------------------------";
 "----------- fun gcd_up ---------------------------------";
 "----------- fun gcd_up ---------------------------------";
-if gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] then ()
-else error "gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] changed";
+(* output from changeset 
+try_new_prime_up: a = [~18, ~15, ~20, 12, 20, ~13, 2], b = [8, 28, 22, ~11, ~14, 1, 2], 
+d = 2, M = 10240, P = 12597, g = [~1, 1, ~1], p = 19 
+try_new_prime_up 1 -----> [~1, 1, ~1] *)
+val (a, b, d, M, P, g, p) = 
+  ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
+    2, 10240, 3, [~1, 1, ~1], 3);
+"-----";
+if try_new_prime_up a b d M P g p = [~1, 1, ~1] 
+  then () else error "try_new_prime_up changed";
+
+(* output from changeset 
+try_new_prime_up: a = [~18, ~15, ~20, 12, 20, ~13, 2], b = [8, 28, 22, ~11, ~14, 1, 2], 
+d = 2, M = 10240, P = 96577, g = [~4, ~2, 2], p = 23 
+try_new_prime_up 1 -----> [~4, ~2, 2] *)
+val (a, b, d, M, P, g, p) = 
+  ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
+    2, 10240, 5, [2, 2, 2, 2], 5);
+if try_new_prime_up a b d M P g p = [~4, ~2, 2]
+  then () else error "try_new_prime_up changed";
 
 "=========== Multivariate Case ==========================";
 "=========== Multivariate Case ==========================";
diff -r 5a83cf4f184a -r cf55b1438731 test/Tools/isac/Test_Some2.thy
--- a/test/Tools/isac/Test_Some2.thy	Fri May 24 16:50:31 2013 +0200
+++ b/test/Tools/isac/Test_Some2.thy	Fri May 31 17:49:34 2013 +0200
@@ -1,16 +1,42 @@
 
 theory Test_Some2
 imports "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly"
+  (*required for export_code ...*)
+        "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_FP"
 begin
-
 ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly.sml"
 
-ML {*
-*}
-ML {*
-*}
-ML {*
-*}
+(*test codegen*)
+(*
+export_code "try_new_prime_up" in SML
+module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
+*)
+ML_file "/home/neuper/devel/isac/codegen/try_new_prime_up.ML"  (*automat. generated *)
+ML_file "/home/neuper/devel/isac/codegen/try_new_prime_up.sml" (*included test:
+ML error (line 769 of "/home/neuper/devel/isac/codegen/try_new_prime_up.sml"):
+Type error in function application.
+   Function: GCD_Univariate.try_new_prime_up :
+      GCD_Univariate.inta list ->
+      GCD_Univariate.inta list -> GCD_Univariate.nat -> GCD_Univariate.nat -> GCD_Univariate.nat -> 
+      GCD_Univariate.inta list -> GCD_Univariate.nat -> GCD_Univariate.inta list
+   Argument: a : int list Reason: Can't unify GCD_Univariate.inta with int (*In Basis*) 
+   (Different type constructors)
+*)
+
+(*ML_file "/home/neuper/devel/isac/codegen/gcd_univariate-error1-swapf.sml"   errors*)
+(*ML_file "/home/neuper/devel/isac/codegen/gcd_univariate-error2-div2.sml"    errors*)
+(*
+export_code "gcd_up" in SML
+module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
+*)
+export_code "gcd_up" in SML (*WITHOUT IMPORT: Not a constant: gcd_up*)
+module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
+
+ML_file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML" (*automat. generated *)
+(*ML error (line 915 of "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"):
+Type error in function application. Function: div2 : inta -> inta -> inta 
+  Argument: (swapf1, m) : (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd
+   Reason: Can't unify inta to (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd (Incompatible types)*)
 ML {*
 *} 
 ML {*
@@ -20,13 +46,35 @@
 ML {*
 *} 
 ML {*
+if gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] then ()
+else error "gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] changed";
+*} 
+ML {*
+
+(* gcd    (1 + x^2) (x + x^2) = (1 + x) *)
+if gcd_up [~1, 0 ,1] [0, 1, 1] = [1, 1]
+    then () else error "gcd_up [~1, 0 ,1] ... changed";
 *}
 ML {*
+val (a, b, d, M, P, g, p) = 
+  ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
+    2, 10240, 3, [~1, 1, ~1], 3);
+if try_new_prime_up a b d M P g p = [~1, 1, ~1] 
+  then () else error "try_new_prime_up changed";
+*} 
+ML {*
+val (a, b, d, M, P, g, p) = 
+  ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
+    2, 10240, 5, [2, 2, 2, 2], 5);
+if try_new_prime_up a b d M P g p = [~4, ~2, 2]
+  then () else error "try_new_prime_up changed";
+*} 
+ML {*
 *} 
 ML {*
 *} 
 ML {*
-*}
+*} 
 (*------------------------------------------------------------------------------------------
 "~~~~~ fun , args:"; val () = ();
 "~~~~~ to  return val:"; val () = ();