4 (c) due to copyright terms
6 is NOT ONLY dependent on Test, but on other thys:
7 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
8 uses from Rational.ML: Rrls cancel_p, Rrls cancel
10 uses from Poly.ML: Rls make_polynomial, Rls expand_binom
12 use"../smltest/ME/solve.sml";
16 "-----------------------------------------------------------------";
17 "table of contents -----------------------------------------------";
18 "-----------------------------------------------------------------";
19 "--------- interSteps on norm_Rational ---------------------------";
20 (*---vvv NOT working after meNEW.04mmdd*)
21 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
22 "--------- prepare pbl, met --------------------------------------";
23 "-------- cancel, without detail ------------------------------";
24 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
25 "-------------- cancel_p, without detail ------------------------------";
26 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
27 (*---^^^ NOT working*)
28 "on 'miniscript with mini-subpbl':";
29 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
30 "------ interSteps'detailrls' after CompleteCalc -----------------";
31 "------ interSteps after appendFormula ---------------------------";
32 (*---vvv not brought to work 0403*)
33 "------ Detail_Set -----------------------------------------------";
34 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
35 "-----------------------------------------------------------------";
36 "-----------------------------------------------------------------";
37 "-----------------------------------------------------------------";
40 "--------- interSteps on norm_Rational ---------------------------";
41 "--------- interSteps on norm_Rational ---------------------------";
42 "--------- interSteps on norm_Rational ---------------------------";
43 states:=[];(*exp_IsacCore_Simp_Rat_Double_No-7.xml*)
44 CalcTree [(["TERM ((2/(x+3) + 2/(x - 3)) / (8*x/(x^2 - 9)))","normalform N"],
46 ["rational","simplification"],
47 ["simplification","of_rationals"]))];
49 autoCalculate 1 CompleteCalc;
50 val ((pt,_),_) = get_calc 1; show_pt pt;
52 (*with "Script SimplifyScript (t_::real) = -----------------
53 \ ((Rewrite_Set norm_Rational False) t_)"
54 case pt of Nd (PblObj _, [Nd _]) => ((*met only applies norm_Rational*))
55 | _ => error "solve.sml: interSteps on norm_Rational 1";
56 interSteps 1 ([1], Res);
57 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
58 interSteps 1 ([1,3], Res);
60 getTactic 1 ([1,4], Res) (*here get the tactic, and ...*);
61 interSteps 1 ([1,5], Res) (*... here get the intermediate steps above*);
63 getTactic 1 ([1,5,1], Frm);
64 val ((pt,_),_) = get_calc 1; show_pt pt;
66 getTactic 1 ([1,8], Res) (*Rewrite_Set "common_nominator_p" *);
67 interSteps 1 ([1,9], Res)(*TODO.WN060606 reverse rew*);
68 --------------------------------------------------------------------*)
70 case pt of Nd (PblObj _, [Nd _, Nd _, Nd _, Nd _, Nd _, Nd _]) => ()
71 | _ => error "solve.sml: interSteps on norm_Rational 1";
72 (*these have been done now by the script ^^^ immediately...
73 interSteps 1 ([1], Res);
74 getFormulaeFromTo 1 ([1], Frm) ([1,12], Res) 99999 false;
76 interSteps 1 ([6], Res);
78 getTactic 1 ([6,1], Frm) (*here get the tactic, and ...*);
79 interSteps 1 ([6,1], Res) (*... here get the intermediate steps above*);
81 getTactic 1 ([3,4,1], Frm);
82 val ((pt,_),_) = get_calc 1; show_pt pt;
83 val (Form form, SOME tac, asm) = pt_extract (pt, ([6], Res));
84 case (term2str form, tac, terms2strs asm) of
85 ("1 / 2", Check_Postcond ["rational", "simplification"],
86 ["-36 * x + 4 * x ^^^ 3 ~= 0"]) => ()
87 | _ => error "solve.sml: interSteps on norm_Rational 2";
91 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
92 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
93 "###### val intermediate_ptyps = !ptyps;val intermediate_mets = !mets";
94 val intermediate_ptyps = !ptyps;
95 val intermediate_mets = !mets;
97 "--------- prepare pbl, met --------------------------------------";
98 "--------- prepare pbl, met --------------------------------------";
99 "--------- prepare pbl, met --------------------------------------";
101 (prep_pbt Test.thy "pbl_ttestt" [] e_pblID
106 (prep_pbt Test.thy "pbl_ttestt_detail" [] e_pblID
108 [("#Given" ,["realTestGiven t_"]),
109 ("#Find" ,["realTestFind s_"])
111 e_rls, NONE, [["Test","test_detail"]]));
114 (prep_met Test.thy "met_detbin" [] e_metID
115 (["Test","test_detail_binom"]:metID,
116 [("#Given" ,["realTestGiven t_"]),
117 ("#Find" ,["realTestFind s_"])
119 {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls,
120 crls=tval_rls, nrls=e_rls(*,
121 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
122 "Script Testterm (g_::real) = \
123 \(((Rewrite_Set expand_binoms False) @@\
124 \ (Rewrite_Set cancel False)) g_)"
127 (prep_met Test.thy "met_detpoly" [] e_metID
128 (["Test","test_detail_poly"]:metID,
129 [("#Given" ,["realTestGiven t_"]),
130 ("#Find" ,["realTestFind s_"])
132 {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls,
133 crls=tval_rls, nrls=e_rls(*,
134 asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]*)},
135 "Script Testterm (g_::real) = \
136 \(((Rewrite_Set make_polynomial False) @@\
137 \ (Rewrite_Set cancel_p False)) g_)"
140 (*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*)
142 "-------- cancel, without detail ------------------------------";
143 "-------- cancel, without detail ------------------------------";
144 "-------- cancel, without detail ------------------------------";
145 val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))",
148 ("Test.thy",["detail","test"],["Test","test_detail_binom"]);
150 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
157 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
162 (*"(3 + -1 * x) / (3 + x)"*)
163 if nxt = ("End_Proof'",End_Proof') then ()
164 else error "details.sml, changed behaviour in: without detail";
166 val str = pr_ptree pr_short pt;
170 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
171 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
172 "-------- cancel, detail rev-rew (cancel) afterwards ----------";
173 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
180 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*)
181 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
182 (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*)
183 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
184 (* val nxt = ("Detail",Detail);"----------------------";*)
187 (*WN.11.9.03: after meNEW not yet implemented -------------------------*)
188 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
189 (*FIXXXXXME.040216 #####################################################
190 # val nxt = ("Detail", Detail) : string * tac
191 val it = "----------------------" : string
192 > val (p,_,f,nxt,_,pt) = me nxt p [] pt;
193 val f = Form' (FormKF (~1, EdUndef, ...)) : mout
194 val nxt = ("Empty_Tac", Empty_Tac) : string * tac
195 val p = ([2, 1], Res) : pos'
196 #########################################################################
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 (p,_,f,nxt,_,pt) = me nxt p [] pt;
201 (*val nxt = ("End_Detail",End_Detail)*)
202 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
203 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
204 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
205 val nxt = ("Detail",Detail);"----------------------";
206 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
207 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
209 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
211 rewrite "Rationals.thy" "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 => 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.thy",["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.thy","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 val SOME (t,_) = rewrite_set_ thy false expand_poly t; term2str t;
260 "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))";
261 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
262 "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))";
263 val SOME (t,_) = rewrite_set_ thy false simplify_power t; term2str t;
264 "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))";
265 val SOME (t,_) = rewrite_set_ thy false collect_numerals t; term2str t;
266 "9 + (0 * x + -1 * x ^^^ 2)";
267 val SOME (t,_) = rewrite_set_ thy false reduce_012 t; term2str t;
271 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
272 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
273 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
274 (*"(3 + -1 * x) / (3 + x)"*)
275 if nxt = ("End_Proof'",End_Proof') then ()
276 else error "details.sml, changed behaviour in: cancel_p, without detail";
278 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
279 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
280 "-------------- cancel_p, detail rev-rew (cancel) afterwards ----------";
281 (* val p = e_pos'; val c = [];
282 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
283 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
284 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
285 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
286 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
287 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)
292 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
293 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
294 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
296 (*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml:
297 fun make_deriv ... Rls_ not yet impl. (| Thm | Calc)
298 Rls_ needed for make_polynomial ----------------------
299 val nxt = ("Detail",Detail);"----------------------";
300 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
301 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
302 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 if nxt = ("End_Detail",End_Detail) then ()
331 else error "details.sml: new behav. in Detail make_polynomial";
332 ----------------------------------------------------------------------*)
335 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
336 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
337 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
338 val nxt = ("Detail",Detail);"----------------------";
339 val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
340 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
341 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
342 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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) handle e => print_exn e;
346 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
347 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
348 andalso nxt = ("End_Proof'",End_Proof') then ()
349 else error "new behaviour in details.sml, cancel_p afterwards";
357 val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))",
360 ("Test.thy",["detail","test"],["Test","test_detail_poly"]);
362 (* val p = e_pos'; val c = [];
363 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
364 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
365 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
366 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
367 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
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 (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*)
373 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
374 (*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ----------------------------
375 (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*)
376 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
377 val nxt = ("Detail",Detail);"----------------------";
378 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
379 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
380 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
381 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
382 -------------------------------------------------------------------------*)
385 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
386 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
387 "------ interSteps'donesteps': on 'miniscript with mini-subpbl'---";
390 [(["equality (x+1=2)", "solveFor x","solutions L"],
392 ["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];
427 "------ interSteps'detailrls' after CompleteCalc -----------------";
428 "------ interSteps'detailrls' after CompleteCalc -----------------";
429 "------ interSteps'detailrls' after CompleteCalc -----------------";
432 [(["equality (x+1=2)", "solveFor x","solutions L"],
434 ["sqroot-test","univariate","equation","test"],
435 ["Test","squ-equ-test-subpbl1"]))];
438 autoCalculate 1 CompleteCalc;
439 interSteps 1 ([],Res);
444 refFormula 1 (get_pos 1 1); (* 2 Res, <ISA> -1 + x = 0 </ISA> *)
446 interSteps 1 ([2],Res);
447 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
448 if length (children (get_nd pt p)) = 6 then ()
449 else error "details.sml: diff.behav. in interSteps'detailrls' 1";
452 moveActiveDown 1; refFormula 1 (get_pos 1 1); (* 3,1 Frm, <ISA> -1 + x = 0 </ISA> *);
454 interSteps 1 ([3,1],Frm) (*<ERROR> first formula on level has NO detail </E*);
455 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
456 if length (children (get_nd pt p)) = 0 then () (*NO detail at ([xxx,1],Frm)*)
457 else error "details.sml: diff.behav. in interSteps'detailrls' 2";
460 refFormula 1 (get_pos 1 1); (* 3,1 Res, <ISA> x = 0 + -1 * -1 </ISA> *)
462 interSteps 1 ([3,1],Res);
463 val ((pt,p),_) = get_calc 1; show_pt pt;
464 term2str (get_obj g_res pt [3,1,1]);(*"x = 0 + -1 * -1" ok*)
465 term2str (get_obj g_form pt [3,2]); (*"x = 0 + -1 * -1" ok*)
466 get_obj g_tac pt [3,1,1]; (*Rewrite_Inst.."risolate_bdv_add ok*)
469 refFormula 1 (get_pos 1 1); (* 3,2 Res, <ISA> x = 1 </ISA> *)
471 interSteps 1 ([3,2],Res);
472 val [(_,(((pt,_),_),[(_,(p,_))]))] = !states;
473 if length (children (get_nd pt p)) = 2 then ()
474 else error "details.sml: diff.behav. in interSteps'detailrls' 3";
476 val ((pt,p),_) = get_calc 1; show_pt pt;
479 "------ interSteps after appendFormula ---------------------------";
480 "------ interSteps after appendFormula ---------------------------";
481 "------ interSteps after appendFormula ---------------------------";
484 [(["equality (x+1=2)", "solveFor x","solutions L"],
486 ["sqroot-test","univariate","equation","test"],
487 ["Test","squ-equ-test-subpbl1"]))];
490 autoCalculate 1 CompleteCalcHead;
491 autoCalculate 1 (Step 1);
492 autoCalculate 1 (Step 1);
493 appendFormula 1 "x - 1 = 0"(*generates intermediate steps*);
494 (*these are not shown, because the resulting formula is on the same
495 level as the previous formula*)
496 interSteps 1 ([2],Res) (*error: last unchanged was ([2, 9], Res)*);
497 (*...and these are the internals*)
498 val ((pt,p),_) = get_calc 1; show_pt pt;
499 val (_,_,lastpos) =detailstep pt p;
500 if p = ([2], Res) andalso lastpos = ([2, 9], Res) then ()
501 else error "solve.sml: diff.beh. after appendFormula x - 1 = 0";
504 "------ Detail_Set -----------------------------------------------";
505 "------ Detail_Set -----------------------------------------------";
506 "------ Detail_Set -----------------------------------------------";
508 CalcTree (*start of calculation, return No.1*)
509 [(["equality (x+1=2)", "solveFor x","solutions L"],
511 ["sqroot-test","univariate","equation","test"],
512 ["Test","squ-equ-test-subpbl1"]))];
513 Iterator 1; moveActiveRoot 1;
514 autoCalculate 1 CompleteCalcHead;
515 autoCalculate 1 (Step 1);
516 autoCalculate 1 (Step 1);
518 fetchProposedTactic 1 (*DG decides to do this tactic in detail*);
520 setNextTactic 1 (Detail_Set "Test_simplify");
523 val ((pt,p),tacis) = get_calc 1;
524 val str = pr_ptree pr_short pt;
528 term2str (fst (get_obj g_result pt [1]));
533 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
534 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
535 "###### ptyps:= intermediate_ptyps;met:= intermediate_mets;#######";
536 ptyps:= intermediate_ptyps;
537 mets:= intermediate_mets;