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 Isac.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 Steps 1 ------------";
31 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
32 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
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 - WITH fun me IN test/../solve.sml";
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 ThyC.id_empty etc. statt leer kommt ???*)
97 "--------- solve_linear as rootpbl FE -------------------";
98 "--------- solve_linear as rootpbl FE -------------------";
99 "--------- solve_linear as rootpbl FE -------------------";
102 CalcTree (*start of calculation, return No.1*)
103 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
105 ["LINEAR","univariate","equation","test"],
106 ["Test","solve_linear"]))];
107 Iterator 1; (*create an active Iterator on CalcTree No.1*)
109 moveActiveRoot 1;(*sets the CalcIterator No.1 at the root of CalcTree No.1*);
110 refFormula 1 (get_pos 1 1) (*gets CalcHead; model is still empty*);
113 (*1*) fetchProposedTactic 1 (*by using Iterator No.1*);
114 setNextTactic 1 (Model_Problem); (*by using Iterator No.1*)
115 autoCalculate 1 (Steps 1);
116 refFormula 1 (get_pos 1 1) (*model contains descriptions for all items*);
117 autoCalculate 1 (Steps 1);
118 (*-----since Model_Problem + complete_mod_ in case cas of SOME-----*
119 (*2*) fetchProposedTactic 1;
120 setNextTactic 1 (Add_Given "equality (1 + -1 * 2 + x = 0)");
121 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*equality added*);
123 (*3*) fetchProposedTactic 1;
124 setNextTactic 1 (Add_Given "solveFor x");
125 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
127 (*4*) fetchProposedTactic 1;
128 setNextTactic 1 (Add_Find "solutions L");
129 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
131 (*5*) fetchProposedTactic 1;
132 setNextTactic 1 (Specify_Theory "Test");
133 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
134 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
136 (*6*) fetchProposedTactic 1;
137 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
138 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
139 (*-------------------------------------------------------------------------*)
140 (*7*) fetchProposedTactic 1;
141 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
143 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
144 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
146 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
147 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
149 (*-------------------------------------------------------------------------*)
150 (*8*) fetchProposedTactic 1;
151 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
153 (*8*) setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
154 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
155 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
156 Specification.is_complete ptp;
157 References.are_complete ptp;
159 (*8*) autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*)
161 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
162 (*+isa=REP*) if p = ([1], Frm) andalso UnparseC.term (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
163 andalso Istate.string_of (get_istate_LI pt p)
164 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)"
165 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
166 (*-------------------------------------------------------------------------*)
168 (*9*) fetchProposedTactic 1; (*<----------------------------------------------------- orig. test code*)
169 (*+\\------------------------------------------ isa == REP -----------------------------------//* )
170 (*+//========================================== isa <> REP (1) ===============================\\*)
171 (*9*) setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")); ( *<------- orig. test code*)
173 "~~~~~ fun setNextTactic , args:"; val (cI, tac) = (1, (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv")));
174 val ((pt'''''_', _), _) = get_calc cI
175 val ip'''''_' = get_pos cI 1;
177 val xxxxx_x(*"ok", (tacis, _, _)*) = (*case*) Step.by_tactic tac (pt'''''_', ip'''''_') (*of*);
178 (*+isa+REP*)val ("ok", ( [ (Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
179 Rewrite_Set_Inst' _, (pos', (istate, ctxt))) ] , _, cstate)) = xxxxx_x;
181 (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
182 Step.by_tactic : Tactic.input -> state -> string * (State_Steps.T * pos' list * state);
183 if Istate.string_of istate
184 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
185 then () else error "from Step.by_tactic return --- changed 1";
187 if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
188 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
189 then () else error "from Step.by_tactic return --- changed 2";
190 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
192 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt'''''_', ip'''''_'));
193 val Applicable.Yes m = (*case*) Step.check tac (pt, p) (*of*);
194 (*if*) Tactic.for_specify' m; (*false*)
196 Step_Solve.by_tactic m (pt, p);
197 "~~~~~ fun by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, p));
198 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*else*)
199 val thy' = get_obj g_domID pt (par_pblobj pt p);
200 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
201 val Safe_Step (istate, _, tac) =
202 (*case*) LI.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
204 (*+*)Safe_Step: Istate.T * Proof.context * Tactic.T -> input_tactic_result;
205 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
206 (*+*)if Istate.string_of istate
207 (*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
208 then case m of Rewrite_Set_Inst' _ => ()
209 else error "from locate_input_tactic return --- changed";
211 val ("ok", (tacis'''''_', _, _)) = xxxxx_x;
212 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI ((pt'''''_', ip'''''_'), tacis'''''_');
213 (*\\=========================================== isa <> REP (1) ===============================//*)
214 (*//=========================================== isa <> REP (2) ===============================\\*)
215 (*9* ) autoCalculate 1 (Steps 1); (*<-------------------------------------------------- orig. test code*)
216 ( *isa: <AUTOCALC><CALCID>1</CALCID><CALCCHANGED><UNCHANGED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></UNCHANGED><DELETED><INTLIST><INT>1</INT></INTLIST><POS>Frm</POS></DELETED><GENERATED><INTLIST><INT>1</INT></INTLIST><POS>Res</POS></GENERATED></CALCCHANGED></AUTOCALC>*)
218 "~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
219 val pold = get_pos cI 1;
220 val xxx = (get_calc cI);
221 (*isa*) val (**)xxxx(**) (**) = (**)
222 (*case*) Math_Engine.autocalc [] pold (xxx) auto (*of*);
223 "~~~~~ fun autocalc , args:"; val (c, ip, cs, (Solve.Steps s)) = ([], pold, (xxx), auto);
224 (*if*) s <= 1; (*then*)
225 (*val (str, (_, c', ptp)) =*)
228 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
230 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
231 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
232 (*+*)if pos' = ([1], Res) andalso Istate.string_of istate
233 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
234 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
236 val pIopt = get_pblID (pt,ip);
237 (*if*) ip = ([], Pos.Res);(*else*)
238 val (_::_) = (*case*) tacis (*of*);
239 (*isa==REP*) (*if*) ip = p;(*then*)
240 (*val (pt',c',p') =*) Solve_Step.s_add_general tacis (pt,[],p);
241 (*//------------------------------------- final test -----------------------------------------\\*)
242 val ("ok", [], ptp as (pt, p)) = xxxx;
244 if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
245 (*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], empty, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
246 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
248 "~~~~~ from TOPLEVEL to states return:"; upd_calc cI (ptp, []); upd_ipos cI 1 p;
249 (*\\=========================================== isa <> REP (2) ===============================//*)
251 (*10*) fetchProposedTactic 1;
252 setNextTactic 1 (Rewrite_Set "Test_simplify");
253 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
255 (*11*) fetchProposedTactic 1;
256 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
257 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
259 (*======= final test ==================================================*)
260 val ((pt,_),_) = get_calc 1;
261 val ip = get_pos 1 1;
263 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
264 (*exception just above means: 'ModSpec' has been returned: error anyway*)
265 if ip = ([], Res) andalso UnparseC.term f = "[x = 1]" then () else
266 error "FE-Kernel-interface.sml: diff.behav. in solve_linear as rootpbl";
269 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
270 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
271 "--------- inspect the CalcTree No.1 with Iterator No.2 -";
272 (*WN041118: inspection shifted to Iterator No.1, because others need pos'*)
273 (*-------- WN190723: doesnt work since changeset 59474 21d4d2868b83
275 refFormula 1 ([],Pbl); getTactic 1 ([],Pbl);(*Error*)
277 refFormula 1 ([1],Frm); getTactic 1 ([1],Frm);(*Error*)
279 refFormula 1 ([1],Res); getTactic 1 ([1],Res);(*OK*)
280 (*getAssumption 1 ([1],Res); TODO.WN041217*)
281 moveActiveDown 1 ; refFormula 1 ([2],Res);
282 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
286 if get_pos 1 1 = ([2], Res) then () else
287 error "FE-interface.sml: diff.behav. in a inspect 1 with Iterator 2";
288 moveActiveDown 1; refFormula 1 ([], Res);
289 if get_pos 1 1 = ([], Res) then () else
290 error "FE-interface.sml: diff.behav. in b inspect 1 with Iterator 2";
291 moveActiveCalcHead 1; refFormula 1 ([],Pbl);
293 ------------------------------------------------------------------------------------------------*)
295 "--------- miniscript with mini-subpbl ------------------";
296 "--------- miniscript with mini-subpbl ------------------";
297 "--------- miniscript with mini-subpbl ------------------";
298 (*WN120210?not ME:\label{SOLVE:MANUAL:TACTIC:enter} UC 30.3.2.1 p.175 !!!!!NOT IMPL IN FE*)
299 "=== this sequence of fun-calls resembles fun me ===";
300 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
301 ("Test", ["sqroot-test","univariate","equation","test"],
302 ["Test","squ-equ-test-subpbl1"]))];
306 refFormula 1 (get_pos 1 1);
307 fetchProposedTactic 1;
308 setNextTactic 1 (Model_Problem);
309 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);(*gets ModSpec;model is still empty*)
311 fetchProposedTactic 1; (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 3</ERROR></SYSERROR>* )
312 setNextTactic 1 (Add_Given "equality (x + 1 = 2)");
313 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
315 fetchProposedTactic 1;
316 setNextTactic 1 (Add_Given "solveFor x");
317 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
319 fetchProposedTactic 1;
320 setNextTactic 1 (Add_Find "solutions L");
321 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
323 fetchProposedTactic 1;
324 setNextTactic 1 (Specify_Theory "Test");
325 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
327 fetchProposedTactic 1;
328 setNextTactic 1 (Specify_Problem
329 ["sqroot-test","univariate","equation","test"]);
330 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
331 "1-----------------------------------------------------------------";
333 fetchProposedTactic 1;
334 setNextTactic 1 (Specify_Method ["Test","squ-equ-test-subpbl1"]);
335 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
337 fetchProposedTactic 1;
338 setNextTactic 1 (Apply_Method ["Test","squ-equ-test-subpbl1"]);
339 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
341 fetchProposedTactic 1;
342 setNextTactic 1 (Rewrite_Set "norm_equation");
343 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
345 fetchProposedTactic 1;
346 setNextTactic 1 (Rewrite_Set "Test_simplify");
347 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
349 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
350 setNextTactic 1 (Subproblem ("Test",
351 ["LINEAR","univariate","equation","test"]));
352 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
354 fetchProposedTactic 1;
355 setNextTactic 1 (Model_Problem );
356 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
358 fetchProposedTactic 1;
359 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
360 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
362 fetchProposedTactic 1;
363 setNextTactic 1 (Add_Given "solveFor x");
364 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
366 fetchProposedTactic 1;
367 setNextTactic 1 (Add_Find "solutions x_i");
368 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
370 fetchProposedTactic 1;
371 setNextTactic 1 (Specify_Theory "Test");
372 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
374 fetchProposedTactic 1;
375 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
376 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
377 "2-----------------------------------------------------------------";
379 fetchProposedTactic 1;
380 setNextTactic 1 (Specify_Method ["Test","solve_linear"]);
381 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
383 fetchProposedTactic 1;
384 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
385 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
387 fetchProposedTactic 1;
388 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
389 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
391 fetchProposedTactic 1;
392 setNextTactic 1 (Rewrite_Set "Test_simplify");
393 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
395 fetchProposedTactic 1;
396 setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
397 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
399 fetchProposedTactic 1;
400 setNextTactic 1 (Check_elementwise "Assumptions");
401 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
403 val xml = fetchProposedTactic 1;
404 setNextTactic 1 (Check_Postcond
405 ["sqroot-test","univariate","equation","test"]);
406 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
408 val ((pt,_),_) = get_calc 1;
409 val str = pr_ctree pr_short pt;
411 val ip = get_pos 1 1;
412 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, ip);
413 (*exception just above means: 'ModSpec' has been returned: error anyway*)
414 if UnparseC.term f = "[x = 1]" then () else
415 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
416 (**)-------------------------------------------------------------------------------------------*)
419 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
420 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
421 "--------- mini-subpbl AUTOCALCULATE Steps 1 -------------";
422 (*WN120210?not ME:\label{SOLVE:AUTO:one} UC 30.3.3.2 p.176*)
423 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
424 ("Test", ["sqroot-test","univariate","equation","test"],
425 ["Test","squ-equ-test-subpbl1"]))];
428 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
429 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
430 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
431 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
432 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
433 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
434 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
435 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
436 (*here the solve-phase starts*)
437 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
438 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
439 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
440 (*------------------------------------*)
441 (* (*default_print_depth 13*) get_calc 1;
443 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
444 (*calc-head of subproblem*)
445 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
446 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
447 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
448 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
449 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
450 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
451 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
452 (*solve-phase of the subproblem*)
453 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
454 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
455 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
456 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
457 (*finish subproblem*)
458 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
460 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
462 (*this checks the test for correctness..*)
463 val ((pt,_),_) = get_calc 1;
465 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
466 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
467 error "FE-interface.sml: diff.behav. in miniscript with mini-subpb";
471 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
472 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
473 "--------- solve_linear as rootpbl AUTO CompleteCalc ----";
474 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
476 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
478 ["LINEAR","univariate","equation","test"],
479 ["Test","solve_linear"]))];
482 getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 999 false;
484 autoCalculate 1 CompleteCalc;
485 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
486 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
488 val ((pt,_),_) = get_calc 1;
490 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
491 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
492 error "FE-interface.sml: diff.behav. in solve_linear/rt AUTOCALCULATE ";
495 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
496 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
497 "--------- solve_linear as rootpbl AUTO CompleteHead/Eval ";
498 (* ERROR: error in kernel ?? *)
500 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
502 ["LINEAR","univariate","equation","test"],
503 ["Test","solve_linear"]))];
507 autoCalculate 1 CompleteCalcHead;
508 refFormula 1 (get_pos 1 1);
509 val ((pt,p),_) = get_calc 1;
511 autoCalculate 1 CompleteCalc;
512 val ((pt,p),_) = get_calc 1;
513 if p=([], Res) then () else
514 error "FE-interface.sml: diff.behav. in solve_linear AUTOC Head/Eval ";
517 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
518 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
519 "--------- mini-subpbl AUTOCALCULATE CompleteCalc -------";
520 (*WN120210?not ME:\label{SPECIFY:START:auto} UC 30.2.4.2 p.174*)
521 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
522 ("Test", ["sqroot-test","univariate","equation","test"],
523 ["Test","squ-equ-test-subpbl1"]))];
526 autoCalculate 1 CompleteCalc;
527 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
529 getTactic 1 ([1],Frm);
530 getTactic 1 ([1],Res);
531 initContext 1 Ptool.Thy_ ([1],Res);
533 (*... returns calcChangedEvent with*)
534 val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));
535 getFormulaeFromTo 1 unc gen 0 (*only result*) false;
536 getFormulaeFromTo 1 unc gen 1 (*only level 1*) false;
537 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
539 val ((pt,_),_) = get_calc 1;
541 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
542 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
543 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
546 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
547 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
548 "--------- mini-subpbl AUTO CompleteCalcHead ------------";
549 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
550 ("Test", ["sqroot-test","univariate","equation","test"],
551 ["Test","squ-equ-test-subpbl1"]))];
554 autoCalculate 1 CompleteCalcHead;
556 val ((Nd (PblObj {fmz = (fm, ("Test", pblID, metID)), loc = (SOME (env, ctxt1), NONE),
558 spec = ("Test", ["sqroot-test", "univariate", "equation", "test"],
559 ["Test", "squ-equ-test-subpbl1"]),
560 probl, branch = TransitiveB, origin, ostate = Incomplete, result}, []),
561 ([], Met)), []) = get_calc 1;
562 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
563 else error "--- mini-subpbl AUTO CompleteCalcHead ---";
566 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
567 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
568 "--------- solve_linear as rootpbl AUTO CompleteModel ---";
571 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
573 ["LINEAR","univariate","equation","test"],
574 ["Test","solve_linear"]))];
577 autoCalculate 1 CompleteModel;
578 refFormula 1 (get_pos 1 1);
580 setProblem 1 ["LINEAR","univariate","equation","test"];
581 val pos = get_pos 1 1;
582 setContext 1 pos (Ptool.kestoreID2guh Ptool.Pbl_["LINEAR","univariate","equation","test"]);
583 refFormula 1 (get_pos 1 1);
585 setMethod 1 ["Test","solve_linear"];
586 setContext 1 pos (Ptool.kestoreID2guh Ptool.Met_ ["Test","solve_linear"]);
587 refFormula 1 (get_pos 1 1);
588 val ((pt,_),_) = get_calc 1;
589 if get_obj g_spec pt [] = ("empty_thy_id",
590 ["LINEAR", "univariate","equation","test"],
591 ["Test","solve_linear"]) then ()
592 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
594 autoCalculate 1 CompleteCalcHead;
595 refFormula 1 (get_pos 1 1);
596 autoCalculate 1 CompleteCalc;
600 refFormula 1 (get_pos 1 1);
601 val ((pt,_),_) = get_calc 1;
603 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
604 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
605 error "FE-interface.sml: diff.behav. in mini-subpbl AUTOCALCULATE 6";
608 "--------- setContext..Thy ------------------------------";
609 "--------- setContext..Thy ------------------------------";
610 "--------- setContext..Thy ------------------------------";
612 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
613 ("Test", ["sqroot-test","univariate","equation","test"],
614 ["Test","squ-equ-test-subpbl1"]))];
615 Iterator 1; moveActiveRoot 1;
616 autoCalculate 1 CompleteCalcHead;
617 autoCalculate 1 (Steps 1);
618 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
620 setNextTactic 1 (Rewrite_Set "Test_simplify"); (*--> "thy_isac_Test-rls-Test_simplify"*)
621 autoCalculate 1 (Steps 1);
622 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
624 "-----^^^^^ and vvvvv do the same -----";
625 setContext 1 p "thy_isac_Test-rls-Test_simplify";
626 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; (*2 lines, OK*)
628 autoCalculate 1 (Steps 1);
629 setContext 1 p "thy_isac_Test-rls-Test_simplify";
630 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
631 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
632 if p = ([1], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "x + 1 + -1 * 2 = 0"
633 then () else error "--- setContext..Thy --- autoCalculate 1 (Steps 1) #1";
635 autoCalculate 1 CompleteCalc;
636 val (((pt,_),_), p) = (get_calc 1, get_pos 1 1);
637 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
639 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then ()
640 else error "--- setContext..Thy --- autoCalculate CompleteCalc";
643 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
644 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
645 "--------- mini-subpbl AUTOCALC CompleteToSubpbl --------";
647 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
648 ("Test", ["sqroot-test","univariate","equation","test"],
649 ["Test","squ-equ-test-subpbl1"]))];
650 Iterator 1; moveActiveRoot 1;
651 autoCalculate 1 CompleteToSubpbl;
652 refFormula 1 (get_pos 1 1); (*<ISA> -1 + x = 0 </ISA>*);
653 val ((pt,_),_) = get_calc 1;
654 val str = pr_ctree pr_short pt;
656 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
658 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl-1";
660 autoCalculate 1 (Steps 1); (*proceeds only, if NOT 1 step before subplb*)
661 autoCalculate 1 CompleteToSubpbl;
662 val ((pt,_),_) = get_calc 1;
663 val str = pr_ctree pr_short pt;
665 autoCalculate 1 CompleteCalc; (*das geht ohnehin !*);
666 val ((pt,_),_) = get_calc 1;
669 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
670 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
671 error "FE-interface.sml: diff.behav. in mini-subpbl CompleteToSubpbl 1";
674 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
675 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
676 "--------- rat-eq + subpbl: no_met, NO solution dropped -";
677 "--------- rat-eq + subpbl: no_met, NO solution dropped - see LI: '--- simpl.rat.term, '..";
678 (*--- THIS IS RE-USED WITH fun me IN test/../MathEngine/solve.sml -------------------
679 ---- rat-eq + subpbl: set_found in check_tac1 ----*)
681 [(["equality ((5*x)/(x - 2) - x/(x+2)=(4::real))", "solveFor x","solutions L"],
682 ("RatEq", ["univariate","equation"], ["no_met"]))];
685 fetchProposedTactic 1;
687 setNextTactic 1 (Model_Problem);
688 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
690 setNextTactic 1 (Specify_Theory "RatEq");
691 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
692 setNextTactic 1 (Specify_Problem ["rational","univariate","equation"]);
693 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
694 setNextTactic 1 (Specify_Method ["RatEq","solve_rat_equation"]);
695 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
696 setNextTactic 1 (Apply_Method ["RatEq","solve_rat_equation"]);
697 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
698 setNextTactic 1 (Rewrite_Set "RatEq_simplify");
699 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
700 setNextTactic 1 (Rewrite_Set "norm_Rational");
701 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
702 setNextTactic 1 (Rewrite_Set "RatEq_eliminate");
703 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
704 (* __________ for "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)"*)
705 setNextTactic 1 (Subproblem ("PolyEq", ["normalise","polynomial",
706 "univariate","equation"]));
707 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
708 setNextTactic 1 (Model_Problem );
709 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
710 setNextTactic 1 (Specify_Theory "PolyEq");
711 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
712 setNextTactic 1 (Specify_Problem ["normalise","polynomial",
713 "univariate","equation"]);
714 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
715 setNextTactic 1 (Specify_Method ["PolyEq","normalise_poly"]);
716 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
717 setNextTactic 1 (Apply_Method ["PolyEq","normalise_poly"]);
718 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
719 setNextTactic 1 (Rewrite ("all_left", ThmC.numerals_to_Free @{thm all_left}));
720 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
721 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "make_ratpoly_in"));
722 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
723 (* __________ for "16 + 12 * x = 0"*)
724 setNextTactic 1 (Subproblem ("PolyEq",
725 ["degree_1","polynomial","univariate","equation"]));
726 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
727 setNextTactic 1 (Model_Problem );
728 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
729 setNextTactic 1 (Specify_Theory "PolyEq");
730 (*------------- some trials in the problem-hierarchy ---------------*)
731 setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
732 autoCalculate 1 (Steps 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
733 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
734 (*------------------------------------------------------------------*)
735 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
736 setNextTactic 1 (Specify_Method ["PolyEq","solve_d1_polyeq_equation"]);
737 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
738 setNextTactic 1 (Apply_Method ["PolyEq","solve_d1_polyeq_equation"]);
739 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
740 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "d1_polyeq_simplify"));
741 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
742 setNextTactic 1 (Rewrite_Set "polyeq_simplify");
743 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
744 setNextTactic 1 Or_to_List;
745 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
746 setNextTactic 1 (Check_elementwise "Assumptions");
747 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
748 setNextTactic 1 (Check_Postcond ["degree_1","polynomial",
749 "univariate","equation"]);
750 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
751 setNextTactic 1 (Check_Postcond ["normalise","polynomial",
752 "univariate","equation"]);
753 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
754 setNextTactic 1 (Check_Postcond ["rational","univariate","equation"]);
755 val (ptp,_) = get_calc 1;
756 val (Form t,_,_) = ME_Misc.pt_extract ptp;
757 if get_pos 1 1 = ([], Res) andalso UnparseC.term t = "[x = -4 / 3]" then ()
758 else writeln "FE-inteface.sml: diff.behav. in rat-eq + subpbl: no_met, NO ..";
762 "--------- tryMatchProblem, tryRefineProblem ------------";
763 "--------- tryMatchProblem, tryRefineProblem ------------";
764 "--------- tryMatchProblem, tryRefineProblem ------------";
765 (*{\bf\UC{Having \isac{} Refine the Problem
766 * Automatically}\label{SPECIFY:refine-auto}\\} test match and refine with
767 * x^^^2 + 4*x + 5 = 2
768 see isac.bridge.TestSpecify#testMatchRefine*)
771 [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
773 ["univariate","equation"],
778 fetchProposedTactic 1;
779 setNextTactic 1 (Model_Problem );
780 (*..this tactic should be done 'tacitly', too !*)
783 autoCalculate 1 CompleteCalcHead;
784 checkContext 1 ([],Pbl) "pbl_equ_univ";
785 checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate","equation"]);
788 autoCalculate 1 (Steps 1);
790 fetchProposedTactic 1;
791 setNextTactic 1 (Add_Given "equality (x ^^^ 2 + 4 * x + 5 = (2::real))");
792 autoCalculate 1 (Steps 1);
794 "--------- we go into the ProblemBrowser (_NO_ pblID selected) -";
795 initContext 1 Ptool.Pbl_ ([],Pbl);
796 (* this would break if a calculation would be inserted before: CALCID...
797 and pattern matching is not available in *.java.
798 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"
799 then () else error "--- tryMatchProblem, tryRefineProblem: initContext 1 Ptool.Pbl_ ([],Pbl); CHANGED";
801 initContext 1 Ptool.Met_ ([],Pbl);
802 (*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 33</ERROR></SYSERROR>*)
804 "--------- this match will show some incomplete items: ---------";
806 checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate","equation"]);
807 checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Met_ ["LinEq", "solve_lineq_equation"]);
810 fetchProposedTactic 1;
811 setNextTactic 1 (Add_Given "solveFor x"); autoCalculate 1 (Steps 1);
813 fetchProposedTactic 1;
814 setNextTactic 1 (Add_Find "solutions L"); autoCalculate 1 (Steps 1);
816 "--------- this is a matching model (all items correct): -------";
817 checkContext 1 ([],Pbl) (Ptool.kestoreID2guh Ptool.Pbl_ ["univariate","equation"]);
818 "--------- this is a NOT matching model (some 'false': ---------";
819 checkContext 1 ([],Pbl)(Ptool.kestoreID2guh Ptool.Pbl_ ["LINEAR","univariate","equation"]);
821 "--------- find out a matching problem: ------------------------";
822 "--------- find out a matching problem (FAILING: no new pbl) ---";
823 refineProblem 1([],Pbl)(Ptool.pblID2guh ["LINEAR","univariate","equation"]);
825 "--------- find out a matching problem (SUCCESSFUL) ------------";
826 refineProblem 1 ([],Pbl) (Ptool.pblID2guh ["univariate","equation"]);
828 "--------- tryMatch, tryRefine did not change the calculation -";
829 "--------- this is done by <TRANSFER> on the pbl-browser: ------";
830 setNextTactic 1 (Specify_Problem ["normalise","polynomial",
831 "univariate","equation"]);
832 autoCalculate 1 (Steps 1);
833 (*WN050904 fetchProposedTactic again --> Specify_Problem ["normalise",...
834 and Specify_Theory skipped in comparison to below ---^^^-inserted *)
835 (*------------vvv-inserted-----------------------------------------------*)
836 fetchProposedTactic 1;
837 (*/-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------\* )
838 setNextTactic 1 (Specify_Problem ["normalise","polynomial",
839 "univariate","equation"]);
840 autoCalculate 1 (Steps 1);
842 (*and Specify_Theory skipped by fetchProposedTactic ?!?*)
844 fetchProposedTactic 1;
845 setNextTactic 1 (Specify_Method ["PolyEq","normalise_poly"]);
846 autoCalculate 1 (Steps 1);
848 fetchProposedTactic 1;
849 setNextTactic 1 (Apply_Method ["PolyEq","normalise_poly"]);
851 autoCalculate 1 CompleteCalc;
853 val ((pt,_),_) = get_calc 1;
854 Test_Tool.show_pt pt;
856 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
857 if UnparseC.term f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
858 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
860 (*------------^^^-inserted-----------------------------------------------*)
861 (*WN050904 the fetchProposedTactic's below may not have worked like that
862 before, too, because there was no check*)
863 fetchProposedTactic 1;
864 setNextTactic 1 (Specify_Theory "PolyEq");
865 autoCalculate 1 (Steps 1);
867 fetchProposedTactic 1;
868 setNextTactic 1 (Specify_Method ["PolyEq","normalise_poly"]);
869 autoCalculate 1 (Steps 1);
871 fetchProposedTactic 1;
872 "--------- now the calc-header is ready for enter 'solving' ----";
873 autoCalculate 1 CompleteCalc;
875 val ((pt,_),_) = get_calc 1;
877 Test_Tool.show_pt pt;
879 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
880 if UnparseC.term f = "[x = -1, x = -3]" andalso p = ([], Res) then () else
881 error "FE-interface.sml: diff.behav. in tryMatchProblem, tryRefine";
883 ( *\-----ERROR INTRODUCED BY CHILD OF 33913fe24685 --------------------------------------------/*)
885 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
886 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
887 "--------- modifyCalcHead, resetCalcHead, modelProblem --";
889 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
890 ("Test", ["sqroot-test","univariate","equation","test"],
891 ["Test","squ-equ-test-subpbl1"]))];
895 modifyCalcHead 1 (([],Pbl),(*the position from refFormula*)
896 "solve (x+1=2, x)",(*the headline*)
897 [P_Spec.Given ["equality (x+1=(2::real))", "solveFor x"],
898 P_Spec.Find ["solutions L"](*,P_Spec.Relate []*)],
901 ["sqroot-test","univariate","equation","test"],
902 ["Test","squ-equ-test-subpbl1"]));
904 val ((Nd (PblObj {fmz = (fm, tpm),
905 loc = (SOME scrst_ctxt, NONE),
909 ["sqroot-test", "univariate", "equation", "test"],
910 ["Test", "squ-equ-test-subpbl1"]),
912 branch = TransitiveB,
919 (*WN110622: is the same as in 2002, but shouldn't be probl = [3 items?]*)
920 if length meth = 0 andalso length probl = 0 (*just some items tested*) then ()
921 else error "--- modifyCalcHead, resetCalcHead, modelProblem 1 --";
927 val ((Nd (PblObj {fmz = (fm, tpm),
928 loc = (SOME scrst_ctxt, NONE),
931 spec = ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]),
933 branch = TransitiveB,
940 if length meth = 3 andalso length probl = 3 (*just some items tested*) then ()
941 else error "--- modifyCalcHead, resetCalcHead, modelProblem 2 --";
943 "--------- maximum-example, UC: Modeling an example -----";
944 "--------- maximum-example, UC: Modeling an example -----";
945 "--------- maximum-example, UC: Modeling an example -----";
946 (* {\bf\UC{Editing the Model}\label{SPECIFY:enter}\label{SPECIFY:check}\\}
947 see isac.bridge.TestModel#testEditItems
949 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
950 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
951 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
952 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
953 (*^^^ these are the elements for the root-problem (in variants)*)
954 (*vvv these are elements required for subproblems*)
955 "boundVariable a","boundVariable b","boundVariable alpha",
956 "interval {x::real. 0 <= x & x <= 2*r}",
957 "interval {x::real. 0 <= x & x <= 2*r}",
958 "interval {x::real. 0 <= x & x <= pi}",
959 "errorBound (eps=(0::real))"]
960 (*specifying is not interesting for this example*)
961 val spec = ("DiffApp", ["maximum_of","function"],
962 ["DiffApp","max_by_calculus"]);
963 (*the empty model with descriptions for user-guidance by Model_Problem*)
964 val empty_model = [P_Spec.Given ["fixedValues []"],
965 P_Spec.Find ["maximum", "valuesFor"],
966 P_Spec.Relate ["relations []"]];
969 "#################################################################";
971 CalcTree [(elems, spec)];
974 refFormula 1 (get_pos 1 1);
975 (*this gives a completely empty model*)
977 fetchProposedTactic 1;
978 (*fill the CalcHead with Descriptions...*)
979 setNextTactic 1 (Model_Problem );
980 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
982 (*user input is !!!!!EITHER!!!!! _some_ (at least one) items of the model
983 !!!!!OR!!!!! _one_ part of the specification !!!!!!!!!!!!!*)
984 (*input of two items, 'fixedValues [r=Arbfix]' and 'maximum b'...*)
985 modifyCalcHead 1 (([],Pbl) (*position, from previous refFormula*),
986 "Problem (DiffApp.thy, [maximum_of, function])",
987 (*the head-form ^^^ is not used for input here*)
988 [P_Spec.Given ["fixedValues [r=Arbfix]"(*new input*)],
989 P_Spec.Find ["maximum b"(*new input*), "valuesFor"],
990 P_Spec.Relate ["relations"]],
991 (*input (Arbfix will dissappear soon)*)
993 References.empty (*no input to the specification*));
995 (*the user does not know, what 'superfluous' for 'maximum b' may mean
996 and asks what to do next*)
997 fetchProposedTactic 1;
998 (*the student follows the advice*)
999 setNextTactic 1 (Add_Find "maximum A"); (*FIXME.17.11.03: does not yet work*)
1000 autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1);
1002 (*this input completes the model*)
1003 modifyCalcHead 1 (([],Pbl), "not used here",
1004 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1005 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1006 P_Spec.Relate ["relations [A=a*b, \
1007 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, References.empty);
1009 (*specification is not interesting and should be skipped by the dialogguide;
1010 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
1011 modifyCalcHead 1 (([],Pbl), "not used here",
1012 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1013 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1014 P_Spec.Relate ["relations [A=a*b, \
1015 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1016 ("DiffApp", ["empty_probl_id"], ["empty_meth_id"]));
1017 modifyCalcHead 1 (([],Pbl), "not used here",
1018 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1019 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1020 P_Spec.Relate ["relations [A=a*b, \
1021 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1022 ("DiffApp", ["maximum_of","function"],
1023 ["empty_meth_id"]));
1024 modifyCalcHead 1 (([],Pbl), "not used here",
1025 [P_Spec.Given ["fixedValues [r=Arbfix]"],
1026 P_Spec.Find ["maximum A", "valuesFor [a,b]"(*new input*)],
1027 P_Spec.Relate ["relations [A=a*b, \
1028 \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl,
1029 ("DiffApp", ["maximum_of","function"],
1030 ["DiffApp","max_by_calculus"]));
1031 (*this final calcHead now has STATUS 'complete' !*)
1034 "--------- solve_linear from pbl-hierarchy --------------";
1035 "--------- solve_linear from pbl-hierarchy --------------";
1036 "--------- solve_linear from pbl-hierarchy --------------";
1038 val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], []));
1039 CalcTree [(fmz, sp)];
1040 Iterator 1; moveActiveRoot 1;
1041 refFormula 1 (get_pos 1 1);
1042 modifyCalcHead 1 (([],Pbl),"solve (1+-1*2+x=(0::real))",
1043 [P_Spec.Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
1044 P_Spec.Find ["solutions L"]],
1046 ("Test", ["LINEAR","univariate","equation","test"],
1047 ["Test","solve_linear"]));
1048 autoCalculate 1 CompleteCalc;
1049 refFormula 1 (get_pos 1 1);
1050 val ((pt,_),_) = get_calc 1;
1051 val p = get_pos 1 1;
1052 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1053 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1054 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 1";
1057 "--------- solve_linear as in an algebra system (CAS)----";
1058 "--------- solve_linear as in an algebra system (CAS)----";
1059 "--------- solve_linear as in an algebra system (CAS)----";
1060 (*WN120210?not ME:\label{UC:cas-input} UC 30.1.2.5 p.168*)
1062 val (fmz, sp) = ([], ("", [], []));
1063 CalcTree [(fmz, sp)];
1064 Iterator 1; moveActiveRoot 1;
1065 modifyCalcHead 1 (([],Pbl),"solveTest (1+-1*2+x=0,x)", [], Pbl, ("", [], []));
1066 autoCalculate 1 CompleteCalc;
1067 refFormula 1 (get_pos 1 1);
1068 val ((pt,_),_) = get_calc 1;
1069 val p = get_pos 1 1;
1070 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1071 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) andalso map UnparseC.term asms = [] then ()
1072 else error "FE-interface.sml: diff.behav. in from pbl -hierarchy 2";
1075 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1076 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1077 "--------- interSteps: on 'miniscript with mini-subpbl' -";
1078 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1079 ("Test", ["sqroot-test","univariate","equation","test"],
1080 ["Test","squ-equ-test-subpbl1"]))];
1083 autoCalculate 1 CompleteCalc;
1084 val ((pt,_),_) = get_calc 1;
1085 Test_Tool.show_pt pt;
1087 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1088 interSteps 1 ([2],Res);
1089 val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt (*new ([2,1],Frm)..([2,6],Res)*);
1090 val (unc, del, gen) = (([1],Res),([1],Res),([2,6],Res));
1091 getFormulaeFromTo 1 unc gen 1 false;
1093 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1094 interSteps 1 ([3,2],Res);
1095 val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt (*new ([3,2,1],Frm)..([3,2,2],Res)*);
1096 val (unc, del, gen) = (([3,1],Res),([3,1],Res),([3,2,2],Res));
1097 getFormulaeFromTo 1 unc gen 1 false;
1099 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1100 interSteps 1 ([3],Res) (*no new steps in subproblems*);
1101 val (unc, del, gen) = (([3],Pbl),([3],Pbl),([3,2],Res));
1102 getFormulaeFromTo 1 unc gen 1 false;
1104 (*UC\label{UC:inter-steps} UC 30.3.5.5 p.178*)
1105 interSteps 1 ([],Res) (*no new steps in subproblems*);
1106 val (unc, del, gen) = (([],Pbl),([],Pbl),([4],Res));
1107 getFormulaeFromTo 1 unc gen 1 false;
1110 "--------- getTactic, fetchApplicableTactics ------------";
1111 "--------- getTactic, fetchApplicableTactics ------------";
1112 "--------- getTactic, fetchApplicableTactics ------------";
1113 (* compare test/../script.sml
1114 "----------- fun from_prog ---------------------------------------";
1116 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1117 ("Test", ["sqroot-test","univariate","equation","test"],
1118 ["Test","squ-equ-test-subpbl1"]))];
1119 Iterator 1; moveActiveRoot 1;
1120 autoCalculate 1 CompleteCalc;
1121 val ((pt,_),_) = get_calc 1;
1122 Test_Tool.show_pt pt;
1124 (*UC\label{SOLVE:HIDE:getTactic} \label{SOLVE:AUTO:tactic} UC 30.3.3.1 p.176
1125 WN120210 not impl. in FE*)
1126 getTactic 1 ([],Pbl);
1127 getTactic 1 ([1],Res);
1128 getTactic 1 ([3],Pbl);
1129 getTactic 1 ([3,1],Frm);
1130 getTactic 1 ([3],Res);
1131 getTactic 1 ([],Res);
1133 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
1134 fetchApplicableTactics 1 99999 ([],Pbl);
1135 fetchApplicableTactics 1 99999 ([1],Res);
1136 fetchApplicableTactics 1 99999 ([3],Pbl);
1137 fetchApplicableTactics 1 99999 ([3,1],Res);
1138 fetchApplicableTactics 1 99999 ([3],Res);
1139 fetchApplicableTactics 1 99999 ([],Res);
1142 "--------- getAssumptions, getAccumulatedAsms -----------";
1143 "--------- getAssumptions, getAccumulatedAsms -----------";
1144 "--------- getAssumptions, getAccumulatedAsms -----------";
1146 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
1147 "solveFor x","solutions L"],
1148 ("RatEq",["univariate","equation"],["no_met"]))];
1149 Iterator 1; moveActiveRoot 1;
1150 autoCalculate 1 CompleteCalc;
1151 val ((pt,_),_) = get_calc 1;
1152 val p = get_pos 1 1;
1153 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1154 (*============ inhibit exn WN120316 compare 2002--2011 ===========================
1155 if map UnparseC.term asms =
1156 ["True |\n~ lhs ((3 + -1 * x + x ^^^ 2) * x =\n" ^
1157 " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x", "-6 * x + 5 * x ^^^ 2 = 0",
1158 "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
1159 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
1160 "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]
1161 andalso UnparseC.term f = "[-6 * x + 5 * x ^^^ 2 = 0]" andalso p = ([], Res) then ()
1162 else error "TODO compare 2002--2011"; (*...data during test --- x / (x ^ 2 - 6 * x + 9) - 1...*)
1163 ============ inhibit exn WN120316 compare 2002--2011 ===========================*)
1165 if p = ([], Res) andalso UnparseC.term f = "[x = 6 / 5]"
1166 andalso map UnparseC.term asms = []
1167 then () else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1169 (*UC\label{SOLVE:HELP:assumptions} UC 30.3.5.1 p.178*)
1170 getAssumptions 1 ([3], Res);
1171 getAssumptions 1 ([5], Res);
1172 (*UC\label{SOLVE:HELP:assumptions-origin} UC 30.3.5.2 p.178
1173 WN0502 still without positions*)
1174 getAccumulatedAsms 1 ([3], Res);
1175 getAccumulatedAsms 1 ([5], Res);
1178 "--------- arbitrary combinations of steps --------------";
1179 "--------- arbitrary combinations of steps --------------";
1180 "--------- arbitrary combinations of steps --------------";
1181 CalcTree (*start of calculation, return No.1*)
1182 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
1184 ["LINEAR","univariate","equation","test"],
1185 ["Test","solve_linear"]))];
1186 Iterator 1; moveActiveRoot 1;
1188 fetchProposedTactic 1;
1189 (*ERROR get_calc 1 not existent*)
1190 setNextTactic 1 (Model_Problem );
1191 autoCalculate 1 (Steps 1);
1192 fetchProposedTactic 1;
1193 fetchProposedTactic 1;
1195 setNextTactic 1 (Add_Find "solutions L");
1196 setNextTactic 1 (Add_Find "solutions L");
1198 autoCalculate 1 (Steps 1);
1199 autoCalculate 1 (Steps 1);
1201 setNextTactic 1 (Specify_Theory "Test");
1202 fetchProposedTactic 1;
1203 autoCalculate 1 (Steps 1);
1205 autoCalculate 1 (Steps 1);
1206 autoCalculate 1 (Steps 1);
1207 autoCalculate 1 (Steps 1);
1208 autoCalculate 1 (Steps 1);
1209 (*------------------------- end calc-head*)
1211 fetchProposedTactic 1;
1212 setNextTactic 1 (Rewrite_Set_Inst (["(''bdv'',x)"], "isolate_bdv"));
1213 autoCalculate 1 (Steps 1);
1215 setNextTactic 1 (Rewrite_Set "Test_simplify");
1216 fetchProposedTactic 1;
1217 autoCalculate 1 (Steps 1);
1219 autoCalculate 1 CompleteCalc;
1220 val ((pt,_),_) = get_calc 1;
1221 val p = get_pos 1 1;
1222 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1223 if UnparseC.term f = "[x = 1]" andalso p = ([], Res) then () else
1224 error "FE-interface.sml: diff.behav. in combinations of steps";
1227 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right"; (*UC 30.3.2.4 p.175*)
1228 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1229 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}right";
1230 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1231 ("Test", ["sqroot-test","univariate","equation","test"],
1232 ["Test","squ-equ-test-subpbl1"]))];
1235 autoCalculate 1 CompleteCalcHead;
1236 autoCalculate 1 (Steps 1);
1237 autoCalculate 1 (Steps 1);
1238 appendFormula 1 "-1 + x = 0" (*|> Future.join*);
1239 (*... returns calcChangedEvent with*)
1240 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1241 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1243 val ((pt,_),_) = get_calc 1;
1244 val p = get_pos 1 1;
1245 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1246 if UnparseC.term f = "-1 + x = 0" andalso p = ([2], Res) then () else
1247 error "FE-interface.sml: diff.behav. in FORMULA:enter} right";
1250 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other"; (*UC 30.3.2.4 p.175*)
1251 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1252 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}other";
1253 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1254 ("Test", ["sqroot-test","univariate","equation","test"],
1255 ["Test","squ-equ-test-subpbl1"]))];
1258 autoCalculate 1 CompleteCalcHead;
1259 autoCalculate 1 (Steps 1);
1260 autoCalculate 1 (Steps 1);
1261 appendFormula 1 "x - 1 = 0" (*|> Future.join*);
1262 val (unc, del, gen) = (([1],Res), ([1],Res), ([2],Res));
1263 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1266 val ((pt,_),_) = get_calc 1;
1267 val p = get_pos 1 1;
1268 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1269 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1270 error "FE-interface.sml: diff.behav. in FORMULA:enter} other";
1273 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2"; (*UC 30.3.2.4 p.175*)
1274 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1275 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}oth 2";
1276 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1277 ("Test", ["sqroot-test","univariate","equation","test"],
1278 ["Test","squ-equ-test-subpbl1"]))];
1281 autoCalculate 1 CompleteCalcHead;
1282 autoCalculate 1 (Steps 1);
1283 autoCalculate 1 (Steps 1);
1284 appendFormula 1 "x = 1" (*|> Future.join*);
1285 (*... returns calcChangedEvent with*)
1286 val (unc, del, gen) = (([1],Res), ([1],Res), ([3,2],Res));
1287 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1290 val ((pt,_),_) = get_calc 1;
1291 val p = get_pos 1 1;
1292 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1293 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1294 error "FE-interface.sml: diff.behav. in FORMULA:enter} oth 2";
1297 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok"; (*UC 30.3.2.4 p.175*)
1298 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1299 "--------- appendF label{SOLVE:MANUAL:FORMULA:enter}NOTok";
1300 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1301 ("Test", ["sqroot-test","univariate","equation","test"],
1302 ["Test","squ-equ-test-subpbl1"]))];
1305 autoCalculate 1 CompleteCalcHead;
1306 autoCalculate 1 (Steps 1);
1307 autoCalculate 1 (Steps 1);
1308 appendFormula 1 "x - 4711 = 0" (*|> Future.join*);
1309 (*... returns <ERROR> no derivation found </ERROR>*)
1311 val ((pt,_),_) = get_calc 1;
1312 val p = get_pos 1 1;
1313 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1314 if UnparseC.term f = "x + 1 + -1 * 2 = 0" andalso p = ([1], Res) then () else
1315 error "FE-interface.sml: diff.behav. in FORMULA:enter} NOTok";
1318 "--------- replaceFormula {SOL:MAN:FOR:replace} right----"; (*UC 30.3.2.5 p.176*)
1319 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1320 "--------- replaceFormula {SOL:MAN:FOR:replace} right----";
1321 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1322 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1323 ("Test", ["sqroot-test","univariate","equation","test"],
1324 ["Test","squ-equ-test-subpbl1"]))];
1327 autoCalculate 1 CompleteCalc;
1328 moveActiveFormula 1 ([2],Res);
1329 replaceFormula 1 "-1 + x = 0" (*i.e. repeats input*);
1330 (*... returns <ERROR> formula not changed </ERROR>*)
1332 val ((pt,_),_) = get_calc 1;
1333 val p = get_pos 1 1;
1334 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1335 if UnparseC.term f = "-1 + x = 0" andalso p = ([2], Res) then () else
1336 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1337 if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1338 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1339 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1340 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
1342 (*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
1343 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1344 ("Test", ["sqroot-test","univariate","equation","test"],
1345 ["Test","squ-equ-test-subpbl1"]))];
1348 autoCalculate 2 CompleteCalc;
1349 moveActiveFormula 2 ([2],Res);
1350 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
1351 (*... returns <ERROR> formula not changed </ERROR>*)
1353 val ((pt,_),_) = get_calc 2;
1354 val p = get_pos 2 1;
1355 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1356 if UnparseC.term f = "-1 + x = 0" andalso p = ([2], Res) then () else
1357 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 1";
1358 if map fst3 (ME_Misc.get_interval ([2],Res) ([],Res) 9999 pt) =
1359 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
1360 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
1361 error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
1364 "--------- replaceFormula {SOL:MAN:FOR:replace} other----"; (*UC 30.3.2.5 p.176*)
1365 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1366 "--------- replaceFormula {SOL:MAN:FOR:replace} other----";
1367 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1368 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1369 ("Test", ["sqroot-test","univariate","equation","test"],
1370 ["Test","squ-equ-test-subpbl1"]))];
1373 autoCalculate 1 CompleteCalc;
1374 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1375 replaceFormula 1 "x - 1 = 0"; (*<-------------------------------------*)
1376 (*... returns calcChangedEvent with*)
1377 val (unc, del, gen) = (([1],Res), ([4],Res), ([2],Res));
1378 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1380 val ((pt,_),_) = get_calc 1;
1381 Test_Tool.show_pt pt;
1382 val p = get_pos 1 1;
1383 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1384 if UnparseC.term f = "x - 1 = 0" andalso p = ([2], Res) then () else
1385 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 1";
1386 (* for getting the list in whole length ...
1387 (*default_print_depth 99*) map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt); (*default_print_depth 3*)
1389 if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1390 [([1], Res), ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1391 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2, 7], Res),
1392 ([2, 8], Res), ([2, 9], Res), ([2], Res)] then () else
1393 error "FE-interface.sml: diff.behav. in FORMULA:replace} other 2";
1396 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--"; (*UC 30.3.2.5 p.176*)
1397 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1398 "--------- replaceFormula {SOL:MAN:FOR:replace} other 2--";
1399 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1400 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1401 ("Test", ["sqroot-test","univariate","equation","test"],
1402 ["Test","squ-equ-test-subpbl1"]))];
1405 autoCalculate 1 CompleteCalc;
1406 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1407 replaceFormula 1 "x = 1"; (*<-------------------------------------*)
1408 (*... returns calcChangedEvent with ...*)
1409 val (unc, del, gen) = (([1],Res), ([4],Res), ([3,2],Res));
1410 getFormulaeFromTo 1 unc gen 99999 (*all levels*) false;
1413 val ((pt,_),_) = get_calc 1;
1414 Test_Tool.show_pt pt; (*error: ...ME_Misc.get_interval drops ([3,2],Res) ...*)
1415 val (t,_) = get_obj g_result pt [3,2]; UnparseC.term t;
1416 if map fst3 (ME_Misc.get_interval ([1],Res) ([],Res) 9999 pt) =
1417 [([1], Res), ([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res),
1418 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1419 ([3,2],Res)] then () else
1420 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 1";
1422 val p = get_pos 1 1;
1423 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1424 if UnparseC.term f = "x = 1" andalso p = ([3,2], Res) then () else
1425 error "FE-interface.sml: diff.behav. in FORMULA:replace} oth2 2";
1428 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----"; (*UC 30.3.2.5 p.176*)
1429 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1430 "--------- replaceFormula {SOL:MAN:FOR:replace} NOTok----";
1431 (*\label{SOLVE:MANUAL:FORMULA:replace}*)
1432 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1433 ("Test", ["sqroot-test","univariate","equation","test"],
1434 ["Test","squ-equ-test-subpbl1"]))];
1437 autoCalculate 1 CompleteCalc;
1438 moveActiveFormula 1 ([2],Res); (*there is "-1 + x = 0"*)
1439 replaceFormula 1 "x - 4711 = 0";
1440 (*... returns <ERROR> no derivation found </ERROR>*)
1442 val ((pt,_),_) = get_calc 1;
1443 Test_Tool.show_pt pt;
1444 val p = get_pos 1 1;
1445 val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p);
1446 if UnparseC.term f = "-1 + x = 0" andalso p = ([2], Res) then () else
1447 error "FE-interface.sml: diff.behav. in FORMULA:replace} NOTok";
1450 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1451 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1452 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
1454 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
1455 ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
1458 autoCalculate 1 CompleteCalcHead;
1459 autoCalculate 1 (Steps 1);
1460 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
1461 appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*); (*<<<<<<<=========================*)
1462 (* the check for errpat is maximally liberal (whole term modulo "nrls" from "type met"),
1463 would recognize "cos (4 * x ^ (4 - 1)) + 2 * x" as well.
1464 results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
1465 instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
1466 val ((pt,pos), _) = get_calc 1;
1467 val p = get_pos 1 1;
1468 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1470 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"
1471 then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
1472 ("diff_sum", thm)) => () | _ => error "embed fun fill_form changed 0"
1473 | _ => error "embed fun fill_form changed 1"
1474 else error "embed fun fill_form changed 2";
1476 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ====================
1477 findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
1478 (*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =
1479 d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
1480 val ((pt,pos),_) = get_calc 1;
1481 val p = get_pos 1 1;
1483 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1484 if p = ([1], Res) andalso UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1485 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"(*?!?*)))
1487 else error "embed fun fill_form changed 2";
1489 (* if we assume, that the fill-patterns are ordered such that the 1st has large gaps
1490 and the last has no gaps, then the number of fill-patterns would suffice
1491 for the DialogGuide to select appropriately. *)
1492 requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
1493 (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
1494 val ((pt,pos),_) = get_calc 1;
1495 val p = get_pos 1 1;
1496 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1497 if p = ([1], Res) andalso existpt [2] pt andalso
1498 UnparseC.term f = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
1499 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "Diff.diff_sum"))
1500 then () else error "embed fun fill_form changed 3";
1502 inputFillFormula 1 "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)";(*<<<<<<<=====*)
1503 val ((pt, _),_) = get_calc 1;
1504 val p = get_pos 1 1;
1505 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1506 if p = ([2], Res) andalso
1507 UnparseC.term f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso
1508 get_obj g_tac pt (fst p) = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", ""))
1509 then () else error "inputFillFormula changed 11";
1511 autoCalculate 1 CompleteCalc;
1513 "~~~~~ final check: the input formula is inserted as it would have been correct from beginning";
1514 val ((pt, _),_) = get_calc 1;
1515 val p = get_pos 1 1;
1516 val (Form f, _, asms) = ME_Misc.pt_extract (pt, p);
1517 if p = ([], Res) andalso UnparseC.term f = "2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3"
1518 then () else error "inputFillFormula changed 12";
1519 Test_Tool.show_pt pt;
1521 (([], Frm), Diff (x ^^^ 2 + sin (x ^^^ 4), x)),
1522 (([1], Frm), d_d x (x ^^^ 2 + sin (x ^^^ 4))),
1523 (([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))),
1524 (([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)), (*<<<<<<<=====*)
1525 (([3], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1526 (([4], Res), 2 * x ^^^ (2 - 1) + cos (x ^^^ 4) * (4 * x ^^^ (4 - 1))),
1527 (([5], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3),
1528 (([], Res), 2 * x + cos (x ^^^ 4) * 4 * x ^^^ 3)] *)
1529 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*)
1532 "--------- UC errpat add-fraction, fillpat by input --------------";
1533 "--------- UC errpat add-fraction, fillpat by input --------------";
1534 "--------- UC errpat add-fraction, fillpat by input --------------";
1535 (*cp from BridgeLog Java <=> SML*)
1536 CalcTree [([], ("empty_thy_id", ["empty_probl_id"], ["empty_meth_id"]))];
1539 moveActiveFormula 1 ([],Pbl);
1540 replaceFormula 1 "Simplify (5 * x / (4 * y) + 3 * x / (4 * y))";
1541 autoCalculate 1 CompleteCalcHead;
1542 autoCalculate 1 (Steps 1);
1543 appendFormula 1 "8 * x / (8 * y)" (*|> Future.join*);
1544 (*<CALCMESSAGE> no derivation found </CALCMESSAGE>
1545 --- but in BridgeLog Java <=> SML:
1546 <CALCMESSAGE> error pattern #addition-of-fractions# </CALCMESSAGE>*)
1549 "--------- UC errpat, fillpat step to Rewrite --------------------";
1550 "--------- UC errpat, fillpat step to Rewrite --------------------";
1551 "--------- UC errpat, fillpat step to Rewrite --------------------";
1554 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1555 "differentiateFor x", "derivative f_f'"],
1556 ("Isac_Knowledge", ["derivative_of","function"],
1557 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
1560 autoCalculate 1 CompleteCalc;
1561 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1564 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1565 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1566 "--------- UC errpat, fillpat step to Rewrite_Set ----------------";
1568 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
1569 "differentiateFor x", "derivative f_f'"],
1570 ("Isac_Knowledge", ["derivative_of","function"],
1571 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
1574 autoCalculate 1 CompleteCalcHead;
1575 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1576 autoCalculate 1 (Steps 1); fetchProposedTactic 1;
1579 <CALCID> 1 </CALCID>
1580 <TACTICERRORPATTERNS>
1582 <STRING> chain-rule-diff-both </STRING>
1583 <STRING> cancel </STRING>
1585 <REWRITESETINSTTACTIC name="Rewrite_Set_Inst">
1586 <RULESET> norm_diff </RULESET>
1601 </REWRITESETINSTTACTIC>
1602 </TACTICERRORPATTERNS>
1606 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)
1607 stepToErrorPatterns 1; (*--> calcChanged, rule immediately calls... *)
1608 stepOnErrorPatterns 1; (*--> calcChanged, rule calls getTactic and displays it *)
1609 (* then --- UC errpat, fillpat by input ---*)
1611 autoCalculate 1 CompleteCalc;
1612 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1613 (*WN1208 postponed due to efforts required for stepToErrorPatterns (NEW rewrite_set_)*)