1.1 --- a/src/Tools/isac/Test_Isac.thy	Fri Mar 18 12:42:28 2011 +0100
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Fri Mar 18 17:24:56 2011 +0100
     1.3 @@ -58,6 +58,92 @@
     1.4  *)
     1.5  use "../../../test/Tools/isac/Interpret/ptyps.sml"   (*TODO*)
     1.6  use "../../../test/Tools/isac/Interpret/calchead.sml"
     1.7 +
     1.8 +ML {* 
     1.9 +"===== start calculation: from problem description (fmz) to origin";
    1.10 +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
    1.11 +val (thyID, pblID, metID) =
    1.12 +  ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
    1.13 +val (p,_,_,nxt,_,pt) = CalcTreeTEST [(fmz, (thyID, pblID, metID))];
    1.14 +"----- ";
    1.15 +(* call sequence: CalcTreeTEST 
    1.16 +                > nxt_specify_init_calc 
    1.17 +                > prep_ori
    1.18 +*)
    1.19 +val (thy, pbt) = (Thy_Info.get_theory thyID, (#ppc o get_pbt) pblID);
    1.20 +"----- in  prep_ori";
    1.21 +val ctxt = ProofContext.init_global thy;
    1.22 +
    1.23 +    val ctopts = map (parse thy) fmz
    1.24 +    val dts = map ((split_dts thy) o term_of o the) ctopts
    1.25 +(*
    1.26 +(term * term list) list
    1.27 +        formulas: e.g. ((1+2)*4/3)^^^2
    1.28 + description: e.g. realTestGiven
    1.29 +*)
    1.30 +*}
    1.31 +
    1.32 +ML {*
    1.33 +"===== interactive specification: from origin to specification (probl)";
    1.34 +val (p,_,_,nxt,_,pt) = me nxt p [1] pt; (*Model_Problem*)
    1.35 +(*
    1.36 +val (p,_,_,nxt,_,pt) = me nxt p [1] pt;*)
    1.37 +val ((_,tac):tac'_) = nxt;
    1.38 +"@@@@@@@@@@@@@@@";
    1.39 +locatetac tac (pt,p);
    1.40 +
    1.41 +*}
    1.42 +
    1.43 +ML {*
    1.44 +"----- ";
    1.45 +(* call sequence: me Model_Problem 
    1.46 +                > me ("Add_Given", Add_Given "realTestGiven (((1 + 2) * 4 / 3) ^^^ 2)")
    1.47 +                > locatetac tac
    1.48 +                > applicable_in
    1.49 +*)
    1.50 +
    1.51 +"----- in locatetac";
    1.52 +(*val ((_,tac), ptp) = (nxt, (pt, p));*)
    1.53 +val (mI,m) = mk_tac'_ tac;
    1.54 +(*val Appl (Add_Find' (ct, is)) =*) applicable_in p pt m;
    1.55 +"----- in applicable_in";
    1.56 +
    1.57 +*}
    1.58 +
    1.59 +ML {*
    1.60 +
    1.61 +*}
    1.62 +
    1.63 +ML {*
    1.64 +*}
    1.65 +
    1.66 +ML {*
    1.67 +*}
    1.68 +
    1.69 +ML {*
    1.70 +
    1.71 +
    1.72 +"===== end specify: from specification (probl) to guard (method)";
    1.73 +"----- ";
    1.74 +
    1.75 +
    1.76 +
    1.77 +
    1.78 +"===== start interpretation: from guard to environment";
    1.79 +"----- ";
    1.80 +
    1.81 +
    1.82 +
    1.83 +
    1.84 +"===== tactic Subproblem: from environment to origin";
    1.85 +"----- ";
    1.86 +
    1.87 +
    1.88 +
    1.89 +
    1.90 +
    1.91 +*}
    1.92 +
    1.93  ML {*print_depth 999*}
    1.94  use "../../../test/Tools/isac/Interpret/rewtools.sml" (**)
    1.95  (*
    1.96 @@ -190,12 +276,12 @@
    1.97  ===== inhibit exn ?===========================================================*)
    1.98  
    1.99  
   1.100 -(*========== inhibit exn ML110317 ==============================================
   1.101 +(*========== inhibit exn WN110318 ==============================================
   1.102  
   1.103  "########### testcode inserted vvv ###########################################";
   1.104  "########### testcode inserted ^^^ ###########################################";
   1.105  
   1.106 -============ inhibit exn ML110317 ============================================*)
   1.107 +============ inhibit exn WN110318 ============================================*)
   1.108  
   1.109  
   1.110  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

     2.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Fri Mar 18 12:42:28 2011 +0100
     2.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Fri Mar 18 17:24:56 2011 +0100
     2.3 @@ -4,17 +4,18 @@
     2.4  12345678901234567890123456789012345678901234567890123456789012345678901234567890
     2.5          10        20        30        40        50        60        70        80
     2.6  *)
     2.7 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     2.8  "--------------------------------------------------------";
     2.9  "table of contents --------------------------------------";
    2.10  "--------------------------------------------------------";
    2.11  "----------- rewriting for usecase1 ---------------------";
    2.12  "----------- mathengine with usecase1 -------------------";
    2.13 +"----------- rewriting for usecase2 ---------------------";
    2.14 +"----------- mathengine with usecase2 -------------------";
    2.15  "--------------------------------------------------------";
    2.16  "--------------------------------------------------------";
    2.17  "--------------------------------------------------------";
    2.18  
    2.19 -(*apparently no way to do these tests within DiophantEq.thy:
    2.20 +(*there seemed to be no way to do these tests within DiophantEq.thy:
    2.21  val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
    2.22    from CalcTreeTest*)
    2.23  (*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
    2.24 @@ -40,19 +41,58 @@
    2.25  "----------- mathengine with usecase1 -------------------";
    2.26  "----------- mathengine with usecase1 -------------------";
    2.27  "----------- mathengine with usecase1 -------------------";
    2.28 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    2.29 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    2.30  val p = e_pos'; val c = [];
    2.31  val (fmz, (thy, pbl, met)) = 
    2.32 -  (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
    2.33 +  (["boolTestGiven (xxx + 111 = abc + (123::int))", "intTestGiven xxx", 
    2.34 +    "intTestFind sss"],
    2.35     (Context.theory_name thy, ["diophantine", "equation"], 
    2.36      ["Test", "solve_diophant"]));
    2.37  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
    2.38  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.39 +(*========== inhibit exn WN110318 ==============================================
    2.40  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.41  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.42  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.43  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.44  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.45  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.46 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    2.47 +============ inhibit exn WN110318 ============================================*)
    2.48 +
    2.49 +"----------- rewriting for usecase2 ---------------------";
    2.50 +"----------- rewriting for usecase2 ---------------------";
    2.51 +val thy = @{theory "Test"};
    2.52 +"----------- rewriting for usecase2 ---------------------";
    2.53 +
    2.54 +val t = parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)";
    2.55 +
    2.56 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
    2.57 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    2.58 +
    2.59 +val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; 
    2.60 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;
    2.61 +
    2.62 +
    2.63 +"----------- mathengine with usecase2 -------------------";
    2.64 +"----------- mathengine with usecase2 -------------------";
    2.65 +"----------- mathengine with usecase2 -------------------";
    2.66 +val p = e_pos'; val c = [];
    2.67 +val (fmz, (thy, pbl, met)) = 
    2.68 +  (["intTestGiven (xxx + abc + -1 * 111 + (123::int))", "intTestFind sss"],
    2.69 +   (Context.theory_name thy, ["inttype","test"], ["Test","intsimp"]));
    2.70 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (thy, pbl, met))];
    2.71 +(*nxt = ("Model_Problem", ...)*)
    2.72 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.73 +(*nxt = ("Add_Given", Add_Given "intTestGiven (xxx + abc + -1 * 111 + 123)")*)
    2.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.75 +(* Add_Find ###########################################*)
    2.76 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.77 +(*nxt = ("Specify_Theory", ...)*)
    2.78 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.79 +(*nxt = ("Specify_Problem", ...)*)
    2.80 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.81 +(*nxt = ("Specify_Method", ...)*)
    2.82 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.83 +(*nxt = ("Empty_Tac", ...) #############################*)
    2.84 +val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    2.85 +(*========== inhibit exn WN110318 ==============================================
    2.86 +============ inhibit exn WN110318 ============================================*)