1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Fri Mar 18 12:42:28 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Fri Mar 18 17:24:56 2011 +0100
     1.3 @@ -4,17 +4,18 @@
     1.4  12345678901234567890123456789012345678901234567890123456789012345678901234567890
     1.5          10        20        30        40        50        60        70        80
     1.6  *)
     1.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     1.8  "--------------------------------------------------------";
     1.9  "table of contents --------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11  "----------- rewriting for usecase1 ---------------------";
    1.12  "----------- mathengine with usecase1 -------------------";
    1.13 +"----------- rewriting for usecase2 ---------------------";
    1.14 +"----------- mathengine with usecase2 -------------------";
    1.15  "--------------------------------------------------------";
    1.16  "--------------------------------------------------------";
    1.17  "--------------------------------------------------------";
    1.18  
    1.19 -(*apparently no way to do these tests within DiophantEq.thy:
    1.20 +(*there seemed to be no way to do these tests within DiophantEq.thy:
    1.21  val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
    1.22    from CalcTreeTest*)
    1.23  (*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
    1.24 @@ -40,19 +41,58 @@
    1.25  "----------- mathengine with usecase1 -------------------";
    1.26  "----------- mathengine with usecase1 -------------------";
    1.27  "----------- mathengine with usecase1 -------------------";
    1.28 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.29 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.30  val p = e_pos'; val c = [];
    1.31  val (fmz, (thy, pbl, met)) = 
    1.32 -  (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
    1.33 +  (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx", 
    1.34 +    "intTestFind sss"],
    1.35     (Context.theory_name thy, ["diophantine", "equation"], 
    1.36      ["Test", "solve_diophant"]));
    1.37  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
    1.38  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.39 +(*========== inhibit exn WN110318 ==============================================
    1.40  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.41  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.42  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.43  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.44  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.45  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.46 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.47 +============ inhibit exn WN110318 ============================================*)
    1.48 +
    1.49 +"----------- rewriting for usecase2 ---------------------";
    1.50 +"----------- rewriting for usecase2 ---------------------";
    1.51 +val thy = @{theory "Test"};
    1.52 +"----------- rewriting for usecase2 ---------------------";
    1.53 +
    1.54 +val t = parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)";
    1.55 +
    1.56 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
    1.57 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.58 +
    1.59 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
    1.60 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    1.61 +
    1.62 +
    1.63 +"----------- mathengine with usecase2 -------------------";
    1.64 +"----------- mathengine with usecase2 -------------------";
    1.65 +"----------- mathengine with usecase2 -------------------";
    1.66 +val p = e_pos'; val c = [];
    1.67 +val (fmz, (thy, pbl, met)) = 
    1.68 +  (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
    1.69 +   (Context.theory_name thy, ["inttype","test"], ["Test","intsimp"]));
    1.70 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
    1.71 +(*nxt = ("Model_Problem", ...)*)
    1.72 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.73 +(*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + -1 * 111 + 123)")*)
    1.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.75 +(* Add_Find ###########################################*)
    1.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.77 +(*nxt = ("Specify_Theory", ...)*)
    1.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.79 +(*nxt = ("Specify_Problem", ...)*)
    1.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.81 +(*nxt = ("Specify_Method", ...)*)
    1.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.83 +(*nxt = ("Empty_Tac", ...) #############################*)
    1.84 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.85 +(*========== inhibit exn WN110318 ==============================================
    1.86 +============ inhibit exn WN110318 ============================================*)