1.1 --- a/test/Tools/isac/Test_Some2.thy	Fri May 24 16:50:31 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Some2.thy	Fri May 31 17:49:34 2013 +0200
     1.3 @@ -1,16 +1,42 @@
     1.4  
     1.5  theory Test_Some2
     1.6  imports "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly"
     1.7 +  (*required for export_code ...*)
     1.8 +        "/usr/local/isabisac/src/Tools/isac/Knowledge/GCD_Poly_FP"
     1.9  begin
    1.10 -
    1.11  ML_file "/usr/local/isabisac/test/Tools/isac/Knowledge/gcd_poly.sml"
    1.12  
    1.13 -ML {*
    1.14 -*}
    1.15 -ML {*
    1.16 -*}
    1.17 -ML {*
    1.18 -*}
    1.19 +(*test codegen*)
    1.20 +(*
    1.21 +export_code "try_new_prime_up" in SML
    1.22 +module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
    1.23 +*)
    1.24 +ML_file "/home/neuper/devel/isac/codegen/try_new_prime_up.ML"  (*automat. generated *)
    1.25 +ML_file "/home/neuper/devel/isac/codegen/try_new_prime_up.sml" (*included test:
    1.26 +ML error (line 769 of "/home/neuper/devel/isac/codegen/try_new_prime_up.sml"):
    1.27 +Type error in function application.
    1.28 +   Function: GCD_Univariate.try_new_prime_up :
    1.29 +      GCD_Univariate.inta list ->
    1.30 +      GCD_Univariate.inta list -> GCD_Univariate.nat -> GCD_Univariate.nat -> GCD_Univariate.nat -> 
    1.31 +      GCD_Univariate.inta list -> GCD_Univariate.nat -> GCD_Univariate.inta list
    1.32 +   Argument: a : int list Reason: Can't unify GCD_Univariate.inta with int (*In Basis*) 
    1.33 +   (Different type constructors)
    1.34 +*)
    1.35 +
    1.36 +(*ML_file "/home/neuper/devel/isac/codegen/gcd_univariate-error1-swapf.sml"   errors*)
    1.37 +(*ML_file "/home/neuper/devel/isac/codegen/gcd_univariate-error2-div2.sml"    errors*)
    1.38 +(*
    1.39 +export_code "gcd_up" in SML
    1.40 +module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
    1.41 +*)
    1.42 +export_code "gcd_up" in SML (*WITHOUT IMPORT: Not a constant: gcd_up*)
    1.43 +module_name GCD_Univariate file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"
    1.44 +
    1.45 +ML_file "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML" (*automat. generated *)
    1.46 +(*ML error (line 915 of "/home/neuper/devel/isac/codegen/gcd_un_Test_Some2.ML"):
    1.47 +Type error in function application. Function: div2 : inta -> inta -> inta 
    1.48 +  Argument: (swapf1, m) : (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd
    1.49 +   Reason: Can't unify inta to (('a -> 'b -> 'c) -> 'b -> 'a -> 'c) * 'd (Incompatible types)*)
    1.50  ML {*
    1.51  *} 
    1.52  ML {*
    1.53 @@ -20,13 +46,35 @@
    1.54  ML {*
    1.55  *} 
    1.56  ML {*
    1.57 +if gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] then ()
    1.58 +else error "gcd_up [~18, ~15, ~20, 12, 20, ~13, 2] [8, 28, 22, ~11, ~14, 1, 2] = [~2, ~1, 1] changed";
    1.59 +*} 
    1.60 +ML {*
    1.61 +
    1.62 +(* gcd    (1 + x^2) (x + x^2) = (1 + x) *)
    1.63 +if gcd_up [~1, 0 ,1] [0, 1, 1] = [1, 1]
    1.64 +    then () else error "gcd_up [~1, 0 ,1] ... changed";
    1.65  *}
    1.66  ML {*
    1.67 +val (a, b, d, M, P, g, p) = 
    1.68 +  ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
    1.69 +    2, 10240, 3, [~1, 1, ~1], 3);
    1.70 +if try_new_prime_up a b d M P g p = [~1, 1, ~1] 
    1.71 +  then () else error "try_new_prime_up changed";
    1.72 +*} 
    1.73 +ML {*
    1.74 +val (a, b, d, M, P, g, p) = 
    1.75 +  ([~18, ~15, ~20, 12, 20, ~13, 2], [8, 28, 22, ~11, ~14, 1, 2],
    1.76 +    2, 10240, 5, [2, 2, 2, 2], 5);
    1.77 +if try_new_prime_up a b d M P g p = [~4, ~2, 2]
    1.78 +  then () else error "try_new_prime_up changed";
    1.79 +*} 
    1.80 +ML {*
    1.81  *} 
    1.82  ML {*
    1.83  *} 
    1.84  ML {*
    1.85 -*}
    1.86 +*} 
    1.87  (*------------------------------------------------------------------------------------------
    1.88  "~~~~~ fun , args:"; val () = ();
    1.89  "~~~~~ to  return val:"; val () = ();