1.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Wed Oct 05 10:51:25 2016 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml Wed Oct 05 13:09:54 2016 +0200
1.3 @@ -29,7 +29,7 @@
1.4 CalcTree [(["equality (x + 1 = (2::real))", "solveFor x", "solutions L"],
1.5 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
1.6 moveActiveRoot 1;
1.7 -autoCalculate' 1 CompleteCalc;
1.8 +autoCalculate 1 CompleteCalc;
1.9
1.10 (*-->ISA: initContext 1 Thy_ ([1],Frm); *)
1.11 val out = initContext 1 Thy_ ([1],Frm);
2.1 --- a/test/Tools/isac/Frontend/use-cases.sml Wed Oct 05 10:51:25 2016 +0200
2.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Wed Oct 05 13:09:54 2016 +0200
2.3 @@ -110,30 +110,30 @@
2.4
2.5 fetchProposedTactic 1 (*by using Iterator No.1*);
2.6 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
2.7 - autoCalculate' 1 (Step 1);
2.8 + autoCalculate 1 (Step 1);
2.9 refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
2.10 - autoCalculate' 1 (Step 1);
2.11 + autoCalculate 1 (Step 1);
2.12 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
2.13 fetchProposedTactic 1;
2.14 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
2.15 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
2.16 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
2.17
2.18 fetchProposedTactic 1;
2.19 setNextTactic 1 (Add_Given "solveFor x");
2.20 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.21 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.22
2.23 fetchProposedTactic 1;
2.24 setNextTactic 1 (Add_Find "solutions L");
2.25 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.26 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.27
2.28 fetchProposedTactic 1;
2.29 setNextTactic 1 (Specify_Theory "Test");
2.30 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.31 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.32 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
2.33
2.34 fetchProposedTactic 1;
2.35 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
2.36 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.37 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.38 (*-------------------------------------------------------------------------*)
2.39 fetchProposedTactic 1;
2.40 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.41 @@ -141,7 +141,7 @@
2.42 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
2.43 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.44
2.45 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.46 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.47 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.48
2.49 (*-------------------------------------------------------------------------*)
2.50 @@ -154,22 +154,22 @@
2.51 is_complete_mod ptp;
2.52 is_complete_spec ptp;
2.53
2.54 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.55 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.56 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
2.57 (*term2str (get_obj g_form pt [1]);*)
2.58 (*-------------------------------------------------------------------------*)
2.59
2.60 fetchProposedTactic 1;
2.61 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
2.62 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.63 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.64
2.65 fetchProposedTactic 1;
2.66 setNextTactic 1 (Rewrite_Set "Test_simplify");
2.67 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.68 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.69
2.70 fetchProposedTactic 1;
2.71 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
2.72 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.73 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.74
2.75 val ((pt,_),_) = get_calc 1;
2.76 val ip = get_pos 1 1;
2.77 @@ -217,104 +217,104 @@
2.78 refFormula 1 (get_pos 1 1);
2.79 fetchProposedTactic 1;
2.80 setNextTactic 1 (Model_Problem);
2.81 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
2.82 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
2.83
2.84 fetchProposedTactic 1;
2.85 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
2.86 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.87 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.88
2.89 fetchProposedTactic 1;
2.90 setNextTactic 1 (Add_Given "solveFor x");
2.91 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.92 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.93
2.94 fetchProposedTactic 1;
2.95 setNextTactic 1 (Add_Find "solutions L");
2.96 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.97 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.98
2.99 fetchProposedTactic 1;
2.100 setNextTactic 1 (Specify_Theory "Test");
2.101 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.102 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.103
2.104 fetchProposedTactic 1;
2.105 setNextTactic 1 (Specify_Problem
2.106 ["sqroot-test","univariate","equation","test"]);
2.107 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.108 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.109 "1-----------------------------------------------------------------";
2.110
2.111 fetchProposedTactic 1;
2.112 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
2.113 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.114 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.115
2.116 fetchProposedTactic 1;
2.117 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
2.118 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.119 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.120
2.121 fetchProposedTactic 1;
2.122 setNextTactic 1 (Rewrite_Set "norm_equation");
2.123 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.124 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.125
2.126 fetchProposedTactic 1;
2.127 setNextTactic 1 (Rewrite_Set "Test_simplify");
2.128 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.129 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.130
2.131 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
2.132 setNextTactic 1 (Subproblem ("Test",
2.133 ["LINEAR","univariate","equation","test"]));
2.134 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.135 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.136
2.137 fetchProposedTactic 1;
2.138 setNextTactic 1 (Model_Problem );
2.139 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.140 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.141
2.142 fetchProposedTactic 1;
2.143 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
2.144 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.145 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.146
2.147 fetchProposedTactic 1;
2.148 setNextTactic 1 (Add_Given "solveFor x");
2.149 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.150 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.151
2.152 fetchProposedTactic 1;
2.153 setNextTactic 1 (Add_Find "solutions x_i");
2.154 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.155 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.156
2.157 fetchProposedTactic 1;
2.158 setNextTactic 1 (Specify_Theory "Test");
2.159 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.160 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.161
2.162 fetchProposedTactic 1;
2.163 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
2.164 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.165 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.166 "2-----------------------------------------------------------------";
2.167
2.168 fetchProposedTactic 1;
2.169 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
2.170 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.171 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.172
2.173 fetchProposedTactic 1;
2.174 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
2.175 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.176 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.177
2.178 fetchProposedTactic 1;
2.179 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
2.180 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.181 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.182
2.183 fetchProposedTactic 1;
2.184 setNextTactic 1 (Rewrite_Set "Test_simplify");
2.185 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.186 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.187
2.188 fetchProposedTactic 1;
2.189 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
2.190 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.191 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.192
2.193 fetchProposedTactic 1;
2.194 setNextTactic 1 (Check_elementwise "Assumptions");
2.195 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.196 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.197
2.198 val xml = fetchProposedTactic 1;
2.199 setNextTactic 1 (Check_Postcond
2.200 ["sqroot-test","univariate","equation","test"]);
2.201 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.202 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.203
2.204 val ((pt,_),_) = get_calc 1;
2.205 val str = pr_ptree pr_short pt;
2.206 @@ -335,39 +335,39 @@
2.207 ["Test","squ-equ-test-subpbl1"]))];
2.208 Iterator 1;
2.209 moveActiveRoot 1;
2.210 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.211 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.212 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.213 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.214 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.215 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.216 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.217 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.218 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.219 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.220 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.221 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.222 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.223 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.224 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.225 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.226 (*here the solve-phase starts*)
2.227 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.228 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.229 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.230 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.231 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.232 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.233 (*------------------------------------*)
2.234 (* default_print_depth 13; get_calc 1;
2.235 *)
2.236 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.237 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.238 (*calc-head of subproblem*)
2.239 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.240 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.241 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.242 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.243 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.244 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.245 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.246 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.247 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.248 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.249 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.250 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.251 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.252 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.253 (*solve-phase of the subproblem*)
2.254 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.255 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.256 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.257 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.258 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.259 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.260 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.261 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.262 (*finish subproblem*)
2.263 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.264 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.265 (*finish problem*)
2.266 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.267 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.268
2.269 (*this checks the test for correctness..*)
2.270 val ((pt,_),_) = get_calc 1;
2.271 @@ -391,7 +391,7 @@
2.272 moveActiveRoot 1;
2.273 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
2.274
2.275 - autoCalculate' 1 CompleteCalc;
2.276 + autoCalculate 1 CompleteCalc;
2.277 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
2.278 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
2.279
2.280 @@ -414,11 +414,11 @@
2.281 Iterator 1;
2.282 moveActiveRoot 1;
2.283
2.284 - autoCalculate' 1 CompleteCalcHead;
2.285 + autoCalculate 1 CompleteCalcHead;
2.286 refFormula 1 (get_pos 1 1);
2.287 val ((pt,p),_) = get_calc 1;
2.288
2.289 - autoCalculate' 1 CompleteCalc;
2.290 + autoCalculate 1 CompleteCalc;
2.291 val ((pt,p),_) = get_calc 1;
2.292 if p=([], Res) then () else
2.293 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
2.294 @@ -433,7 +433,7 @@
2.295 ["Test","squ-equ-test-subpbl1"]))];
2.296 Iterator 1;
2.297 moveActiveRoot 1;
2.298 - autoCalculate' 1 CompleteCalc;
2.299 + autoCalculate 1 CompleteCalc;
2.300 val ((pt,p),_) = get_calc 1; show_pt pt;
2.301 (*
2.302 getTactic 1 ([1],Frm);
2.303 @@ -461,7 +461,7 @@
2.304 ["Test","squ-equ-test-subpbl1"]))];
2.305 Iterator 1;
2.306 moveActiveRoot 1;
2.307 - autoCalculate' 1 CompleteCalcHead;
2.308 + autoCalculate 1 CompleteCalcHead;
2.309
2.310 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
2.311 cell = NONE, ctxt = ctxt2, meth,
2.312 @@ -483,7 +483,7 @@
2.313 ["Test","solve_linear"]))];
2.314 Iterator 1;
2.315 moveActiveRoot 1;
2.316 - autoCalculate' 1 CompleteModel;
2.317 + autoCalculate 1 CompleteModel;
2.318 refFormula 1 (get_pos 1 1);
2.319
2.320 setProblem 1 ["LINEAR","univariate","equation","test"];
2.321 @@ -500,9 +500,9 @@
2.322 ["Test","solve_linear"]) then ()
2.323 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
2.324
2.325 - autoCalculate' 1 CompleteCalcHead;
2.326 + autoCalculate 1 CompleteCalcHead;
2.327 refFormula 1 (get_pos 1 1);
2.328 - autoCalculate' 1 CompleteCalc;
2.329 + autoCalculate 1 CompleteCalc;
2.330 moveActiveDown 1;
2.331 moveActiveDown 1;
2.332 moveActiveDown 1;
2.333 @@ -522,31 +522,31 @@
2.334 ("Test", ["sqroot-test","univariate","equation","test"],
2.335 ["Test","squ-equ-test-subpbl1"]))];
2.336 Iterator 1; moveActiveRoot 1;
2.337 - autoCalculate' 1 CompleteCalcHead;
2.338 - autoCalculate' 1 (Step 1);
2.339 + autoCalculate 1 CompleteCalcHead;
2.340 + autoCalculate 1 (Step 1);
2.341 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
2.342 (*
2.343 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
2.344 - autoCalculate' 1 (Step 1);
2.345 + autoCalculate 1 (Step 1);
2.346 val ((pt,p),_) = get_calc 1; show_pt pt;
2.347 *)
2.348 "-----^^^^^ and vvvvv do the same -----";
2.349 setContext 1 p "thy_isac_Test-rls-Test_simplify";
2.350 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
2.351
2.352 - autoCalculate' 1 (Step 1);
2.353 + autoCalculate 1 (Step 1);
2.354 setContext 1 p "thy_isac_Test-rls-Test_simplify";
2.355 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
2.356 val (Form f, tac, asms) = pt_extract (pt, p);
2.357 if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
2.358 - then () else error "--- setContext..Thy --- autoCalculate' 1 (Step 1) #1";
2.359 + then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
2.360
2.361 - autoCalculate' 1 CompleteCalc;
2.362 + autoCalculate 1 CompleteCalc;
2.363 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
2.364 val (Form f, tac, asms) = pt_extract (pt, p);
2.365
2.366 if term2str f = "[x = 1]" andalso p = ([], Res) then ()
2.367 - else error "--- setContext..Thy --- autoCalculate' CompleteCalc";
2.368 + else error "--- setContext..Thy --- autoCalculate CompleteCalc";
2.369 DEconstrCalcTree 1;
2.370
2.371 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
2.372 @@ -556,7 +556,7 @@
2.373 ("Test", ["sqroot-test","univariate","equation","test"],
2.374 ["Test","squ-equ-test-subpbl1"]))];
2.375 Iterator 1; moveActiveRoot 1;
2.376 - autoCalculate' 1 CompleteToSubpbl;
2.377 + autoCalculate 1 CompleteToSubpbl;
2.378 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
2.379 val ((pt,_),_) = get_calc 1;
2.380 val str = pr_ptree pr_short pt;
2.381 @@ -565,12 +565,12 @@
2.382 then () else
2.383 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
2.384
2.385 - autoCalculate' 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
2.386 - autoCalculate' 1 CompleteToSubpbl;
2.387 + autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
2.388 + autoCalculate 1 CompleteToSubpbl;
2.389 val ((pt,_),_) = get_calc 1;
2.390 val str = pr_ptree pr_short pt;
2.391 writeln str;
2.392 - autoCalculate' 1 CompleteCalc; (*das geht ohnehin !*);
2.393 + autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
2.394 val ((pt,_),_) = get_calc 1;
2.395 val p = get_pos 1 1;
2.396
2.397 @@ -590,72 +590,72 @@
2.398 fetchProposedTactic 1;
2.399
2.400 setNextTactic 1 (Model_Problem);
2.401 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.402 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.403
2.404 setNextTactic 1 (Specify_Theory "RatEq");
2.405 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.406 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.407 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
2.408 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.409 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.410 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
2.411 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.412 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.413 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
2.414 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.415 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.416 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
2.417 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.418 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.419 setNextTactic 1 (Rewrite_Set "norm_Rational");
2.420 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.421 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.422 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
2.423 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.424 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.425 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
2.426 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
2.427 "univariate","equation"]));
2.428 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.429 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.430 setNextTactic 1 (Model_Problem );
2.431 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.432 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.433 setNextTactic 1 (Specify_Theory "PolyEq");
2.434 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.435 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.436 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
2.437 "univariate","equation"]);
2.438 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.439 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.440 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
2.441 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.442 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.443 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
2.444 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.445 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.446 setNextTactic 1 (Rewrite ("all_left",""));
2.447 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.448 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.449 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
2.450 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.451 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.452 (* __________ for "16 + 12 * x = 0"*)
2.453 setNextTactic 1 (Subproblem ("PolyEq",
2.454 ["degree_1","polynomial","univariate","equation"]));
2.455 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.456 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.457 setNextTactic 1 (Model_Problem );
2.458 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.459 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.460 setNextTactic 1 (Specify_Theory "PolyEq");
2.461 (*------------- some trials in the problem-hierarchy ---------------*)
2.462 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
2.463 - autoCalculate' 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
2.464 + autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
2.465 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
2.466 (*------------------------------------------------------------------*)
2.467 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.468 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.469 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
2.470 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.471 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.472 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
2.473 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.474 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.475 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
2.476 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.477 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.478 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
2.479 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.480 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.481 setNextTactic 1 Or_to_List;
2.482 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.483 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.484 setNextTactic 1 (Check_elementwise "Assumptions");
2.485 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.486 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.487 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
2.488 "univariate","equation"]);
2.489 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.490 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.491 setNextTactic 1 (Check_Postcond ["normalize","polynomial",
2.492 "univariate","equation"]);
2.493 - autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.494 + autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.495 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
2.496 val (ptp,_) = get_calc 1;
2.497 val (Form t,_,_) = pt_extract ptp;
2.498 @@ -683,16 +683,16 @@
2.499 (*..this tactic should be done 'tacitly', too !*)
2.500
2.501 (*
2.502 -autoCalculate' 1 CompleteCalcHead;
2.503 +autoCalculate 1 CompleteCalcHead;
2.504 checkContext 1 ([],Pbl) "pbl_equ_univ";
2.505 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.506 *)
2.507
2.508 - autoCalculate' 1 (Step 1);
2.509 + autoCalculate 1 (Step 1);
2.510
2.511 fetchProposedTactic 1;
2.512 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
2.513 - autoCalculate' 1 (Step 1);
2.514 + autoCalculate 1 (Step 1);
2.515
2.516 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
2.517 initContext 1 Pbl_ ([],Pbl);
2.518 @@ -711,10 +711,10 @@
2.519
2.520
2.521 fetchProposedTactic 1;
2.522 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate' 1 (Step 1);
2.523 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
2.524
2.525 fetchProposedTactic 1;
2.526 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate' 1 (Step 1);
2.527 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
2.528
2.529 "--------- this is a matching model (all items correct): -------";
2.530 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.531 @@ -732,25 +732,25 @@
2.532 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
2.533 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
2.534 "univariate","equation"]);
2.535 - autoCalculate' 1 (Step 1);
2.536 + autoCalculate 1 (Step 1);
2.537 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
2.538 and Specify_Theory skipped in comparison to below ---^^^-inserted *)
2.539 (*------------vvv-inserted-----------------------------------------------*)
2.540 fetchProposedTactic 1;
2.541 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
2.542 "univariate","equation"]);
2.543 - autoCalculate' 1 (Step 1);
2.544 + autoCalculate 1 (Step 1);
2.545
2.546 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
2.547
2.548 fetchProposedTactic 1;
2.549 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
2.550 - autoCalculate' 1 (Step 1);
2.551 + autoCalculate 1 (Step 1);
2.552
2.553 fetchProposedTactic 1;
2.554 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
2.555
2.556 - autoCalculate' 1 CompleteCalc;
2.557 + autoCalculate 1 CompleteCalc;
2.558
2.559 val ((pt,_),_) = get_calc 1;
2.560 show_pt pt;
2.561 @@ -764,15 +764,15 @@
2.562 before, too, because there was no check*)
2.563 fetchProposedTactic 1;
2.564 setNextTactic 1 (Specify_Theory "PolyEq");
2.565 - autoCalculate' 1 (Step 1);
2.566 + autoCalculate 1 (Step 1);
2.567
2.568 fetchProposedTactic 1;
2.569 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
2.570 - autoCalculate' 1 (Step 1);
2.571 + autoCalculate 1 (Step 1);
2.572
2.573 fetchProposedTactic 1;
2.574 "--------- now the calc-header is ready for enter 'solving' ----";
2.575 - autoCalculate' 1 CompleteCalc;
2.576 + autoCalculate 1 CompleteCalc;
2.577
2.578 val ((pt,_),_) = get_calc 1;
2.579 rootthy pt;
2.580 @@ -882,7 +882,7 @@
2.581 fetchProposedTactic 1;
2.582 (*fill the CalcHead with Descriptions...*)
2.583 setNextTactic 1 (Model_Problem );
2.584 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.585 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.586
2.587 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
2.588 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
2.589 @@ -902,7 +902,7 @@
2.590 fetchProposedTactic 1;
2.591 (*the student follows the advice*)
2.592 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
2.593 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
2.594 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.595
2.596 (*this input completes the model*)
2.597 modifyCalcHead 1 (([],Pbl), "not used here",
2.598 @@ -949,7 +949,7 @@
2.599 Pbl,
2.600 ("Test", ["LINEAR","univariate","equation","test"],
2.601 ["Test","solve_linear"]));
2.602 - autoCalculate' 1 CompleteCalc;
2.603 + autoCalculate 1 CompleteCalc;
2.604 refFormula 1 (get_pos 1 1);
2.605 val ((pt,_),_) = get_calc 1;
2.606 val p = get_pos 1 1;
2.607 @@ -967,7 +967,7 @@
2.608 CalcTree [(fmz, sp)];
2.609 Iterator 1; moveActiveRoot 1;
2.610 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
2.611 - autoCalculate' 1 CompleteCalc;
2.612 + autoCalculate 1 CompleteCalc;
2.613 refFormula 1 (get_pos 1 1);
2.614 val ((pt,_),_) = get_calc 1;
2.615 val p = get_pos 1 1;
2.616 @@ -985,7 +985,7 @@
2.617 ["Test","squ-equ-test-subpbl1"]))];
2.618 Iterator 1;
2.619 moveActiveRoot 1;
2.620 - autoCalculate' 1 CompleteCalc;
2.621 + autoCalculate 1 CompleteCalc;
2.622 val ((pt,_),_) = get_calc 1;
2.623 show_pt pt;
2.624
2.625 @@ -1022,7 +1022,7 @@
2.626 ("Test", ["sqroot-test","univariate","equation","test"],
2.627 ["Test","squ-equ-test-subpbl1"]))];
2.628 Iterator 1; moveActiveRoot 1;
2.629 - autoCalculate' 1 CompleteCalc;
2.630 + autoCalculate 1 CompleteCalc;
2.631 val ((pt,_),_) = get_calc 1;
2.632 show_pt pt;
2.633
2.634 @@ -1052,7 +1052,7 @@
2.635 "solveFor x","solutions L"],
2.636 ("RatEq",["univariate","equation"],["no_met"]))];
2.637 Iterator 1; moveActiveRoot 1;
2.638 -autoCalculate' 1 CompleteCalc;
2.639 +autoCalculate 1 CompleteCalc;
2.640 val ((pt,_),_) = get_calc 1;
2.641 val p = get_pos 1 1;
2.642 val (Form f, tac, asms) = pt_extract (pt, p);
2.643 @@ -1092,35 +1092,35 @@
2.644 fetchProposedTactic 1;
2.645 (*ERROR get_calc 1 not existent*)
2.646 setNextTactic 1 (Model_Problem );
2.647 - autoCalculate' 1 (Step 1);
2.648 + autoCalculate 1 (Step 1);
2.649 fetchProposedTactic 1;
2.650 fetchProposedTactic 1;
2.651
2.652 setNextTactic 1 (Add_Find "solutions L");
2.653 setNextTactic 1 (Add_Find "solutions L");
2.654
2.655 - autoCalculate' 1 (Step 1);
2.656 - autoCalculate' 1 (Step 1);
2.657 + autoCalculate 1 (Step 1);
2.658 + autoCalculate 1 (Step 1);
2.659
2.660 setNextTactic 1 (Specify_Theory "Test");
2.661 fetchProposedTactic 1;
2.662 - autoCalculate' 1 (Step 1);
2.663 + autoCalculate 1 (Step 1);
2.664
2.665 - autoCalculate' 1 (Step 1);
2.666 - autoCalculate' 1 (Step 1);
2.667 - autoCalculate' 1 (Step 1);
2.668 - autoCalculate' 1 (Step 1);
2.669 + autoCalculate 1 (Step 1);
2.670 + autoCalculate 1 (Step 1);
2.671 + autoCalculate 1 (Step 1);
2.672 + autoCalculate 1 (Step 1);
2.673 (*------------------------- end calc-head*)
2.674
2.675 fetchProposedTactic 1;
2.676 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
2.677 - autoCalculate' 1 (Step 1);
2.678 + autoCalculate 1 (Step 1);
2.679
2.680 setNextTactic 1 (Rewrite_Set "Test_simplify");
2.681 fetchProposedTactic 1;
2.682 - autoCalculate' 1 (Step 1);
2.683 + autoCalculate 1 (Step 1);
2.684
2.685 - autoCalculate' 1 CompleteCalc;
2.686 + autoCalculate 1 CompleteCalc;
2.687 val ((pt,_),_) = get_calc 1;
2.688 val p = get_pos 1 1;
2.689 val (Form f, tac, asms) = pt_extract (pt, p);
2.690 @@ -1136,9 +1136,9 @@
2.691 ["Test","squ-equ-test-subpbl1"]))];
2.692 Iterator 1;
2.693 moveActiveRoot 1;
2.694 - autoCalculate' 1 CompleteCalcHead;
2.695 - autoCalculate' 1 (Step 1);
2.696 - autoCalculate' 1 (Step 1);
2.697 + autoCalculate 1 CompleteCalcHead;
2.698 + autoCalculate 1 (Step 1);
2.699 + autoCalculate 1 (Step 1);
2.700 appendFormula 1 "-1 + x = 0" (*|> Future.join*);
2.701 (*... returns calcChangedEvent with*)
2.702 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
2.703 @@ -1159,9 +1159,9 @@
2.704 ["Test","squ-equ-test-subpbl1"]))];
2.705 Iterator 1;
2.706 moveActiveRoot 1;
2.707 - autoCalculate' 1 CompleteCalcHead;
2.708 - autoCalculate' 1 (Step 1);
2.709 - autoCalculate' 1 (Step 1);
2.710 + autoCalculate 1 CompleteCalcHead;
2.711 + autoCalculate 1 (Step 1);
2.712 + autoCalculate 1 (Step 1);
2.713 appendFormula 1 "x - 1 = 0" (*|> Future.join*);
2.714 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
2.715 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
2.716 @@ -1182,9 +1182,9 @@
2.717 ["Test","squ-equ-test-subpbl1"]))];
2.718 Iterator 1;
2.719 moveActiveRoot 1;
2.720 - autoCalculate' 1 CompleteCalcHead;
2.721 - autoCalculate' 1 (Step 1);
2.722 - autoCalculate' 1 (Step 1);
2.723 + autoCalculate 1 CompleteCalcHead;
2.724 + autoCalculate 1 (Step 1);
2.725 + autoCalculate 1 (Step 1);
2.726 appendFormula 1 "x = 1" (*|> Future.join*);
2.727 (*... returns calcChangedEvent with*)
2.728 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
2.729 @@ -1206,9 +1206,9 @@
2.730 ["Test","squ-equ-test-subpbl1"]))];
2.731 Iterator 1;
2.732 moveActiveRoot 1;
2.733 - autoCalculate' 1 CompleteCalcHead;
2.734 - autoCalculate' 1 (Step 1);
2.735 - autoCalculate' 1 (Step 1);
2.736 + autoCalculate 1 CompleteCalcHead;
2.737 + autoCalculate 1 (Step 1);
2.738 + autoCalculate 1 (Step 1);
2.739 appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
2.740 (*... returns <ERROR> no derivation found </ERROR>*)
2.741
2.742 @@ -1228,7 +1228,7 @@
2.743 ["Test","squ-equ-test-subpbl1"]))];
2.744 Iterator 1;
2.745 moveActiveRoot 1;
2.746 - autoCalculate' 1 CompleteCalc;
2.747 + autoCalculate 1 CompleteCalc;
2.748 moveActiveFormula 1 ([2],Res);
2.749 replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
2.750 (*... returns <ERROR> formula not changed </ERROR>*)
2.751 @@ -1249,7 +1249,7 @@
2.752 ["Test","squ-equ-test-subpbl1"]))];
2.753 Iterator 2;
2.754 moveActiveRoot 2;
2.755 - autoCalculate' 2 CompleteCalc;
2.756 + autoCalculate 2 CompleteCalc;
2.757 moveActiveFormula 2 ([2],Res);
2.758 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
2.759 (*... returns <ERROR> formula not changed </ERROR>*)
2.760 @@ -1274,7 +1274,7 @@
2.761 ["Test","squ-equ-test-subpbl1"]))];
2.762 Iterator 1;
2.763 moveActiveRoot 1;
2.764 - autoCalculate' 1 CompleteCalc;
2.765 + autoCalculate 1 CompleteCalc;
2.766 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
2.767 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
2.768 (*... returns calcChangedEvent with*)
2.769 @@ -1308,7 +1308,7 @@
2.770 ["Test","squ-equ-test-subpbl1"]))];
2.771 Iterator 1;
2.772 moveActiveRoot 1;
2.773 - autoCalculate' 1 CompleteCalc;
2.774 + autoCalculate 1 CompleteCalc;
2.775 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
2.776 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
2.777 (*... returns calcChangedEvent with ...*)
2.778 @@ -1340,7 +1340,7 @@
2.779 ["Test","squ-equ-test-subpbl1"]))];
2.780 Iterator 1;
2.781 moveActiveRoot 1;
2.782 - autoCalculate' 1 CompleteCalc;
2.783 + autoCalculate 1 CompleteCalc;
2.784 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
2.785 replaceFormula 1 "x - 4711 = 0";
2.786 (*... returns <ERROR> no derivation found </ERROR>*)
2.787 @@ -1362,9 +1362,9 @@
2.788 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
2.789 Iterator 1;
2.790 moveActiveRoot 1;
2.791 -autoCalculate' 1 CompleteCalcHead;
2.792 -autoCalculate' 1 (Step 1);
2.793 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
2.794 +autoCalculate 1 CompleteCalcHead;
2.795 +autoCalculate 1 (Step 1);
2.796 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
2.797 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
2.798 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
2.799 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
2.800 @@ -1414,7 +1414,7 @@
2.801 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
2.802 then () else error "inputFillFormula changed 11";
2.803
2.804 -autoCalculate' 1 CompleteCalc;
2.805 +autoCalculate 1 CompleteCalc;
2.806
2.807 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
2.808 val ((pt, _),_) = get_calc 1;
2.809 @@ -1444,8 +1444,8 @@
2.810 moveActiveRoot 1;
2.811 moveActiveFormula 1 ([],Pbl);
2.812 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
2.813 -autoCalculate' 1 CompleteCalcHead;
2.814 -autoCalculate' 1 (Step 1);
2.815 +autoCalculate 1 CompleteCalcHead;
2.816 +autoCalculate 1 (Step 1);
2.817 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
2.818 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
2.819 --- but in BridgeLog Java <=> SML:
2.820 @@ -1463,7 +1463,7 @@
2.821 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
2.822 Iterator 1;
2.823 moveActiveRoot 1;
2.824 -autoCalculate' 1 CompleteCalc;
2.825 +autoCalculate 1 CompleteCalc;
2.826 val ((pt,p),_) = get_calc 1; show_pt pt;
2.827
2.828 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
2.829 @@ -1477,9 +1477,9 @@
2.830 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
2.831 Iterator 1;
2.832 moveActiveRoot 1;
2.833 -autoCalculate' 1 CompleteCalcHead;
2.834 -autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.835 -autoCalculate' 1 (Step 1); fetchProposedTactic 1;
2.836 +autoCalculate 1 CompleteCalcHead;
2.837 +autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.838 +autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.839 (*
2.840 <NEXTTAC>
2.841 <CALCID> 1 </CALCID>
2.842 @@ -1514,7 +1514,7 @@
2.843 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
2.844 (* then --- UC errpat, fillpat by input ---*)
2.845 *)
2.846 -autoCalculate' 1 CompleteCalc;
2.847 +autoCalculate 1 CompleteCalc;
2.848 val ((pt,p),_) = get_calc 1; show_pt pt;
2.849 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
2.850
3.1 --- a/test/Tools/isac/Interpret/calchead.sml Wed Oct 05 10:51:25 2016 +0200
3.2 +++ b/test/Tools/isac/Interpret/calchead.sml Wed Oct 05 13:09:54 2016 +0200
3.3 @@ -32,7 +32,7 @@
3.4 ["Test","squ-equ-test-subpbl1"]))];
3.5 Iterator 1;
3.6 moveActiveRoot 1;
3.7 - autoCalculate' 1 CompleteCalc;
3.8 + autoCalculate 1 CompleteCalc;
3.9 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
3.10 replaceFormula 1 "x = 1";
3.11 (*... returns calcChangedEvent with ...*)
4.1 --- a/test/Tools/isac/Interpret/ctree.sml Wed Oct 05 10:51:25 2016 +0200
4.2 +++ b/test/Tools/isac/Interpret/ctree.sml Wed Oct 05 13:09:54 2016 +0200
4.3 @@ -389,7 +389,7 @@
4.4 ("Test", ["sqroot-test","univariate","equation","test"],
4.5 ["Test","squ-equ-test-subpbl1"]))];
4.6 Iterator 1; moveActiveRoot 1;
4.7 - autoCalculate' 1 CompleteCalc;
4.8 + autoCalculate 1 CompleteCalc;
4.9
4.10 interSteps 1 ([3,2],Res);
4.11
4.12 @@ -557,7 +557,7 @@
4.13 ("Test", ["sqroot-test","univariate","equation","test"],
4.14 ["Test","squ-equ-test-subpbl1"]))];
4.15 Iterator 1; moveActiveRoot 1;
4.16 - autoCalculate' 1 CompleteCalc;
4.17 + autoCalculate 1 CompleteCalc;
4.18
4.19 val ((pt,_),_) = get_calc 1;
4.20 show_pt pt;
4.21 @@ -594,8 +594,8 @@
4.22 ["LINEAR","univariate","equation","test"],
4.23 ["Test","solve_linear"]))];
4.24 Iterator 1; moveActiveRoot 1;
4.25 - autoCalculate' 1 CompleteCalcHead;
4.26 - autoCalculate' 1 (Step 1);
4.27 + autoCalculate 1 CompleteCalcHead;
4.28 + autoCalculate 1 (Step 1);
4.29 refFormula 1 (get_pos 1 1);
4.30
4.31 moveActiveRoot 1;
4.32 @@ -604,7 +604,7 @@
4.33 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
4.34 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
4.35
4.36 - autoCalculate' 1 (Step 1);
4.37 + autoCalculate 1 (Step 1);
4.38 refFormula 1 (get_pos 1 1);
4.39
4.40 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
4.41 @@ -639,7 +639,7 @@
4.42 ("Test", ["sqroot-test","univariate","equation","test"],
4.43 ["Test","squ-equ-test-subpbl1"]))];
4.44 Iterator 1; moveActiveRoot 1;
4.45 - autoCalculate' 1 CompleteCalc;
4.46 + autoCalculate 1 CompleteCalc;
4.47 moveActiveRoot 1;
4.48 moveActiveDown 1;
4.49 moveActiveDown 1;
4.50 @@ -671,10 +671,10 @@
4.51 ("Test", ["sqroot-test","univariate","equation","test"],
4.52 ["Test","squ-equ-test-subpbl1"]))];
4.53 Iterator 1; moveActiveRoot 1;
4.54 - autoCalculate' 1 CompleteCalcHead;
4.55 - autoCalculate' 1 (Step 1);
4.56 - autoCalculate' 1 (Step 1);
4.57 - autoCalculate' 1 (Step 1);
4.58 + autoCalculate 1 CompleteCalcHead;
4.59 + autoCalculate 1 (Step 1);
4.60 + autoCalculate 1 (Step 1);
4.61 + autoCalculate 1 (Step 1);
4.62 val ((pt,_),_) = get_calc 1;
4.63 val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
4.64 val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
4.65 @@ -705,7 +705,7 @@
4.66 "solveFor x","solutions L"],
4.67 ("RatEq",["univariate","equation"],["no_met"]))];
4.68 Iterator 1; moveActiveRoot 1;
4.69 -autoCalculate' 1 CompleteCalc;
4.70 +autoCalculate 1 CompleteCalc;
4.71
4.72 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
4.73 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
4.74 @@ -899,7 +899,7 @@
4.75 "solveFor x","solutions L"],
4.76 ("RatEq",["univariate","equation"],["no_met"]))];
4.77 Iterator 1; moveActiveRoot 1;
4.78 -autoCalculate' 1 CompleteCalc;
4.79 +autoCalculate 1 CompleteCalc;
4.80 val ((pt,_),_) = get_calc 1;
4.81 val p = get_pos 1 1;
4.82 val (Form f, tac, asms) = pt_extract (pt, p);
4.83 @@ -947,7 +947,7 @@
4.84 ("Test", ["sqroot-test","univariate","equation","test"],
4.85 ["Test","squ-equ-test-subpbl1"]))];
4.86 Iterator 1; moveActiveRoot 1;
4.87 -autoCalculate' 1 CompleteCalc;
4.88 +autoCalculate 1 CompleteCalc;
4.89 val ((pt,_),_) = get_calc 1;
4.90 show_pt pt;
4.91
4.92 @@ -1026,7 +1026,7 @@
4.93 ("Test", ["sqroot-test","univariate","equation","test"],
4.94 ["Test","squ-equ-test-subpbl1"]))];
4.95 Iterator 1; moveActiveRoot 1;
4.96 -autoCalculate' 1 CompleteCalc;
4.97 +autoCalculate 1 CompleteCalc;
4.98 interSteps 1 ([2],Res);
4.99 interSteps 1 ([3,2],Res);
4.100 val ((pt,_),_) = get_calc 1;
5.1 --- a/test/Tools/isac/Interpret/generate.sml Wed Oct 05 10:51:25 2016 +0200
5.2 +++ b/test/Tools/isac/Interpret/generate.sml Wed Oct 05 13:09:54 2016 +0200
5.3 @@ -20,9 +20,9 @@
5.4 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
5.5 Iterator 1;
5.6 moveActiveRoot 1;
5.7 -autoCalculate' 1 CompleteCalcHead;
5.8 -autoCalculate' 1 (Step 1);
5.9 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
5.10 +autoCalculate 1 CompleteCalcHead;
5.11 +autoCalculate 1 (Step 1);
5.12 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
5.13 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
5.14 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
5.15 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
6.1 --- a/test/Tools/isac/Interpret/inform.sml Wed Oct 05 10:51:25 2016 +0200
6.2 +++ b/test/Tools/isac/Interpret/inform.sml Wed Oct 05 13:09:54 2016 +0200
6.3 @@ -56,9 +56,9 @@
6.4 ("Test", ["sqroot-test","univariate","equation","test"],
6.5 ["Test","squ-equ-test-subpbl1"]))];
6.6 Iterator 1; moveActiveRoot 1;
6.7 - autoCalculate' 1 CompleteCalcHead;
6.8 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.9 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.10 + autoCalculate 1 CompleteCalcHead;
6.11 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.12 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.13
6.14 appendFormula 1 "-2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (get_pos 1 1);
6.15 val ((pt,_),_) = get_calc 1;
6.16 @@ -98,11 +98,11 @@
6.17 else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
6.18 ============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
6.19
6.20 - autoCalculate' 1 CompleteCalc;
6.21 + autoCalculate 1 CompleteCalc;
6.22 val ((pt,_),_) = get_calc 1;
6.23 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.24 else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
6.25 - (* autoCalculate' 1 CompleteCalc;
6.26 + (* autoCalculate 1 CompleteCalc;
6.27 val ((pt,p),_) = get_calc 1;
6.28 (writeln o istates2str) (get_obj g_loc pt [ ]);
6.29 (writeln o istates2str) (get_obj g_loc pt [1]);
6.30 @@ -141,8 +141,8 @@
6.31 ("Test", ["sqroot-test","univariate","equation","test"],
6.32 ["Test","squ-equ-test-subpbl1"]))];
6.33 Iterator 1; moveActiveRoot 1;
6.34 - autoCalculate' 1 CompleteCalcHead;
6.35 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
6.36 + autoCalculate 1 CompleteCalcHead;
6.37 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
6.38 appendFormula 1 "2+ -1 + x = 2" (*|> Future.join*); refFormula 1 (get_pos 1 1);
6.39
6.40 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
6.41 @@ -162,7 +162,7 @@
6.42 val (_,(tac,_,_)::_) = get_calc 1;
6.43 if tac = Rewrite_Set "norm_equation" then ()
6.44 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
6.45 - autoCalculate' 1 CompleteCalc;
6.46 + autoCalculate 1 CompleteCalc;
6.47 val ((pt,_),_) = get_calc 1;
6.48 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.49 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
6.50 @@ -176,9 +176,9 @@
6.51 ("Test", ["sqroot-test","univariate","equation","test"],
6.52 ["Test","squ-equ-test-subpbl1"]))];
6.53 Iterator 1; moveActiveRoot 1;
6.54 - autoCalculate' 1 CompleteCalcHead;
6.55 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.56 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.57 + autoCalculate 1 CompleteCalcHead;
6.58 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.59 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.60
6.61 appendFormula 1 "x = 2" (*|> Future.join*);
6.62 val ((pt,p),_) = get_calc 1;
6.63 @@ -192,7 +192,7 @@
6.64 val (_,(tac,_,_)::_) = get_calc 1;
6.65 if tac = Rewrite_Set "Test_simplify" then ()
6.66 else error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
6.67 - autoCalculate' 1 CompleteCalc;
6.68 + autoCalculate 1 CompleteCalc;
6.69 val ((pt,_),_) = get_calc 1;
6.70 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.71 else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
6.72 @@ -206,9 +206,9 @@
6.73 ("Test", ["sqroot-test","univariate","equation","test"],
6.74 ["Test","squ-equ-test-subpbl1"]))];
6.75 Iterator 1; moveActiveRoot 1;
6.76 - autoCalculate' 1 CompleteCalcHead;
6.77 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.78 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.79 + autoCalculate 1 CompleteCalcHead;
6.80 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.81 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.82
6.83 appendFormula 1 "x = 1" (*|> Future.join*);
6.84 val ((pt,p),_) = get_calc 1;
6.85 @@ -222,7 +222,7 @@
6.86 val (_,(tac,_,_)::_) = get_calc 1;
6.87 if tac = Check_Postcond ["LINEAR", "univariate", "equation", "test"] then ()
6.88 else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
6.89 - autoCalculate' 1 CompleteCalc;
6.90 + autoCalculate 1 CompleteCalc;
6.91 val ((pt,_),_) = get_calc 1;
6.92 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.93 else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
6.94 @@ -236,16 +236,16 @@
6.95 ("Test", ["sqroot-test","univariate","equation","test"],
6.96 ["Test","squ-equ-test-subpbl1"]))];
6.97 Iterator 1; moveActiveRoot 1;
6.98 - autoCalculate' 1 CompleteCalcHead;
6.99 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.100 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.101 + autoCalculate 1 CompleteCalcHead;
6.102 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.103 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.104 appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
6.105 val ((pt,p),_) = get_calc 1;
6.106 val str = pr_ptree pr_short pt;
6.107 writeln str;
6.108 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
6.109 else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
6.110 - autoCalculate' 1 CompleteCalc;
6.111 + autoCalculate 1 CompleteCalc;
6.112 val ((pt,p),_) = get_calc 1;
6.113 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
6.114 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
6.115 @@ -261,10 +261,10 @@
6.116 ("Test", ["sqroot-test","univariate","equation","test"],
6.117 ["Test","squ-equ-test-subpbl1"]))];
6.118 Iterator 1; moveActiveRoot 1;
6.119 - autoCalculate' 1 CompleteCalcHead;
6.120 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.121 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.122 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
6.123 + autoCalculate 1 CompleteCalcHead;
6.124 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.125 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.126 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
6.127
6.128 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
6.129 val ((pt,_),_) = get_calc 1;
6.130 @@ -293,7 +293,7 @@
6.131 "2.6. 1 + x + -2 * 1 = 0\n" then()
6.132 else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
6.133
6.134 - autoCalculate' 1 CompleteCalc;
6.135 + autoCalculate 1 CompleteCalc;
6.136 val ((pt,pos as (p,_)),_) = get_calc 1;
6.137 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst) (get_obj g_result pt p) then()
6.138 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
6.139 @@ -306,9 +306,9 @@
6.140 ("Test", ["sqroot-test","univariate","equation","test"],
6.141 ["Test","squ-equ-test-subpbl1"]))];
6.142 Iterator 1; moveActiveRoot 1;
6.143 - autoCalculate' 1 CompleteCalcHead;
6.144 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.145 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.146 + autoCalculate 1 CompleteCalcHead;
6.147 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.148 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.149
6.150 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
6.151 val ((pt,_),_) = get_calc 1;
6.152 @@ -316,7 +316,7 @@
6.153 writeln str;
6.154 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
6.155 else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
6.156 - autoCalculate' 1 CompleteCalc;
6.157 + autoCalculate 1 CompleteCalc;
6.158 val ((pt,pos as (p,_)),_) = get_calc 1;
6.159 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
6.160 else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
6.161 @@ -330,8 +330,8 @@
6.162 ("Test", ["sqroot-test","univariate","equation","test"],
6.163 ["Test","squ-equ-test-subpbl1"]))];
6.164 Iterator 1; moveActiveRoot 1;
6.165 - autoCalculate' 1 CompleteCalcHead;
6.166 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.167 + autoCalculate 1 CompleteCalcHead;
6.168 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.169
6.170 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
6.171 val ((pt,_),_) = get_calc 1;
6.172 @@ -339,7 +339,7 @@
6.173 writeln str;
6.174 if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
6.175 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
6.176 - autoCalculate' 1 CompleteCalc;
6.177 + autoCalculate 1 CompleteCalc;
6.178 val ((pt,pos as (p,_)),_) = get_calc 1;
6.179 if pos = ([],Res) andalso "[x = 1]" = (term2str o fst)(get_obj g_result pt p) then()
6.180 else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
6.181 @@ -353,7 +353,7 @@
6.182 ("Test", ["sqroot-test","univariate","equation","test"],
6.183 ["Test","squ-equ-test-subpbl1"]))];
6.184 Iterator 1; moveActiveRoot 1;
6.185 - autoCalculate' 1 CompleteCalc;
6.186 + autoCalculate 1 CompleteCalc;
6.187 moveActiveRoot 1; moveActiveDown 1;
6.188 if get_pos 1 1 = ([1], Frm) then ()
6.189 else error "inform.sml: diff.behav. cut calculation 1";
6.190 @@ -449,9 +449,9 @@
6.191 ("Test", ["sqroot-test","univariate","equation","test"],
6.192 ["Test","squ-equ-test-subpbl1"]))];
6.193 Iterator 1; moveActiveRoot 1;
6.194 - autoCalculate' 1 CompleteCalcHead;
6.195 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.196 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.197 + autoCalculate 1 CompleteCalcHead;
6.198 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
6.199 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
6.200
6.201 appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
6.202 val ((pt,_),_) = get_calc 1;
6.203 @@ -483,7 +483,7 @@
6.204 Iterator 1;
6.205 moveActiveRoot 1;
6.206 replaceFormula 1 "solve(x+1=2,x)";
6.207 -autoCalculate' 1 CompleteCalc;
6.208 +autoCalculate 1 CompleteCalc;
6.209 val ((pt,p),_) = get_calc 1;
6.210 show_pt pt;
6.211 if p = ([], Res) then ()
6.212 @@ -497,11 +497,11 @@
6.213 CalcTree [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
6.214 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
6.215 Iterator 1; moveActiveRoot 1;
6.216 -autoCalculate' 1 CompleteCalcHead;
6.217 +autoCalculate 1 CompleteCalcHead;
6.218
6.219 "--- (-1) give a preview on the calculation without any input";
6.220 (*
6.221 -autoCalculate' 1 CompleteCalc;
6.222 +autoCalculate 1 CompleteCalc;
6.223 val ((pt, p), _) = get_calc 1;
6.224 show_pt pt;
6.225 [
6.226 @@ -515,8 +515,8 @@
6.227 EXAMPLE NOT OPTIMAL
6.228 *)
6.229 "--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
6.230 -autoCalculate' 1 (Step 1);
6.231 -autoCalculate' 1 (Step 1);
6.232 +autoCalculate 1 (Step 1);
6.233 +autoCalculate 1 (Step 1);
6.234 val ((pt, p), _) = get_calc 1;
6.235 (*show_pt pt;
6.236 [
6.237 @@ -543,7 +543,7 @@
6.238
6.239 "--- (2) input the next formula that would be presented by mat-engine";
6.240 (* generate a preview:
6.241 -autoCalculate' 1 (Step 1);
6.242 +autoCalculate 1 (Step 1);
6.243 val ((pt, p), _) = get_calc 1;
6.244 show_pt pt;
6.245 [
6.246 @@ -594,7 +594,7 @@
6.247 else error ("inform.sml: [rational,simplification] 3");
6.248
6.249 "--- (4) finish the calculation + check the postcondition (in the future)";
6.250 -autoCalculate' 1 CompleteCalc;
6.251 +autoCalculate 1 CompleteCalc;
6.252 val ((pt, p), _) = get_calc 1;
6.253 val (t, asm) = get_obj g_result pt [];
6.254 if term2str t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
6.255 @@ -648,7 +648,7 @@
6.256
6.257 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
6.258 (*081016 NOT necessary (but leave it in Java):*)
6.259 -(*6>*)(*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
6.260 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
6.261 "----- here the CalcHead has been completed --- ONCE MORE ?????";
6.262
6.263 (***difference II***)
6.264 @@ -678,7 +678,7 @@
6.265 writeln"-----------------------------------------------------------";
6.266 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
6.267 (*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
6.268 -autoCalculate' 1 CompleteCalc;
6.269 +autoCalculate 1 CompleteCalc;
6.270 val ((pt,p),_) = get_calc 1;
6.271 val Form res = (#1 o pt_extract) (pt, ([],Res));
6.272 show_pt pt;
6.273 @@ -694,7 +694,7 @@
6.274 (*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
6.275 (*3>*)Iterator 1; moveActiveRoot 1;
6.276
6.277 -(*6>*)(*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
6.278 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
6.279 (***difference II***)
6.280 val ((pt,_),_) = get_calc 1;
6.281 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
6.282 @@ -720,7 +720,7 @@
6.283 (3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
6.284 writeln"-----------------------------------------------------------";
6.285 (*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
6.286 -autoCalculate' 1 (Step 1);
6.287 +autoCalculate 1 (Step 1);
6.288 val ((pt,p),_) = get_calc 1;
6.289 val Form res = (#1 o pt_extract) (pt, p);
6.290 if term2str res = "d_d x (x ^^^ 2 + x + 1)" then ()
6.291 @@ -996,10 +996,10 @@
6.292 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.293 Iterator 1;
6.294 moveActiveRoot 1;
6.295 -autoCalculate' 1 CompleteCalcHead;
6.296 -autoCalculate' 1 (Step 1);
6.297 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.298 -(*autoCalculate' 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
6.299 +autoCalculate 1 CompleteCalcHead;
6.300 +autoCalculate 1 (Step 1);
6.301 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.302 +(*autoCalculate 1 (Step 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
6.303
6.304 "~~~~~ fun appendFormula, args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
6.305 val cs = get_calc cI
6.306 @@ -1116,9 +1116,9 @@
6.307 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.308 Iterator 1;
6.309 moveActiveRoot 1;
6.310 -autoCalculate' 1 CompleteCalcHead;
6.311 -autoCalculate' 1 (Step 1);
6.312 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.313 +autoCalculate 1 CompleteCalcHead;
6.314 +autoCalculate 1 (Step 1);
6.315 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.316 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
6.317 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
6.318 (*or
6.319 @@ -1198,9 +1198,9 @@
6.320 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
6.321 Iterator 1;
6.322 moveActiveRoot 1;
6.323 -autoCalculate' 1 CompleteCalcHead;
6.324 -autoCalculate' 1 (Step 1);
6.325 -autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.326 +autoCalculate 1 CompleteCalcHead;
6.327 +autoCalculate 1 (Step 1);
6.328 +autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
6.329 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
6.330 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
6.331 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
7.1 --- a/test/Tools/isac/Interpret/mathengine.sml Wed Oct 05 10:51:25 2016 +0200
7.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Wed Oct 05 13:09:54 2016 +0200
7.3 @@ -17,7 +17,7 @@
7.4 "----------- fun step: Apply_Method without init_form ---";
7.5 "----------- fun step -----------------------------------";
7.6 "----------- fun autocalc -------------------------------";
7.7 -"----------- fun autoCalculate' --------------------------";
7.8 +"----------- fun autoCalculate --------------------------";
7.9 "----------- fun autoCalculate..CompleteCalc ------------";
7.10 "----------- search for Or_to_List ----------------------";
7.11 "----------- check thy in CalcTreeTEST ------------------";
7.12 @@ -205,7 +205,7 @@
7.13 "solveFor x", "solutions L"],
7.14 ("RatEq",["univariate","equation"],["no_met"]))];
7.15 Iterator 1;
7.16 -moveActiveRoot 1; autoCalculate' 1 CompleteCalc;
7.17 +moveActiveRoot 1; autoCalculate 1 CompleteCalc;
7.18
7.19 refineProblem 1 ([1],Res) "pbl_equ_univ"
7.20 (*gives "pbl_equ_univ_rat" correct*);
7.21 @@ -227,7 +227,7 @@
7.22 moveActiveRoot 1;
7.23 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
7.24 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
7.25 -(*completeCalcHead*)autoCalculate' 1 CompleteCalcHead;
7.26 +(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
7.27 (*completeCalcHead*)getActiveFormula 1 ;
7.28 (*completeCalcHead*)refFormula 1 ([],Met);
7.29 refFormula 1 ([],Pbl);
7.30 @@ -339,9 +339,9 @@
7.31 ========== inhibit exn AK110718 ==============================================*)
7.32
7.33
7.34 -"----------- fun autoCalculate' -----------------------------------";
7.35 -"----------- fun autoCalculate' -----------------------------------";
7.36 -"----------- fun autoCalculate' -----------------------------------";
7.37 +"----------- fun autoCalculate -----------------------------------";
7.38 +"----------- fun autoCalculate -----------------------------------";
7.39 +"----------- fun autoCalculate -----------------------------------";
7.40 reset_states ();
7.41 CalcTree (*ATTENTION: encode_fmz ... unlike CalcTreeTEST*)
7.42 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
7.43 @@ -352,42 +352,42 @@
7.44 modeling is skipped FIXME
7.45 see test/../interface -- solve_linear as rootpbl FE -- for OTHER expl:
7.46 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
7.47 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
7.48 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
7.49
7.50 fetchProposedTactic 1;
7.51 setNextTactic 1 (Add_Given "solveFor x");
7.52 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
7.53 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
7.54
7.55 fetchProposedTactic 1;
7.56 setNextTactic 1 (Add_Find "solutions L");
7.57 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
7.58 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
7.59
7.60 fetchProposedTactic 1;
7.61 setNextTactic 1 (Specify_Theory "Test");
7.62 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
7.63 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
7.64 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
7.65 -autoCalculate' 1 (Step 1);
7.66 +autoCalculate 1 (Step 1);
7.67 "----- step 1 ---";
7.68 -autoCalculate' 1 (Step 1);
7.69 +autoCalculate 1 (Step 1);
7.70 "----- step 2 ---";
7.71 -autoCalculate' 1 (Step 1);
7.72 +autoCalculate 1 (Step 1);
7.73 "----- step 3 ---";
7.74 -autoCalculate' 1 (Step 1);
7.75 +autoCalculate 1 (Step 1);
7.76 "----- step 4 ---";
7.77 -autoCalculate' 1 (Step 1);
7.78 +autoCalculate 1 (Step 1);
7.79 "----- step 5 ---";
7.80 -autoCalculate' 1 (Step 1);
7.81 +autoCalculate 1 (Step 1);
7.82 "----- step 6 ---";
7.83 -autoCalculate' 1 (Step 1);
7.84 +autoCalculate 1 (Step 1);
7.85 "----- step 7 ---";
7.86 -autoCalculate' 1 (Step 1);
7.87 +autoCalculate 1 (Step 1);
7.88 "----- step 8 ---";
7.89 -autoCalculate' 1 (Step 1);
7.90 +autoCalculate 1 (Step 1);
7.91 val (ptp as (_, p), _) = get_calc 1;
7.92 val (Form t,_,_) = pt_extract ptp;
7.93
7.94 if term2str t = "c + x + 1 / 3 * x ^^^ 3" andalso p = ([], Res) then ()
7.95 -else error "mathengine.sml -- fun autoCalculate' -- end";
7.96 +else error "mathengine.sml -- fun autoCalculate -- end";
7.97
7.98 "----------- fun autoCalculate..CompleteCalc ------------";
7.99 "----------- fun autoCalculate..CompleteCalc ------------";
7.100 @@ -398,7 +398,7 @@
7.101 ["Test","squ-equ-test-subpbl1"]))];
7.102 Iterator 1;
7.103 moveActiveRoot 1;
7.104 -(*autoCalculate' 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
7.105 +(*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
7.106 "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
7.107 val pold = get_pos cI 1;
7.108 (*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
7.109 @@ -570,10 +570,10 @@
7.110 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
7.111 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
7.112 moveActiveRoot 1;
7.113 -autoCalculate' 1 CompleteCalcHead;
7.114 -autoCalculate' 1 (Step 1);
7.115 -autoCalculate' 1 (Step 1);
7.116 -autoCalculate' 1 (Step 1);
7.117 +autoCalculate 1 CompleteCalcHead;
7.118 +autoCalculate 1 (Step 1);
7.119 +autoCalculate 1 (Step 1);
7.120 +autoCalculate 1 (Step 1);
7.121 getTactic 1 ([1],Frm); (*<RULESET> norm_equation </RULESET>*)
7.122 interSteps 1 ([1],Res);
7.123 "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1],Res));
7.124 @@ -687,8 +687,8 @@
7.125 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
7.126 ("Test",["sqroot-test","univariate","equation","test"],["Test","squ-equ-test-subpbl1"]))];
7.127 moveActiveRoot 1;
7.128 -autoCalculate' 1 CompleteCalcHead;
7.129 -autoCalculate' 1 (Step 1);
7.130 +autoCalculate 1 CompleteCalcHead;
7.131 +autoCalculate 1 (Step 1);
7.132
7.133 val cs = get_calc cI (* we improve from the calcstate here [*] *);
7.134 val pos as (_,p_) = get_pos cI 1 (* we improve from the calcstate here [*] *);
8.1 --- a/test/Tools/isac/Interpret/me.sml Wed Oct 05 10:51:25 2016 +0200
8.2 +++ b/test/Tools/isac/Interpret/me.sml Wed Oct 05 13:09:54 2016 +0200
8.3 @@ -34,7 +34,7 @@
8.4 "solveFor x","solutions L"],
8.5 ("RatEq",["univariate","equation"],["no_met"]))];
8.6 Iterator 1; moveActiveRoot 1;
8.7 -autoCalculate' 1 CompleteCalc;
8.8 +autoCalculate 1 CompleteCalc;
8.9
8.10 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
8.11 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
8.12 @@ -228,7 +228,7 @@
8.13 "solveFor x","solutions L"],
8.14 ("RatEq",["univariate","equation"],["no_met"]))];
8.15 Iterator 1; moveActiveRoot 1;
8.16 -autoCalculate' 1 CompleteCalc;
8.17 +autoCalculate 1 CompleteCalc;
8.18 val ((pt,_),_) = get_calc 1;
8.19 val p = get_pos 1 1;
8.20 val (Form f, tac, asms) = pt_extract (pt, p);
8.21 @@ -384,27 +384,27 @@
8.22 Iterator 1; moveActiveRoot 1;
8.23
8.24 (*
8.25 - autoCalculate' 1 CompleteCalcHead;
8.26 - autoCalculate' 1 (Step 1);
8.27 + autoCalculate 1 CompleteCalcHead;
8.28 + autoCalculate 1 (Step 1);
8.29 refFormula 1 (get_pos 1 1);
8.30
8.31 ... works
8.32
8.33 - autoCalculate' 1 CompleteCalcHead;
8.34 + autoCalculate 1 CompleteCalcHead;
8.35 fetchProposedTactic 1; (*-> Apply_Method*);
8.36 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
8.37 - autoCalculate' 1 (Step 1);
8.38 + autoCalculate 1 (Step 1);
8.39 refFormula 1 (get_pos 1 1);
8.40
8.41 ... works *)
8.42
8.43 - autoCalculate' 1 (Step 1);
8.44 + autoCalculate 1 (Step 1);
8.45 refFormula 1 (get_pos 1 1);
8.46
8.47 - autoCalculate' 1 CompleteModel;
8.48 + autoCalculate 1 CompleteModel;
8.49 refFormula 1 (get_pos 1 1);
8.50
8.51 - autoCalculate' 1 CompleteCalcHead;
8.52 + autoCalculate 1 CompleteCalcHead;
8.53 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
8.54
8.55
9.1 --- a/test/Tools/isac/Interpret/rewtools.sml Wed Oct 05 10:51:25 2016 +0200
9.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Oct 05 13:09:54 2016 +0200
9.3 @@ -68,7 +68,7 @@
9.4 ["diff","integration"]))];
9.5 Iterator 1;
9.6 moveActiveRoot 1;
9.7 -autoCalculate' 1 CompleteCalc;
9.8 +autoCalculate 1 CompleteCalc;
9.9 interSteps 1 ([1],Res);
9.10 interSteps 1 ([1,1],Res);
9.11 val ((pt,p),_) = get_calc 1; show_pt pt;
9.12 @@ -84,7 +84,7 @@
9.13 ("Test", ["sqroot-test","univariate","equation","test"],
9.14 ["Test","squ-equ-test-subpbl1"]))];
9.15 Iterator 1; moveActiveRoot 1;
9.16 -autoCalculate' 1 CompleteCalc;
9.17 +autoCalculate 1 CompleteCalc;
9.18
9.19 "----- no thy-context at result -----";
9.20 val p = ([], Res);
9.21 @@ -238,13 +238,13 @@
9.22 ["Test","squ-equ-test-subpbl1"]))];
9.23 Iterator 1; moveActiveRoot 1;
9.24
9.25 -autoCalculate' 1 CompleteCalcHead;
9.26 -autoCalculate' 1 (Step 1);
9.27 +autoCalculate 1 CompleteCalcHead;
9.28 +autoCalculate 1 (Step 1);
9.29 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.30 initContext 1 Thy_ ([1], Frm);
9.31 checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
9.32
9.33 -autoCalculate' 1 (Step 1);
9.34 +autoCalculate 1 (Step 1);
9.35 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.36 initContext 1 Thy_ ([1], Res);
9.37 checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
9.38 @@ -283,13 +283,13 @@
9.39 ["LINEAR","univariate","equation","test"],
9.40 ["Test","solve_linear"]))];
9.41 Iterator 1; moveActiveRoot 1;
9.42 -autoCalculate' 1 CompleteCalcHead;
9.43 +autoCalculate 1 CompleteCalcHead;
9.44
9.45 -autoCalculate' 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.46 +autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.47 if is_curr_endof_calc pt ([1],Frm) then ()
9.48 else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
9.49
9.50 -autoCalculate' 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.51 +autoCalculate 1 (Step 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.52
9.53 if not (is_curr_endof_calc pt ([1],Frm)) then ()
9.54 else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
9.55 @@ -306,7 +306,7 @@
9.56 ["LINEAR","univariate","equation","test"],
9.57 ["Test","solve_linear"]))];
9.58 Iterator 1; moveActiveRoot 1;
9.59 -autoCalculate' 1 CompleteCalc;
9.60 +autoCalculate 1 CompleteCalc;
9.61 interSteps 1 ([1],Res);
9.62
9.63 val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
9.64 @@ -375,9 +375,9 @@
9.65 ["MomentBestimmte","Biegelinien"],
9.66 ["IntegrierenUndKonstanteBestimmen"]))];
9.67 moveActiveRoot 1;
9.68 -autoCalculate' 1 CompleteCalcHead;
9.69 -autoCalculate' 1 (Step 1) (*Apply_Method*);
9.70 -autoCalculate' 1 (Step 1) (*->GENERATED ([1], Frm)*);
9.71 +autoCalculate 1 CompleteCalcHead;
9.72 +autoCalculate 1 (Step 1) (*Apply_Method*);
9.73 +autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
9.74 (*========== inhibit exn 110718 ================================================
9.75
9.76 "--- this was corrupted before 'fun string_of_thmI'";
10.1 --- a/test/Tools/isac/Interpret/script.sml Wed Oct 05 10:51:25 2016 +0200
10.2 +++ b/test/Tools/isac/Interpret/script.sml Wed Oct 05 13:09:54 2016 +0200
10.3 @@ -190,9 +190,9 @@
10.4 ["Test","squ-equ-test-subpbl1"]))];
10.5 Iterator 1;
10.6 moveActiveRoot 1;
10.7 -autoCalculate' 1 CompleteCalcHead;
10.8 -autoCalculate' 1 (Step 1);
10.9 -autoCalculate' 1 (Step 1);
10.10 +autoCalculate 1 CompleteCalcHead;
10.11 +autoCalculate 1 (Step 1);
10.12 +autoCalculate 1 (Step 1);
10.13 val ((pt, p), _) = get_calc 1; show_pt pt;
10.14 val appltacs = sel_appl_atomic_tacs pt p;
10.15 if appltacs =
10.16 @@ -239,7 +239,7 @@
10.17 (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
10.18 assoc_thy;
10.19
10.20 -autoCalculate' 1 CompleteCalc;
10.21 +autoCalculate 1 CompleteCalc;
10.22
10.23 "----------- fun init_form, fun get_stac -------------------------";
10.24 "----------- fun init_form, fun get_stac -------------------------";
10.25 @@ -479,7 +479,7 @@
10.26 ["Test","squ-equ-test-subpbl1"]))];
10.27 Iterator 1;
10.28 moveActiveRoot 1;
10.29 - autoCalculate' 1 CompleteCalc;
10.30 + autoCalculate 1 CompleteCalc;
10.31 val ((pt,_),_) = get_calc 1;
10.32 show_pt pt;
10.33
10.34 @@ -522,7 +522,7 @@
10.35 ["Test","squ-equ-test-subpbl1"]))];
10.36 Iterator 1;
10.37 moveActiveRoot 1;
10.38 - autoCalculate' 1 CompleteCalc;
10.39 + autoCalculate 1 CompleteCalc;
10.40
10.41 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
10.42 fetchApplicableTactics 1 99999 ([],Pbl);
11.1 --- a/test/Tools/isac/Interpret/solve.sml Wed Oct 05 10:51:25 2016 +0200
11.2 +++ b/test/Tools/isac/Interpret/solve.sml Wed Oct 05 13:09:54 2016 +0200
11.3 @@ -44,7 +44,7 @@
11.4 CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))", "normalform N"],
11.5 ("Rational", ["rational","simplification"], ["simplification","of_rationals"]))];
11.6 moveActiveRoot 1;
11.7 -autoCalculate' 1 CompleteCalc;
11.8 +autoCalculate 1 CompleteCalc;
11.9 val ((pt, _), _) = get_calc 1; show_pt pt;
11.10 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
11.11 | _ => error "solve.sml: interSteps on norm_Rational 1";
12.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Wed Oct 05 10:51:25 2016 +0200
12.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Wed Oct 05 13:09:54 2016 +0200
12.3 @@ -246,13 +246,13 @@
12.4 CalcTree [(fmz, (dI,pI,mI))];
12.5 Iterator 1;
12.6 moveActiveRoot 1;
12.7 -autoCalculate' 1 CompleteCalc;
12.8 +autoCalculate 1 CompleteCalc;
12.9
12.10 val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
12.11 val (Form f, tac, asms) = pt_extract (pt, p);
12.12 if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
12.13 andalso p = ([], Res) then ()
12.14 - else error "inv Z, exp 1 autoCalculate' changed"
12.15 + else error "inv Z, exp 1 autoCalculate changed"
12.16
12.17
12.18 "----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
12.19 @@ -266,13 +266,13 @@
12.20 CalcTree [(fmz, (dI,pI,mI))];
12.21 Iterator 1;
12.22 moveActiveRoot 1;
12.23 -autoCalculate' 1 CompleteCalc;
12.24 +autoCalculate 1 CompleteCalc;
12.25
12.26 val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
12.27 val (Form f, tac, asms) = pt_extract (pt, p);
12.28 if term2str f = "X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]"
12.29 andalso p = ([], Res) then ()
12.30 - else error "inv Z, exp 1 autoCalculate' changed"
12.31 + else error "inv Z, exp 1 autoCalculate changed"
12.32
12.33 show_pt pt;
12.34 (*[
12.35 @@ -351,12 +351,12 @@
12.36 ML {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; *}
12.37 text {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; *}
12.38 ML {* "##### 1.<NEXT> ############################################" *}
12.39 -ML {* (*completeCalcHead*)autoCalculate' 1 CompleteCalcHead; *}
12.40 +ML {* (*completeCalcHead*)autoCalculate 1 CompleteCalcHead; *}
12.41 text {* (*completeCalcHead*)getActiveFormula 1 ; *}
12.42 text {* (*completeCalcHead*)refFormula 1 ([],Met); *}
12.43 text {* refFormula 1 ([],Pbl); *}
12.44 text {* fetchProposedTactic 1; *}
12.45 -ML {* autoCalculate' 1 (Step 1); *}
12.46 +ML {* autoCalculate 1 (Step 1); *}
12.47 text {* getFormulaeFromTo 1 ([],Met) ([1],Frm) 0 false; *}
12.48 text {* getFormulaeFromTo 1 ([],Met) ([1],Frm) 0 false; *}
12.49 ML {* refFormula 1 ([1],Frm); *}
12.50 @@ -364,7 +364,7 @@
12.51 text {* refFormula 1 ([1],Frm); *}
12.52 ML {* "##### 2.<NEXT> ############################################" *}
12.53 text {* refFormula 1 ([1],Frm); *}
12.54 -ML {* autoCalculate' 1 (Step 1); *}
12.55 +ML {* autoCalculate 1 (Step 1); *}
12.56 text {* getFormulaeFromTo 1 ([1],Frm) ([1],Res) 0 false; *}
12.57 text {* getFormulaeFromTo 1 ([1],Frm) ([1],Res) 0 false; *}
12.58 ML {* refFormula 1 ([1],Res); *}
12.59 @@ -372,7 +372,7 @@
12.60 ML {* refFormula 1 ([1],Res); *}
12.61 ML {* "##### 3.<NEXT> ############################################" *}
12.62 text {* refFormula 1 ([1],Res); *}
12.63 -ML {* autoCalculate' 1 (Step 1); *}
12.64 +ML {* autoCalculate 1 (Step 1); *}
12.65 text {* getFormulaeFromTo 1 ([1],Res) ([2],Res) 0 false; *}
12.66 text {* getFormulaeFromTo 1 ([1],Res) ([2],Res) 0 false; *}
12.67 ML {* refFormula 1 ([2],Res); *}
12.68 @@ -380,7 +380,7 @@
12.69 text {* refFormula 1 ([2],Res); *}
12.70 ML {* "##### 4.<NEXT> ############################################" *}
12.71 text {* refFormula 1 ([2],Res); *}
12.72 -ML {* autoCalculate' 1 (Step 1); *}
12.73 +ML {* autoCalculate 1 (Step 1); *}
12.74 text {* getFormulaeFromTo 1 ([2],Res) ([3],Frm) 0 false; *}
12.75 text {* getFormulaeFromTo 1 ([2],Res) ([3],Frm) 0 false; *}
12.76 ML {* refFormula 1 ([3],Frm); *}
12.77 @@ -388,7 +388,7 @@
12.78 text {* refFormula 1 ([3],Frm); *}
12.79 ML {* "##### 5.<NEXT> ############################################" *}
12.80 text {* refFormula 1 ([3],Frm); *}
12.81 -ML {* autoCalculate' 1 (Step 1); *}
12.82 +ML {* autoCalculate 1 (Step 1); *}
12.83 text {*<CALCMESSAGE> helpless </CALCMESSAGE>*}
12.84 ====================================================================*)
12.85
13.1 --- a/test/Tools/isac/Knowledge/algein.sml Wed Oct 05 10:51:25 2016 +0200
13.2 +++ b/test/Tools/isac/Knowledge/algein.sml Wed Oct 05 13:09:54 2016 +0200
13.3 @@ -90,7 +90,7 @@
13.4 ["Berechnung","erstSymbolisch"]))];
13.5 Iterator 1;
13.6 moveActiveRoot 1;
13.7 -autoCalculate' 1 CompleteCalc;
13.8 +autoCalculate 1 CompleteCalc;
13.9 val ((pt,p),_) = get_calc 1; show_pt pt;
13.10 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "L = 104" then()
13.11 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
14.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Wed Oct 05 10:51:25 2016 +0200
14.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Wed Oct 05 13:09:54 2016 +0200
14.3 @@ -10,7 +10,7 @@
14.4 "----------- IntegrierenUndKonstanteBestimmen by rewriting -------";
14.5 "----------- simplify_leaf for this script -----------------------";
14.6 "----------- Bsp 7.27 me -----------------------------------------";
14.7 -"----------- Bsp 7.27 autoCalculate' ------------------------------";
14.8 +"----------- Bsp 7.27 autoCalculate ------------------------------";
14.9 "----------- SubProblem (_,[vonBelastungZu,Biegelinien] ----------";
14.10 "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
14.11 "----------- method [Biegelinien,setzeRandbedingungenEin] + exec -";
14.12 @@ -367,9 +367,9 @@
14.13 (Integral L * q_0 * x / 2 D x + Integral -1 * q_0 * x ^^^ 2 / 2 D x) / EI +
14.14 c)]*)
14.15
14.16 -"----------- Bsp 7.27 autoCalculate' ------------------------------";
14.17 -"----------- Bsp 7.27 autoCalculate' ------------------------------";
14.18 -"----------- Bsp 7.27 autoCalculate' ------------------------------";
14.19 +"----------- Bsp 7.27 autoCalculate ------------------------------";
14.20 +"----------- Bsp 7.27 autoCalculate ------------------------------";
14.21 +"----------- Bsp 7.27 autoCalculate ------------------------------";
14.22 reset_states ();
14.23 CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
14.24 "RandbedingungenBiegung [y 0 = 0, y L = 0]",
14.25 @@ -379,7 +379,7 @@
14.26 ["MomentBestimmte","Biegelinien"],
14.27 ["IntegrierenUndKonstanteBestimmen"]))];
14.28 moveActiveRoot 1;
14.29 - autoCalculate' 1 CompleteCalcHead;
14.30 + autoCalculate 1 CompleteCalcHead;
14.31
14.32 fetchProposedTactic 1 (*->"Apply_Method" IntegrierenUndKonstanteBestimmen*);
14.33 (*
14.34 @@ -387,12 +387,12 @@
14.35 > is = e_scrstate;
14.36 val it = true : bool
14.37 *)
14.38 - autoCalculate' 1 (Step 1) (*->GENERATED ([1], Frm)*);
14.39 + autoCalculate 1 (Step 1) (*->GENERATED ([1], Frm)*);
14.40 val ((pt,_),_) = get_calc 1;
14.41 case pt of Nd (PblObj _, [Nd _]) => ((*Apply_Method + Take*))
14.42 | _ => error "biegelinie.sml: Bsp 7.27 autoCalculate#4c";
14.43
14.44 - autoCalculate' 1 CompleteCalc;
14.45 + autoCalculate 1 CompleteCalc;
14.46 val ((pt,p),_) = get_calc 1;
14.47 if p = ([], Res) andalso length (children pt) = 23 andalso
14.48 term2str (get_obj g_res pt (fst p)) =
14.49 @@ -678,7 +678,7 @@
14.50 ("Biegelinie", ["Biegelinien"],
14.51 ["IntegrierenUndKonstanteBestimmen2"]))];
14.52 moveActiveRoot 1;
14.53 -autoCalculate' 1 CompleteCalc;
14.54 +autoCalculate 1 CompleteCalc;
14.55 val ((pt,p),_) = get_calc 1; show_pt pt;
14.56 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
14.57 "y x =\n-6 * q_0 * L ^^^ 2 / (-24 * EI) * x ^^^ 2 +\n4 * L * q_0 / (-24 * EI) * x ^^^ 3 +\n-1 * q_0 / (-24 * EI) * x ^^^ 4" then ()
15.1 --- a/test/Tools/isac/Knowledge/diff.sml Wed Oct 05 10:51:25 2016 +0200
15.2 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Oct 05 13:09:54 2016 +0200
15.3 @@ -16,9 +16,9 @@
15.4 "----------- 1.5.02 me from script ----------------------";
15.5 "----------- primed id ----------------------------------";
15.6 "----------- diff_conv, sym_diff_conv -------------------";
15.7 -"----------- autoCalculate' differentiate_on_R 2/x^2 -----";
15.8 -"----------- autoCalculate' diff after_simplification ----";
15.9 -"----------- autoCalculate' differentiate_equality -------";
15.10 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
15.11 +"----------- autoCalculate diff after_simplification ----";
15.12 +"----------- autoCalculate differentiate_equality -------";
15.13 "----------- tests for examples -------------------------";
15.14 "------------inform for x^2+x+1 -------------------------";
15.15 "--------------------------------------------------------";
15.16 @@ -346,9 +346,9 @@
15.17 *)
15.18 (*@@@@*)
15.19
15.20 -"----------- autoCalculate' differentiate_on_R 2/x^2 -----";
15.21 -"----------- autoCalculate' differentiate_on_R 2/x^2 -----";
15.22 -"----------- autoCalculate' differentiate_on_R 2/x^2 -----";
15.23 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
15.24 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
15.25 +"----------- autoCalculate differentiate_on_R 2/x^2 -----";
15.26 reset_states ();
15.27 CalcTree
15.28 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
15.29 @@ -358,7 +358,7 @@
15.30 ["diff","differentiate_on_R"]))];
15.31 Iterator 1;
15.32 moveActiveRoot 1;
15.33 -autoCalculate' 1 CompleteCalc;
15.34 +autoCalculate 1 CompleteCalc;
15.35 val ((pt,p),_) = get_calc 1; show_pt pt;
15.36 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
15.37 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
15.38 @@ -376,7 +376,7 @@
15.39 (* trace_rewrite := true;
15.40 trace_script := true;
15.41 *)
15.42 -autoCalculate' 1 CompleteCalc;
15.43 +autoCalculate 1 CompleteCalc;
15.44 (* trace_rewrite := false;
15.45 trace_script := false;
15.46 *)
15.47 @@ -386,9 +386,9 @@
15.48 "8 * x ^^^ 7" then ()
15.49 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
15.50
15.51 -"----------- autoCalculate' diff after_simplification ----";
15.52 -"----------- autoCalculate' diff after_simplification ----";
15.53 -"----------- autoCalculate' diff after_simplification ----";
15.54 +"----------- autoCalculate diff after_simplification ----";
15.55 +"----------- autoCalculate diff after_simplification ----";
15.56 +"----------- autoCalculate diff after_simplification ----";
15.57 reset_states ();
15.58 CalcTree
15.59 [(["functionTerm (x^3 * x^5)",
15.60 @@ -400,7 +400,7 @@
15.61 (* trace_rewrite := true;
15.62 trace_script := true;
15.63 *)
15.64 -autoCalculate' 1 CompleteCalc;
15.65 +autoCalculate 1 CompleteCalc;
15.66 (* trace_rewrite := false;
15.67 trace_script := false;
15.68 *)
15.69 @@ -417,14 +417,14 @@
15.70 ["diff","after_simplification"]))];
15.71 Iterator 1;
15.72 moveActiveRoot 1;
15.73 -autoCalculate' 1 CompleteCalc;
15.74 +autoCalculate 1 CompleteCalc;
15.75 val ((pt,p),_) = get_calc 1; show_pt pt;
15.76 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
15.77 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
15.78
15.79 -"----------- autoCalculate' differentiate_equality -------";
15.80 -"----------- autoCalculate' differentiate_equality -------";
15.81 -"----------- autoCalculate' differentiate_equality -------";
15.82 +"----------- autoCalculate differentiate_equality -------";
15.83 +"----------- autoCalculate differentiate_equality -------";
15.84 +"----------- autoCalculate differentiate_equality -------";
15.85 reset_states ();
15.86 CalcTree
15.87 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
15.88 @@ -432,7 +432,7 @@
15.89 ["diff","differentiate_equality"]))];
15.90 Iterator 1;
15.91 moveActiveRoot 1;
15.92 -autoCalculate' 1 CompleteCalc;
15.93 +autoCalculate 1 CompleteCalc;
15.94 val ((pt,p),_) = get_calc 1; show_pt pt;
15.95
15.96 "----------- tests for examples -------------------------";
15.97 @@ -459,10 +459,10 @@
15.98 ["diff","differentiate_on_R"]))];
15.99 Iterator 1;
15.100 moveActiveRoot 1;
15.101 -autoCalculate' 1 CompleteCalcHead;
15.102 -autoCalculate' 1 (Step 1);
15.103 -autoCalculate' 1 (Step 1);
15.104 -autoCalculate' 1 (Step 1);
15.105 +autoCalculate 1 CompleteCalcHead;
15.106 +autoCalculate 1 (Step 1);
15.107 +autoCalculate 1 (Step 1);
15.108 +autoCalculate 1 (Step 1);
15.109 val ((pt,p),_) = get_calc 1; show_pt pt;
15.110 appendFormula 1 "2*x + d_d x x + d_d x 1" (*|> Future.join*);
15.111 val ((pt,p),_) = get_calc 1; show_pt pt;
16.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Oct 05 10:51:25 2016 +0200
16.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Oct 05 13:09:54 2016 +0200
16.3 @@ -429,16 +429,16 @@
16.4
16.5 CalcTree [(fmz, (dI',pI',mI'))];
16.6 Iterator 1; moveActiveRoot 1;
16.7 - autoCalculate' 1 CompleteCalcHead;
16.8 + autoCalculate 1 CompleteCalcHead;
16.9 refFormula 1 (get_pos 1 1);
16.10
16.11 fetchProposedTactic 1;
16.12 - autoCalculate' 1 (Step 1);
16.13 + autoCalculate 1 (Step 1);
16.14
16.15 fetchProposedTactic 1;
16.16 - autoCalculate' 1 (Step 1);
16.17 + autoCalculate 1 (Step 1);
16.18 (*Subproblem on_interval maximum_of function*)
16.19 - autoCalculate' 1 CompleteCalcHead;
16.20 + autoCalculate 1 CompleteCalcHead;
16.21
16.22 fetchProposedTactic 1;
16.23 val ((pt,p),_) = get_calc 1;
17.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Oct 05 10:51:25 2016 +0200
17.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Oct 05 13:09:54 2016 +0200
17.3 @@ -653,7 +653,7 @@
17.4 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
17.5 moveActiveRoot 1;
17.6 (*
17.7 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.8 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.9 ##7.27## ordered substs
17.10 c_4 c_2
17.11 c c_2 c_3 c_4 c c_2 1->2: c
17.12 @@ -698,7 +698,7 @@
17.13 ["Biegelinien", "AusMomentenlinie"]))];
17.14 (*
17.15 moveActiveRoot 1;
17.16 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.17 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.18 *)
17.19
17.20 "------- Bsp 7.69";
17.21 @@ -709,7 +709,7 @@
17.22 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))];
17.23 moveActiveRoot 1;
17.24 (*
17.25 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.26 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.27 ##7.69## ordered subst 2x2
17.28 c_4 c_3
17.29 c c_2 c_3 c_4 c c_2 c_3 1:c_3 -> 2:c c_2 2: c c_2
17.30 @@ -729,7 +729,7 @@
17.31 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"] ))];
17.32 moveActiveRoot 1;
17.33 (*
17.34 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.35 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.36 ##7.70## |subst
17.37 c |
17.38 c c_2 |1:c -> 2:c_2
17.39 @@ -845,7 +845,7 @@
17.40 ["IntegrierenUndKonstanteBestimmen2"] ))];
17.41 moveActiveRoot 1;
17.42 (*
17.43 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.44 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.45 ##7.71## |ordered |subst.singles (recurs) |2x2 |diagonal
17.46 c c_2 |c c_2 |1' |1': c c_2 |
17.47 c_4 | c_3 |2:c_3 -> 4' :c c_2 c_4 | |
17.48 @@ -867,7 +867,7 @@
17.49 ["Biegelinien", "AusMomentenlinie"]))];
17.50 moveActiveRoot 1;
17.51 (*
17.52 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.53 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.54 *)
17.55
17.56 "------- Bsp 7.72b";
17.57 @@ -879,7 +879,7 @@
17.58 ["IntegrierenUndKonstanteBestimmen2"] ))];
17.59 moveActiveRoot 1;
17.60 (*
17.61 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.62 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.63 ##7.72b## |ord. |subst.singles |ord.triang.
17.64 c_2 | | |c_2
17.65 c c_2 | |1:c_2 -> 2':c |c_2 c
17.66 @@ -900,7 +900,7 @@
17.67 ["Biegelinien", "AusMomentenlinie"]))];
17.68 moveActiveRoot 1;
17.69 (*
17.70 -trace_script := true; autoCalculate' 1 CompleteCalc; trace_script := false;
17.71 +trace_script := true; autoCalculate 1 CompleteCalc; trace_script := false;
17.72 *)
17.73
17.74 "----------- 4x4 systems from Biegelinie -------------------------";
18.1 --- a/test/Tools/isac/Knowledge/equation.sml Wed Oct 05 10:51:25 2016 +0200
18.2 +++ b/test/Tools/isac/Knowledge/equation.sml Wed Oct 05 13:09:54 2016 +0200
18.3 @@ -24,7 +24,7 @@
18.4 moveActiveRoot 1;
18.5 replaceFormula 1 "solve (x+1=2, x)";
18.6 (*========== inhibit exn 130719 Isabelle2013 ===================================loops
18.7 -autoCalculate' 1 CompleteCalc;
18.8 +autoCalculate 1 CompleteCalc;
18.9 val ((pt,p),_) = get_calc 1;
18.10 val Form res = (#1 o pt_extract) (pt, ([],Res));
18.11 show_pt pt;
19.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Oct 05 10:51:25 2016 +0200
19.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Oct 05 13:09:54 2016 +0200
19.3 @@ -15,7 +15,7 @@
19.4 "----------- check probem type --------------------------";
19.5 "----------- check Scripts ------------------------------";
19.6 "----------- me method [diff,integration] ---------------";
19.7 -"----------- autoCalculate' [diff,integration] -----------";
19.8 +"----------- autoCalculate [diff,integration] -----------";
19.9 "----------- me method [diff,integration,named] ---------";
19.10 "----------- me met [diff,integration,named] Biegelinie.Q";
19.11 "----------- interSteps [diff,integration] --------------";
19.12 @@ -418,16 +418,16 @@
19.13 else error "integrate.sml -- me method [diff,integration] -- end";
19.14
19.15
19.16 -"----------- autoCalculate' [diff,integration] -----------";
19.17 -"----------- autoCalculate' [diff,integration] -----------";
19.18 -"----------- autoCalculate' [diff,integration] -----------";
19.19 +"----------- autoCalculate [diff,integration] -----------";
19.20 +"----------- autoCalculate [diff,integration] -----------";
19.21 +"----------- autoCalculate [diff,integration] -----------";
19.22 reset_states ();
19.23 CalcTree
19.24 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
19.25 ("Integrate", ["integrate","function"], ["diff","integration"]))];
19.26 Iterator 1;
19.27 moveActiveRoot 1;
19.28 -autoCalculate' 1 CompleteCalc;
19.29 +autoCalculate 1 CompleteCalc;
19.30 val ((pt,p),_) = get_calc 1; PolyML.makestring p; show_pt pt;
19.31 val (Form t,_,_) = pt_extract (pt, p);
19.32 if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
19.33 @@ -495,7 +495,7 @@
19.34 ("Integrate", ["integrate","function"], ["diff","integration"]))];
19.35 Iterator 1;
19.36 moveActiveRoot 1;
19.37 -autoCalculate' 1 CompleteCalc;
19.38 +autoCalculate 1 CompleteCalc;
19.39 interSteps 1 ([1],Res);
19.40 val ((pt,p),_) = get_calc 1; show_pt pt;
19.41 if existpt' ([1,3], Res) pt then ()
19.42 @@ -508,22 +508,22 @@
19.43 ("Integrate", ["integrate","function"], ["diff","integration","test"]))];
19.44 Iterator 1;
19.45 moveActiveRoot 1;
19.46 -autoCalculate' 1 CompleteCalcHead;
19.47 +autoCalculate 1 CompleteCalcHead;
19.48
19.49 fetchProposedTactic 1 (*..Apply_Method*);
19.50 -autoCalculate' 1 (Step 1);
19.51 +autoCalculate 1 (Step 1);
19.52 getTactic 1 ([1], Frm) (*still empty*);
19.53
19.54 fetchProposedTactic 1 (*Rewrite_Set_Inst integration_rules*);
19.55 -autoCalculate' 1 (Step 1);
19.56 +autoCalculate 1 (Step 1);
19.57
19.58 fetchProposedTactic 1 (*Rewrite_Set_Inst add_new_c*);
19.59 -autoCalculate' 1 (Step 1);
19.60 +autoCalculate 1 (Step 1);
19.61
19.62 fetchProposedTactic 1 (*Rewrite_Set_Inst simplify_Integral*);
19.63 -autoCalculate' 1 (Step 1);
19.64 +autoCalculate 1 (Step 1);
19.65
19.66 -autoCalculate' 1 CompleteCalc;
19.67 +autoCalculate 1 CompleteCalc;
19.68 val ((pt,p),_) = get_calc 1; show_pt pt;
19.69 val (Form t,_,_) = pt_extract (pt, p); term2str t;
19.70 if existpt' ([3], Res) pt andalso term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
19.71 @@ -540,7 +540,7 @@
19.72 ["diff","integration"]))];
19.73 Iterator 1;
19.74 moveActiveRoot 1;
19.75 -autoCalculate' 1 CompleteCalc;
19.76 +autoCalculate 1 CompleteCalc;
19.77 val ((pt,p),_) = get_calc 1; show_pt pt;
19.78 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3"
19.79 then () else error "Ambiguous input: Integral ?u + ?v D ?bdv ="
19.80 @@ -592,7 +592,7 @@
19.81 Iterator 1;
19.82 moveActiveRoot 1;
19.83 replaceFormula 1 "Integrate (x^2 + x + 1, x)";
19.84 -autoCalculate' 1 CompleteCalc;
19.85 +autoCalculate 1 CompleteCalc;
19.86 val ((pt,p),_) = get_calc 1;
19.87 val Form res = (#1 o pt_extract) (pt, ([],Res));
19.88 show_pt pt;
20.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Wed Oct 05 10:51:25 2016 +0200
20.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Oct 05 13:09:54 2016 +0200
20.3 @@ -12,7 +12,7 @@
20.4 "----------- Logic.unvarify_global ----------------------";
20.5 "----------- eval_drop_questionmarks --------------------";
20.6 "----------- = me for met_partial_fraction --------------";
20.7 -"----------- autoCalculate' for met_partial_fraction -----";
20.8 +"----------- autoCalculate for met_partial_fraction -----";
20.9 "----------- progr.vers.2: check erls for multiply_ansatz";
20.10 "----------- progr.vers.2: improve program --------------";
20.11 "--------------------------------------------------------";
20.12 @@ -222,9 +222,9 @@
20.13 if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
20.14 else error "= me .. met_partial_fraction broken";
20.15
20.16 -"----------- autoCalculate' for met_partial_fraction -----";
20.17 -"----------- autoCalculate' for met_partial_fraction -----";
20.18 -"----------- autoCalculate' for met_partial_fraction -----";
20.19 +"----------- autoCalculate for met_partial_fraction -----";
20.20 +"----------- autoCalculate for met_partial_fraction -----";
20.21 +"----------- autoCalculate for met_partial_fraction -----";
20.22 reset_states ();
20.23 val fmz =
20.24 ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
20.25 @@ -236,11 +236,11 @@
20.26 CalcTree [(fmz, (dI' ,pI' ,mI'))];
20.27 Iterator 1;
20.28 moveActiveRoot 1;
20.29 -autoCalculate' 1 CompleteCalc;
20.30 +autoCalculate 1 CompleteCalc;
20.31
20.32 val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
20.33 if p = ip andalso ip = ([], Res) then ()
20.34 - else error "autoCalculate' for met_partial_fraction changed: final pos'";
20.35 + else error "autoCalculate for met_partial_fraction changed: final pos'";
20.36
20.37 val (Form f, tac, asms) = pt_extract (pt, p);
20.38 if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
20.39 @@ -253,7 +253,7 @@
20.40 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
20.41 "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
20.42 then ()
20.43 - else error "autoCalculate' for met_partial_fraction changed: final result"
20.44 + else error "autoCalculate for met_partial_fraction changed: final result"
20.45
20.46 show_pt pt;
20.47 (*[
21.1 --- a/test/Tools/isac/Knowledge/poly.sml Wed Oct 05 10:51:25 2016 +0200
21.2 +++ b/test/Tools/isac/Knowledge/poly.sml Wed Oct 05 13:09:54 2016 +0200
21.3 @@ -440,7 +440,7 @@
21.4 ["simplification","for_polynomials"]))];
21.5 Iterator 1;
21.6 moveActiveRoot 1;
21.7 -autoCalculate' 1 CompleteCalc;
21.8 +autoCalculate 1 CompleteCalc;
21.9 val ((pt,p),_) = get_calc 1; show_pt pt;
21.10
21.11 interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
22.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Oct 05 10:51:25 2016 +0200
22.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Oct 05 13:09:54 2016 +0200
22.3 @@ -1130,7 +1130,7 @@
22.4 ("PolyEq",["univariate","equation"],["no_met"]))];
22.5 Iterator 1;
22.6 moveActiveRoot 1;
22.7 -autoCalculate' 1 CompleteCalc;
22.8 +autoCalculate 1 CompleteCalc;
22.9 val ((pt,p),_) = get_calc 1; show_pt pt;
22.10 interSteps 1 ([1],Res)
22.11 (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
23.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Wed Oct 05 10:51:25 2016 +0200
23.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Oct 05 13:09:54 2016 +0200
23.3 @@ -276,7 +276,7 @@
23.4 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.5 ["simplification","for_polynomials","with_minus"]))];
23.6 moveActiveRoot 1;
23.7 -autoCalculate' 1 CompleteCalc;
23.8 +autoCalculate 1 CompleteCalc;
23.9 val ((pt,p),_) = get_calc 1; show_pt pt;
23.10 if p = ([], Res) andalso
23.11 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"
23.12 @@ -289,7 +289,7 @@
23.13 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.14 ["simplification","for_polynomials","with_minus"]))];
23.15 moveActiveRoot 1;
23.16 -autoCalculate' 1 CompleteCalc;
23.17 +autoCalculate 1 CompleteCalc;
23.18 val ((pt,p),_) = get_calc 1; show_pt pt;
23.19 if p = ([], Res) andalso
23.20 term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
23.21 @@ -302,7 +302,7 @@
23.22 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.23 ["simplification","for_polynomials","with_minus"]))];
23.24 moveActiveRoot 1;
23.25 -autoCalculate' 1 CompleteCalc;
23.26 +autoCalculate 1 CompleteCalc;
23.27 val ((pt,p),_) = get_calc 1; show_pt pt;
23.28 if p = ([], Res) andalso
23.29 term2str (get_obj g_res pt (fst p)) = "- (3 * f)"
23.30 @@ -315,7 +315,7 @@
23.31 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.32 ["simplification","for_polynomials","with_minus"]))];
23.33 moveActiveRoot 1;
23.34 -autoCalculate' 1 CompleteCalc;
23.35 +autoCalculate 1 CompleteCalc;
23.36 val ((pt,p),_) = get_calc 1; show_pt pt;
23.37 if p = ([], Res) andalso
23.38 term2str (get_obj g_res pt (fst p)) = "-3 * u - v"
23.39 @@ -328,7 +328,7 @@
23.40 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.41 ["simplification","for_polynomials","with_minus"]))];
23.42 moveActiveRoot 1;
23.43 -autoCalculate' 1 CompleteCalc;
23.44 +autoCalculate 1 CompleteCalc;
23.45 val ((pt,p),_) = get_calc 1; show_pt pt;
23.46 if p = ([], Res) andalso
23.47 term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"
23.48 @@ -358,10 +358,10 @@
23.49 ("PolyMinus",["polynom","probe"],
23.50 ["probe","fuer_polynom"]))];
23.51 moveActiveRoot 1;
23.52 -autoCalculate' 1 CompleteCalc;
23.53 -(* autoCalculate' 1 CompleteCalcHead;
23.54 - autoCalculate' 1 (Step 1);
23.55 - autoCalculate' 1 (Step 1);
23.56 +autoCalculate 1 CompleteCalc;
23.57 +(* autoCalculate 1 CompleteCalcHead;
23.58 + autoCalculate 1 (Step 1);
23.59 + autoCalculate 1 (Step 1);
23.60 val ((pt,p),_) = get_calc 1; term2str (get_obj g_res pt (fst p));
23.61 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
23.62 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
23.63 @@ -379,7 +379,7 @@
23.64 ("PolyMinus",["klammer","polynom","vereinfachen"],
23.65 ["simplification","for_polynomials","with_parentheses"]))];
23.66 moveActiveRoot 1;
23.67 -autoCalculate' 1 CompleteCalc;
23.68 +autoCalculate 1 CompleteCalc;
23.69 val ((pt,p),_) = get_calc 1;
23.70 if p = ([], Res) andalso
23.71 term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"
23.72 @@ -394,7 +394,7 @@
23.73 ("PolyMinus",["polynom","probe"],
23.74 ["probe","fuer_polynom"]))];
23.75 moveActiveRoot 1;
23.76 -autoCalculate' 1 CompleteCalc;
23.77 +autoCalculate 1 CompleteCalc;
23.78 val ((pt,p),_) = get_calc 1;
23.79 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"
23.80 then () else error "polyminus.sml: Probe 29 = 29";
23.81 @@ -409,9 +409,9 @@
23.82 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.83 ["simplification","for_polynomials","with_minus"]))];
23.84 moveActiveRoot 1;
23.85 -autoCalculate' 1 CompleteCalcHead;
23.86 -autoCalculate' 1 (Step 1);
23.87 -autoCalculate' 1 (Step 1);
23.88 +autoCalculate 1 CompleteCalcHead;
23.89 +autoCalculate 1 (Step 1);
23.90 +autoCalculate 1 (Step 1);
23.91 val ((pt,p),_) = get_calc 1; show_pt pt;
23.92 "----- 1 ^^^";
23.93 fetchApplicableTactics 1 0 p;
23.94 @@ -455,7 +455,7 @@
23.95 val ((pt,p),_) = get_calc 1; show_pt pt;
23.96 "----- 7 ^^^";
23.97 *)
23.98 -autoCalculate' 1 CompleteCalc;
23.99 +autoCalculate 1 CompleteCalc;
23.100 val ((pt,p),_) = get_calc 1; show_pt pt;
23.101 (*independent from failure above: met_simp_poly_minus not confluent:
23.102 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
23.103 @@ -470,7 +470,7 @@
23.104 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.105 ["simplification","for_polynomials","with_minus"]))];
23.106 moveActiveRoot 1;
23.107 -autoCalculate' 1 CompleteCalc;
23.108 +autoCalculate 1 CompleteCalc;
23.109 val ((pt,p),_) = get_calc 1; show_pt pt;
23.110 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h"
23.111 then () else error "polyminus.sml: addiere_vor_minus";
23.112 @@ -483,7 +483,7 @@
23.113 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
23.114 ["simplification","for_polynomials","with_minus"]))];
23.115 moveActiveRoot 1;
23.116 -autoCalculate' 1 CompleteCalc;
23.117 +autoCalculate 1 CompleteCalc;
23.118 val ((pt,p),_) = get_calc 1; show_pt pt;
23.119 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"
23.120 then () else error "polyminus.sml: tausche_vor_plus";
23.121 @@ -527,7 +527,7 @@
23.122 ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
23.123 ["simplification","for_polynomials","with_parentheses_mult"]))];
23.124 moveActiveRoot 1;
23.125 -autoCalculate' 1 CompleteCalc;
23.126 +autoCalculate 1 CompleteCalc;
23.127 val ((pt,p),_) = get_calc 1; show_pt pt;
23.128 if p = ([], Res) andalso
23.129 term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
23.130 @@ -541,7 +541,7 @@
23.131 ("PolyMinus",["binom_klammer","polynom","vereinfachen"],
23.132 ["simplification","for_polynomials","with_parentheses_mult"]))];
23.133 moveActiveRoot 1;
23.134 -autoCalculate' 1 CompleteCalc;
23.135 +autoCalculate 1 CompleteCalc;
23.136 val ((pt,p),_) = get_calc 1; show_pt pt;
23.137 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "12 * a - 16 * q"
23.138 then () else error "pbl binom polynom vereinfachen: cube";
24.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Oct 05 10:51:25 2016 +0200
24.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Oct 05 13:09:54 2016 +0200
24.3 @@ -1445,7 +1445,7 @@
24.4 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
24.5 Iterator 1;
24.6 moveActiveRoot 1;
24.7 -autoCalculate' 1 CompleteCalc;
24.8 +autoCalculate 1 CompleteCalc;
24.9 val ((pt, p), _) = get_calc 1;
24.10 (*
24.11 show_pt pt;
24.12 @@ -1489,7 +1489,7 @@
24.13 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
24.14 Iterator 1;
24.15 moveActiveRoot 1;
24.16 -autoCalculate' 1 CompleteCalc;
24.17 +autoCalculate 1 CompleteCalc;
24.18 val ((pt, p), _) = get_calc 1;
24.19 (*show_pt pt;
24.20 [
24.21 @@ -1620,7 +1620,7 @@
24.22 ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
24.23 Iterator 1;
24.24 moveActiveRoot 1;
24.25 -autoCalculate' 1 CompleteCalc;
24.26 +autoCalculate 1 CompleteCalc;
24.27 val ((pt, p), _) = get_calc 1;
24.28 (*show_pt pt;
24.29 [
25.1 --- a/test/Tools/isac/OLDTESTS/modspec.sml Wed Oct 05 10:51:25 2016 +0200
25.2 +++ b/test/Tools/isac/OLDTESTS/modspec.sml Wed Oct 05 13:09:54 2016 +0200
25.3 @@ -17,7 +17,7 @@
25.4 ["Test","squ-equ-test-subpbl1"]))];
25.5 Iterator 1;
25.6 moveActiveRoot 1;
25.7 - autoCalculate' 1 CompleteCalc;
25.8 + autoCalculate 1 CompleteCalc;
25.9 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
25.10 replaceFormula 1 "x = 1";
25.11 (*... returns calcChangedEvent with ...*)
26.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Wed Oct 05 10:51:25 2016 +0200
26.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Wed Oct 05 13:09:54 2016 +0200
26.3 @@ -3,72 +3,72 @@
26.4 use"tacis.sml";
26.5 *)
26.6 "=================================================================";
26.7 -"------ fetchProposedTactic -> autoCalculate' (Step1 ) ------------";
26.8 -"------ setNextTactic -> autoCalculate' (Step1 ) ------------------";
26.9 +"------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
26.10 +"------ setNextTactic -> autoCalculate (Step1 ) ------------------";
26.11 "=================================================================";
26.12
26.13
26.14
26.15 -"------ fetchProposedTactic -> autoCalculate' (Step1 ) ------------";
26.16 -"------ fetchProposedTactic -> autoCalculate' (Step1 ) ------------";
26.17 -"------ fetchProposedTactic -> autoCalculate' (Step1 ) ------------";
26.18 +"------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
26.19 +"------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
26.20 +"------ fetchProposedTactic -> autoCalculate (Step1 ) ------------";
26.21 reset_states ();
26.22 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
26.23 ("Test", ["sqroot-test","univariate","equation","test"],
26.24 ["Test","squ-equ-test-subpbl1"]))];
26.25 Iterator 1; moveActiveRoot 1;
26.26 - autoCalculate' 1 CompleteCalcHead;
26.27 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
26.28 + autoCalculate 1 CompleteCalcHead;
26.29 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
26.30
26.31 fetchProposedTactic 1 (*'Rewrite_Set norm_equation' in tacis*);
26.32 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
26.33 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
26.34
26.35 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
26.36 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.37 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.38 val ((pt,_),_) = get_calc 1;
26.39 val str = pr_ptree pr_short pt;
26.40 writeln str;
26.41
26.42 fetchProposedTactic 1 (*'Subproblem ...' in tacis*);
26.43 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0,x)*);
26.44 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0,x)*);
26.45
26.46 fetchProposedTactic 1 (*'Model_Problem' in tacis*);
26.47 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality ///*);
26.48 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality ///*);
26.49 (*----- WN060222 since complete_mod_ case cas of SOME headline -----
26.50 fetchProposedTactic 1 (*'Add_Given equality (-1 + x = 0)' in tacis*);
26.51 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality (-1 + x =0)*);
26.52 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality (-1 + x =0)*);
26.53 ---------------------------------------------------------------------*)
26.54
26.55 fetchProposedTactic 1 (*'Add_Given solveFor x' in tacis*);
26.56 (*----- WN060222 since complete_mod_ case cas of SOME headline:
26.57 (*Specify_Theory Test.thy*)
26.58 ---------------------------------------------------------------------*)
26.59 - autoCalculate' 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
26.60 - (*###########################################autoCalculate' 1 (Step 1);*)
26.61 + autoCalculate 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
26.62 + (*###########################################autoCalculate 1 (Step 1);*)
26.63 fetchProposedTactic 1 (*'Apply_Method Test solve_linear' in tacis*);
26.64 (* there was the only error ^^^^^^^^^ in step/nxt_solv ..Apply_Method..
26.65 val (str', (tacis', (pt',p'))) = step ip (ptp, tacis);
26.66 writeln (tacis2str tacis');
26.67 ######################################################################*)
26.68 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.69 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.70
26.71 fetchProposedTactic 1 (*'Rewrite_Set_Inst isolate_bdv' in tacis*);
26.72 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
26.73 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
26.74
26.75 fetchProposedTactic 1 (*'Rewrite_Set Test_simplify' in tacis*);
26.76 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*);
26.77 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*);
26.78 val ((pt,_),_) = get_calc 1;
26.79 val str = pr_ptree pr_short pt;
26.80 writeln str;
26.81
26.82 fetchProposedTactic 1 (*'Check_Postcond linear...' in tacis*);
26.83 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.84 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.85
26.86 fetchProposedTactic 1 (*'Check_elementwise Assumptions' in tacis*);
26.87 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.88 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.89
26.90 fetchProposedTactic 1 (*'Check_Postcond sqroot-test...' in tacis*);
26.91 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.92 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.93
26.94 fetchProposedTactic 1 (*'' in tacis*);
26.95 val ((pt,p),tacis) = get_calc 1;
26.96 @@ -79,64 +79,64 @@
26.97
26.98
26.99
26.100 -"------ setNextTactic -> autoCalculate' (Step1 ) ------------------";
26.101 -"------ setNextTactic -> autoCalculate' (Step1 ) ------------------";
26.102 -"------ setNextTactic -> autoCalculate' (Step1 ) ------------------";
26.103 +"------ setNextTactic -> autoCalculate (Step1 ) ------------------";
26.104 +"------ setNextTactic -> autoCalculate (Step1 ) ------------------";
26.105 +"------ setNextTactic -> autoCalculate (Step1 ) ------------------";
26.106 reset_states ();
26.107 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
26.108 ("Test", ["sqroot-test","univariate","equation","test"],
26.109 ["Test","squ-equ-test-subpbl1"]))];
26.110 Iterator 1; moveActiveRoot 1;
26.111 - autoCalculate' 1 CompleteCalcHead;
26.112 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
26.113 + autoCalculate 1 CompleteCalcHead;
26.114 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
26.115
26.116 setNextTactic 1 (Rewrite_Set "norm_equation");
26.117 val (_, tacis) = get_calc 1;
26.118 case tacis of [(Rewrite_Set "norm_equation",_,(([1], Res), _))] => () | _ =>
26.119 - error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate' (1)";
26.120 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
26.121 + error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (1)";
26.122 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 + -1 * 2 = 0*);
26.123
26.124 setNextTactic 1 (Rewrite_Set "Test_simplify");
26.125 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.126 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.127 val ((pt,_),_) = get_calc 1;
26.128 val str = pr_ptree pr_short pt;
26.129 writeln str;
26.130
26.131 setNextTactic 1 (Subproblem ("Test",["LINEAR","univariate",
26.132 "equation","test"]));
26.133 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*);
26.134 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*);
26.135 val ((pt,_),_) = get_calc 1;
26.136 val str = pr_ptree pr_short pt;
26.137 writeln str;
26.138
26.139 setNextTactic 1 (Model_Problem (*["LINEAR","univariate","equation","test"]*));
26.140 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality ///*);
26.141 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality ///*);
26.142
26.143 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
26.144 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality (-1 + x = 0)*);
26.145 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality (-1 + x = 0)*);
26.146
26.147 setNextTactic 1 (Add_Given "solveFor x");
26.148 - autoCalculate' 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
26.149 + autoCalculate 1 CompleteCalcHead; refFormula 1 (get_pos 1 1) (*OK*);
26.150
26.151 setNextTactic 1 (Apply_Method ["Test", "solve_linear"]);
26.152 val (_, tacis) = get_calc 1;
26.153 case tacis of
26.154 [((Apply_Method ["Test","solve_linear"],_,(([3,1], Frm), _)))] =>() | _ =>
26.155 - error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate' (2)";
26.156 + error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (2)";
26.157 (*#######################################################################*)
26.158 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.159 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*-1 + x = 0*);
26.160
26.161 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
26.162 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
26.163 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 0 + -1 * -1*);
26.164
26.165 setNextTactic 1 (Rewrite_Set "Test_simplify");
26.166 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*);
26.167 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*);
26.168
26.169 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
26.170 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.171 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.172
26.173 setNextTactic 1 (Check_elementwise "Assumptions");
26.174 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.175 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.176 val ((pt,_),_) = get_calc 1;
26.177 val str = pr_ptree pr_short pt;
26.178 writeln str;
26.179 @@ -147,15 +147,15 @@
26.180
26.181 (*case tacis of 040609 suddenly ???!
26.182 [((Check_Postcond _, _,(([], Res), _)))] =>() | _ =>
26.183 - error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate' (3)";
26.184 + error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (3)";
26.185 #######################################################################*)
26.186 - autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.187 + autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
26.188
26.189 val ((pt,p),tacis) = get_calc 1;
26.190 val ip = get_pos 1 1;
26.191 val (Form f, tac, asms) = pt_extract (pt, p);
26.192 if term2str f = "[x = 1]"andalso p = ([],Res) andalso ip = ([],Res)then()else
26.193 - error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate' (4)";
26.194 + error "tacis.sml: diff.behav. in setNextTactic -> autoCalculate (4)";
26.195
26.196
26.197
27.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Wed Oct 05 10:51:25 2016 +0200
27.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Wed Oct 05 13:09:54 2016 +0200
27.3 @@ -36,22 +36,22 @@
27.4 ["Test","test_interSteps_1"]))];
27.5 Iterator 1;
27.6 moveActiveRoot 1;
27.7 -autoCalculate' 1 CompleteCalcHead;
27.8 +autoCalculate 1 CompleteCalcHead;
27.9
27.10 fetchProposedTactic 1 (*..Apply_Method*);
27.11 -autoCalculate' 1 (Step 1);
27.12 +autoCalculate 1 (Step 1);
27.13 getTactic 1 ([1], Frm) (*still empty*);
27.14
27.15 fetchProposedTactic 1 (*discard_minus_*);
27.16 -autoCalculate' 1 (Step 1);
27.17 +autoCalculate 1 (Step 1);
27.18
27.19 fetchProposedTactic 1 (*order_add_rls_*);
27.20 -autoCalculate' 1 (Step 1);
27.21 +autoCalculate 1 (Step 1);
27.22
27.23 fetchProposedTactic 1 (*collect_numerals_*);
27.24 -autoCalculate' 1 (Step 1);
27.25 +autoCalculate 1 (Step 1);
27.26
27.27 -autoCalculate' 1 CompleteCalc;
27.28 +autoCalculate 1 CompleteCalc;
27.29
27.30 val ((pt,p),_) = get_calc 1; show_pt pt;
27.31 if existpt' ([1], Frm) pt then ()
27.32 @@ -72,7 +72,7 @@
27.33 ["simplification","for_polynomials"]))];
27.34 Iterator 1;
27.35 moveActiveRoot 1;
27.36 -autoCalculate' 1 CompleteCalc;
27.37 +autoCalculate 1 CompleteCalc;
27.38
27.39 interSteps 1 ([], Res);
27.40 val ((pt,p),_) = get_calc 1; show_pt pt;
27.41 @@ -132,7 +132,7 @@
27.42 ["simplification","of_rationals"]))];
27.43 Iterator 1;
27.44 moveActiveRoot 1;
27.45 -autoCalculate' 1 CompleteCalc;
27.46 +autoCalculate 1 CompleteCalc;
27.47
27.48 interSteps 1 ([], Res);
27.49 val ((pt,p),_) = get_calc 1; show_pt pt;
28.1 --- a/test/Tools/isac/Test_Isac.thy Wed Oct 05 10:51:25 2016 +0200
28.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Oct 05 13:09:54 2016 +0200
28.3 @@ -46,7 +46,7 @@
28.4
28.5 ML {*
28.6 KEStore_Elems.set_ref_thy @{theory};
28.7 - fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*);
28.8 + (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
28.9 *}
28.10
28.11 section {* trials with Isabelle's functions *}