1 (* Title: tests on solve.sml
2 Author: Walther Neuper 060508,
3 (c) due to copyright terms
5 is NOT ONLY dependent on Test, but on other thys:
6 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
7 uses from Rational.ML: Rrls cancel_p, Rrls cancel
9 uses from Poly.ML: Rls make_polynomial, Rls expand_binom
11 use"../smltest/ME/solve.sml";
15 "-----------------------------------------------------------------";
16 "table of contents -----------------------------------------------";
17 "-----------------------------------------------------------------";
18 "--------- interSteps on norm_Rational ---------------------------";
19 (*---vvv NOT working after meNEW.04mmdd*)
20 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
21 "--------- prepare pbl, met --------------------------------------";
22 "-------- cancel, without detail ------------------------------";
23 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
24 "-------------- cancel_p, without detail ------------------------------";
25 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
26 (*---^^^ NOT working*)
27 "on 'miniscript with mini-subpbl':";
28 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
29 "------ interSteps'detailrls' after CompleteCalc -----------------";
30 "------ interSteps after appendFormula ---------------------------";
31 (*---vvv not brought to work 0403*)
32 "------ Detail_Set -----------------------------------------------";
33 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
34 "-----------------------------------------------------------------";
35 "-----------------------------------------------------------------";
36 "-----------------------------------------------------------------";
39 "--------- interSteps on norm_Rational ---------------------------";
40 "--------- interSteps on norm_Rational ---------------------------";
41 "--------- interSteps on norm_Rational ---------------------------";
42 states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
43 CalcTree [(["Term ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
45 ["rational","simplification"],
46 ["simplification","of_rationals"]))];
48 autoCalculate 1 CompleteCalc;
49 val ((pt,_),_) = get_calc 1; show_pt pt;
51 (*with "Script SimplifyScript (t_::real) = -----------------
52 \ ((Rewrite_Set norm_Rational False) t_)"
53 case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
54 | _ => error "solve.sml: interSteps on norm_Rational 1";
55 interSteps 1 ([1], Res);
56 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
57 interSteps 1 ([1,3], Res);
59 getTactic 1 ([1,4], Res) (*here get the tactic, and ...*);
60 interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);
62 getTactic 1 ([1,5,1], Frm);
63 val ((pt,_),_) = get_calc 1; show_pt pt;
65 getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
66 interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
67 --------------------------------------------------------------------*)
69 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
70 | _ => error "solve.sml: interSteps on norm_Rational 1";
71 (*these have been done now by the script ^^^ immediately...
72 interSteps 1 ([1], Res);
73 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
75 interSteps 1 ([6], Res);
77 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
78 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
80 getTactic 1 ([3,4,1], Frm);
81 val ((pt,_),_) = get_calc 1; show_pt pt;
82 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
83 case (term2str form, tac, terms2strs asm) of
84 ("1 / 2", Check_Postcond ["rational", "simplification"],
85 ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
86 | _ => error "solve.sml: interSteps on norm_Rational 2";
90 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
91 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
92 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
93 val intermediate_ptyps = !ptyps;
94 val intermediate_mets = !mets;
96 "--------- prepare pbl, met --------------------------------------";
97 "--------- prepare pbl, met --------------------------------------";
98 "--------- prepare pbl, met --------------------------------------";
100 (prep_pbt @{theory Test} "pbl_ttestt" [] e_pblID
105 (prep_pbt @{theory Test} "pbl_ttestt_detail" [] e_pblID
107 [("#Given" ,["realTestGiven t_t"]),
108 ("#Find" ,["realTestFind s_s"])
110 e_rls, NONE, [["Test","test_detail"]]));
113 (prep_met @{theory Test} "met_detbin" [] e_metID
114 (["Test","test_detail_binom"]:metID,
115 [("#Given" ,["realTestGiven t_t"]),
116 ("#Find" ,["realTestFind s_s"])
118 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
119 crls = tval_rls, nrls = e_rls(*,
120 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
121 "Script Testterm (g_g::real) = \
122 \(((Rewrite_Set expand_binoms False) @@\
123 \ (Rewrite_Set cancel False)) g_g)"
126 (prep_met @{theory Test} "met_detpoly" [] e_metID
127 (["Test","test_detail_poly"]:metID,
128 [("#Given" ,["realTestGiven t_t"]),
129 ("#Find" ,["realTestFind s_s"])
131 {rew_ord' = "sqrt_right", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,
132 crls = tval_rls, nrls = e_rls(*,
133 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
134 "Script Testterm (g_g::real) = \
135 \(((Rewrite_Set make_polynomial False) @@\
136 \ (Rewrite_Set cancel_p False)) g_g)"
139 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
141 "-------- cancel, without detail ------------------------------";
142 "-------- cancel, without detail ------------------------------";
143 "-------- cancel, without detail ------------------------------";
144 val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
147 ("Test",["detail","test"],["Test","test_detail_binom"]);
149 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
150 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
156 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
157 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
160 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
161 (*"(3 + -1 * x) / (3 + x)"*)
162 if nxt = ("End_Proof'",End_Proof') then ()
163 else error "details.sml, changed behaviour in: without detail";
165 val str = pr_ptree pr_short pt;
169 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
170 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
171 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
172 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
173 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
174 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
175 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
176 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
177 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
178 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
179 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
180 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
181 (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
182 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
183 (* val nxt = ("Detail",Detail);"----------------------";*)
186 (*WN.11.9.03: after meNEW not yet implemented -------------------------*)
187 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
188 (*FIXXXXXME.040216 #####################################################
189 # val nxt = ("Detail", Detail) : string * tac
190 val it = "----------------------" : string
191 > val (p,_,f,nxt,_,pt) = me nxt p [] pt;
192 val f = Form' (FormKF (~1, EdUndef, ...)) : mout
193 val nxt = ("Empty_Tac", Empty_Tac) : string * tac
194 val p = ([2, 1], Res) : pos'
195 #########################################################################
196 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
197 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
199 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
200 (*val nxt = ("End_Detail",End_Detail)*)
201 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
202 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
203 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
204 val nxt = ("Detail",Detail);"----------------------";
205 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
206 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
209 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
211 rewrite "Rationals" "tless_true""e_rls"true("sym_real_plus_minus_binom","")
214 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
215 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
216 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
217 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
218 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
219 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
220 andalso nxt = ("End_Proof'",End_Proof') then ()
221 else error "new behaviour in details.sml, \
222 \cancel, rev-rew (cancel) afterwards";
223 FIXXXXXME.040216 #####################################################*)
225 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
227 "-------------- cancel_p, without detail ------------------------------";
228 "-------------- cancel_p, without detail ------------------------------";
229 "-------------- cancel_p, without detail ------------------------------";
230 val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))",
233 ("Test",["detail","test"],["Test","test_detail_poly"]);
235 (*val p = e_pos'; val c = [];
236 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
237 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
238 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
239 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
240 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
241 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
242 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
243 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
244 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
245 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail"))*)
246 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
247 "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
250 (*---------------WN060614?!?---
251 val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))";
252 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
253 "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)";
254 val SOME (t,_) = rewrite_set_ thy false cancel_p t; term2str t;
256 (---------------WN060614?!?---*)
258 val t = str2term "(3 + x) * (3 + -1 * x)";
259 (*========== inhibit exn AK110725 ================================================
260 (* ERROR: Argument: thy : domID * rls Reason: Can't unify theory to domID * rls *)
261 val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
262 "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
263 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
264 "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";
265 val SOME (t,_) = rewrite_set_ thy false simplify_power t; term2str t;
266 "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";
267 val SOME (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;
268 "9 + (0 * x + -1 * x ^^^ 2)";
269 val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
272 ========== inhibit exn AK110725 ================================================*)
274 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
275 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
276 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
277 (*"(3 + -1 * x) / (3 + x)"*)
278 if nxt = ("End_Proof'",End_Proof') then ()
279 else error "details.sml, changed behaviour in: cancel_p, without detail";
281 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
282 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
283 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
284 (* val p = e_pos'; val c = [];
285 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
286 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
287 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
288 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
289 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
290 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
291 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
292 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
293 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
294 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
295 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
296 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
297 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
299 (*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:
300 fun make_deriv ... Rls_ not yet impl. (| Thm | Calc)
301 Rls_ needed for make_polynomial ----------------------
302 val nxt = ("Detail",Detail);"----------------------";
303 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
304 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
305 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
306 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
307 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
308 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
309 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
311 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
312 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
313 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
314 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
315 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
316 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
317 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
319 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
320 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
321 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
322 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
323 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
324 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
325 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
326 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
327 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
328 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
329 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
330 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
331 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
332 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
333 if nxt = ("End_Detail",End_Detail) then ()
334 else error "details.sml: new behav. in Detail make_polynomial";
335 ----------------------------------------------------------------------*)
338 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
339 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
340 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
341 val nxt = ("Detail",Detail);"----------------------";
342 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
343 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
344 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
345 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
346 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
347 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
348 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
349 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
350 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
351 andalso nxt = ("End_Proof'",End_Proof') then ()
352 else error "new behaviour in details.sml, cancel_p afterwards";
359 val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
362 ("Test",["detail","test"],["Test","test_detail_poly"]);
364 (* val p = e_pos'; val c = [];
365 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
366 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
367 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
368 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
369 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
370 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
371 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
372 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
373 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
374 (*nxt = ("Apply_Method",Apply_Method ("Test","test_detail_poly"))*)
375 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
376 (*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
377 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
378 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
379 val nxt = ("Detail",Detail);"----------------------";
380 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
381 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
382 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
383 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
384 -------------------------------------------------------------------------*)
387 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
388 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
389 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
391 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
392 ("Test", ["sqroot-test","univariate","equation","test"],
393 ["Test","squ-equ-test-subpbl1"]))];
396 autoCalculate 1 CompleteCalc;
399 interSteps 1 ([],Res);
400 val [(_,(((pt,_),_),[(_,ip)]))] = !states;
401 val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
402 (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3),(_,_,t4),(_,_,t5),(_,_,t6)] =>
403 (writeln o terms2str) [t1,t2,t3,t4,t5,t6]
404 | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([4], Res) then ()
405 else error "details.sml: diff.behav. in interSteps'donesteps' 1";
412 interSteps 1 ([3],Pbl) (*subproblem*);
413 val [(_,(((pt,_),_),[(_,ip)]))] = !states;
414 val ("donesteps",_(*,ss*), lastpos) = detailstep pt ip;
415 (*case ss of [(_,_,t1),(_,_,t2),(_,_,t3)] =>
416 (writeln o terms2str) [t1,t2,t3]
417 | _ => error "details.sml: diff.behav. in detail miniscript";*) if lastpos = ([3, 2], Res) then ()
418 else error "details.sml: diff.behav. in interSteps'donesteps' 1";
421 (* val [(_,(((pt,_),_),[(_,ip)]))] = !states;
422 writeln (pr_ptree pr_short pt);
423 get_obj g_tac pt [4];
426 "------ interSteps'detailrls' after CompleteCalc -----------------";
427 "------ interSteps'detailrls' after CompleteCalc -----------------";
428 "------ interSteps'detailrls' after CompleteCalc -----------------";
430 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
431 ("Test", ["sqroot-test","univariate","equation","test"],
432 ["Test","squ-equ-test-subpbl1"]))];
435 autoCalculate 1 CompleteCalc;
436 interSteps 1 ([],Res);
441 refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)
443 interSteps 1 ([2],Res);
444 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
445 if length (children (get_nd pt p)) = 6 then ()
446 else error "details.sml: diff.behav. in interSteps'detailrls' 1";
449 moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA> *);
451 interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);
452 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
453 if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)
454 else error "details.sml: diff.behav. in interSteps'detailrls' 2";
457 refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)
459 interSteps 1 ([3,1],Res);
460 val ((pt,p),_) = get_calc 1; show_pt pt;
461 term2str (get_obj g_res pt [3,1,1]);(*"x = 0 + -1 * -1" ok*)
462 term2str (get_obj g_form pt [3,2]); (*"x = 0 + -1 * -1" ok*)
463 get_obj g_tac pt [3,1,1]; (*Rewrite_Inst.."risolate_bdv_add ok*)
466 refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)
468 interSteps 1 ([3,2],Res);
469 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
470 if length (children (get_nd pt p)) = 2 then ()
471 else error "details.sml: diff.behav. in interSteps'detailrls' 3";
473 val ((pt,p),_) = get_calc 1; show_pt pt;
476 "------ interSteps after appendFormula ---------------------------";
477 "------ interSteps after appendFormula ---------------------------";
478 "------ interSteps after appendFormula ---------------------------";
480 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
481 ("Test", ["sqroot-test","univariate","equation","test"],
482 ["Test","squ-equ-test-subpbl1"]))];
485 autoCalculate 1 CompleteCalcHead;
486 autoCalculate 1 (Step 1);
487 autoCalculate 1 (Step 1);
488 appendFormula 1 "x - 1 = 0"(*generates intermediate steps*);
489 (*these are not shown, because the resulting formula is on the same
490 level as the previous formula*)
491 interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*);
492 (*...and these are the internals*)
493 val ((pt,p),_) = get_calc 1; show_pt pt;
494 val (_,_,lastpos) =detailstep pt p;
495 if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()
496 else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
499 "------ Detail_Set -----------------------------------------------";
500 "------ Detail_Set -----------------------------------------------";
501 "------ Detail_Set -----------------------------------------------";
502 states:=[]; (*start of calculation, return No.1*)
503 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
504 ("Test", ["sqroot-test","univariate","equation","test"],
505 ["Test","squ-equ-test-subpbl1"]))];
506 Iterator 1; moveActiveRoot 1;
507 autoCalculate 1 CompleteCalcHead;
508 autoCalculate 1 (Step 1);
509 autoCalculate 1 (Step 1);
511 fetchProposedTactic 1 (*DG decides to do this tactic in detail*);
513 setNextTactic 1 (Detail_Set "Test_simplify");
516 val ((pt,p),tacis) = get_calc 1;
517 val str = pr_ptree pr_short pt;
521 term2str (fst (get_obj g_result pt [1]));
526 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
527 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
528 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
529 ptyps:= intermediate_ptyps;
530 mets:= intermediate_mets;