1.1 --- a/test/Tools/isac/Frontend/use-cases.sml Fri Jun 13 12:06:38 2014 +0200
1.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Fri Jun 13 12:42:15 2014 +0200
1.3 @@ -105,30 +105,30 @@
1.4
1.5 fetchProposedTactic 1 (*by using Iterator No.1*);
1.6 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
1.7 - autoCalculate 1 (Step 1);
1.8 + autoCalculate' 1 (Step 1);
1.9 refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
1.10 - autoCalculate 1 (Step 1);
1.11 + autoCalculate' 1 (Step 1);
1.12 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
1.13 fetchProposedTactic 1;
1.14 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
1.15 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
1.16 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
1.17
1.18 fetchProposedTactic 1;
1.19 setNextTactic 1 (Add_Given "solveFor x");
1.20 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.21 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.22
1.23 fetchProposedTactic 1;
1.24 setNextTactic 1 (Add_Find "solutions L");
1.25 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.26 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.27
1.28 fetchProposedTactic 1;
1.29 setNextTactic 1 (Specify_Theory "Test");
1.30 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.31 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.32 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
1.33
1.34 fetchProposedTactic 1;
1.35 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
1.36 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.37 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.38 (*-------------------------------------------------------------------------*)
1.39 fetchProposedTactic 1;
1.40 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.41 @@ -136,7 +136,7 @@
1.42 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
1.43 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.44
1.45 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.46 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.47 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.48
1.49 (*-------------------------------------------------------------------------*)
1.50 @@ -149,22 +149,22 @@
1.51 is_complete_mod ptp;
1.52 is_complete_spec ptp;
1.53
1.54 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.55 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.56 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
1.57 (*term2str (get_obj g_form pt [1]);*)
1.58 (*-------------------------------------------------------------------------*)
1.59
1.60 fetchProposedTactic 1;
1.61 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.62 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.63 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.64
1.65 fetchProposedTactic 1;
1.66 setNextTactic 1 (Rewrite_Set "Test_simplify");
1.67 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.68 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.69
1.70 fetchProposedTactic 1;
1.71 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
1.72 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.73 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.74
1.75 val ((pt,_),_) = get_calc 1;
1.76 val ip = get_pos 1 1;
1.77 @@ -212,104 +212,104 @@
1.78 refFormula 1 (get_pos 1 1);
1.79 fetchProposedTactic 1;
1.80 setNextTactic 1 (Model_Problem);
1.81 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
1.82 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
1.83
1.84 fetchProposedTactic 1;
1.85 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
1.86 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.87 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.88
1.89 fetchProposedTactic 1;
1.90 setNextTactic 1 (Add_Given "solveFor x");
1.91 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.92 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.93
1.94 fetchProposedTactic 1;
1.95 setNextTactic 1 (Add_Find "solutions L");
1.96 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.97 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.98
1.99 fetchProposedTactic 1;
1.100 setNextTactic 1 (Specify_Theory "Test");
1.101 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.102 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.103
1.104 fetchProposedTactic 1;
1.105 setNextTactic 1 (Specify_Problem
1.106 ["sqroot-test","univariate","equation","test"]);
1.107 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.108 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.109 "1-----------------------------------------------------------------";
1.110
1.111 fetchProposedTactic 1;
1.112 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
1.113 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.114 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.115
1.116 fetchProposedTactic 1;
1.117 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
1.118 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.119 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.120
1.121 fetchProposedTactic 1;
1.122 setNextTactic 1 (Rewrite_Set "norm_equation");
1.123 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.124 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.125
1.126 fetchProposedTactic 1;
1.127 setNextTactic 1 (Rewrite_Set "Test_simplify");
1.128 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.129 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.130
1.131 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
1.132 setNextTactic 1 (Subproblem ("Test",
1.133 ["LINEAR","univariate","equation","test"]));
1.134 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.135 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.136
1.137 fetchProposedTactic 1;
1.138 setNextTactic 1 (Model_Problem );
1.139 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.140 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.141
1.142 fetchProposedTactic 1;
1.143 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
1.144 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.145 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.146
1.147 fetchProposedTactic 1;
1.148 setNextTactic 1 (Add_Given "solveFor x");
1.149 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.150 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.151
1.152 fetchProposedTactic 1;
1.153 setNextTactic 1 (Add_Find "solutions x_i");
1.154 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.155 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.156
1.157 fetchProposedTactic 1;
1.158 setNextTactic 1 (Specify_Theory "Test");
1.159 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.160 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.161
1.162 fetchProposedTactic 1;
1.163 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
1.164 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.165 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.166 "2-----------------------------------------------------------------";
1.167
1.168 fetchProposedTactic 1;
1.169 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
1.170 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.171 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.172
1.173 fetchProposedTactic 1;
1.174 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
1.175 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.176 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.177
1.178 fetchProposedTactic 1;
1.179 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.180 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.181 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.182
1.183 fetchProposedTactic 1;
1.184 setNextTactic 1 (Rewrite_Set "Test_simplify");
1.185 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.186 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.187
1.188 fetchProposedTactic 1;
1.189 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
1.190 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.191 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.192
1.193 fetchProposedTactic 1;
1.194 setNextTactic 1 (Check_elementwise "Assumptions");
1.195 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.196 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.197
1.198 val xml = fetchProposedTactic 1;
1.199 setNextTactic 1 (Check_Postcond
1.200 ["sqroot-test","univariate","equation","test"]);
1.201 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.202 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.203
1.204 val ((pt,_),_) = get_calc 1;
1.205 val str = pr_ptree pr_short pt;
1.206 @@ -330,39 +330,39 @@
1.207 ["Test","squ-equ-test-subpbl1"]))];
1.208 Iterator 1;
1.209 moveActiveRoot 1;
1.210 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.211 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.212 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.213 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.214 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.215 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.216 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.217 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.218 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.219 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.220 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.221 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.222 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.223 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.224 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.225 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.226 (*here the solve-phase starts*)
1.227 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.228 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.229 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.230 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.231 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.232 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.233 (*------------------------------------*)
1.234 (* print_depth 13; get_calc 1;
1.235 *)
1.236 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.237 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.238 (*calc-head of subproblem*)
1.239 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.240 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.241 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.242 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.243 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.244 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.245 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.246 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.247 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.248 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.249 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.250 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.251 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.252 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.253 (*solve-phase of the subproblem*)
1.254 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.255 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.256 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.257 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.258 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.259 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.260 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.261 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.262 (*finish subproblem*)
1.263 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.264 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.265 (*finish problem*)
1.266 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.267 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.268
1.269 (*this checks the test for correctness..*)
1.270 val ((pt,_),_) = get_calc 1;
1.271 @@ -386,7 +386,7 @@
1.272 moveActiveRoot 1;
1.273 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
1.274
1.275 - autoCalculate 1 CompleteCalc;
1.276 + autoCalculate' 1 CompleteCalc;
1.277 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
1.278 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
1.279
1.280 @@ -409,11 +409,11 @@
1.281 Iterator 1;
1.282 moveActiveRoot 1;
1.283
1.284 - autoCalculate 1 CompleteCalcHead;
1.285 + autoCalculate' 1 CompleteCalcHead;
1.286 refFormula 1 (get_pos 1 1);
1.287 val ((pt,p),_) = get_calc 1;
1.288
1.289 - autoCalculate 1 CompleteCalc;
1.290 + autoCalculate' 1 CompleteCalc;
1.291 val ((pt,p),_) = get_calc 1;
1.292 if p=([], Res) then () else
1.293 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
1.294 @@ -428,7 +428,7 @@
1.295 ["Test","squ-equ-test-subpbl1"]))];
1.296 Iterator 1;
1.297 moveActiveRoot 1;
1.298 - autoCalculate 1 CompleteCalc;
1.299 + autoCalculate' 1 CompleteCalc;
1.300 val ((pt,p),_) = get_calc 1; show_pt pt;
1.301 (*
1.302 getTactic 1 ([1],Frm);
1.303 @@ -456,7 +456,7 @@
1.304 ["Test","squ-equ-test-subpbl1"]))];
1.305 Iterator 1;
1.306 moveActiveRoot 1;
1.307 - autoCalculate 1 CompleteCalcHead;
1.308 + autoCalculate' 1 CompleteCalcHead;
1.309
1.310 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
1.311 cell = NONE, ctxt = ctxt2, meth,
1.312 @@ -478,7 +478,7 @@
1.313 ["Test","solve_linear"]))];
1.314 Iterator 1;
1.315 moveActiveRoot 1;
1.316 - autoCalculate 1 CompleteModel;
1.317 + autoCalculate' 1 CompleteModel;
1.318 refFormula 1 (get_pos 1 1);
1.319
1.320 setProblem 1 ["LINEAR","univariate","equation","test"];
1.321 @@ -495,9 +495,9 @@
1.322 ["Test","solve_linear"]) then ()
1.323 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
1.324
1.325 - autoCalculate 1 CompleteCalcHead;
1.326 + autoCalculate' 1 CompleteCalcHead;
1.327 refFormula 1 (get_pos 1 1);
1.328 - autoCalculate 1 CompleteCalc;
1.329 + autoCalculate' 1 CompleteCalc;
1.330 moveActiveDown 1;
1.331 moveActiveDown 1;
1.332 moveActiveDown 1;
1.333 @@ -517,31 +517,31 @@
1.334 ("Test", ["sqroot-test","univariate","equation","test"],
1.335 ["Test","squ-equ-test-subpbl1"]))];
1.336 Iterator 1; moveActiveRoot 1;
1.337 - autoCalculate 1 CompleteCalcHead;
1.338 - autoCalculate 1 (Step 1);
1.339 + autoCalculate' 1 CompleteCalcHead;
1.340 + autoCalculate' 1 (Step 1);
1.341 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
1.342 (*
1.343 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
1.344 - autoCalculate 1 (Step 1);
1.345 + autoCalculate' 1 (Step 1);
1.346 val ((pt,p),_) = get_calc 1; show_pt pt;
1.347 *)
1.348 "-----^^^^^ and vvvvv do the same -----";
1.349 setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.350 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
1.351
1.352 - autoCalculate 1 (Step 1);
1.353 + autoCalculate' 1 (Step 1);
1.354 setContext 1 p "thy_isac_Test-rls-Test_simplify";
1.355 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
1.356 val (Form f, tac, asms) = pt_extract (pt, p);
1.357 if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
1.358 - then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
1.359 + then () else error "--- setContext..Thy --- autoCalculate' 1 (Step 1) #1";
1.360
1.361 - autoCalculate 1 CompleteCalc;
1.362 + autoCalculate' 1 CompleteCalc;
1.363 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
1.364 val (Form f, tac, asms) = pt_extract (pt, p);
1.365
1.366 if term2str f = "[x = 1]" andalso p = ([], Res) then ()
1.367 - else error "--- setContext..Thy --- autoCalculate CompleteCalc";
1.368 + else error "--- setContext..Thy --- autoCalculate' CompleteCalc";
1.369 DEconstrCalcTree 1;
1.370
1.371 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
1.372 @@ -551,7 +551,7 @@
1.373 ("Test", ["sqroot-test","univariate","equation","test"],
1.374 ["Test","squ-equ-test-subpbl1"]))];
1.375 Iterator 1; moveActiveRoot 1;
1.376 - autoCalculate 1 CompleteToSubpbl;
1.377 + autoCalculate' 1 CompleteToSubpbl;
1.378 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
1.379 val ((pt,_),_) = get_calc 1;
1.380 val str = pr_ptree pr_short pt;
1.381 @@ -560,12 +560,12 @@
1.382 then () else
1.383 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
1.384
1.385 - autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
1.386 - autoCalculate 1 CompleteToSubpbl;
1.387 + autoCalculate' 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
1.388 + autoCalculate' 1 CompleteToSubpbl;
1.389 val ((pt,_),_) = get_calc 1;
1.390 val str = pr_ptree pr_short pt;
1.391 writeln str;
1.392 - autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
1.393 + autoCalculate' 1 CompleteCalc; (*das geht ohnehin !*);
1.394 val ((pt,_),_) = get_calc 1;
1.395 val p = get_pos 1 1;
1.396
1.397 @@ -585,72 +585,72 @@
1.398 fetchProposedTactic 1;
1.399
1.400 setNextTactic 1 (Model_Problem);
1.401 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.402 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.403
1.404 setNextTactic 1 (Specify_Theory "RatEq");
1.405 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.406 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.407 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
1.408 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.409 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.410 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
1.411 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.412 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.413 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
1.414 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.415 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.416 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
1.417 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.418 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.419 setNextTactic 1 (Rewrite_Set "norm_Rational");
1.420 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.421 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.422 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
1.423 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.424 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.425 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
1.426 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
1.427 "univariate","equation"]));
1.428 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.429 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.430 setNextTactic 1 (Model_Problem );
1.431 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.432 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.433 setNextTactic 1 (Specify_Theory "PolyEq");
1.434 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.435 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.436 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.437 "univariate","equation"]);
1.438 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.439 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.440 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.441 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.442 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.443 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.444 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.445 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.446 setNextTactic 1 (Rewrite ("all_left",""));
1.447 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.448 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.449 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
1.450 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.451 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.452 (* __________ for "16 + 12 * x = 0"*)
1.453 setNextTactic 1 (Subproblem ("PolyEq",
1.454 ["degree_1","polynomial","univariate","equation"]));
1.455 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.456 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.457 setNextTactic 1 (Model_Problem );
1.458 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.459 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.460 setNextTactic 1 (Specify_Theory "PolyEq");
1.461 (*------------- some trials in the problem-hierarchy ---------------*)
1.462 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
1.463 - autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.464 + autoCalculate' 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
1.465 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
1.466 (*------------------------------------------------------------------*)
1.467 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.468 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.469 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.470 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.471 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.472 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
1.473 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.474 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.475 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
1.476 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.477 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.478 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
1.479 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.480 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.481 setNextTactic 1 Or_to_List;
1.482 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.483 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.484 setNextTactic 1 (Check_elementwise "Assumptions");
1.485 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.486 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.487 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
1.488 "univariate","equation"]);
1.489 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.490 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.491 setNextTactic 1 (Check_Postcond ["normalize","polynomial",
1.492 "univariate","equation"]);
1.493 - autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.494 + autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.495 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
1.496 val (ptp,_) = get_calc 1;
1.497 val (Form t,_,_) = pt_extract ptp;
1.498 @@ -678,16 +678,16 @@
1.499 (*..this tactic should be done 'tacitly', too !*)
1.500
1.501 (*
1.502 -autoCalculate 1 CompleteCalcHead;
1.503 +autoCalculate' 1 CompleteCalcHead;
1.504 checkContext 1 ([],Pbl) "pbl_equ_univ";
1.505 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.506 *)
1.507
1.508 - autoCalculate 1 (Step 1);
1.509 + autoCalculate' 1 (Step 1);
1.510
1.511 fetchProposedTactic 1;
1.512 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
1.513 - autoCalculate 1 (Step 1);
1.514 + autoCalculate' 1 (Step 1);
1.515
1.516 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
1.517 initContext 1 Pbl_ ([],Pbl);
1.518 @@ -700,10 +700,10 @@
1.519
1.520
1.521 fetchProposedTactic 1;
1.522 - setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
1.523 + setNextTactic 1 (Add_Given "solveFor x"); autoCalculate' 1 (Step 1);
1.524
1.525 fetchProposedTactic 1;
1.526 - setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
1.527 + setNextTactic 1 (Add_Find "solutions L"); autoCalculate' 1 (Step 1);
1.528
1.529 "--------- this is a matching model (all items correct): -------";
1.530 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
1.531 @@ -721,25 +721,25 @@
1.532 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
1.533 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.534 "univariate","equation"]);
1.535 - autoCalculate 1 (Step 1);
1.536 + autoCalculate' 1 (Step 1);
1.537 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
1.538 and Specify_Theory skipped in comparison to below ---^^^-inserted *)
1.539 (*------------vvv-inserted-----------------------------------------------*)
1.540 fetchProposedTactic 1;
1.541 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
1.542 "univariate","equation"]);
1.543 - autoCalculate 1 (Step 1);
1.544 + autoCalculate' 1 (Step 1);
1.545
1.546 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
1.547
1.548 fetchProposedTactic 1;
1.549 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.550 - autoCalculate 1 (Step 1);
1.551 + autoCalculate' 1 (Step 1);
1.552
1.553 fetchProposedTactic 1;
1.554 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
1.555
1.556 - autoCalculate 1 CompleteCalc;
1.557 + autoCalculate' 1 CompleteCalc;
1.558
1.559 val ((pt,_),_) = get_calc 1;
1.560 show_pt pt;
1.561 @@ -753,15 +753,15 @@
1.562 before, too, because there was no check*)
1.563 fetchProposedTactic 1;
1.564 setNextTactic 1 (Specify_Theory "PolyEq");
1.565 - autoCalculate 1 (Step 1);
1.566 + autoCalculate' 1 (Step 1);
1.567
1.568 fetchProposedTactic 1;
1.569 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
1.570 - autoCalculate 1 (Step 1);
1.571 + autoCalculate' 1 (Step 1);
1.572
1.573 fetchProposedTactic 1;
1.574 "--------- now the calc-header is ready for enter 'solving' ----";
1.575 - autoCalculate 1 CompleteCalc;
1.576 + autoCalculate' 1 CompleteCalc;
1.577
1.578 val ((pt,_),_) = get_calc 1;
1.579 rootthy pt;
1.580 @@ -871,7 +871,7 @@
1.581 fetchProposedTactic 1;
1.582 (*fill the CalcHead with Descriptions...*)
1.583 setNextTactic 1 (Model_Problem );
1.584 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.585 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.586
1.587 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
1.588 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
1.589 @@ -891,7 +891,7 @@
1.590 fetchProposedTactic 1;
1.591 (*the student follows the advice*)
1.592 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1.593 - autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
1.594 + autoCalculate' 1 (Step 1); refFormula 1 (get_pos 1 1);
1.595
1.596 (*this input completes the model*)
1.597 modifyCalcHead 1 (([],Pbl), "not used here",
1.598 @@ -938,7 +938,7 @@
1.599 Pbl,
1.600 ("Test", ["LINEAR","univariate","equation","test"],
1.601 ["Test","solve_linear"]));
1.602 - autoCalculate 1 CompleteCalc;
1.603 + autoCalculate' 1 CompleteCalc;
1.604 refFormula 1 (get_pos 1 1);
1.605 val ((pt,_),_) = get_calc 1;
1.606 val p = get_pos 1 1;
1.607 @@ -956,7 +956,7 @@
1.608 CalcTree [(fmz, sp)];
1.609 Iterator 1; moveActiveRoot 1;
1.610 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
1.611 - autoCalculate 1 CompleteCalc;
1.612 + autoCalculate' 1 CompleteCalc;
1.613 refFormula 1 (get_pos 1 1);
1.614 val ((pt,_),_) = get_calc 1;
1.615 val p = get_pos 1 1;
1.616 @@ -974,7 +974,7 @@
1.617 ["Test","squ-equ-test-subpbl1"]))];
1.618 Iterator 1;
1.619 moveActiveRoot 1;
1.620 - autoCalculate 1 CompleteCalc;
1.621 + autoCalculate' 1 CompleteCalc;
1.622 val ((pt,_),_) = get_calc 1;
1.623 show_pt pt;
1.624
1.625 @@ -1011,7 +1011,7 @@
1.626 ("Test", ["sqroot-test","univariate","equation","test"],
1.627 ["Test","squ-equ-test-subpbl1"]))];
1.628 Iterator 1; moveActiveRoot 1;
1.629 - autoCalculate 1 CompleteCalc;
1.630 + autoCalculate' 1 CompleteCalc;
1.631 val ((pt,_),_) = get_calc 1;
1.632 show_pt pt;
1.633
1.634 @@ -1041,7 +1041,7 @@
1.635 "solveFor x","solutions L"],
1.636 ("RatEq",["univariate","equation"],["no_met"]))];
1.637 Iterator 1; moveActiveRoot 1;
1.638 -autoCalculate 1 CompleteCalc;
1.639 +autoCalculate' 1 CompleteCalc;
1.640 val ((pt,_),_) = get_calc 1;
1.641 val p = get_pos 1 1;
1.642 val (Form f, tac, asms) = pt_extract (pt, p);
1.643 @@ -1081,35 +1081,35 @@
1.644 fetchProposedTactic 1;
1.645 (*ERROR get_calc 1 not existent*)
1.646 setNextTactic 1 (Model_Problem );
1.647 - autoCalculate 1 (Step 1);
1.648 + autoCalculate' 1 (Step 1);
1.649 fetchProposedTactic 1;
1.650 fetchProposedTactic 1;
1.651
1.652 setNextTactic 1 (Add_Find "solutions L");
1.653 setNextTactic 1 (Add_Find "solutions L");
1.654
1.655 - autoCalculate 1 (Step 1);
1.656 - autoCalculate 1 (Step 1);
1.657 + autoCalculate' 1 (Step 1);
1.658 + autoCalculate' 1 (Step 1);
1.659
1.660 setNextTactic 1 (Specify_Theory "Test");
1.661 fetchProposedTactic 1;
1.662 - autoCalculate 1 (Step 1);
1.663 + autoCalculate' 1 (Step 1);
1.664
1.665 - autoCalculate 1 (Step 1);
1.666 - autoCalculate 1 (Step 1);
1.667 - autoCalculate 1 (Step 1);
1.668 - autoCalculate 1 (Step 1);
1.669 + autoCalculate' 1 (Step 1);
1.670 + autoCalculate' 1 (Step 1);
1.671 + autoCalculate' 1 (Step 1);
1.672 + autoCalculate' 1 (Step 1);
1.673 (*------------------------- end calc-head*)
1.674
1.675 fetchProposedTactic 1;
1.676 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1.677 - autoCalculate 1 (Step 1);
1.678 + autoCalculate' 1 (Step 1);
1.679
1.680 setNextTactic 1 (Rewrite_Set "Test_simplify");
1.681 fetchProposedTactic 1;
1.682 - autoCalculate 1 (Step 1);
1.683 + autoCalculate' 1 (Step 1);
1.684
1.685 - autoCalculate 1 CompleteCalc;
1.686 + autoCalculate' 1 CompleteCalc;
1.687 val ((pt,_),_) = get_calc 1;
1.688 val p = get_pos 1 1;
1.689 val (Form f, tac, asms) = pt_extract (pt, p);
1.690 @@ -1125,9 +1125,9 @@
1.691 ["Test","squ-equ-test-subpbl1"]))];
1.692 Iterator 1;
1.693 moveActiveRoot 1;
1.694 - autoCalculate 1 CompleteCalcHead;
1.695 - autoCalculate 1 (Step 1);
1.696 - autoCalculate 1 (Step 1);
1.697 + autoCalculate' 1 CompleteCalcHead;
1.698 + autoCalculate' 1 (Step 1);
1.699 + autoCalculate' 1 (Step 1);
1.700 appendFormula 1 "-1 + x = 0" |> Future.join;
1.701 (*... returns calcChangedEvent with*)
1.702 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.703 @@ -1148,9 +1148,9 @@
1.704 ["Test","squ-equ-test-subpbl1"]))];
1.705 Iterator 1;
1.706 moveActiveRoot 1;
1.707 - autoCalculate 1 CompleteCalcHead;
1.708 - autoCalculate 1 (Step 1);
1.709 - autoCalculate 1 (Step 1);
1.710 + autoCalculate' 1 CompleteCalcHead;
1.711 + autoCalculate' 1 (Step 1);
1.712 + autoCalculate' 1 (Step 1);
1.713 appendFormula 1 "x - 1 = 0" |> Future.join;
1.714 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1.715 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1.716 @@ -1171,9 +1171,9 @@
1.717 ["Test","squ-equ-test-subpbl1"]))];
1.718 Iterator 1;
1.719 moveActiveRoot 1;
1.720 - autoCalculate 1 CompleteCalcHead;
1.721 - autoCalculate 1 (Step 1);
1.722 - autoCalculate 1 (Step 1);
1.723 + autoCalculate' 1 CompleteCalcHead;
1.724 + autoCalculate' 1 (Step 1);
1.725 + autoCalculate' 1 (Step 1);
1.726 appendFormula 1 "x = 1" |> Future.join;
1.727 (*... returns calcChangedEvent with*)
1.728 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1.729 @@ -1195,9 +1195,9 @@
1.730 ["Test","squ-equ-test-subpbl1"]))];
1.731 Iterator 1;
1.732 moveActiveRoot 1;
1.733 - autoCalculate 1 CompleteCalcHead;
1.734 - autoCalculate 1 (Step 1);
1.735 - autoCalculate 1 (Step 1);
1.736 + autoCalculate' 1 CompleteCalcHead;
1.737 + autoCalculate' 1 (Step 1);
1.738 + autoCalculate' 1 (Step 1);
1.739 appendFormula 1 "x - 4711 = 0" |> Future.join;
1.740 (*... returns <ERROR> no derivation found </ERROR>*)
1.741
1.742 @@ -1217,7 +1217,7 @@
1.743 ["Test","squ-equ-test-subpbl1"]))];
1.744 Iterator 1;
1.745 moveActiveRoot 1;
1.746 - autoCalculate 1 CompleteCalc;
1.747 + autoCalculate' 1 CompleteCalc;
1.748 moveActiveFormula 1 ([2],Res);
1.749 replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1.750 (*... returns <ERROR> formula not changed </ERROR>*)
1.751 @@ -1238,7 +1238,7 @@
1.752 ["Test","squ-equ-test-subpbl1"]))];
1.753 Iterator 2;
1.754 moveActiveRoot 2;
1.755 - autoCalculate 2 CompleteCalc;
1.756 + autoCalculate' 2 CompleteCalc;
1.757 moveActiveFormula 2 ([2],Res);
1.758 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1.759 (*... returns <ERROR> formula not changed </ERROR>*)
1.760 @@ -1263,7 +1263,7 @@
1.761 ["Test","squ-equ-test-subpbl1"]))];
1.762 Iterator 1;
1.763 moveActiveRoot 1;
1.764 - autoCalculate 1 CompleteCalc;
1.765 + autoCalculate' 1 CompleteCalc;
1.766 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.767 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1.768 (*... returns calcChangedEvent with*)
1.769 @@ -1297,7 +1297,7 @@
1.770 ["Test","squ-equ-test-subpbl1"]))];
1.771 Iterator 1;
1.772 moveActiveRoot 1;
1.773 - autoCalculate 1 CompleteCalc;
1.774 + autoCalculate' 1 CompleteCalc;
1.775 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.776 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1.777 (*... returns calcChangedEvent with ...*)
1.778 @@ -1329,7 +1329,7 @@
1.779 ["Test","squ-equ-test-subpbl1"]))];
1.780 Iterator 1;
1.781 moveActiveRoot 1;
1.782 - autoCalculate 1 CompleteCalc;
1.783 + autoCalculate' 1 CompleteCalc;
1.784 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1.785 replaceFormula 1 "x - 4711 = 0";
1.786 (*... returns <ERROR> no derivation found </ERROR>*)
1.787 @@ -1351,9 +1351,9 @@
1.788 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1.789 Iterator 1;
1.790 moveActiveRoot 1;
1.791 -autoCalculate 1 CompleteCalcHead;
1.792 -autoCalculate 1 (Step 1);
1.793 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.794 +autoCalculate' 1 CompleteCalcHead;
1.795 +autoCalculate' 1 (Step 1);
1.796 +autoCalculate' 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1.797 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" |> Future.join; (*<<<<<<<=========================*)
1.798 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1.799 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1.800 @@ -1402,7 +1402,7 @@
1.801 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
1.802 then () else error "inputFillFormula changed 11";
1.803
1.804 -autoCalculate 1 CompleteCalc;
1.805 +autoCalculate' 1 CompleteCalc;
1.806
1.807 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1.808 val ((pt, _),_) = get_calc 1;
1.809 @@ -1432,8 +1432,8 @@
1.810 moveActiveRoot 1;
1.811 moveActiveFormula 1 ([],Pbl);
1.812 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1.813 -autoCalculate 1 CompleteCalcHead;
1.814 -autoCalculate 1 (Step 1);
1.815 +autoCalculate' 1 CompleteCalcHead;
1.816 +autoCalculate' 1 (Step 1);
1.817 appendFormula 1 "8 * x / (8 * y)" |> Future.join;
1.818 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1.819 --- but in BridgeLog Java <=> SML:
1.820 @@ -1451,7 +1451,7 @@
1.821 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1.822 Iterator 1;
1.823 moveActiveRoot 1;
1.824 -autoCalculate 1 CompleteCalc;
1.825 +autoCalculate' 1 CompleteCalc;
1.826 val ((pt,p),_) = get_calc 1; show_pt pt;
1.827
1.828 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1.829 @@ -1465,9 +1465,9 @@
1.830 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1.831 Iterator 1;
1.832 moveActiveRoot 1;
1.833 -autoCalculate 1 CompleteCalcHead;
1.834 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.835 -autoCalculate 1 (Step 1); fetchProposedTactic 1;
1.836 +autoCalculate' 1 CompleteCalcHead;
1.837 +autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.838 +autoCalculate' 1 (Step 1); fetchProposedTactic 1;
1.839 (*
1.840 <NEXTTAC>
1.841 <CALCID> 1 </CALCID>
1.842 @@ -1502,7 +1502,7 @@
1.843 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1.844 (* then --- UC errpat, fillpat by input ---*)
1.845 *)
1.846 -autoCalculate 1 CompleteCalc;
1.847 +autoCalculate' 1 CompleteCalc;
1.848 val ((pt,p),_) = get_calc 1; show_pt pt;
1.849 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1.850