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).
11 theory Test_Some imports Build_Thydata begin
12 ML {* KEStore_Elems.set_ref_thy @{theory};
13 fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*) *}
14 ML_file "Frontend/use-cases.sml"
17 "--------------------------------------------------------";
18 "table of contents --------------------------------------";
19 "--------------------------------------------------------";
20 "within struct ------------------------------------------";
21 "--------------------------------------------------------";
22 "--------- encode ^ -> ^^^ ------------------------------";
23 "--------------------------------------------------------";
24 "exported from struct -----------------------------------";
25 "--------------------------------------------------------";
26 "--------- empty rootpbl --------------------------------";
27 "--------- solve_linear as rootpbl FE -------------------";
28 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
29 "--------- miniscript with mini-subpbl ------------------";
30 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
31 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
32 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
33 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
34 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
35 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
36 "--------- setContext..Thy ------------------------------";
37 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
38 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
39 "--------- tryMatchProblem, tryRefineProblem ------------";
40 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
41 "--------- maximum-example, UC: Modeling an example -----";
42 "--------- solve_linear from pbl-hierarchy --------------";
43 "--------- solve_linear as in an algebra system (CAS)----";
44 "--------- interSteps: on 'miniscript with mini-subpbl' -";
45 "--------- getTactic, fetchApplicableTactics ------------";
46 "--------- getAssumptions, getAccumulatedAsms -----------";
47 "--------- arbitrary combinations of steps --------------";
48 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
49 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
50 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
51 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
52 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
53 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
54 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
55 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
56 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
57 "--------- UC errpat add-fraction, fillpat by input --------------";
58 "--------- UC errpat, fillpat step to Rewrite --------------------";
59 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
60 "--------------------------------------------------------";
62 "within struct ---------------------------------------------------";
63 "within struct ---------------------------------------------------";
64 "within struct ---------------------------------------------------";
65 (*==================================================================
68 "--------- encode ^ -> ^^^ ------------------------------";
69 "--------- encode ^ -> ^^^ ------------------------------";
70 "--------- encode ^ -> ^^^ ------------------------------";
71 if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
72 else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
74 if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
75 else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
77 ==================================================================*)
78 "exported from struct --------------------------------------------";
79 "exported from struct --------------------------------------------";
80 "exported from struct --------------------------------------------";
83 (*------------ set at startup of the Kernel ----------------------*)
84 reset_states (); (*resets all state information in Kernel *)
85 (*----------------------------------------------------------------*)
87 "--------- empty rootpbl --------------------------------";
88 "--------- empty rootpbl --------------------------------";
89 "--------- empty rootpbl --------------------------------";
90 CalcTree [([], ("", [], []))];
93 refFormula 1 (get_pos 1 1);
94 (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
97 "--------- solve_linear as rootpbl FE -------------------";
98 "--------- solve_linear as rootpbl FE -------------------";
99 "--------- solve_linear as rootpbl FE -------------------";
100 CalcTree (*start of calculation, return No.1*)
101 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
103 ["LINEAR","univariate","equation","test"],
104 ["Test","solve_linear"]))];
105 Iterator 1; (*create an active Iterator on CalcTree No.1*)
107 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
108 refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
111 fetchProposedTactic 1 (*by using Iterator No.1*);
112 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
113 autoCalculate 1 (Step 1);
114 refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
115 autoCalculate 1 (Step 1);
116 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
117 fetchProposedTactic 1;
118 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
119 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
121 fetchProposedTactic 1;
122 setNextTactic 1 (Add_Given "solveFor x");
123 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
125 fetchProposedTactic 1;
126 setNextTactic 1 (Add_Find "solutions L");
127 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
129 fetchProposedTactic 1;
130 setNextTactic 1 (Specify_Theory "Test");
131 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
132 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
134 fetchProposedTactic 1;
135 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
136 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
137 (*-------------------------------------------------------------------------*)
138 fetchProposedTactic 1;
139 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
141 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
142 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
144 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
145 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
147 (*-------------------------------------------------------------------------*)
148 fetchProposedTactic 1;
149 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
151 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
152 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
153 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
155 is_complete_spec ptp;
157 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
158 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
159 (*term2str (get_obj g_form pt [1]);*)
160 (*-------------------------------------------------------------------------*)
162 fetchProposedTactic 1;
163 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
164 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
166 fetchProposedTactic 1;
167 setNextTactic 1 (Rewrite_Set "Test_simplify");
168 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
170 fetchProposedTactic 1;
171 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
172 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
174 val ((pt,_),_) = get_calc 1;
175 val ip = get_pos 1 1;
176 val (Form f, tac, asms) = pt_extract (pt, ip);
177 (*exception just above means: 'ModSpec' has been returned: error anyway*)
178 if term2str f = "[x = 1]" then () else
179 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
181 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
182 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
183 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
184 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
186 refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
188 refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
190 refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
191 (*getAssumption 1 ([1],Res); TODO.WN041217*)
192 moveActiveDown 1 ; refFormula 1 ([2],Res);
193 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
197 if get_pos 1 1 = ([2], Res) then () else
198 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
199 moveActiveDown 1; refFormula 1 ([], Res);
200 if get_pos 1 1 = ([], Res) then () else
201 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
202 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
205 "--------- miniscript with mini-subpbl ------------------";
206 "--------- miniscript with mini-subpbl ------------------";
207 "--------- miniscript with mini-subpbl ------------------";
208 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
209 "=== this sequence of fun-calls resembles fun me ===";
210 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
211 ("Test", ["sqroot-test","univariate","equation","test"],
212 ["Test","squ-equ-test-subpbl1"]))];
216 refFormula 1 (get_pos 1 1);
217 fetchProposedTactic 1;
218 setNextTactic 1 (Model_Problem);
219 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
221 fetchProposedTactic 1;
222 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
223 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
225 fetchProposedTactic 1;
226 setNextTactic 1 (Add_Given "solveFor x");
227 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
229 fetchProposedTactic 1;
230 setNextTactic 1 (Add_Find "solutions L");
231 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
233 fetchProposedTactic 1;
234 setNextTactic 1 (Specify_Theory "Test");
235 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
237 fetchProposedTactic 1;
238 setNextTactic 1 (Specify_Problem
239 ["sqroot-test","univariate","equation","test"]);
240 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
241 "1-----------------------------------------------------------------";
243 fetchProposedTactic 1;
244 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
245 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
247 fetchProposedTactic 1;
248 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
249 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
251 fetchProposedTactic 1;
252 setNextTactic 1 (Rewrite_Set "norm_equation");
253 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
255 fetchProposedTactic 1;
256 setNextTactic 1 (Rewrite_Set "Test_simplify");
257 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
259 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
260 setNextTactic 1 (Subproblem ("Test",
261 ["LINEAR","univariate","equation","test"]));
262 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
264 fetchProposedTactic 1;
265 setNextTactic 1 (Model_Problem );
266 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
268 fetchProposedTactic 1;
269 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
270 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
272 fetchProposedTactic 1;
273 setNextTactic 1 (Add_Given "solveFor x");
274 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
276 fetchProposedTactic 1;
277 setNextTactic 1 (Add_Find "solutions x_i");
278 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
280 fetchProposedTactic 1;
281 setNextTactic 1 (Specify_Theory "Test");
282 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
284 fetchProposedTactic 1;
285 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
286 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
287 "2-----------------------------------------------------------------";
289 fetchProposedTactic 1;
290 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
291 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
293 fetchProposedTactic 1;
294 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
295 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
297 fetchProposedTactic 1;
298 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
299 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
301 fetchProposedTactic 1;
302 setNextTactic 1 (Rewrite_Set "Test_simplify");
303 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
305 fetchProposedTactic 1;
306 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
307 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
309 fetchProposedTactic 1;
310 setNextTactic 1 (Check_elementwise "Assumptions");
311 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
313 val xml = fetchProposedTactic 1;
314 setNextTactic 1 (Check_Postcond
315 ["sqroot-test","univariate","equation","test"]);
316 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
318 val ((pt,_),_) = get_calc 1;
319 val str = pr_ptree pr_short pt;
321 val ip = get_pos 1 1;
322 val (Form f, tac, asms) = pt_extract (pt, ip);
323 (*exception just above means: 'ModSpec' has been returned: error anyway*)
324 if term2str f = "[x = 1]" then () else
325 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
328 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
329 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
330 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
331 (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
332 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
333 ("Test", ["sqroot-test","univariate","equation","test"],
334 ["Test","squ-equ-test-subpbl1"]))];
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 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 (*here the solve-phase starts*)
346 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
347 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
348 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
349 (*------------------------------------*)
350 (* default_print_depth 13; get_calc 1;
352 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
353 (*calc-head of subproblem*)
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 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 (*solve-phase of the subproblem*)
362 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
363 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
364 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
365 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
366 (*finish subproblem*)
367 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
369 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
371 (*this checks the test for correctness..*)
372 val ((pt,_),_) = get_calc 1;
374 val (Form f, tac, asms) = pt_extract (pt, p);
375 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
376 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
380 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
381 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
382 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
383 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
385 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
387 ["LINEAR","univariate","equation","test"],
388 ["Test","solve_linear"]))];
391 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
393 autoCalculate 1 CompleteCalc;
394 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
395 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
397 val ((pt,_),_) = get_calc 1;
399 val (Form f, tac, asms) = pt_extract (pt, p);
400 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
401 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
404 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
405 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
406 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
407 (* ERROR: error in kernel ?? *)
409 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
411 ["LINEAR","univariate","equation","test"],
412 ["Test","solve_linear"]))];
416 autoCalculate 1 CompleteCalcHead;
417 refFormula 1 (get_pos 1 1);
418 val ((pt,p),_) = get_calc 1;
420 autoCalculate 1 CompleteCalc;
421 val ((pt,p),_) = get_calc 1;
422 if p=([], Res) then () else
423 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
426 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
427 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
428 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
429 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
430 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
431 ("Test", ["sqroot-test","univariate","equation","test"],
432 ["Test","squ-equ-test-subpbl1"]))];
435 autoCalculate 1 CompleteCalc;
436 val ((pt,p),_) = get_calc 1; show_pt pt;
438 getTactic 1 ([1],Frm);
439 getTactic 1 ([1],Res);
440 initContext 1 Thy_ ([1],Res);
442 (*... returns calcChangedEvent with*)
443 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
444 getFormulaeFromTo 1 unc gen 0 (*only result*) false;
445 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
446 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
448 val ((pt,_),_) = get_calc 1;
450 val (Form f, tac, asms) = pt_extract (pt, p);
451 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
452 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
455 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
456 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
457 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
458 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
459 ("Test", ["sqroot-test","univariate","equation","test"],
460 ["Test","squ-equ-test-subpbl1"]))];
463 autoCalculate 1 CompleteCalcHead;
465 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
466 cell = NONE, ctxt = ctxt2, meth,
467 spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
468 ["Test", "squ-equ-test-subpbl1"]),
469 probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
470 ([], Met)), []) = get_calc 1;
471 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
472 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
475 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
476 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
477 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
479 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
481 ["LINEAR","univariate","equation","test"],
482 ["Test","solve_linear"]))];
485 autoCalculate 1 CompleteModel;
486 refFormula 1 (get_pos 1 1);
488 setProblem 1 ["LINEAR","univariate","equation","test"];
489 val pos = get_pos 1 1;
490 setContext 1 pos (kestoreID2guh Pbl_["LINEAR","univariate","equation","test"]);
491 refFormula 1 (get_pos 1 1);
493 setMethod 1 ["Test","solve_linear"];
494 setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
495 refFormula 1 (get_pos 1 1);
496 val ((pt,_),_) = get_calc 1;
497 if get_obj g_spec pt [] = ("e_domID",
498 ["LINEAR", "univariate","equation","test"],
499 ["Test","solve_linear"]) then ()
500 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
502 autoCalculate 1 CompleteCalcHead;
503 refFormula 1 (get_pos 1 1);
504 autoCalculate 1 CompleteCalc;
508 refFormula 1 (get_pos 1 1);
509 val ((pt,_),_) = get_calc 1;
511 val (Form f, tac, asms) = pt_extract (pt, p);
512 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
513 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
516 "--------- setContext..Thy ------------------------------";
517 "--------- setContext..Thy ------------------------------";
518 "--------- setContext..Thy ------------------------------";
519 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
520 ("Test", ["sqroot-test","univariate","equation","test"],
521 ["Test","squ-equ-test-subpbl1"]))];
522 Iterator 1; moveActiveRoot 1;
523 autoCalculate 1 CompleteCalcHead;
524 autoCalculate 1 (Step 1);
525 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
527 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
528 autoCalculate 1 (Step 1);
529 val ((pt,p),_) = get_calc 1; show_pt pt;
531 "-----^^^^^ and vvvvv do the same -----";
532 setContext 1 p "thy_isac_Test-rls-Test_simplify";
533 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
535 autoCalculate 1 (Step 1);
536 setContext 1 p "thy_isac_Test-rls-Test_simplify";
537 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
538 val (Form f, tac, asms) = pt_extract (pt, p);
539 if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
540 then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1";
542 autoCalculate 1 CompleteCalc;
543 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
544 val (Form f, tac, asms) = pt_extract (pt, p);
546 if term2str f = "[x = 1]" andalso p = ([], Res) then ()
547 else error "--- setContext..Thy --- autoCalculate CompleteCalc";
550 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
551 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
552 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
553 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
554 ("Test", ["sqroot-test","univariate","equation","test"],
555 ["Test","squ-equ-test-subpbl1"]))];
556 Iterator 1; moveActiveRoot 1;
557 autoCalculate 1 CompleteToSubpbl;
558 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
559 val ((pt,_),_) = get_calc 1;
560 val str = pr_ptree pr_short pt;
562 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
564 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
566 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
567 autoCalculate 1 CompleteToSubpbl;
568 val ((pt,_),_) = get_calc 1;
569 val str = pr_ptree pr_short pt;
571 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
572 val ((pt,_),_) = get_calc 1;
575 val (Form f, tac, asms) = pt_extract (pt, p);
576 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
577 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
580 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
581 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
582 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
584 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
585 ("RatEq", ["univariate","equation"], ["no_met"]))];
588 fetchProposedTactic 1;
590 setNextTactic 1 (Model_Problem);
591 autoCalculate 1 (Step 1); fetchProposedTactic 1;
593 setNextTactic 1 (Specify_Theory "RatEq");
594 autoCalculate 1 (Step 1); fetchProposedTactic 1;
595 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
596 autoCalculate 1 (Step 1); fetchProposedTactic 1;
597 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
598 autoCalculate 1 (Step 1); fetchProposedTactic 1;
599 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
600 autoCalculate 1 (Step 1); fetchProposedTactic 1;
601 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
602 autoCalculate 1 (Step 1); fetchProposedTactic 1;
603 setNextTactic 1 (Rewrite_Set "norm_Rational");
604 autoCalculate 1 (Step 1); fetchProposedTactic 1;
605 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
606 autoCalculate 1 (Step 1); fetchProposedTactic 1;
607 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
608 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
609 "univariate","equation"]));
610 autoCalculate 1 (Step 1); fetchProposedTactic 1;
611 setNextTactic 1 (Model_Problem );
612 autoCalculate 1 (Step 1); fetchProposedTactic 1;
613 setNextTactic 1 (Specify_Theory "PolyEq");
614 autoCalculate 1 (Step 1); fetchProposedTactic 1;
615 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
616 "univariate","equation"]);
617 autoCalculate 1 (Step 1); fetchProposedTactic 1;
618 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
619 autoCalculate 1 (Step 1); fetchProposedTactic 1;
620 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
621 autoCalculate 1 (Step 1); fetchProposedTactic 1;
622 setNextTactic 1 (Rewrite ("all_left", @{thm all_left}));
623 autoCalculate 1 (Step 1); fetchProposedTactic 1;
624 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
625 autoCalculate 1 (Step 1); fetchProposedTactic 1;
626 (* __________ for "16 + 12 * x = 0"*)
627 setNextTactic 1 (Subproblem ("PolyEq",
628 ["degree_1","polynomial","univariate","equation"]));
629 autoCalculate 1 (Step 1); fetchProposedTactic 1;
630 setNextTactic 1 (Model_Problem );
631 autoCalculate 1 (Step 1); fetchProposedTactic 1;
632 setNextTactic 1 (Specify_Theory "PolyEq");
633 (*------------- some trials in the problem-hierarchy ---------------*)
634 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
635 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
636 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
637 (*------------------------------------------------------------------*)
638 autoCalculate 1 (Step 1); fetchProposedTactic 1;
639 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
640 autoCalculate 1 (Step 1); fetchProposedTactic 1;
641 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
642 autoCalculate 1 (Step 1); fetchProposedTactic 1;
643 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
644 autoCalculate 1 (Step 1); fetchProposedTactic 1;
645 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
646 autoCalculate 1 (Step 1); fetchProposedTactic 1;
647 setNextTactic 1 Or_to_List;
648 autoCalculate 1 (Step 1); fetchProposedTactic 1;
649 setNextTactic 1 (Check_elementwise "Assumptions");
650 autoCalculate 1 (Step 1); fetchProposedTactic 1;
651 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
652 "univariate","equation"]);
653 autoCalculate 1 (Step 1); fetchProposedTactic 1;
654 setNextTactic 1 (Check_Postcond ["normalize","polynomial",
655 "univariate","equation"]);
656 autoCalculate 1 (Step 1); fetchProposedTactic 1;
657 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
658 val (ptp,_) = get_calc 1;
659 val (Form t,_,_) = pt_extract ptp;
660 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
661 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
664 "--------- tryMatchProblem, tryRefineProblem ------------";
665 "--------- tryMatchProblem, tryRefineProblem ------------";
666 "--------- tryMatchProblem, tryRefineProblem ------------";
667 (*{\bf\UC{Having \isac{} Refine the Problem
668 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
669 * x^^^2 + 4*x + 5 = 2
670 see isac.bridge.TestSpecify#testMatchRefine*)
672 [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
674 ["univariate","equation"],
679 fetchProposedTactic 1;
680 setNextTactic 1 (Model_Problem );
681 (*..this tactic should be done 'tacitly', too !*)
684 autoCalculate 1 CompleteCalcHead;
685 checkContext 1 ([],Pbl) "pbl_equ_univ";
686 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
689 autoCalculate 1 (Step 1);
691 fetchProposedTactic 1;
692 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
693 autoCalculate 1 (Step 1);
695 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
696 initContext 1 Pbl_ ([],Pbl);
697 (* this would break if a calculation would be inserted before: CALCID...
698 and pattern matching is not available in *.java.
699 if cut_xml xml = "(CONTEXTPBL)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (CONTEXTDATA)\n. . (GUH)\n. . . pbl_equ_univ\n. . (/GUH)\n. . (STATUS)\n. . . correct\n. . (/STATUS)\n. . (HEAD)\n. . . (MATHML)\n. . . . (ISA)\n. . . . . solve (x ^ 2 + 4 * x + 5 = 2, x)\n. . . . (/ISA)\n. . . (/MATHML)\n. . (/HEAD)\n. . (MODEL)\n. . . (GIVEN)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . equality (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solveFor x\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/GIVEN)\n. . . (WHERE)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . matches (?a = ?b) (x ^ 2 + 4 * x + 5 = 2)\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/WHERE)\n. . . (FIND)\n. . . . (ITEM status=correct)\n. . . . . (MATHML)\n. . . . . . (ISA)\n. . . . . . . solutions L\n. . . . . . (/ISA)\n. . . . . (/MATHML)\n. . . . (/ITEM)\n. . . (/FI"
700 then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Pbl_ ([],Pbl); CHANGED";
702 initContext 1 Met_ ([],Pbl);
703 (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
705 "--------- this match will show some incomplete items: ---------";
707 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
708 checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
711 fetchProposedTactic 1;
712 setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
714 fetchProposedTactic 1;
715 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
717 "--------- this is a matching model (all items correct): -------";
718 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
719 "--------- this is a NOT matching model (some 'false': ---------";
720 checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["LINEAR","univariate","equation"]);
722 "--------- find out a matching problem: ------------------------";
723 "--------- find out a matching problem (FAILING: no new pbl) ---";
724 refineProblem 1([],Pbl)(pblID2guh ["LINEAR","univariate","equation"]);
726 "--------- find out a matching problem (SUCCESSFUL) ------------";
727 refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
729 "--------- tryMatch, tryRefine did not change the calculation -";
730 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
731 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
732 "univariate","equation"]);
733 autoCalculate 1 (Step 1);
734 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
735 and Specify_Theory skipped in comparison to below ---^^^-inserted *)
736 (*------------vvv-inserted-----------------------------------------------*)
737 fetchProposedTactic 1;
738 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
739 "univariate","equation"]);
740 autoCalculate 1 (Step 1);
742 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
744 fetchProposedTactic 1;
745 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
746 autoCalculate 1 (Step 1);
748 fetchProposedTactic 1;
749 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
751 autoCalculate 1 CompleteCalc;
753 val ((pt,_),_) = get_calc 1;
756 val (Form f, tac, asms) = pt_extract (pt, p);
757 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
758 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
760 (*------------^^^-inserted-----------------------------------------------*)
761 (*WN050904 the fetchProposedTactic's below may not have worked like that
762 before, too, because there was no check*)
763 fetchProposedTactic 1;
764 setNextTactic 1 (Specify_Theory "PolyEq");
765 autoCalculate 1 (Step 1);
767 fetchProposedTactic 1;
768 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
769 autoCalculate 1 (Step 1);
771 fetchProposedTactic 1;
772 "--------- now the calc-header is ready for enter 'solving' ----";
773 autoCalculate 1 CompleteCalc;
775 val ((pt,_),_) = get_calc 1;
779 val (Form f, tac, asms) = pt_extract (pt, p);
780 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
781 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
784 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
785 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
786 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
787 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
788 ("Test", ["sqroot-test","univariate","equation","test"],
789 ["Test","squ-equ-test-subpbl1"]))];
793 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
794 "solve (x+1=2, x)",(*the headline*)
795 [Given ["equality (x+1=(2::real))", "solveFor x"],
796 Find ["solutions L"](*,Relate []*)],
799 ["sqroot-test","univariate","equation","test"],
800 ["Test","squ-equ-test-subpbl1"]));
802 val ((Nd (PblObj {env = NONE,
804 loc = (SOME scrst_ctxt, NONE),
809 ["sqroot-test", "univariate", "equation", "test"],
810 ["Test", "squ-equ-test-subpbl1"]),
812 branch = TransitiveB,
819 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
820 if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
821 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
827 val ((Nd (PblObj {env = NONE,
829 loc = (SOME scrst_ctxt, NONE),
833 spec = ("e_domID", ["e_pblID"], ["e_metID"]),
835 branch = TransitiveB,
842 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
843 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
845 "--------- maximum-example, UC: Modeling an example -----";
846 "--------- maximum-example, UC: Modeling an example -----";
847 "--------- maximum-example, UC: Modeling an example -----";
848 (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
849 see isac.bridge.TestModel#testEditItems
851 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
852 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
853 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
854 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
855 (*^^^ these are the elements for the root-problem (in variants)*)
856 (*vvv these are elements required for subproblems*)
857 "boundVariable a","boundVariable b","boundVariable alpha",
858 "interval {x::real. 0 <= x & x <= 2*r}",
859 "interval {x::real. 0 <= x & x <= 2*r}",
860 "interval {x::real. 0 <= x & x <= pi}",
861 "errorBound (eps=(0::real))"]
862 (*specifying is not interesting for this example*)
863 val spec = ("DiffApp", ["maximum_of","function"],
864 ["DiffApp","max_by_calculus"]);
865 (*the empty model with descriptions for user-guidance by Model_Problem*)
866 val empty_model = [Given ["fixedValues []"],
867 Find ["maximum", "valuesFor"],
868 Relate ["relations []"]];
871 "#################################################################";
873 CalcTree [(elems, spec)];
876 refFormula 1 (get_pos 1 1);
877 (*this gives a completely empty model*)
879 fetchProposedTactic 1;
880 (*fill the CalcHead with Descriptions...*)
881 setNextTactic 1 (Model_Problem );
882 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
884 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
885 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
886 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
887 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
888 "Problem (DiffApp.thy, [maximum_of, function])",
889 (*the head-form ^^^ is not used for input here*)
890 [Given ["fixedValues [r=Arbfix]"(*new input*)],
891 Find ["maximum b"(*new input*), "valuesFor"],
892 Relate ["relations"]],
893 (*input (Arbfix will dissappear soon)*)
895 e_spec (*no input to the specification*));
897 (*the user does not know, what 'superfluous' for 'maximum b' may mean
898 and asks what to do next*)
899 fetchProposedTactic 1;
900 (*the student follows the advice*)
901 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
902 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
904 (*this input completes the model*)
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, e_spec);
911 (*specification is not interesting and should be skipped by the dialogguide;
912 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
913 modifyCalcHead 1 (([],Pbl), "not used here",
914 [Given ["fixedValues [r=Arbfix]"],
915 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
916 Relate ["relations [A=a*b, \
917 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
918 ("DiffApp", ["e_pblID"], ["e_metID"]));
919 modifyCalcHead 1 (([],Pbl), "not used here",
920 [Given ["fixedValues [r=Arbfix]"],
921 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
922 Relate ["relations [A=a*b, \
923 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
924 ("DiffApp", ["maximum_of","function"],
926 modifyCalcHead 1 (([],Pbl), "not used here",
927 [Given ["fixedValues [r=Arbfix]"],
928 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
929 Relate ["relations [A=a*b, \
930 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
931 ("DiffApp", ["maximum_of","function"],
932 ["DiffApp","max_by_calculus"]));
933 (*this final calcHead now has STATUS 'complete' !*)
936 "--------- solve_linear from pbl-hierarchy --------------";
937 "--------- solve_linear from pbl-hierarchy --------------";
938 "--------- solve_linear from pbl-hierarchy --------------";
939 val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], []));
940 CalcTree [(fmz, sp)];
941 Iterator 1; moveActiveRoot 1;
942 refFormula 1 (get_pos 1 1);
943 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
944 [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
945 Find ["solutions L"]],
947 ("Test", ["LINEAR","univariate","equation","test"],
948 ["Test","solve_linear"]));
949 autoCalculate 1 CompleteCalc;
950 refFormula 1 (get_pos 1 1);
951 val ((pt,_),_) = get_calc 1;
953 val (Form f, tac, asms) = pt_extract (pt, p);
954 if term2str f = "[x = 1]" andalso p = ([], Res)
955 andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
956 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
959 "--------- solve_linear as in an algebra system (CAS)----";
960 "--------- solve_linear as in an algebra system (CAS)----";
961 "--------- solve_linear as in an algebra system (CAS)----";
962 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
963 val (fmz, sp) = ([], ("", [], []));
964 CalcTree [(fmz, sp)];
965 Iterator 1; moveActiveRoot 1;
966 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
967 autoCalculate 1 CompleteCalc;
968 refFormula 1 (get_pos 1 1);
969 val ((pt,_),_) = get_calc 1;
971 val (Form f, tac, asms) = pt_extract (pt, p);
972 if term2str f = "[x = 1]" andalso p = ([], Res)
973 andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
974 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
977 "--------- interSteps: on 'miniscript with mini-subpbl' -";
978 "--------- interSteps: on 'miniscript with mini-subpbl' -";
979 "--------- interSteps: on 'miniscript with mini-subpbl' -";
980 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
981 ("Test", ["sqroot-test","univariate","equation","test"],
982 ["Test","squ-equ-test-subpbl1"]))];
985 autoCalculate 1 CompleteCalc;
986 val ((pt,_),_) = get_calc 1;
989 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
990 interSteps 1 ([2],Res);
991 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
992 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
993 getFormulaeFromTo 1 unc gen 1 false;
995 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
996 interSteps 1 ([3,2],Res);
997 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
998 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
999 getFormulaeFromTo 1 unc gen 1 false;
1001 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1002 interSteps 1 ([3],Res) (*no new steps in subproblems*);
1003 val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1004 getFormulaeFromTo 1 unc gen 1 false;
1006 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1007 interSteps 1 ([],Res) (*no new steps in subproblems*);
1008 val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1009 getFormulaeFromTo 1 unc gen 1 false;
1012 "--------- getTactic, fetchApplicableTactics ------------";
1013 "--------- getTactic, fetchApplicableTactics ------------";
1014 "--------- getTactic, fetchApplicableTactics ------------";
1015 (* compare test/../script.sml
1016 "----------- fun sel_rules ---------------------------------------";
1018 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1019 ("Test", ["sqroot-test","univariate","equation","test"],
1020 ["Test","squ-equ-test-subpbl1"]))];
1021 Iterator 1; moveActiveRoot 1;
1022 autoCalculate 1 CompleteCalc;
1023 val ((pt,_),_) = get_calc 1;
1026 (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1027 WN120210 not impl. in FE*)
1028 getTactic 1 ([],Pbl);
1029 getTactic 1 ([1],Res);
1030 getTactic 1 ([3],Pbl);
1031 getTactic 1 ([3,1],Frm);
1032 getTactic 1 ([3],Res);
1033 getTactic 1 ([],Res);
1035 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1036 fetchApplicableTactics 1 99999 ([],Pbl);
1037 fetchApplicableTactics 1 99999 ([1],Res);
1038 fetchApplicableTactics 1 99999 ([3],Pbl);
1039 fetchApplicableTactics 1 99999 ([3,1],Res);
1040 fetchApplicableTactics 1 99999 ([3],Res);
1041 fetchApplicableTactics 1 99999 ([],Res);
1044 "--------- getAssumptions, getAccumulatedAsms -----------";
1045 "--------- getAssumptions, getAccumulatedAsms -----------";
1046 "--------- getAssumptions, getAccumulatedAsms -----------";
1048 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1049 "solveFor x","solutions L"],
1050 ("RatEq",["univariate","equation"],["no_met"]))];
1051 Iterator 1; moveActiveRoot 1;
1052 autoCalculate 1 CompleteCalc;
1053 val ((pt,_),_) = get_calc 1;
1054 val p = get_pos 1 1;
1055 val (Form f, tac, asms) = pt_extract (pt, p);
1056 (*============ inhibit exn WN120316 compare 2002--2011 ===========================
1057 if map term2str asms =
1058 ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^
1059 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
1060 "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
1061 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
1062 "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
1063 andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
1064 else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*)
1065 ============ inhibit exn WN120316 compare 2002--2011 ===========================*)
1066 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
1067 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
1068 then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1070 (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1071 getAssumptions 1 ([3], Res);
1072 getAssumptions 1 ([5], Res);
1073 (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1074 WN0502 still without positions*)
1075 getAccumulatedAsms 1 ([3], Res);
1076 getAccumulatedAsms 1 ([5], Res);
1079 "--------- arbitrary combinations of steps --------------";
1080 "--------- arbitrary combinations of steps --------------";
1081 "--------- arbitrary combinations of steps --------------";
1082 CalcTree (*start of calculation, return No.1*)
1083 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1085 ["LINEAR","univariate","equation","test"],
1086 ["Test","solve_linear"]))];
1087 Iterator 1; moveActiveRoot 1;
1089 fetchProposedTactic 1;
1090 (*ERROR get_calc 1 not existent*)
1091 setNextTactic 1 (Model_Problem );
1092 autoCalculate 1 (Step 1);
1093 fetchProposedTactic 1;
1094 fetchProposedTactic 1;
1096 setNextTactic 1 (Add_Find "solutions L");
1097 setNextTactic 1 (Add_Find "solutions L");
1099 autoCalculate 1 (Step 1);
1100 autoCalculate 1 (Step 1);
1102 setNextTactic 1 (Specify_Theory "Test");
1103 fetchProposedTactic 1;
1104 autoCalculate 1 (Step 1);
1106 autoCalculate 1 (Step 1);
1107 autoCalculate 1 (Step 1);
1108 autoCalculate 1 (Step 1);
1109 autoCalculate 1 (Step 1);
1110 (*------------------------- end calc-head*)
1112 fetchProposedTactic 1;
1113 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1114 autoCalculate 1 (Step 1);
1116 setNextTactic 1 (Rewrite_Set "Test_simplify");
1117 fetchProposedTactic 1;
1118 autoCalculate 1 (Step 1);
1120 autoCalculate 1 CompleteCalc;
1121 val ((pt,_),_) = get_calc 1;
1122 val p = get_pos 1 1;
1123 val (Form f, tac, asms) = pt_extract (pt, p);
1124 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1125 error "FE-interface.sml: diff.behav. in combinations of steps";
1128 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1129 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1130 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1131 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1132 ("Test", ["sqroot-test","univariate","equation","test"],
1133 ["Test","squ-equ-test-subpbl1"]))];
1136 autoCalculate 1 CompleteCalcHead;
1137 autoCalculate 1 (Step 1);
1138 autoCalculate 1 (Step 1);
1139 appendFormula 1 "-1 + x = 0" (*|> Future.join*);
1140 (*... returns calcChangedEvent with*)
1141 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1142 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1144 val ((pt,_),_) = get_calc 1;
1145 val p = get_pos 1 1;
1146 val (Form f, tac, asms) = pt_extract (pt, p);
1147 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1148 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1151 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1152 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1153 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1154 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1155 ("Test", ["sqroot-test","univariate","equation","test"],
1156 ["Test","squ-equ-test-subpbl1"]))];
1159 autoCalculate 1 CompleteCalcHead;
1160 autoCalculate 1 (Step 1);
1161 autoCalculate 1 (Step 1);
1162 appendFormula 1 "x - 1 = 0" (*|> Future.join*);
1163 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1164 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1167 val ((pt,_),_) = get_calc 1;
1168 val p = get_pos 1 1;
1169 val (Form f, tac, asms) = pt_extract (pt, p);
1170 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1171 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1174 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1175 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1176 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1177 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1178 ("Test", ["sqroot-test","univariate","equation","test"],
1179 ["Test","squ-equ-test-subpbl1"]))];
1182 autoCalculate 1 CompleteCalcHead;
1183 autoCalculate 1 (Step 1);
1184 autoCalculate 1 (Step 1);
1185 appendFormula 1 "x = 1" (*|> Future.join*);
1186 (*... returns calcChangedEvent with*)
1187 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1188 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1191 val ((pt,_),_) = get_calc 1;
1192 val p = get_pos 1 1;
1193 val (Form f, tac, asms) = pt_extract (pt, p);
1194 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1195 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1198 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1199 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1200 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1201 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1202 ("Test", ["sqroot-test","univariate","equation","test"],
1203 ["Test","squ-equ-test-subpbl1"]))];
1206 autoCalculate 1 CompleteCalcHead;
1207 autoCalculate 1 (Step 1);
1208 autoCalculate 1 (Step 1);
1209 appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
1210 (*... returns <ERROR> no derivation found </ERROR>*)
1212 val ((pt,_),_) = get_calc 1;
1213 val p = get_pos 1 1;
1214 val (Form f, tac, asms) = pt_extract (pt, p);
1215 if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
1216 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1219 "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1220 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1221 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1222 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1223 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1224 ("Test", ["sqroot-test","univariate","equation","test"],
1225 ["Test","squ-equ-test-subpbl1"]))];
1228 autoCalculate 1 CompleteCalc;
1229 moveActiveFormula 1 ([2],Res);
1230 replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1231 (*... returns <ERROR> formula not changed </ERROR>*)
1233 val ((pt,_),_) = get_calc 1;
1234 val p = get_pos 1 1;
1235 val (Form f, tac, asms) = pt_extract (pt, p);
1236 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1237 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1238 if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1239 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1240 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1241 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1243 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1244 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1245 ("Test", ["sqroot-test","univariate","equation","test"],
1246 ["Test","squ-equ-test-subpbl1"]))];
1249 autoCalculate 2 CompleteCalc;
1250 moveActiveFormula 2 ([2],Res);
1251 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1252 (*... returns <ERROR> formula not changed </ERROR>*)
1254 val ((pt,_),_) = get_calc 2;
1255 val p = get_pos 2 1;
1256 val (Form f, tac, asms) = pt_extract (pt, p);
1257 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1258 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1259 if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1260 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1261 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1262 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1265 "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1266 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1267 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1268 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1269 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1270 ("Test", ["sqroot-test","univariate","equation","test"],
1271 ["Test","squ-equ-test-subpbl1"]))];
1274 autoCalculate 1 CompleteCalc;
1275 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1276 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1277 (*... returns calcChangedEvent with*)
1278 val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1279 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1281 val ((pt,_),_) = get_calc 1;
1283 val p = get_pos 1 1;
1284 val (Form f, tac, asms) = pt_extract (pt, p);
1285 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1286 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1287 (* for getting the list in whole length ...
1288 default_print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);default_print_depth 3;
1290 if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1291 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1292 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1293 ([2, 8], Res), ([2, 9], Res), ([2], Res)
1294 (*WN060727 {cutlevup->test_trans} removed: ,
1295 ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
1296 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1299 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1300 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1301 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1302 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1303 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1304 ("Test", ["sqroot-test","univariate","equation","test"],
1305 ["Test","squ-equ-test-subpbl1"]))];
1308 autoCalculate 1 CompleteCalc;
1309 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1310 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1311 (*... returns calcChangedEvent with ...*)
1312 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1313 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1316 val ((pt,_),_) = get_calc 1;
1317 show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
1318 val (t,_) = get_obj g_result pt [3,2]; term2str t;
1319 if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1320 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1321 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1322 ([3,2],Res)] then () else
1323 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1325 val p = get_pos 1 1;
1326 val (Form f, tac, asms) = pt_extract (pt, p);
1327 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1328 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1331 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1332 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1333 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1334 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1335 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1336 ("Test", ["sqroot-test","univariate","equation","test"],
1337 ["Test","squ-equ-test-subpbl1"]))];
1340 autoCalculate 1 CompleteCalc;
1341 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1342 replaceFormula 1 "x - 4711 = 0";
1343 (*... returns <ERROR> no derivation found </ERROR>*)
1345 val ((pt,_),_) = get_calc 1;
1347 val p = get_pos 1 1;
1348 val (Form f, tac, asms) = pt_extract (pt, p);
1349 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1350 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1353 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1354 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1355 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1357 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1358 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1361 autoCalculate 1 CompleteCalcHead;
1362 autoCalculate 1 (Step 1);
1363 autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1364 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1365 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1366 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1367 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1368 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1369 val ((pt,pos), _) = get_calc 1;
1370 val p = get_pos 1 1;
1371 val (Form f, _, asms) = pt_extract (pt, p);
1373 if p = ([2], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
1374 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(bdv, x)"],
1375 ("diff_sum", thm)) => () | _ => error "embed fun get_fillform changed 0"
1376 | _ => error "embed fun get_fillform changed 1"
1377 else error "embed fun get_fillform changed 2";
1378 ============ inhibit exn WN161019 TODO ========================================================*)
1380 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1381 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1382 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1383 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1384 val ((pt,pos),_) = get_calc 1;
1385 val p = get_pos 1 1;
1387 val (Form f, _, asms) = pt_extract (pt, p);
1388 if p = ([1], Res) andalso term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1389 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1391 else error "embed fun get_fillform changed 2";
1393 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1394 and the last has no gaps, then the number of fill-patterns would suffice
1395 for the DialogGuide to select appropriately. *)
1396 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1397 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1398 val ((pt,pos),_) = get_calc 1;
1399 val p = get_pos 1 1;
1400 val (Form f, _, asms) = pt_extract (pt, p);
1401 if p = ([1], Res) andalso existpt [2] pt andalso
1402 term2str f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1403 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sum", "Diff.diff_sum"))
1404 then () else error "embed fun get_fillform changed 3";
1406 inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
1407 val ((pt, _),_) = get_calc 1;
1408 val p = get_pos 1 1;
1409 val (Form f, _, asms) = pt_extract (pt, p);
1410 if p = ([2], Res) andalso
1411 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1412 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", ""))
1413 then () else error "inputFillFormula changed 11";
1415 autoCalculate 1 CompleteCalc;
1417 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1418 val ((pt, _),_) = get_calc 1;
1419 val p = get_pos 1 1;
1420 val (Form f, _, asms) = pt_extract (pt, p);
1421 if p = ([], Res) andalso term2str f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
1422 then () else error "inputFillFormula changed 12";
1425 (([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
1426 (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
1427 (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
1428 (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*)
1429 (([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1430 (([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1431 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
1432 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
1433 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1436 "--------- UC errpat add-fraction, fillpat by input --------------";
1437 "--------- UC errpat add-fraction, fillpat by input --------------";
1438 "--------- UC errpat add-fraction, fillpat by input --------------";
1439 (*cp from BridgeLog Java <=> SML*)
1440 =CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
1443 moveActiveFormula 1 ([],Pbl);
1444 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1445 autoCalculate 1 CompleteCalcHead;
1446 autoCalculate 1 (Step 1);
1447 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
1448 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1449 --- but in BridgeLog Java <=> SML:
1450 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1453 "--------- UC errpat, fillpat step to Rewrite --------------------";
1454 "--------- UC errpat, fillpat step to Rewrite --------------------";
1455 "--------- UC errpat, fillpat step to Rewrite --------------------";
1458 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1459 "differentiateFor x", "derivative f_f'"],
1460 ("Isac", ["derivative_of","function"],
1461 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1464 autoCalculate 1 CompleteCalc;
1465 val ((pt,p),_) = get_calc 1; show_pt pt;
1468 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1469 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1470 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1472 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1473 "differentiateFor x", "derivative f_f'"],
1474 ("Isac", ["derivative_of","function"],
1475 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1478 autoCalculate 1 CompleteCalcHead;
1479 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1480 autoCalculate 1 (Step 1); fetchProposedTactic 1;
1483 <CALCID> 1 </CALCID>
1484 <TACTICERRORPATTERNS>
1486 <STRING> chain-rule-diff-both </STRING>
1487 <STRING> cancel </STRING>
1489 <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1490 <RULESET> norm_diff </RULESET>
1505 </REWRITESETINSTTACTIC>
1506 </TACTICERRORPATTERNS>
1510 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1511 stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1512 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1513 (* then --- UC errpat, fillpat by input ---*)
1515 autoCalculate 1 CompleteCalc;
1516 val ((pt,p),_) = get_calc 1; show_pt pt;
1517 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)