1 (* Title: tests the interface of isac's SML-kernel in accordance to
2 java-tests/isac.bridge.
4 (c) copyright due to lincense terms.
6 WN050707 ... if true, the test ist marked with a \label referring
7 to the same UC in isac-docu.tex as the JUnit testcase.
8 WN120210?not ME: added some labels, which are not among the above,
9 repaired lost \label (s).
12 "--------------------------------------------------------";
13 "table of contents --------------------------------------";
14 "--------------------------------------------------------";
15 "within struct ------------------------------------------";
16 "--------------------------------------------------------";
17 "--------- encode ^ -> ^^^ ------------------------------";
18 "--------------------------------------------------------";
19 "exported from struct -----------------------------------";
20 "--------------------------------------------------------";
21 "--------- empty rootpbl --------------------------------";
22 "--------- solve_linear as rootpbl FE -------------------";
23 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
24 "--------- miniscript with mini-subpbl ------------------";
25 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
26 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
27 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
28 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
29 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
30 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
31 "--------- setContext..Thy ------------------------------";
32 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
33 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
34 "--------- tryMatchProblem, tryRefineProblem ------------";
35 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
36 "--------- maximum-example, UC: Modeling an example -----";
37 "--------- solve_linear from pbl-hierarchy --------------";
38 "--------- solve_linear as in an algebra system (CAS)----";
39 "--------- interSteps: on 'miniscript with mini-subpbl' -";
40 "--------- getTactic, fetchApplicableTactics ------------";
41 "--------- getAssumptions, getAccumulatedAsms -----------";
42 "--------- arbitrary combinations of steps --------------";
43 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
44 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
45 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
46 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
47 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
48 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
49 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
50 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
51 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
52 "--------- UC errpat add-fraction, fillpat by input --------------";
53 "--------- UC errpat, fillpat step to Rewrite --------------------";
54 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
55 "--------------------------------------------------------";
57 "within struct ---------------------------------------------------";
58 "within struct ---------------------------------------------------";
59 "within struct ---------------------------------------------------";
60 (*==================================================================
63 "--------- encode ^ -> ^^^ ------------------------------";
64 "--------- encode ^ -> ^^^ ------------------------------";
65 "--------- encode ^ -> ^^^ ------------------------------";
66 if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
67 else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
69 if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
70 else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
72 ==================================================================*)
73 "exported from struct --------------------------------------------";
74 "exported from struct --------------------------------------------";
75 "exported from struct --------------------------------------------";
78 (*------------ set at startup of the Kernel ----------------------*)
79 states:= []; (*resets all state information in Kernel *)
80 (*----------------------------------------------------------------*)
82 "--------- empty rootpbl --------------------------------";
83 "--------- empty rootpbl --------------------------------";
84 "--------- empty rootpbl --------------------------------";
85 CalcTree [([], ("", [], []))];
88 refFormula 1 (get_pos 1 1);
89 (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
92 "--------- solve_linear as rootpbl FE -------------------";
93 "--------- solve_linear as rootpbl FE -------------------";
94 "--------- solve_linear as rootpbl FE -------------------";
95 CalcTree (*start of calculation, return No.1*)
96 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
98 ["LINEAR","univariate","equation","test"],
99 ["Test","solve_linear"]))];
100 Iterator 1; (*create an active Iterator on CalcTree No.1*)
102 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
103 refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
106 fetchProposedTactic 1 (*by using Iterator No.1*);
107 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
108 autoCalculate 1 (Step 1);
109 refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
110 autoCalculate 1 (Step 1);
111 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
112 fetchProposedTactic 1;
113 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
114 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
116 fetchProposedTactic 1;
117 setNextTactic 1 (Add_Given "solveFor x");
118 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
120 fetchProposedTactic 1;
121 setNextTactic 1 (Add_Find "solutions L");
122 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
124 fetchProposedTactic 1;
125 setNextTactic 1 (Specify_Theory "Test");
126 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
127 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
129 fetchProposedTactic 1;
130 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
131 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
132 (*-------------------------------------------------------------------------*)
133 fetchProposedTactic 1;
134 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
136 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
137 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
139 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
140 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
142 (*-------------------------------------------------------------------------*)
143 fetchProposedTactic 1;
144 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
146 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
147 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
148 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
150 is_complete_spec ptp;
152 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
153 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
154 (*term2str (get_obj g_form pt [1]);*)
155 (*-------------------------------------------------------------------------*)
157 fetchProposedTactic 1;
158 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
159 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
161 fetchProposedTactic 1;
162 setNextTactic 1 (Rewrite_Set "Test_simplify");
163 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
165 fetchProposedTactic 1;
166 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
167 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
169 val ((pt,_),_) = get_calc 1;
170 val ip = get_pos 1 1;
171 val (Form f, tac, asms) = pt_extract (pt, ip);
172 (*exception just above means: 'ModSpec' has been returned: error anyway*)
173 if term2str f = "[x = 1]" then () else
174 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
176 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
177 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
178 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
179 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
181 refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
183 refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
185 refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
186 (*getAssumption 1 ([1],Res); TODO.WN041217*)
187 moveActiveDown 1 ; refFormula 1 ([2],Res);
188 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
192 if get_pos 1 1 = ([2], Res) then () else
193 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
194 moveActiveDown 1; refFormula 1 ([], Res);
195 if get_pos 1 1 = ([], Res) then () else
196 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
197 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
200 "--------- miniscript with mini-subpbl ------------------";
201 "--------- miniscript with mini-subpbl ------------------";
202 "--------- miniscript with mini-subpbl ------------------";
203 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
204 "=== this sequence of fun-calls resembles fun me ===";
205 states:=[]; (*start of calculation, return No.1*)
206 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
207 ("Test", ["sqroot-test","univariate","equation","test"],
208 ["Test","squ-equ-test-subpbl1"]))];
212 refFormula 1 (get_pos 1 1);
213 fetchProposedTactic 1;
214 setNextTactic 1 (Model_Problem);
215 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
217 fetchProposedTactic 1;
218 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
219 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
221 fetchProposedTactic 1;
222 setNextTactic 1 (Add_Given "solveFor x");
223 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
225 fetchProposedTactic 1;
226 setNextTactic 1 (Add_Find "solutions L");
227 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
229 fetchProposedTactic 1;
230 setNextTactic 1 (Specify_Theory "Test");
231 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
233 fetchProposedTactic 1;
234 setNextTactic 1 (Specify_Problem
235 ["sqroot-test","univariate","equation","test"]);
236 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
237 "1-----------------------------------------------------------------";
239 fetchProposedTactic 1;
240 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
241 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
243 fetchProposedTactic 1;
244 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
245 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
247 fetchProposedTactic 1;
248 setNextTactic 1 (Rewrite_Set "norm_equation");
249 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
251 fetchProposedTactic 1;
252 setNextTactic 1 (Rewrite_Set "Test_simplify");
253 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
255 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
256 setNextTactic 1 (Subproblem ("Test",
257 ["LINEAR","univariate","equation","test"]));
258 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
260 fetchProposedTactic 1;
261 setNextTactic 1 (Model_Problem );
262 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
264 fetchProposedTactic 1;
265 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
266 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
268 fetchProposedTactic 1;
269 setNextTactic 1 (Add_Given "solveFor x");
270 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
272 fetchProposedTactic 1;
273 setNextTactic 1 (Add_Find "solutions x_i");
274 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
276 fetchProposedTactic 1;
277 setNextTactic 1 (Specify_Theory "Test");
278 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
280 fetchProposedTactic 1;
281 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
282 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
283 "2-----------------------------------------------------------------";
285 fetchProposedTactic 1;
286 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
287 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
289 fetchProposedTactic 1;
290 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
291 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
293 fetchProposedTactic 1;
294 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
295 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
297 fetchProposedTactic 1;
298 setNextTactic 1 (Rewrite_Set "Test_simplify");
299 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
301 fetchProposedTactic 1;
302 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
303 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
305 fetchProposedTactic 1;
306 setNextTactic 1 (Check_elementwise "Assumptions");
307 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
309 val xml = fetchProposedTactic 1;
310 setNextTactic 1 (Check_Postcond
311 ["sqroot-test","univariate","equation","test"]);
312 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
314 val ((pt,_),_) = get_calc 1;
315 val str = pr_ptree pr_short pt;
317 val ip = get_pos 1 1;
318 val (Form f, tac, asms) = pt_extract (pt, ip);
319 (*exception just above means: 'ModSpec' has been returned: error anyway*)
320 if term2str f = "[x = 1]" then () else
321 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
324 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
325 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
326 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
327 (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
328 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
329 ("Test", ["sqroot-test","univariate","equation","test"],
330 ["Test","squ-equ-test-subpbl1"]))];
333 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
334 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
335 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
336 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
337 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
338 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
339 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
340 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
341 (*here the solve-phase starts*)
342 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
343 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
344 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
345 (*------------------------------------*)
346 (* print_depth 13; get_calc 1;
348 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
349 (*calc-head of subproblem*)
350 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
351 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
352 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
353 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
354 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
355 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
356 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
357 (*solve-phase of the subproblem*)
358 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
359 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
360 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
361 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
362 (*finish subproblem*)
363 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
365 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
367 (*this checks the test for correctness..*)
368 val ((pt,_),_) = get_calc 1;
370 val (Form f, tac, asms) = pt_extract (pt, p);
371 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
372 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
376 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
377 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
378 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
379 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
381 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
383 ["LINEAR","univariate","equation","test"],
384 ["Test","solve_linear"]))];
387 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
389 autoCalculate 1 CompleteCalc;
390 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
391 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
393 val ((pt,_),_) = get_calc 1;
395 val (Form f, tac, asms) = pt_extract (pt, p);
396 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
397 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
400 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
401 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
402 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
403 (* ERROR: error in kernel ?? *)
405 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
407 ["LINEAR","univariate","equation","test"],
408 ["Test","solve_linear"]))];
412 autoCalculate 1 CompleteCalcHead;
413 refFormula 1 (get_pos 1 1);
414 val ((pt,p),_) = get_calc 1;
416 autoCalculate 1 CompleteCalc;
417 val ((pt,p),_) = get_calc 1;
418 if p=([], Res) then () else
419 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
422 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
423 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
424 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
425 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
426 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
427 ("Test", ["sqroot-test","univariate","equation","test"],
428 ["Test","squ-equ-test-subpbl1"]))];
431 autoCalculate 1 CompleteCalc;
432 val ((pt,p),_) = get_calc 1; show_pt pt;
434 getTactic 1 ([1],Frm);
435 getTactic 1 ([1],Res);
436 initContext 1 Thy_ ([1],Res);
438 (*... returns calcChangedEvent with*)
439 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
440 getFormulaeFromTo 1 unc gen 0 (*only result*) false;
441 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
442 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
444 val ((pt,_),_) = get_calc 1;
446 val (Form f, tac, asms) = pt_extract (pt, p);
447 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
448 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
451 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
452 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
453 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
454 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
455 ("Test", ["sqroot-test","univariate","equation","test"],
456 ["Test","squ-equ-test-subpbl1"]))];
459 autoCalculate 1 CompleteCalcHead;
461 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
462 cell = NONE, ctxt = ctxt2, meth,
463 spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
464 ["Test", "squ-equ-test-subpbl1"]),
465 probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
466 ([], Met)), []) = get_calc 1;
467 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
468 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
471 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
472 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
473 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
475 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
477 ["LINEAR","univariate","equation","test"],
478 ["Test","solve_linear"]))];
481 autoCalculate 1 CompleteModel;
482 refFormula 1 (get_pos 1 1);
484 setProblem 1 ["LINEAR","univariate","equation","test"];
485 val pos = get_pos 1 1;
486 setContext 1 pos (kestoreID2guh Pbl_["LINEAR","univariate","equation","test"]);
487 refFormula 1 (get_pos 1 1);
489 setMethod 1 ["Test","solve_linear"];
490 setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
491 refFormula 1 (get_pos 1 1);
492 val ((pt,_),_) = get_calc 1;
493 if get_obj g_spec pt [] = ("e_domID",
494 ["LINEAR", "univariate","equation","test"],
495 ["Test","solve_linear"]) then ()
496 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
498 autoCalculate 1 CompleteCalcHead;
499 refFormula 1 (get_pos 1 1);
500 autoCalculate 1 CompleteCalc;
504 refFormula 1 (get_pos 1 1);
505 val ((pt,_),_) = get_calc 1;
507 val (Form f, tac, asms) = pt_extract (pt, p);
508 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
509 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
512 "--------- setContext..Thy ------------------------------";
513 "--------- setContext..Thy ------------------------------";
514 "--------- setContext..Thy ------------------------------";
516 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
517 ("Test", ["sqroot-test","univariate","equation","test"],
518 ["Test","squ-equ-test-subpbl1"]))];
519 Iterator 1; moveActiveRoot 1;
520 autoCalculate 1 CompleteCalcHead;
521 autoCalculate 1 (Step 1);
522 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
524 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
525 autoCalculate 1 (Step 1);
526 val ((pt,p),_) = get_calc 1; show_pt pt;
528 "-----^^^^^ and vvvvv do the same -----";
529 setContext 1 p "thy_isac_Test-rls-Test_simplify";
530 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
532 autoCalculate 1 (Step 1);
533 setContext 1 p "thy_isac_Test-rls-Test_simplify";
534 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
535 val (Form f, tac, asms) = pt_extract (pt, p);
536 if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
537 then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
539 autoCalculate 1 CompleteCalc;
540 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
541 val (Form f, tac, asms) = pt_extract (pt, p);
543 if term2str f = "[x = 1]" andalso p = ([], Res) then ()
544 else error "--- setContext..Thy --- autoCalculate CompleteCalc";
547 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
548 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
549 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
550 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
551 ("Test", ["sqroot-test","univariate","equation","test"],
552 ["Test","squ-equ-test-subpbl1"]))];
553 Iterator 1; moveActiveRoot 1;
554 autoCalculate 1 CompleteToSubpbl;
555 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
556 val ((pt,_),_) = get_calc 1;
557 val str = pr_ptree pr_short pt;
559 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
561 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
563 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
564 autoCalculate 1 CompleteToSubpbl;
565 val ((pt,_),_) = get_calc 1;
566 val str = pr_ptree pr_short pt;
568 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
569 val ((pt,_),_) = get_calc 1;
572 val (Form f, tac, asms) = pt_extract (pt, p);
573 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
574 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
577 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
578 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
579 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
581 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
582 ("RatEq", ["univariate","equation"], ["no_met"]))];
585 fetchProposedTactic 1;
587 setNextTactic 1 (Model_Problem);
588 autoCalculate 1 (Step 1); fetchProposedTactic 1;
590 setNextTactic 1 (Specify_Theory "RatEq");
591 autoCalculate 1 (Step 1); fetchProposedTactic 1;
592 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
593 autoCalculate 1 (Step 1); fetchProposedTactic 1;
594 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
595 autoCalculate 1 (Step 1); fetchProposedTactic 1;
596 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
597 autoCalculate 1 (Step 1); fetchProposedTactic 1;
598 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
599 autoCalculate 1 (Step 1); fetchProposedTactic 1;
600 setNextTactic 1 (Rewrite_Set "norm_Rational");
601 autoCalculate 1 (Step 1); fetchProposedTactic 1;
602 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
603 autoCalculate 1 (Step 1); fetchProposedTactic 1;
604 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
605 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
606 "univariate","equation"]));
607 autoCalculate 1 (Step 1); fetchProposedTactic 1;
608 setNextTactic 1 (Model_Problem );
609 autoCalculate 1 (Step 1); fetchProposedTactic 1;
610 setNextTactic 1 (Specify_Theory "PolyEq");
611 autoCalculate 1 (Step 1); fetchProposedTactic 1;
612 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
613 "univariate","equation"]);
614 autoCalculate 1 (Step 1); fetchProposedTactic 1;
615 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
616 autoCalculate 1 (Step 1); fetchProposedTactic 1;
617 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
618 autoCalculate 1 (Step 1); fetchProposedTactic 1;
619 setNextTactic 1 (Rewrite ("all_left",""));
620 autoCalculate 1 (Step 1); fetchProposedTactic 1;
621 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
622 autoCalculate 1 (Step 1); fetchProposedTactic 1;
623 (* __________ for "16 + 12 * x = 0"*)
624 setNextTactic 1 (Subproblem ("PolyEq",
625 ["degree_1","polynomial","univariate","equation"]));
626 autoCalculate 1 (Step 1); fetchProposedTactic 1;
627 setNextTactic 1 (Model_Problem );
628 autoCalculate 1 (Step 1); fetchProposedTactic 1;
629 setNextTactic 1 (Specify_Theory "PolyEq");
630 (*------------- some trials in the problem-hierarchy ---------------*)
631 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
632 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
633 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
634 (*------------------------------------------------------------------*)
635 autoCalculate 1 (Step 1); fetchProposedTactic 1;
636 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
637 autoCalculate 1 (Step 1); fetchProposedTactic 1;
638 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
639 autoCalculate 1 (Step 1); fetchProposedTactic 1;
640 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
641 autoCalculate 1 (Step 1); fetchProposedTactic 1;
642 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
643 autoCalculate 1 (Step 1); fetchProposedTactic 1;
644 setNextTactic 1 Or_to_List;
645 autoCalculate 1 (Step 1); fetchProposedTactic 1;
646 setNextTactic 1 (Check_elementwise "Assumptions");
647 autoCalculate 1 (Step 1); fetchProposedTactic 1;
648 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
649 "univariate","equation"]);
650 autoCalculate 1 (Step 1); fetchProposedTactic 1;
651 setNextTactic 1 (Check_Postcond ["normalize","polynomial",
652 "univariate","equation"]);
653 autoCalculate 1 (Step 1); fetchProposedTactic 1;
654 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
655 val (ptp,_) = get_calc 1;
656 val (Form t,_,_) = pt_extract ptp;
657 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
658 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
661 "--------- tryMatchProblem, tryRefineProblem ------------";
662 "--------- tryMatchProblem, tryRefineProblem ------------";
663 "--------- tryMatchProblem, tryRefineProblem ------------";
664 (*{\bf\UC{Having \isac{} Refine the Problem
665 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
666 * x^^^2 + 4*x + 5 = 2
667 see isac.bridge.TestSpecify#testMatchRefine*)
669 [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
671 ["univariate","equation"],
676 fetchProposedTactic 1;
677 setNextTactic 1 (Model_Problem );
678 (*..this tactic should be done 'tacitly', too !*)
681 autoCalculate 1 CompleteCalcHead;
682 checkContext 1 ([],Pbl) "pbl_equ_univ";
683 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
686 autoCalculate 1 (Step 1);
688 fetchProposedTactic 1;
689 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
690 autoCalculate 1 (Step 1);
692 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
693 initContext 1 Pbl_ ([],Pbl);
694 initContext 1 Met_ ([],Pbl);
696 "--------- this match will show some incomplete items: ---------";
698 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
699 checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
702 fetchProposedTactic 1;
703 setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
705 fetchProposedTactic 1;
706 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
708 "--------- this is a matching model (all items correct): -------";
709 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
710 "--------- this is a NOT matching model (some 'false': ---------";
711 checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["LINEAR","univariate","equation"]);
713 "--------- find out a matching problem: ------------------------";
714 "--------- find out a matching problem (FAILING: no new pbl) ---";
715 refineProblem 1([],Pbl)(pblID2guh ["LINEAR","univariate","equation"]);
717 "--------- find out a matching problem (SUCCESSFUL) ------------";
718 refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
720 "--------- tryMatch, tryRefine did not change the calculation -";
721 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
722 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
723 "univariate","equation"]);
724 autoCalculate 1 (Step 1);
725 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
726 and Specify_Theory skipped in comparison to below ---^^^-inserted *)
727 (*------------vvv-inserted-----------------------------------------------*)
728 fetchProposedTactic 1;
729 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
730 "univariate","equation"]);
731 autoCalculate 1 (Step 1);
733 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
735 fetchProposedTactic 1;
736 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
737 autoCalculate 1 (Step 1);
739 fetchProposedTactic 1;
740 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
742 autoCalculate 1 CompleteCalc;
744 val ((pt,_),_) = get_calc 1;
747 val (Form f, tac, asms) = pt_extract (pt, p);
748 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
749 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
751 (*------------^^^-inserted-----------------------------------------------*)
752 (*WN050904 the fetchProposedTactic's below may not have worked like that
753 before, too, because there was no check*)
754 fetchProposedTactic 1;
755 setNextTactic 1 (Specify_Theory "PolyEq");
756 autoCalculate 1 (Step 1);
758 fetchProposedTactic 1;
759 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
760 autoCalculate 1 (Step 1);
762 fetchProposedTactic 1;
763 "--------- now the calc-header is ready for enter 'solving' ----";
764 autoCalculate 1 CompleteCalc;
766 val ((pt,_),_) = get_calc 1;
770 val (Form f, tac, asms) = pt_extract (pt, p);
771 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
772 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
776 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
777 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
778 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
779 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
780 ("Test", ["sqroot-test","univariate","equation","test"],
781 ["Test","squ-equ-test-subpbl1"]))];
785 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
786 "solve (x+1=2, x)",(*the headline*)
787 [Given ["equality (x+1=(2::real))", "solveFor x"],
788 Find ["solutions L"](*,Relate []*)],
791 ["sqroot-test","univariate","equation","test"],
792 ["Test","squ-equ-test-subpbl1"]));
794 val ((Nd (PblObj {env = NONE,
796 loc = (SOME scrst_ctxt, NONE),
801 ["sqroot-test", "univariate", "equation", "test"],
802 ["Test", "squ-equ-test-subpbl1"]),
804 branch = TransitiveB,
811 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
812 if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
813 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
819 val ((Nd (PblObj {env = NONE,
821 loc = (SOME scrst_ctxt, NONE),
825 spec = ("e_domID", ["e_pblID"], ["e_metID"]),
827 branch = TransitiveB,
834 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
835 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
837 "--------- maximum-example, UC: Modeling an example -----";
838 "--------- maximum-example, UC: Modeling an example -----";
839 "--------- maximum-example, UC: Modeling an example -----";
840 (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
841 see isac.bridge.TestModel#testEditItems
843 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
844 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
845 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
846 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
847 (*^^^ these are the elements for the root-problem (in variants)*)
848 (*vvv these are elements required for subproblems*)
849 "boundVariable a","boundVariable b","boundVariable alpha",
850 "interval {x::real. 0 <= x & x <= 2*r}",
851 "interval {x::real. 0 <= x & x <= 2*r}",
852 "interval {x::real. 0 <= x & x <= pi}",
853 "errorBound (eps=(0::real))"]
854 (*specifying is not interesting for this example*)
855 val spec = ("DiffApp", ["maximum_of","function"],
856 ["DiffApp","max_by_calculus"]);
857 (*the empty model with descriptions for user-guidance by Model_Problem*)
858 val empty_model = [Given ["fixedValues []"],
859 Find ["maximum", "valuesFor"],
860 Relate ["relations []"]];
863 "#################################################################";
865 CalcTree [(elems, spec)];
868 refFormula 1 (get_pos 1 1);
869 (*this gives a completely empty model*)
871 fetchProposedTactic 1;
872 (*fill the CalcHead with Descriptions...*)
873 setNextTactic 1 (Model_Problem );
874 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
876 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
877 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
878 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
879 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
880 "Problem (DiffApp.thy, [maximum_of, function])",
881 (*the head-form ^^^ is not used for input here*)
882 [Given ["fixedValues [r=Arbfix]"(*new input*)],
883 Find ["maximum b"(*new input*), "valuesFor"],
884 Relate ["relations"]],
885 (*input (Arbfix will dissappear soon)*)
887 e_spec (*no input to the specification*));
889 (*the user does not know, what 'superfluous' for 'maximum b' may mean
890 and asks what to do next*)
891 fetchProposedTactic 1;
892 (*the student follows the advice*)
893 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
894 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
896 (*this input completes the model*)
897 modifyCalcHead 1 (([],Pbl), "not used here",
898 [Given ["fixedValues [r=Arbfix]"],
899 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
900 Relate ["relations [A=a*b, \
901 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
903 (*specification is not interesting and should be skipped by the dialogguide;
904 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
905 modifyCalcHead 1 (([],Pbl), "not used here",
906 [Given ["fixedValues [r=Arbfix]"],
907 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
908 Relate ["relations [A=a*b, \
909 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
910 ("DiffApp", ["e_pblID"], ["e_metID"]));
911 modifyCalcHead 1 (([],Pbl), "not used here",
912 [Given ["fixedValues [r=Arbfix]"],
913 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
914 Relate ["relations [A=a*b, \
915 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
916 ("DiffApp", ["maximum_of","function"],
918 modifyCalcHead 1 (([],Pbl), "not used here",
919 [Given ["fixedValues [r=Arbfix]"],
920 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
921 Relate ["relations [A=a*b, \
922 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
923 ("DiffApp", ["maximum_of","function"],
924 ["DiffApp","max_by_calculus"]));
925 (*this final calcHead now has STATUS 'complete' !*)
928 "--------- solve_linear from pbl-hierarchy --------------";
929 "--------- solve_linear from pbl-hierarchy --------------";
930 "--------- solve_linear from pbl-hierarchy --------------";
931 val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], []));
932 CalcTree [(fmz, sp)];
933 Iterator 1; moveActiveRoot 1;
934 refFormula 1 (get_pos 1 1);
935 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
936 [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
937 Find ["solutions L"]],
939 ("Test", ["LINEAR","univariate","equation","test"],
940 ["Test","solve_linear"]));
941 autoCalculate 1 CompleteCalc;
942 refFormula 1 (get_pos 1 1);
943 val ((pt,_),_) = get_calc 1;
945 val (Form f, tac, asms) = pt_extract (pt, p);
946 if term2str f = "[x = 1]" andalso p = ([], Res)
947 andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
948 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
951 "--------- solve_linear as in an algebra system (CAS)----";
952 "--------- solve_linear as in an algebra system (CAS)----";
953 "--------- solve_linear as in an algebra system (CAS)----";
954 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
955 val (fmz, sp) = ([], ("", [], []));
956 CalcTree [(fmz, sp)];
957 Iterator 1; moveActiveRoot 1;
958 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
959 autoCalculate 1 CompleteCalc;
960 refFormula 1 (get_pos 1 1);
961 val ((pt,_),_) = get_calc 1;
963 val (Form f, tac, asms) = pt_extract (pt, p);
964 if term2str f = "[x = 1]" andalso p = ([], Res)
965 andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
966 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
969 "--------- interSteps: on 'miniscript with mini-subpbl' -";
970 "--------- interSteps: on 'miniscript with mini-subpbl' -";
971 "--------- interSteps: on 'miniscript with mini-subpbl' -";
972 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
973 ("Test", ["sqroot-test","univariate","equation","test"],
974 ["Test","squ-equ-test-subpbl1"]))];
977 autoCalculate 1 CompleteCalc;
978 val ((pt,_),_) = get_calc 1;
981 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
982 interSteps 1 ([2],Res);
983 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
984 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
985 getFormulaeFromTo 1 unc gen 1 false;
987 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
988 interSteps 1 ([3,2],Res);
989 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
990 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
991 getFormulaeFromTo 1 unc gen 1 false;
993 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
994 interSteps 1 ([3],Res) (*no new steps in subproblems*);
995 val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
996 getFormulaeFromTo 1 unc gen 1 false;
998 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
999 interSteps 1 ([],Res) (*no new steps in subproblems*);
1000 val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1001 getFormulaeFromTo 1 unc gen 1 false;
1004 "--------- getTactic, fetchApplicableTactics ------------";
1005 "--------- getTactic, fetchApplicableTactics ------------";
1006 "--------- getTactic, fetchApplicableTactics ------------";
1007 (* compare test/../script.sml
1008 "----------- fun sel_rules ---------------------------------------";
1010 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1011 ("Test", ["sqroot-test","univariate","equation","test"],
1012 ["Test","squ-equ-test-subpbl1"]))];
1013 Iterator 1; moveActiveRoot 1;
1014 autoCalculate 1 CompleteCalc;
1015 val ((pt,_),_) = get_calc 1;
1018 (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1019 WN120210 not impl. in FE*)
1020 getTactic 1 ([],Pbl);
1021 getTactic 1 ([1],Res);
1022 getTactic 1 ([3],Pbl);
1023 getTactic 1 ([3,1],Frm);
1024 getTactic 1 ([3],Res);
1025 getTactic 1 ([],Res);
1027 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1028 fetchApplicableTactics 1 99999 ([],Pbl);
1029 fetchApplicableTactics 1 99999 ([1],Res);
1030 fetchApplicableTactics 1 99999 ([3],Pbl);
1031 fetchApplicableTactics 1 99999 ([3,1],Res);
1032 fetchApplicableTactics 1 99999 ([3],Res);
1033 fetchApplicableTactics 1 99999 ([],Res);
1036 "--------- getAssumptions, getAccumulatedAsms -----------";
1037 "--------- getAssumptions, getAccumulatedAsms -----------";
1038 "--------- getAssumptions, getAccumulatedAsms -----------";
1040 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1041 "solveFor x","solutions L"],
1042 ("RatEq",["univariate","equation"],["no_met"]))];
1043 Iterator 1; moveActiveRoot 1;
1044 autoCalculate 1 CompleteCalc;
1045 val ((pt,_),_) = get_calc 1;
1046 val p = get_pos 1 1;
1047 val (Form f, tac, asms) = pt_extract (pt, p);
1048 (*============ inhibit exn WN120316 compare 2002--2011 ===========================
1049 if map term2str asms =
1050 ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^
1051 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
1052 "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
1053 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
1054 "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
1055 andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
1056 else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*)
1057 ============ inhibit exn WN120316 compare 2002--2011 ===========================*)
1058 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
1059 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
1060 then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1062 (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1063 getAssumptions 1 ([3], Res);
1064 getAssumptions 1 ([5], Res);
1065 (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1066 WN0502 still without positions*)
1067 getAccumulatedAsms 1 ([3], Res);
1068 getAccumulatedAsms 1 ([5], Res);
1071 "--------- arbitrary combinations of steps --------------";
1072 "--------- arbitrary combinations of steps --------------";
1073 "--------- arbitrary combinations of steps --------------";
1074 CalcTree (*start of calculation, return No.1*)
1075 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1077 ["LINEAR","univariate","equation","test"],
1078 ["Test","solve_linear"]))];
1079 Iterator 1; moveActiveRoot 1;
1081 fetchProposedTactic 1;
1082 (*ERROR get_calc 1 not existent*)
1083 setNextTactic 1 (Model_Problem );
1084 autoCalculate 1 (Step 1);
1085 fetchProposedTactic 1;
1086 fetchProposedTactic 1;
1088 setNextTactic 1 (Add_Find "solutions L");
1089 setNextTactic 1 (Add_Find "solutions L");
1091 autoCalculate 1 (Step 1);
1092 autoCalculate 1 (Step 1);
1094 setNextTactic 1 (Specify_Theory "Test");
1095 fetchProposedTactic 1;
1096 autoCalculate 1 (Step 1);
1098 autoCalculate 1 (Step 1);
1099 autoCalculate 1 (Step 1);
1100 autoCalculate 1 (Step 1);
1101 autoCalculate 1 (Step 1);
1102 (*------------------------- end calc-head*)
1104 fetchProposedTactic 1;
1105 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1106 autoCalculate 1 (Step 1);
1108 setNextTactic 1 (Rewrite_Set "Test_simplify");
1109 fetchProposedTactic 1;
1110 autoCalculate 1 (Step 1);
1112 autoCalculate 1 CompleteCalc;
1113 val ((pt,_),_) = get_calc 1;
1114 val p = get_pos 1 1;
1115 val (Form f, tac, asms) = pt_extract (pt, p);
1116 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1117 error "FE-interface.sml: diff.behav. in combinations of steps";
1120 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1121 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1122 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1123 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1124 ("Test", ["sqroot-test","univariate","equation","test"],
1125 ["Test","squ-equ-test-subpbl1"]))];
1128 autoCalculate 1 CompleteCalcHead;
1129 autoCalculate 1 (Step 1);
1130 autoCalculate 1 (Step 1);
1131 appendFormula 1 "-1 + x = 0";
1132 (*... returns calcChangedEvent with*)
1133 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1134 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1136 val ((pt,_),_) = get_calc 1;
1137 val p = get_pos 1 1;
1138 val (Form f, tac, asms) = pt_extract (pt, p);
1139 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1140 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1143 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1144 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1145 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1146 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1147 ("Test", ["sqroot-test","univariate","equation","test"],
1148 ["Test","squ-equ-test-subpbl1"]))];
1151 autoCalculate 1 CompleteCalcHead;
1152 autoCalculate 1 (Step 1);
1153 autoCalculate 1 (Step 1);
1154 appendFormula 1 "x - 1 = 0";
1155 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1156 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1159 val ((pt,_),_) = get_calc 1;
1160 val p = get_pos 1 1;
1161 val (Form f, tac, asms) = pt_extract (pt, p);
1162 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1163 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1166 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1167 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1168 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1169 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1170 ("Test", ["sqroot-test","univariate","equation","test"],
1171 ["Test","squ-equ-test-subpbl1"]))];
1174 autoCalculate 1 CompleteCalcHead;
1175 autoCalculate 1 (Step 1);
1176 autoCalculate 1 (Step 1);
1177 appendFormula 1 "x = 1";
1178 (*... returns calcChangedEvent with*)
1179 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1180 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1183 val ((pt,_),_) = get_calc 1;
1184 val p = get_pos 1 1;
1185 val (Form f, tac, asms) = pt_extract (pt, p);
1186 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1187 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1190 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1191 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1192 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1193 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1194 ("Test", ["sqroot-test","univariate","equation","test"],
1195 ["Test","squ-equ-test-subpbl1"]))];
1198 autoCalculate 1 CompleteCalcHead;
1199 autoCalculate 1 (Step 1);
1200 autoCalculate 1 (Step 1);
1201 appendFormula 1 "x - 4711 = 0";
1202 (*... returns <ERROR> no derivation found </ERROR>*)
1204 val ((pt,_),_) = get_calc 1;
1205 val p = get_pos 1 1;
1206 val (Form f, tac, asms) = pt_extract (pt, p);
1207 if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
1208 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1211 "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1212 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1213 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1214 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1215 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1216 ("Test", ["sqroot-test","univariate","equation","test"],
1217 ["Test","squ-equ-test-subpbl1"]))];
1220 autoCalculate 1 CompleteCalc;
1221 moveActiveFormula 1 ([2],Res);
1222 replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1223 (*... returns <ERROR> formula not changed </ERROR>*)
1225 val ((pt,_),_) = get_calc 1;
1226 val p = get_pos 1 1;
1227 val (Form f, tac, asms) = pt_extract (pt, p);
1228 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1229 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1230 if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1231 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1232 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1233 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1235 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1236 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1237 ("Test", ["sqroot-test","univariate","equation","test"],
1238 ["Test","squ-equ-test-subpbl1"]))];
1241 autoCalculate 2 CompleteCalc;
1242 moveActiveFormula 2 ([2],Res);
1243 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1244 (*... returns <ERROR> formula not changed </ERROR>*)
1246 val ((pt,_),_) = get_calc 2;
1247 val p = get_pos 2 1;
1248 val (Form f, tac, asms) = pt_extract (pt, p);
1249 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1250 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1251 if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1252 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1253 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1254 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1257 "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1258 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1259 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1260 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1261 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1262 ("Test", ["sqroot-test","univariate","equation","test"],
1263 ["Test","squ-equ-test-subpbl1"]))];
1266 autoCalculate 1 CompleteCalc;
1267 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1268 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1269 (*... returns calcChangedEvent with*)
1270 val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1271 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1273 val ((pt,_),_) = get_calc 1;
1275 val p = get_pos 1 1;
1276 val (Form f, tac, asms) = pt_extract (pt, p);
1277 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1278 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1279 (* for getting the list in whole length ...
1280 print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
1282 if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1283 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1284 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1285 ([2, 8], Res), ([2, 9], Res), ([2], Res)
1286 (*WN060727 {cutlevup->test_trans} removed: ,
1287 ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
1288 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1291 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1292 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1293 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1294 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1295 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1296 ("Test", ["sqroot-test","univariate","equation","test"],
1297 ["Test","squ-equ-test-subpbl1"]))];
1300 autoCalculate 1 CompleteCalc;
1301 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1302 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1303 (*... returns calcChangedEvent with ...*)
1304 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1305 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1308 val ((pt,_),_) = get_calc 1;
1309 show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
1310 val (t,_) = get_obj g_result pt [3,2]; term2str t;
1311 if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1312 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1313 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1314 ([3,2],Res)] then () else
1315 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1317 val p = get_pos 1 1;
1318 val (Form f, tac, asms) = pt_extract (pt, p);
1319 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1320 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1323 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1324 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1325 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1326 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1327 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1328 ("Test", ["sqroot-test","univariate","equation","test"],
1329 ["Test","squ-equ-test-subpbl1"]))];
1332 autoCalculate 1 CompleteCalc;
1333 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1334 replaceFormula 1 "x - 4711 = 0";
1335 (*... returns <ERROR> no derivation found </ERROR>*)
1337 val ((pt,_),_) = get_calc 1;
1339 val p = get_pos 1 1;
1340 val (Form f, tac, asms) = pt_extract (pt, p);
1341 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1342 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1345 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1346 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1347 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1350 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1351 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1354 autoCalculate 1 CompleteCalcHead;
1355 autoCalculate 1 (Step 1);
1356 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1357 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)"; (*<<<<<<<=========================*)
1358 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1359 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1360 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1361 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1362 val ((pt,pos), _) = get_calc 1;
1363 val p = get_pos 1 1;
1364 val (Form f, _, asms) = pt_extract (pt, p);
1366 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1367 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1368 then () else error "embed fun get_fillform changed 1";
1370 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1371 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1372 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1373 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1374 val ((pt,pos),_) = get_calc 1;
1375 val p = get_pos 1 1;
1377 val (Form f, _, asms) = pt_extract (pt, p);
1378 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1379 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1381 else error "embed fun get_fillform changed 2";
1383 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1384 and the last has no gaps, then the number of fill-patterns would suffice
1385 for the DialogGuide to select appropriately. *)
1386 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1387 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1388 val ((pt,pos),_) = get_calc 1;
1389 val p = get_pos 1 1;
1390 val (Form f, _, asms) = pt_extract (pt, p);
1391 if p = ([1], Res) andalso existpt [2] pt andalso
1392 term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1393 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
1394 then () else error "embed fun get_fillform changed 3";
1396 inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
1397 val ((pt, _),_) = get_calc 1;
1398 val p = get_pos 1 1;
1399 val (Form f, _, asms) = pt_extract (pt, p);
1400 if p = ([2], Res) andalso
1401 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1402 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
1403 then () else error "inputFillFormula changed 11";
1405 autoCalculate 1 CompleteCalc;
1407 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1408 val ((pt, _),_) = get_calc 1;
1409 val p = get_pos 1 1;
1410 val (Form f, _, asms) = pt_extract (pt, p);
1411 if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
1412 then () else error "inputFillFormula changed 12";
1415 (([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
1416 (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
1417 (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
1418 (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*)
1419 (([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1420 (([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1421 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
1422 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
1423 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1425 "--------- UC errpat add-fraction, fillpat by input --------------";
1426 "--------- UC errpat add-fraction, fillpat by input --------------";
1427 "--------- UC errpat add-fraction, fillpat by input --------------";
1428 (*cp from BridgeLog Java <=> SML*)
1430 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1433 moveActiveFormula 1 ([],Pbl);
1434 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1435 autoCalculate 1 CompleteCalcHead;
1436 autoCalculate 1 (Step 1);
1437 appendFormula 1 "8 * x / (8 * y)";
1438 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1439 --- but in BridgeLog Java <=> SML:
1440 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1442 "--------- UC errpat, fillpat step to Rewrite --------------------";
1443 "--------- UC errpat, fillpat step to Rewrite --------------------";
1444 "--------- UC errpat, fillpat step to Rewrite --------------------";
1448 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1449 "differentiateFor x", "derivative f_f'"],
1450 ("Isac", ["derivative_of","function"],
1451 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1454 autoCalculate 1 CompleteCalc;
1455 val ((pt,p),_) = get_calc 1; show_pt pt;
1457 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1458 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1459 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1462 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1463 "differentiateFor x", "derivative f_f'"],
1464 ("Isac", ["derivative_of","function"],
1465 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1468 autoCalculate 1 CompleteCalcHead;
1469 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1470 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1473 <CALCID> 1 </CALCID>
1474 <TACTICERRORPATTERNS>
1476 <STRING> chain-rule-diff-both </STRING>
1477 <STRING> cancel </STRING>
1479 <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1480 <RULESET> norm_diff </RULESET>
1495 </REWRITESETINSTTACTIC>
1496 </TACTICERRORPATTERNS>
1500 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1501 stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1502 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1503 (* then --- UC errpat, fillpat by input ---*)
1505 autoCalculate 1 CompleteCalc;
1506 val ((pt,p),_) = get_calc 1; show_pt pt;
1507 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)