1 (* tests the interface of isac's SML-kernel in accordance to
2 java-tests/isac.bridge.
4 WN050707 ... if true, the test ist marked with a \label referring
5 to the same UC in isac-docu.tex as the JUnit testcase.
6 use"../smltest/FE-interface/interface.sml";
10 "--------------------------------------------------------";
11 "table of contents --------------------------------------";
12 "--------------------------------------------------------";
13 "within struct ------------------------------------------";
14 "--------------------------------------------------------";
15 "--------- encode ^ -> ^^^ ------------------------------";
16 "--------------------------------------------------------";
17 "exported from struct -----------------------------------";
18 "--------------------------------------------------------";
19 "--------- empty rootpbl --------------------------------";
20 "--------- solve_linear as rootpbl FE -------------------";
21 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
22 "--------- miniscript with mini-subpbl ------------------";
23 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
24 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
25 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
26 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
27 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
28 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
29 "--------- setContext..Thy ------------------------------";
30 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
31 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
32 "--------- tryMatchProblem, tryRefineProblem ------------";
33 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
34 "--------- maximum-example, UC: Modeling an example -----";
35 "--------- solve_linear from pbl-hierarchy --------------";
36 "--------- solve_linear as in an algebra system (CAS)----";
37 "--------- interSteps: on 'miniscript with mini-subpbl' -";
38 "--------- getTactic, fetchApplicableTactics ------------";
39 "--------- getAssumptions, getAccumulatedAsms -----------";
40 "--------- arbitrary combinations of steps --------------";
41 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
42 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
43 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
44 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
45 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
46 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
47 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
48 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
49 "--------------------------------------------------------";
51 "within struct ---------------------------------------------------";
52 "within struct ---------------------------------------------------";
53 "within struct ---------------------------------------------------";
54 (*==================================================================
57 "--------- encode ^ -> ^^^ ------------------------------";
58 "--------- encode ^ -> ^^^ ------------------------------";
59 "--------- encode ^ -> ^^^ ------------------------------";
60 if encode "a^2+b^2=c^2" = "a^^^2+b^^^2=c^^^2" then ()
61 else error "interface.sml: diff.behav. in encode ^ -> ^^^ ";
63 if (decode o encode) "a^2+b^2=c^2" = "a^2+b^2=c^2" then ()
64 else error "interface.sml: diff.behav. in de/encode ^ <-> ^^^ ";
66 ==================================================================*)
67 "exported from struct --------------------------------------------";
68 "exported from struct --------------------------------------------";
69 "exported from struct --------------------------------------------";
72 (*------------ set at startup of the Kernel --------------------------*)
73 states:= []; (*resets all state information in Kernel *)
74 (*----------------------------------------------------------------*)
76 "--------- empty rootpbl --------------------------------";
77 "--------- empty rootpbl --------------------------------";
78 "--------- empty rootpbl --------------------------------";
79 CalcTree [([], ("", [], []))];
82 refFormula 1 (get_pos 1 1);
83 (*WN.040222: stoert das sehr, dass e_domID etc. statt leer kommt ???*)
86 "--------- solve_linear as rootpbl FE -------------------";
87 "--------- solve_linear as rootpbl FE -------------------";
88 "--------- solve_linear as rootpbl FE -------------------";
90 CalcTree (*start of calculation, return No.1*)
91 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
93 ["linear","univariate","equation","test"],
94 ["Test","solve_linear"]))];
95 Iterator 1; (*create an active Iterator on CalcTree No.1*)
97 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
98 refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
101 fetchProposedTactic 1 (*by using Iterator No.1*);
102 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
103 autoCalculate 1 (Step 1);
104 refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
105 autoCalculate 1 (Step 1);
106 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
107 fetchProposedTactic 1;
108 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
109 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1); (*equality added*);
111 fetchProposedTactic 1;
112 setNextTactic 1 (Add_Given "solveFor x");
113 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
115 fetchProposedTactic 1;
116 setNextTactic 1 (Add_Find "solutions L");
117 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
119 fetchProposedTactic 1;
120 setNextTactic 1 (Specify_Theory "Test");
121 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
122 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
124 fetchProposedTactic 1;
125 setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
126 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
127 (*-------------------------------------------------------------------------*)
128 fetchProposedTactic 1;
129 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
131 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
132 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
134 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
135 val (ptp as (pt,p), tacis) = get_calc 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 (Apply_Method ["Test","solve_linear"]);
142 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
143 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
145 is_complete_spec ptp;
147 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
148 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
149 (*term2str (get_obj g_form pt [1]);*)
150 (*-------------------------------------------------------------------------*)
152 fetchProposedTactic 1;
153 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
154 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
156 fetchProposedTactic 1;
157 setNextTactic 1 (Rewrite_Set "Test_simplify");
158 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
160 fetchProposedTactic 1;
161 setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
162 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
164 val ((pt,_),_) = get_calc 1;
165 val ip = get_pos 1 1;
166 val (Form f, tac, asms) = pt_extract (pt, ip);
167 (*exception just above means: 'ModSpec' has been returned: error anyway*)
168 if term2str f = "[x = 1]" then () else
169 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
173 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
174 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
175 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
176 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
178 refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
180 refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
182 refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
183 (*getAssumption 1 ([1],Res); TODO.WN041217*)
184 moveActiveDown 1 ; refFormula 1 ([2],Res);
185 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
189 if get_pos 1 1 = ([2], Res) then () else
190 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
191 moveActiveDown 1; refFormula 1 ([], Res);
192 if get_pos 1 1 = ([], Res) then () else
193 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
194 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
197 "--------- miniscript with mini-subpbl ------------------";
198 "--------- miniscript with mini-subpbl ------------------";
199 "--------- miniscript with mini-subpbl ------------------";
200 "=== this sequence of fun-calls resembles fun me ===";
201 states:=[]; (*start of calculation, return No.1*)
202 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
203 ("Test", ["sqroot-test","univariate","equation","test"],
204 ["Test","squ-equ-test-subpbl1"]))];
208 refFormula 1 (get_pos 1 1);
209 fetchProposedTactic 1;
210 setNextTactic 1 (Model_Problem);
211 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
213 fetchProposedTactic 1;
214 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
215 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
217 fetchProposedTactic 1;
218 setNextTactic 1 (Add_Given "solveFor x");
219 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
221 fetchProposedTactic 1;
222 setNextTactic 1 (Add_Find "solutions L");
223 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
225 fetchProposedTactic 1;
226 setNextTactic 1 (Specify_Theory "Test");
227 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
229 fetchProposedTactic 1;
230 setNextTactic 1 (Specify_Problem
231 ["sqroot-test","univariate","equation","test"]);
232 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
233 "1-----------------------------------------------------------------";
235 fetchProposedTactic 1;
236 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
237 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
239 fetchProposedTactic 1;
240 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
241 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
243 fetchProposedTactic 1;
244 setNextTactic 1 (Rewrite_Set "norm_equation");
245 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
247 fetchProposedTactic 1;
248 setNextTactic 1 (Rewrite_Set "Test_simplify");
249 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
251 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
252 setNextTactic 1 (Subproblem ("Test",
253 ["linear","univariate","equation","test"]));
254 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
256 fetchProposedTactic 1;
257 setNextTactic 1 (Model_Problem );
258 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
260 fetchProposedTactic 1;
261 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
262 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
264 fetchProposedTactic 1;
265 setNextTactic 1 (Add_Given "solveFor x");
266 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
268 fetchProposedTactic 1;
269 setNextTactic 1 (Add_Find "solutions x_i");
270 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
272 fetchProposedTactic 1;
273 setNextTactic 1 (Specify_Theory "Test");
274 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
276 fetchProposedTactic 1;
277 setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
278 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
279 "2-----------------------------------------------------------------";
281 fetchProposedTactic 1;
282 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
283 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
285 fetchProposedTactic 1;
286 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
287 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
289 fetchProposedTactic 1;
290 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
291 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
293 fetchProposedTactic 1;
294 setNextTactic 1 (Rewrite_Set "Test_simplify");
295 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
297 fetchProposedTactic 1;
298 setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
299 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
301 fetchProposedTactic 1;
302 setNextTactic 1 (Check_elementwise "Assumptions");
303 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
305 val xml = fetchProposedTactic 1;
306 setNextTactic 1 (Check_Postcond
307 ["sqroot-test","univariate","equation","test"]);
308 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
310 val ((pt,_),_) = get_calc 1;
311 val str = pr_ptree pr_short pt;
313 val ip = get_pos 1 1;
314 val (Form f, tac, asms) = pt_extract (pt, ip);
315 (*exception just above means: 'ModSpec' has been returned: error anyway*)
316 if term2str f = "[x = 1]" then () else
317 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
321 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
322 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
323 "--------- mini-subpbl AUTOCALCULATE Step 1 -------------";
325 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
326 ("Test", ["sqroot-test","univariate","equation","test"],
327 ["Test","squ-equ-test-subpbl1"]))];
330 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
331 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
332 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 (*here the solve-phase starts*)
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 (*------------------------------------*)
343 (* print_depth 13; get_calc 1;
345 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
346 (*calc-head of subproblem*)
347 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
348 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
349 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
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 (*solve-phase of the subproblem*)
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 (*finish subproblem*)
360 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
362 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
364 (*this checks the test for correctness..*)
365 val ((pt,_),_) = get_calc 1;
367 val (Form f, tac, asms) = pt_extract (pt, p);
368 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
369 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
373 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
374 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
375 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
378 [(["equality (1+-1*2+x=(0::real)", "solveFor x","solutions L"],
380 ["linear","univariate","equation","test"],
381 ["Test","solve_linear"]))];
384 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
386 autoCalculate 1 CompleteCalc;
387 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
388 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
390 (*========== inhibit exn 110718 ================================================
392 val ((pt,_),_) = get_calc 1;
397 val (Form f, tac, asms) = pt_extract (pt, p);
398 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
399 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
401 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
402 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
403 "--------- solve_linear as rootpbl AUTO CompleteHead/Calc ";
404 ========== inhibit exn 110718 ================================================*)
408 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
410 ["linear","univariate","equation","test"],
411 ["Test","solve_linear"]))];
414 autoCalculate 1 CompleteCalcHead;
415 (*========== inhibit exn 110718 ================================================
417 refFormula 1 (get_pos 1 1);
419 val ((pt,p),_) = get_calc 1;
421 autoCalculate 1 CompleteCalc;
422 val ((pt,p),_) = get_calc 1;
423 if p=([], Res) then () else
424 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Calc ";
425 ============ inhibit exn 110718 ==============================================*)
427 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
428 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
429 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
431 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
432 ("Test", ["sqroot-test","univariate","equation","test"],
433 ["Test","squ-equ-test-subpbl1"]))];
436 autoCalculate 1 CompleteCalc;
438 val ((pt,p),_) = get_calc 1; show_pt pt;
439 (*ERROR 110620 there is only 1 PblObj*)
441 getTactic 1 ([1],Frm);
442 getTactic 1 ([1],Res);
443 initContext 1 Thy_ ([1],Res);
446 (*... returns calcChangedEvent with*)
447 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
448 getFormulaeFromTo 1 unc gen 0 (*only result*) false;
449 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
450 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
452 val ((pt,_),_) = get_calc 1;
454 val (Form f, tac, asms) = pt_extract (pt, p);
455 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
456 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
460 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
461 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
462 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
464 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
465 ("Test", ["sqroot-test","univariate","equation","test"],
466 ["Test","squ-equ-test-subpbl1"]))];
469 autoCalculate 1 CompleteCalcHead;
471 val ((Nd (PblObj {env = NONE, fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
472 cell = NONE, ctxt = ctxt2, meth,
473 spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
474 ["Test", "squ-equ-test-subpbl1"]),
475 probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
476 ([], Met)), []) = get_calc 1;
477 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
478 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
480 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
481 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
482 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
485 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
487 ["linear","univariate","equation","test"],
488 ["Test","solve_linear"]))];
491 autoCalculate 1 CompleteModel;
492 (*========== inhibit exn 110718 ================================================
493 refFormula 1 (get_pos 1 1);
494 <ERROR> error in kernel </ERROR>
495 get_pos: calc 1 not existent
497 setProblem 1 ["linear","univariate","equation","test"];
498 val pos = get_pos 1 1;
499 setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
500 refFormula 1 (get_pos 1 1);
502 setMethod 1 ["Test","solve_linear"];
503 setContext 1 pos (kestoreID2guh Met_ ["Test","solve_linear"]);
504 refFormula 1 (get_pos 1 1);
505 val ((pt,_),_) = get_calc 1;
506 if get_obj g_spec pt [] = ("e_domID",
507 ["linear", "univariate","equation","test"],
508 ["Test","solve_linear"]) then ()
509 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
510 ============ inhibit exn 110718 ==============================================*)
512 autoCalculate 1 CompleteCalcHead;
513 (*========== inhibit exn 110718 ================================================
514 refFormula 1 (get_pos 1 1);
515 ============ inhibit exn 110718 ==============================================*)
516 autoCalculate 1 CompleteCalc;
520 (*========== inhibit exn 110718 ================================================
522 refFormula 1 (get_pos 1 1);
523 val ((pt,_),_) = get_calc 1;
525 val (Form f, tac, asms) = pt_extract (pt, p);
526 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
527 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
528 ============ inhibit exn 110718 ==============================================*)
531 "--------- setContext..Thy ------------------------------";
532 "--------- setContext..Thy ------------------------------";
533 "--------- setContext..Thy ------------------------------";
535 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
536 ("Test", ["sqroot-test","univariate","equation","test"],
537 ["Test","squ-equ-test-subpbl1"]))];
538 Iterator 1; moveActiveRoot 1;
539 autoCalculate 1 CompleteCalcHead;
540 autoCalculate 1 (Step 1);
541 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
543 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
544 autoCalculate 1 (Step 1);
545 val ((pt,p),_) = get_calc 1; show_pt pt;
547 "-----^^^^^ and vvvvv do the same -----";
548 setContext 1 p "thy_isac_Test-rls-Test_simplify";
549 val ((pt,p),_) = get_calc 1; show_pt pt; (*2 lines, OK*)
551 autoCalculate 1 (Step 1);
552 setContext 1 p "thy_isac_Test-rls-Test_simplify";
553 val ((pt,p),_) = get_calc 1; show_pt pt; (*3 lines, OK*)
554 if p = ([1], Res) andalso term2str (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
555 then () else error "--- setContext..Thy --- autoCalculate 1 (Step 1) #1"
557 autoCalculate 1 CompleteCalc;
558 val ((pt,p),_) = get_calc 1; show_pt pt;
559 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
560 (*========== inhibit exn 110718 ================================================
562 val (Form f, tac, asms) = pt_extract (pt, p);
563 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
564 error "--- setContext..Thy --- autoCalculate CompleteCalc";
565 ============ inhibit exn 110718 ==============================================*)
567 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
568 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
569 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
571 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
572 ("Test", ["sqroot-test","univariate","equation","test"],
573 ["Test","squ-equ-test-subpbl1"]))];
574 Iterator 1; moveActiveRoot 1;
575 autoCalculate 1 CompleteToSubpbl;
576 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
577 val ((pt,_),_) = get_calc 1;
578 val str = pr_ptree pr_short pt;
580 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
582 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
584 autoCalculate 1 (Step 1); (*proceeds only, of NOT 1 step before subplb*)
585 autoCalculate 1 CompleteToSubpbl;
586 val ((pt,_),_) = get_calc 1;
587 val str = pr_ptree pr_short pt;
589 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
590 val ((pt,_),_) = get_calc 1;
593 val (Form f, tac, asms) = pt_extract (pt, p);
594 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
595 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
598 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
599 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
600 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
603 [(["equality ((5*x)/(x - 2) - x/(x+2)=4)", "solveFor x","solutions L"],
604 ("RatEq", ["univariate","equation"], ["no_met"]))];
607 fetchProposedTactic 1;
609 (*========== inhibit exn 110718 ================================================
610 (*ERROR: setNextTactic 1 produces "get_calc 1 not existent"*)
611 setNextTactic 1 (Model_Problem );
612 autoCalculate 1 (Step 1); fetchProposedTactic 1;
614 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
615 setNextTactic 1 (Add_Given "equality (5 * x / (x - 2) - x / (x + 2) = 4)");
616 autoCalculate 1 (Step 1); fetchProposedTactic 1;
617 setNextTactic 1 (Add_Given "solveFor x");
618 autoCalculate 1 (Step 1); fetchProposedTactic 1;
619 setNextTactic 1 (Add_Find "solutions L");
620 autoCalculate 1 (Step 1); fetchProposedTactic 1;
621 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
624 setNextTactic 1 (Specify_Theory "RatEq");
625 autoCalculate 1 (Step 1); fetchProposedTactic 1;
626 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
627 autoCalculate 1 (Step 1); fetchProposedTactic 1;
628 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
629 autoCalculate 1 (Step 1); fetchProposedTactic 1;
630 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
631 autoCalculate 1 (Step 1); fetchProposedTactic 1;
632 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
633 autoCalculate 1 (Step 1); fetchProposedTactic 1;
634 setNextTactic 1 (Rewrite_Set "norm_Rational");
635 autoCalculate 1 (Step 1); fetchProposedTactic 1;
636 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
637 autoCalculate 1 (Step 1); fetchProposedTactic 1;
639 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
640 setNextTactic 1 (Subproblem ("PolyEq", ["normalize","polynomial",
641 "univariate","equation"]));
642 autoCalculate 1 (Step 1); fetchProposedTactic 1;
643 setNextTactic 1 (Model_Problem );
644 autoCalculate 1 (Step 1); fetchProposedTactic 1;
645 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
646 setNextTactic 1 (Add_Given
647 "equality (12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2))");
648 autoCalculate 1 (Step 1); fetchProposedTactic 1;
649 setNextTactic 1 (Add_Given "solveFor x");
650 autoCalculate 1 (Step 1); fetchProposedTactic 1;
651 setNextTactic 1 (Add_Find "solutions x_i");
652 autoCalculate 1 (Step 1); fetchProposedTactic 1;
653 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
654 setNextTactic 1 (Specify_Theory "PolyEq");
655 autoCalculate 1 (Step 1); fetchProposedTactic 1;
656 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
657 "univariate","equation"]);
658 autoCalculate 1 (Step 1); fetchProposedTactic 1;
659 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
660 autoCalculate 1 (Step 1); fetchProposedTactic 1;
661 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
662 autoCalculate 1 (Step 1); fetchProposedTactic 1;
663 setNextTactic 1 (Rewrite ("all_left",""));
664 autoCalculate 1 (Step 1); fetchProposedTactic 1;
665 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "make_ratpoly_in"));
666 autoCalculate 1 (Step 1); fetchProposedTactic 1;
667 (* __________ for "16 + 12 * x = 0"*)
668 setNextTactic 1 (Subproblem ("PolyEq",
669 ["degree_1","polynomial","univariate","equation"]));
670 autoCalculate 1 (Step 1); fetchProposedTactic 1;
671 setNextTactic 1 (Model_Problem );
672 autoCalculate 1 (Step 1); fetchProposedTactic 1;
673 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
674 setNextTactic 1 (Add_Given
675 "equality (16 + 12 * x = 0)");
676 autoCalculate 1 (Step 1); fetchProposedTactic 1;
677 setNextTactic 1 (Add_Given "solveFor x");
678 autoCalculate 1 (Step 1); fetchProposedTactic 1;
679 setNextTactic 1 (Add_Find "solutions x_i");
680 autoCalculate 1 (Step 1); fetchProposedTactic 1;
681 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
682 setNextTactic 1 (Specify_Theory "PolyEq");
683 (*------------- some trials in the problem-hierarchy ---------------*)
684 setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
685 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
686 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
688 (*------------------------------------------------------------------*)
689 autoCalculate 1 (Step 1); fetchProposedTactic 1;
690 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
691 autoCalculate 1 (Step 1); fetchProposedTactic 1;
692 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
693 autoCalculate 1 (Step 1); fetchProposedTactic 1;
694 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "d1_polyeq_simplify"));
695 autoCalculate 1 (Step 1); fetchProposedTactic 1;
696 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
697 autoCalculate 1 (Step 1); fetchProposedTactic 1;
698 (*==================================================================*)
699 setNextTactic 1 Or_to_List;
700 autoCalculate 1 (Step 1); fetchProposedTactic 1;
701 setNextTactic 1 (Check_elementwise "Assumptions");
702 autoCalculate 1 (Step 1); fetchProposedTactic 1;
703 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
704 "univariate","equation"]);
705 autoCalculate 1 (Step 1); fetchProposedTactic 1;
706 setNextTactic 1 (Check_Postcond ["normalize","polynomial",
707 "univariate","equation"]);
708 autoCalculate 1 (Step 1); fetchProposedTactic 1;
709 (*========== inhibit exn 2009 ==================================================
710 *** exception TYPE raised (line 460 of "old_goals.ML"):
711 *** Type error in application: Incompatible operand type
713 *** Operator: equality :: bool => una
714 *** Operand: [((x * 3) = -4)] :: bool list
721 setNextTactic 1 (Check_elementwise "Assumptions");
722 autoCalculate 1 (Step 1); fetchProposedTactic 1;
723 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
724 val (ptp,_) = get_calc 1;
725 val (Form t,_,_) = pt_extract ptp;
726 if get_pos 1 1 = ([], Res) andalso term2str t = "[x = -4 / 3]" then ()
727 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
728 ============ inhibit exn 2009 ================================================*)
729 ============ inhibit exn 110718 ==============================================*)
732 "--------- tryMatchProblem, tryRefineProblem ------------";
733 "--------- tryMatchProblem, tryRefineProblem ------------";
734 "--------- tryMatchProblem, tryRefineProblem ------------";
735 (*{\bf\UC{Having \isac{} Refine the Problem
736 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
737 * x^^^2 + 4*x + 5 = 2
738 see isac.bridge.TestSpecify#testMatchRefine*)
741 [(["equality (x^2 + 4*x + 5 = 2)", "solveFor x","solutions L"],
743 ["univariate","equation"],
748 fetchProposedTactic 1;
749 setNextTactic 1 (Model_Problem );
750 (*..this tactic should be done 'tacitly', too !*)
753 autoCalculate 1 CompleteCalcHead;
754 checkContext 1 ([],Pbl) "pbl_equ_univ";
755 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
758 autoCalculate 1 (Step 1);
760 fetchProposedTactic 1;
761 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = 2)");
762 autoCalculate 1 (Step 1);
764 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
765 initContext 1 Pbl_ ([],Pbl);
766 initContext 1 Met_ ([],Pbl);
768 "--------- this match will show some incomplete items: ---------";
769 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
770 checkContext 1 ([],Pbl) (kestoreID2guh Met_ ["LinEq", "solve_lineq_equation"]);
773 fetchProposedTactic 1;
774 setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Step 1);
776 fetchProposedTactic 1;
777 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Step 1);
779 "--------- this is a matching model (all items correct): -------";
780 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
781 "--------- this is a NOT matching model (some 'false': ---------";
782 checkContext 1 ([],Pbl)(kestoreID2guh Pbl_["linear","univariate","equation"]);
784 "--------- find out a matching problem: ------------------------";
785 "--------- find out a matching problem (FAILING: no new pbl) ---";
786 refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
788 "--------- find out a matching problem (SUCCESSFUL) ------------";
789 refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
791 "--------- tryMatch, tryRefine did not change the calculation -";
792 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
793 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
794 "univariate","equation"]);
795 autoCalculate 1 (Step 1);
796 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalize",...
797 and Specify_Theory skipped in comparison to below ---^^^-inserted *)
798 (*------------vvv-inserted-----------------------------------------------*)
799 fetchProposedTactic 1;
800 setNextTactic 1 (Specify_Problem ["normalize","polynomial",
801 "univariate","equation"]);
802 autoCalculate 1 (Step 1);
804 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
806 fetchProposedTactic 1;
807 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
808 autoCalculate 1 (Step 1);
810 fetchProposedTactic 1;
811 setNextTactic 1 (Apply_Method ["PolyEq","normalize_poly"]);
812 autoCalculate 1 CompleteCalc;
813 val ((pt,_),_) = get_calc 1;
816 val (Form f, tac, asms) = pt_extract (pt, p);
818 (*========== inhibit exn 110718 ================================================
819 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
820 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
821 ========== inhibit exn 110718 ================================================*)
823 (*------------^^^-inserted-----------------------------------------------*)
824 (*WN050904 the fetchProposedTactic's below may not have worked like that
825 before, too, because there was no check*)
826 fetchProposedTactic 1;
827 setNextTactic 1 (Specify_Theory "PolyEq");
828 autoCalculate 1 (Step 1);
830 fetchProposedTactic 1;
831 setNextTactic 1 (Specify_Method ["PolyEq","normalize_poly"]);
832 autoCalculate 1 (Step 1);
834 fetchProposedTactic 1;
835 "--------- now the calc-header is ready for enter 'solving' ----";
836 autoCalculate 1 CompleteCalc;
838 val ((pt,_),_) = get_calc 1;
842 (*========== inhibit exn 110718 ================================================
844 val (Form f, tac, asms) = pt_extract (pt, p);
845 if term2str f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
846 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
848 ============ inhibit exn 110718 ==============================================*)
851 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
852 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
853 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
856 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
857 ("Test", ["sqroot-test","univariate","equation","test"],
858 ["Test","squ-equ-test-subpbl1"]))];
862 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
863 "solve (x+1=2, x)",(*the headline*)
864 [Given ["equality (x+1=2)", "solveFor x"],
865 Find ["solutions L"](*,Relate []*)],
868 ["sqroot-test","univariate","equation","test"],
869 ["Test","squ-equ-test-subpbl1"]));
871 val ((Nd (PblObj {env = NONE,
873 loc = (SOME scrst_ctxt, NONE),
878 ["sqroot-test", "univariate", "equation", "test"],
879 ["Test", "squ-equ-test-subpbl1"]),
881 branch = TransitiveB,
888 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
889 if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
890 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
896 val ((Nd (PblObj {env = NONE,
898 loc = (SOME scrst_ctxt, NONE),
902 spec = ("e_domID", ["e_pblID"], ["e_metID"]),
904 branch = TransitiveB,
911 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
912 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
914 "--------- maximum-example, UC: Modeling an example -----";
915 "--------- maximum-example, UC: Modeling an example -----";
916 "--------- maximum-example, UC: Modeling an example -----";
917 (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
918 see isac.bridge.TestModel#testEditItems
920 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
921 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
922 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
923 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
924 (*^^^ these are the elements for the root-problem (in variants)*)
925 (*vvv these are elements required for subproblems*)
926 "boundVariable a","boundVariable b","boundVariable alpha",
927 "interval {x::real. 0 <= x & x <= 2*r}",
928 "interval {x::real. 0 <= x & x <= 2*r}",
929 "interval {x::real. 0 <= x & x <= pi}",
930 "errorBound (eps=(0::real))"]
931 (*specifying is not interesting for this example*)
932 val spec = ("DiffApp", ["maximum_of","function"],
933 ["DiffApp","max_by_calculus"]);
934 (*the empty model with descriptions for user-guidance by Model_Problem*)
935 val empty_model = [Given ["fixedValues []"],
936 Find ["maximum", "valuesFor"],
937 Relate ["relations []"]];
940 CalcTree [(elems, spec)];
943 refFormula 1 (get_pos 1 1);
944 (*this gives a completely empty model*)
946 fetchProposedTactic 1;
947 (*fill the CalcHead with Descriptions...*)
948 setNextTactic 1 (Model_Problem );
949 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
951 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
952 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
953 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
954 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
955 "Problem (DiffApp.thy, [maximum_of, function])",
956 (*the head-form ^^^ is not used for input here*)
957 [Given ["fixedValues [r=Arbfix]"(*new input*)],
958 Find ["maximum b"(*new input*), "valuesFor"],
959 Relate ["relations"]],
960 (*input (Arbfix will dissappear soon)*)
962 e_spec (*no input to the specification*));
964 (*the user does not know, what 'superfluous' for 'maximum b' may mean
965 and asks what to do next*)
966 fetchProposedTactic 1;
967 (*the student follows the advice*)
968 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
969 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
971 (*this input completes the model*)
972 modifyCalcHead 1 (([],Pbl), "not used here",
973 [Given ["fixedValues [r=Arbfix]"],
974 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
975 Relate ["relations [A=a*b, \
976 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, e_spec);
978 (*specification is not interesting an should be skipped by the dialogguide;
979 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
980 modifyCalcHead 1 (([],Pbl), "not used here",
981 [Given ["fixedValues [r=Arbfix]"],
982 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
983 Relate ["relations [A=a*b, \
984 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
985 ("DiffApp", ["e_pblID"], ["e_metID"]));
986 modifyCalcHead 1 (([],Pbl), "not used here",
987 [Given ["fixedValues [r=Arbfix]"],
988 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
989 Relate ["relations [A=a*b, \
990 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
991 ("DiffApp", ["maximum_of","function"],
993 modifyCalcHead 1 (([],Pbl), "not used here",
994 [Given ["fixedValues [r=Arbfix]"],
995 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
996 Relate ["relations [A=a*b, \
997 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
998 ("DiffApp", ["maximum_of","function"],
999 ["DiffApp","max_by_calculus"]));
1000 (*this final calcHead now has STATUS 'complete' !*)
1003 "--------- solve_linear from pbl-hierarchy --------------";
1004 "--------- solve_linear from pbl-hierarchy --------------";
1005 "--------- solve_linear from pbl-hierarchy --------------";
1007 val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
1008 CalcTree [(fmz, sp)];
1009 Iterator 1; moveActiveRoot 1;
1010 refFormula 1 (get_pos 1 1);
1011 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=0)",
1012 [Given ["equality (1+-1*2+x=0)", "solveFor x"],
1013 Find ["solutions L"]],
1015 ("Test", ["linear","univariate","equation","test"],
1016 ["Test","solve_linear"]));
1017 autoCalculate 1 CompleteCalc;
1018 refFormula 1 (get_pos 1 1);
1019 val ((pt,_),_) = get_calc 1;
1020 val p = get_pos 1 1;
1021 val (Form f, tac, asms) = pt_extract (pt, p);
1022 if term2str f = "[x = 1]" andalso p = ([], Res)
1023 andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
1024 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
1026 "--------- solve_linear as in an algebra system (CAS)----";
1027 "--------- solve_linear as in an algebra system (CAS)----";
1028 "--------- solve_linear as in an algebra system (CAS)----";
1030 val (fmz, sp) = ([], ("", [], []));
1031 CalcTree [(fmz, sp)];
1032 Iterator 1; moveActiveRoot 1;
1033 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
1034 autoCalculate 1 CompleteCalc;
1035 refFormula 1 (get_pos 1 1);
1036 val ((pt,_),_) = get_calc 1;
1037 val p = get_pos 1 1;
1038 val (Form f, tac, asms) = pt_extract (pt, p);
1039 if term2str f = "[x = 1]" andalso p = ([], Res)
1040 andalso terms2str asms = "[\"matches (?a = ?b) (1 + -1 * 2 + x = 0)\"]" then ()
1041 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy";
1043 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1044 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1045 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1047 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1048 ("Test", ["sqroot-test","univariate","equation","test"],
1049 ["Test","squ-equ-test-subpbl1"]))];
1052 autoCalculate 1 CompleteCalc;
1053 val ((pt,_),_) = get_calc 1;
1056 (*UC\label{SOLVE:INFO:intermediate-steps}*)
1057 interSteps 1 ([2],Res);
1058 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1059 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1060 getFormulaeFromTo 1 unc gen 1 false;
1062 (*UC\label{SOLVE:INFO:intermediate-steps}*)
1063 interSteps 1 ([3,2],Res);
1064 val ((pt,_),_) = get_calc 1; show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1065 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1066 getFormulaeFromTo 1 unc gen 1 false;
1068 (*UC\label{SOLVE:INFO:intermediate-steps}*)
1069 interSteps 1 ([3],Res) (*no new steps in subproblems*);
1070 val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1071 getFormulaeFromTo 1 unc gen 1 false;
1073 (*UC\label{SOLVE:INFO:intermediate-steps}*)
1074 interSteps 1 ([],Res) (*no new steps in subproblems*);
1075 val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1076 getFormulaeFromTo 1 unc gen 1 false;
1079 "--------- getTactic, fetchApplicableTactics ------------";
1080 "--------- getTactic, fetchApplicableTactics ------------";
1081 "--------- getTactic, fetchApplicableTactics ------------";
1083 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1084 ("Test", ["sqroot-test","univariate","equation","test"],
1085 ["Test","squ-equ-test-subpbl1"]))];
1086 Iterator 1; moveActiveRoot 1;
1087 autoCalculate 1 CompleteCalc;
1088 val ((pt,_),_) = get_calc 1;
1091 (*UC\label{SOLVE:HIDE:getTactic}*)
1092 getTactic 1 ([],Pbl);
1093 getTactic 1 ([1],Res);
1094 getTactic 1 ([3],Pbl);
1095 getTactic 1 ([3,1],Frm);
1096 getTactic 1 ([3],Res);
1097 getTactic 1 ([],Res);
1099 (*UC\label{SOLVE:MANUAL:TACTIC:listall}*)
1100 fetchApplicableTactics 1 99999 ([],Pbl);
1101 fetchApplicableTactics 1 99999 ([1],Res);
1102 fetchApplicableTactics 1 99999 ([3],Pbl);
1103 fetchApplicableTactics 1 99999 ([3,1],Res);
1104 fetchApplicableTactics 1 99999 ([3],Res);
1105 fetchApplicableTactics 1 99999 ([],Res);
1108 "--------- getAssumptions, getAccumulatedAsms -----------";
1109 "--------- getAssumptions, getAccumulatedAsms -----------";
1110 "--------- getAssumptions, getAccumulatedAsms -----------";
1113 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1114 "solveFor x","solutions L"],
1115 ("RatEq",["univariate","equation"],["no_met"]))];
1116 Iterator 1; moveActiveRoot 1;
1117 autoCalculate 1 CompleteCalc;
1118 val ((pt,_),_) = get_calc 1;
1119 val p = get_pos 1 1;
1120 val (Form f, tac, asms) = pt_extract (pt, p);
1121 if map term2str asms =
1122 ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
1123 "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
1124 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
1125 "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
1126 andalso term2str f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
1127 else error "TODO compare 2002--2011";
1129 (*UC\label{SOLVE:HELP:assumptions}*)
1130 getAssumptions 1 ([3], Res);
1131 getAssumptions 1 ([5], Res);
1132 (*UC\label{SOLVE:HELP:assumptions-origin} WN0502 still without positions*)
1133 getAccumulatedAsms 1 ([3], Res);
1134 getAccumulatedAsms 1 ([5], Res);
1137 "--------- arbitrary combinations of steps --------------";
1138 "--------- arbitrary combinations of steps --------------";
1139 "--------- arbitrary combinations of steps --------------";
1141 CalcTree (*start of calculation, return No.1*)
1142 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
1144 ["linear","univariate","equation","test"],
1145 ["Test","solve_linear"]))];
1146 Iterator 1; moveActiveRoot 1;
1148 fetchProposedTactic 1;
1149 (*========== inhibit exn 110719 ================================================
1150 (*ERROR get_calc 1 not existent*)
1151 setNextTactic 1 (Model_Problem );
1152 autoCalculate 1 (Step 1);
1153 ========== inhibit exn 110719 ================================================*)
1155 fetchProposedTactic 1;
1156 fetchProposedTactic 1;
1157 (*========== inhibit exn 110719 ================================================
1159 setNextTactic 1 (Add_Find "solutions L");
1160 setNextTactic 1 (Add_Find "solutions L");
1162 autoCalculate 1 (Step 1);
1163 autoCalculate 1 (Step 1);
1165 setNextTactic 1 (Specify_Theory "Test");
1166 fetchProposedTactic 1;
1167 autoCalculate 1 (Step 1);
1169 autoCalculate 1 (Step 1);
1170 autoCalculate 1 (Step 1);
1171 autoCalculate 1 (Step 1);
1172 autoCalculate 1 (Step 1);
1173 (*------------------------- end calc-head*)
1175 fetchProposedTactic 1;
1176 setNextTactic 1 (Rewrite_Set_Inst (["(bdv,x)"], "isolate_bdv"));
1177 autoCalculate 1 (Step 1);
1179 setNextTactic 1 (Rewrite_Set "Test_simplify");
1180 fetchProposedTactic 1;
1181 autoCalculate 1 (Step 1);
1182 ============ inhibit exn 110719 ==============================================*)
1184 autoCalculate 1 CompleteCalc;
1185 (*============ inhibit exn 110719 ==============================================
1187 val ((pt,_),_) = get_calc 1;
1188 val p = get_pos 1 1;
1189 val (Form f, tac, asms) = pt_extract (pt, p);
1190 if term2str f = "[x = 1]" andalso p = ([], Res) then () else
1191 error "FE-interface.sml: diff.behav. in combinations of steps";
1192 ============ inhibit exn 110719 ==============================================*)
1196 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1197 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1198 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1200 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1201 ("Test", ["sqroot-test","univariate","equation","test"],
1202 ["Test","squ-equ-test-subpbl1"]))];
1205 autoCalculate 1 CompleteCalcHead;
1206 autoCalculate 1 (Step 1);
1207 autoCalculate 1 (Step 1);
1208 appendFormula 1 "-1 + x = 0";
1209 (*... returns calcChangedEvent with*)
1210 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1211 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1213 val ((pt,_),_) = get_calc 1;
1214 val p = get_pos 1 1;
1215 val (Form f, tac, asms) = pt_extract (pt, p);
1216 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1217 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1221 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1222 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1223 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1225 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1226 ("Test", ["sqroot-test","univariate","equation","test"],
1227 ["Test","squ-equ-test-subpbl1"]))];
1230 autoCalculate 1 CompleteCalcHead;
1231 autoCalculate 1 (Step 1);
1232 autoCalculate 1 (Step 1);
1233 appendFormula 1 "x - 1 = 0";
1234 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1235 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1238 val ((pt,_),_) = get_calc 1;
1239 val p = get_pos 1 1;
1240 val (Form f, tac, asms) = pt_extract (pt, p);
1241 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1242 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1245 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1246 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1247 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1249 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1250 ("Test", ["sqroot-test","univariate","equation","test"],
1251 ["Test","squ-equ-test-subpbl1"]))];
1254 autoCalculate 1 CompleteCalcHead;
1255 autoCalculate 1 (Step 1);
1256 autoCalculate 1 (Step 1);
1257 appendFormula 1 "x = 1";
1258 (*... returns calcChangedEvent with*)
1259 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1260 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1263 val ((pt,_),_) = get_calc 1;
1264 val p = get_pos 1 1;
1265 val (Form f, tac, asms) = pt_extract (pt, p);
1266 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1267 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1270 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1271 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1272 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1274 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1275 ("Test", ["sqroot-test","univariate","equation","test"],
1276 ["Test","squ-equ-test-subpbl1"]))];
1279 autoCalculate 1 CompleteCalcHead;
1280 autoCalculate 1 (Step 1);
1281 autoCalculate 1 (Step 1);
1282 appendFormula 1 "x - 4711 = 0";
1283 (*... returns <ERROR> no derivation found </ERROR>*)
1285 val ((pt,_),_) = get_calc 1;
1286 val p = get_pos 1 1;
1287 val (Form f, tac, asms) = pt_extract (pt, p);
1288 if term2str f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
1289 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1292 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1293 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1294 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1296 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1297 ("Test", ["sqroot-test","univariate","equation","test"],
1298 ["Test","squ-equ-test-subpbl1"]))];
1301 autoCalculate 1 CompleteCalc;
1302 moveActiveFormula 1 ([2],Res);
1303 replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1304 (*... returns <ERROR> formula not changed </ERROR>*)
1306 val ((pt,_),_) = get_calc 1;
1307 val p = get_pos 1 1;
1308 val (Form f, tac, asms) = pt_extract (pt, p);
1309 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1310 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1311 if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1312 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1313 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1314 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1316 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1317 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1318 ("Test", ["sqroot-test","univariate","equation","test"],
1319 ["Test","squ-equ-test-subpbl1"]))];
1322 autoCalculate 2 CompleteCalc;
1323 moveActiveFormula 2 ([2],Res);
1324 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1325 (*... returns <ERROR> formula not changed </ERROR>*)
1327 val ((pt,_),_) = get_calc 2;
1328 val p = get_pos 2 1;
1329 val (Form f, tac, asms) = pt_extract (pt, p);
1330 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1331 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1332 if map fst (get_interval ([2],Res) ([],Res) 9999 pt) =
1333 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1334 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1335 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1337 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1338 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1339 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1341 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1342 ("Test", ["sqroot-test","univariate","equation","test"],
1343 ["Test","squ-equ-test-subpbl1"]))];
1346 autoCalculate 1 CompleteCalc;
1347 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1348 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1349 (*... returns calcChangedEvent with*)
1350 val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1351 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1353 val ((pt,_),_) = get_calc 1;
1355 val p = get_pos 1 1;
1356 val (Form f, tac, asms) = pt_extract (pt, p);
1357 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
1358 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1359 (* for getting the list in whole length ...
1360 print_depth 99;map fst (get_interval ([1],Res) ([],Res) 9999 pt);print_depth 3;
1362 if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1363 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1364 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1365 ([2, 8], Res), ([2, 9], Res), ([2], Res)
1366 (*WN060727 {cutlevup->test_trans} removed: ,
1367 ([], Res)(*dropped, if test_trans doesnt stop at PblNd*)*)] then () else
1368 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1371 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1372 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1373 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1375 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1376 ("Test", ["sqroot-test","univariate","equation","test"],
1377 ["Test","squ-equ-test-subpbl1"]))];
1380 autoCalculate 1 CompleteCalc;
1381 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1382 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1383 (*... returns calcChangedEvent with ...*)
1384 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1385 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1388 val ((pt,_),_) = get_calc 1;
1389 show_pt pt; (*error: ...get_interval drops ([3,2],Res) ...*)
1390 val (t,_) = get_obj g_result pt [3,2]; term2str t;
1391 if map fst (get_interval ([1],Res) ([],Res) 9999 pt) =
1392 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1393 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1394 ([3,2],Res)] then () else
1395 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1397 val p = get_pos 1 1;
1398 val (Form f, tac, asms) = pt_extract (pt, p);
1399 if term2str f = "x = 1" andalso p = ([3,2], Res) then () else
1400 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1403 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1404 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1405 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1407 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1408 ("Test", ["sqroot-test","univariate","equation","test"],
1409 ["Test","squ-equ-test-subpbl1"]))];
1412 autoCalculate 1 CompleteCalc;
1413 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1414 replaceFormula 1 "x - 4711 = 0";
1415 (*... returns <ERROR> no derivation found </ERROR>*)
1417 val ((pt,_),_) = get_calc 1;
1419 val p = get_pos 1 1;
1420 val (Form f, tac, asms) = pt_extract (pt, p);
1421 if term2str f = "-1 + x = 0" andalso p = ([2], Res) then () else
1422 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";