1 (* tests for sml/ME/ctree.sml
2 authors: Walther Neuper 060113
3 (c) due to copyright terms
5 use"../smltest/ME/ctree.sml";
9 "-----------------------------------------------------------------";
10 "table of contents -----------------------------------------------";
11 "-----------------------------------------------------------------";
12 "-----------------------------------------------------------------";
13 "-------------- fun get_ctxt, g_ctxt -----------------------------";
14 "-------------- check positions in miniscript --------------------";
15 "-------------- get_allpos' (from ctree above)--------------------";
16 "-------------- cut_level (from ctree above)----------------------";
17 "-------------- cut_tree (from ctree above)-----------------------";
18 "=====new ctree 1a miniscript with mini-subpbl ===================";
19 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
20 "=====new ctree 2 miniscript with mini-subpbl ====================";
21 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
22 "-------------- cappend (from ctree above)------------------------";
23 "-------------- cappend minisubpbl -------------------------------";
24 "=====new ctree 3 ================================================";
25 "-------------- move_dn ------------------------------------------";
26 "-------------- move_dn: Frm -> Res ------------------------------";
27 "-------------- move_up ------------------------------------------";
28 "------ move into detail -----------------------------------------";
29 "=====new ctree 3a ===============================================";
30 "-------------- move_dn in Incomplete ctree ----------------------";
31 "=====new ctree 4: crooked by cut_level_'_ =======================";
32 (*//############## development stopped 0501 ########################\\*)
33 (******************************************************************)
34 (* val SAVE_get_trace = get_trace; *)
35 (******************************************************************)
36 "-------------- ME_Misc.get_interval from ctree: incremental development--";
37 (******************************************************************)
38 (* val get_trace = SAVE_get_trace; *)
39 (******************************************************************)
40 (*\\############## development stopped 0501 ########################//*)
41 "=====new ctree 4 ratequation ====================================";
42 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
43 "=====new ctree 5 minisubpbl =====================================";
44 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
45 "=====new ctree 6 minisubpbl intersteps ==========================";
46 "-------------- get_allpos' new ----------------------------------";
47 "-------------- cut_tree new (from ctree above)-------------------";
48 "-------------- repl_app------------------------------------------";
49 "-----------------------------------------------------------------";
50 "-----------------------------------------------------------------";
51 "-----------------------------------------------------------------";
54 "-------------- fun get_ctxt, g_ctxt -----------------------------";
55 "-------------- fun get_ctxt, g_ctxt -----------------------------";
56 "-------------- fun get_ctxt, g_ctxt -----------------------------";
57 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
59 ("Test", ["sqroot-test", "univariate", "equation", "test"],
60 ["Test", "squ-equ-test-subpbl1"]);
61 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
63 handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";
64 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
66 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
69 val pt = append_problem [] (Istate.empty, ContextC.empty) Formalise.empty ([(*oris*)], References.empty, TermC.empty, ContextC.empty) pt;
70 val ctxt = get_obj g_ctxt pt [];
71 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
73 "-------------- check positions in miniscript --------------------";
74 "-------------- check positions in miniscript --------------------";
75 "-------------- check positions in miniscript --------------------";
76 val fmz = ["equality (x+1=(2::real))",
77 "solveFor x", "solutions L"];
79 ("Test",["sqroot-test", "univariate", "equation", "test"],
80 ["Test", "squ-equ-test-subpbl1"]);
81 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
83 (* nxt = Add_Given "equality (x + 1 = 2)"
84 (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
87 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
95 "ctree.sml-------------- get_allpos' new ------------------------\"";
96 val (PP, pp) = split_last [1];
97 val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);
99 val cuts = get_allp [] ([], ([],Frm)) pt;
100 val cuts2 = get_allps [] [1] (children pt);
101 "ctree.sml-------------- cut_tree new (from ctree above)----------";
102 val (pt', cuts) = cut_tree pt ([1],Frm);
103 "ctree.sml-------------- cappend on complete ctree from above ----";
104 val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (TermC.str2term "Inform[1]");
105 "----------------------------------------------------------------/";
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);
112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
114 (*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 (*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
127 val Test_Out.FormKF res = f;
129 then case nxt of End_Proof' => ()
130 | _ => error "new behaviour in test: miniscript with mini-subpbl 1"
131 else error "new behaviour in test: miniscript with mini-subpbl 2"
133 Test_Tool.show_pt pt;
135 "-------------- get_allpos' (from ctree above)--------------------";
136 "-------------- get_allpos' (from ctree above)--------------------";
137 "-------------- get_allpos' (from ctree above)--------------------";
138 if get_allpos' ([], 1) pt =
150 then () else error "ctree.sml: diff:behav. in get_allpos' 1";
152 if get_allpos's ([], 1) (children pt) =
162 then () else error "ctree.sml: diff:behav. in get_allpos' 2";
164 if get_allpos's ([], 2) (takerest (1, children pt)) =
172 then () else error "ctree.sml: diff:behav. in get_allpos' 3";
174 if get_allpos's ([], 3) (takerest (2, children pt)) =
181 then () else error "ctree.sml: diff:behav. in get_allpos' 4";
183 if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
187 then () else error "ctree.sml: diff:behav. in get_allpos' 5";
189 if get_allpos' ([3], 1) (nth 3 (children pt)) =
195 then () else error "ctree.sml: diff:behav. in get_allpos' 6";
202 "-------------- cut_level (from ctree above)----------------------";
203 "-------------- cut_level (from ctree above)----------------------";
204 "-------------- cut_level (from ctree above)----------------------";
205 Test_Tool.show_pt pt;
206 Test_Tool.show_pt pt';
207 (*default_print_depth 99*) cuts; (*default_print_depth 3*)
209 (*if cuts = [([2], Res),
216 then () else error "ctree.sml: diff:behav. in cut_level 1a";
217 val (res,asm) = get_obj g_result pt' [2];
218 if res = TermC.empty andalso asm = [] then () else
219 error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
220 if not (existpt [2] pt') then () else
221 error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
223 val (res,asm) = get_obj g_result pt' [];
225 (*============ inhibit exn AK110726 ==============================================
226 if UnparseC.term res = "[x = 1]" (*WN050219 TermC.empty in cut_tree!!!*) then () else
227 error "ctree.sml: diff:behav. in cut_level 1ab";
228 ============ inhibit exn AK110726 ==============================================*)
229 (*============ inhibit exn AK110726 ==============================================
230 if map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt') =
234 ([2], Res),(*, TermC.empty in cut_tree!!!*)
235 ([], Res)] then () else
236 error "ctree.sml: diff:behav. in cut_level 1b";
237 ============ inhibit exn AK110726 ==============================================*)
239 val (pt',cuts) = cut_level [] [] pt ([2],Res);
240 if cuts = [([3], Frm),
246 then () else error "ctree.sml: diff:behav. in cut_level 2a";
248 if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
249 then () else error "ctree.sml: diff:behav. in cut_level 2b";
251 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
252 if cuts = [([3, 1], Res), ([3, 2], Res)]
253 then () else error "ctree.sml: diff:behav. in cut_level 3a";
254 if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
255 then () else error "ctree.sml: diff:behav. in cut_level 3b";
257 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
258 if cuts = [([3, 2], Res)]
259 then () else error "ctree.sml: diff:behav. in cut_level 4a";
260 if pr_ctree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n4. [x = 1]\n"
261 then () else error "ctree.sml: diff:behav. in cut_level 4b";
264 "-------------- cut_tree (from ctree above)-----------------------";
265 "-------------- cut_tree (from ctree above)-----------------------";
266 "-------------- cut_tree (from ctree above)-----------------------";
267 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
269 (*============ inhibit exn AK110726 ==============================================
270 if cuts = [([2], Res),
278 then () else error "ctree.sml: diff:behav. in cut_tree 1a";
280 val (res,asm) = get_obj g_result pt' [2];
281 ============ inhibit exn AK110726 ==============================================*)
283 if res = TermC.empty (*WN050219 done by cut_level*) then () else
284 error "ctree.sml: diff:behav. in cut_tree 1aa";
286 (*============ inhibit exn AK110726 ==============================================
287 val form = get_obj g_form pt' [2];
288 if UnparseC.term form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
289 error "ctree.sml: diff:behav. in cut_tree 1ab";
290 ============ inhibit exn AK110726 ==============================================*)
292 (* get_obj g_form pt' [2];
293 (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"
294 raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)
295 "~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)
297 val (res,asm) = get_obj g_result pt' [];
298 if res = TermC.empty (*WN050219 done by cut_tree*) then () else
299 error "ctree.sml: diff:behav. in cut_tree 1ac";
301 if map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt') =
304 ([1], Res)] then () else
305 error "ctree.sml: diff:behav. in cut_tree 1ad";
307 val (pt', cuts) = cut_tree pt ([2],Res);
308 (*============ inhibit exn AK110726 ==============================================
309 if cuts = [([3], Frm),
316 then () else error "ctree.sml: diff:behav. in cut_tree 2";
317 ============ inhibit exn AK110726 ==============================================*)
319 val (pt', cuts) = cut_tree pt ([3,1],Frm);
320 (*============ inhibit exn AK110726 ==============================================
321 if cuts = [([3, 1], Res),
326 then () else error "ctree.sml: diff:behav. in cut_tree 3";
327 ============ inhibit exn AK110726 ==============================================*)
329 val (pt', cuts) = cut_tree pt ([3,1],Res);
330 if cuts = [([3, 2], Res),
334 then () else error "ctree.sml: diff:behav. in cut_tree 4";
336 "=====new ctree 1a miniscript with mini-subpbl ===================";
337 "=====new ctree 1a miniscript with mini-subpbl ===================";
338 "=====new ctree 1a miniscript with mini-subpbl ===================";
339 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
341 ("Test",["sqroot-test", "univariate", "equation", "test"],
342 ["Test", "squ-equ-test-subpbl1"]);
343 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
345 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
346 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
347 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
348 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
349 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
350 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
351 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
352 Test_Tool.show_pt pt;
354 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
355 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
356 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
358 val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
359 if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
360 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
362 val (pt', cuts) = cut_tree pt ([1],Frm);
364 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
367 val pos as ([p],_) = ([1],Frm);
368 val pt as Nd (b,_) = pt;
371 Test_Tool.show_pt pt;
372 Test_Tool.show_pt pt';
373 (*default_print_depth 99;*)cuts;(*default_print_depth 3;*)
374 (*default_print_depth 99;*)map fst3 (ME_Misc.get_interval ([],Frm) ([],Res) 9999 pt');(*default_print_depth 3;*)
375 ####################################################################*)
379 "=====new ctree 2 miniscript with mini-subpbl ====================";
380 "=====new ctree 2 miniscript with mini-subpbl ====================";
381 "=====new ctree 2 miniscript with mini-subpbl ====================";
383 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
384 ("Test", ["sqroot-test", "univariate", "equation", "test"],
385 ["Test", "squ-equ-test-subpbl1"]))];
386 Iterator 1; moveActiveRoot 1;
387 autoCalculate 1 CompleteCalc;
389 interSteps 1 ([3,2],Res);
391 val ((pt,_),_) = get_calc 1;
392 Test_Tool.show_pt pt;
394 if (UnparseC.term o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
395 else error "mini-subpbl interSteps broken";
397 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
398 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
399 "-------------- cut_tree (intermedi.ctree: 3rd level)-------------";
400 (*WN050225 intermed. outcommented
401 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
402 if cuts = [([3, 2, 1], Res),
407 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
409 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
410 if cuts = [([3, 2, 2], Res),
414 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
417 "-------------- cappend (from ctree above)------------------------";
418 "-------------- cappend (from ctree above)------------------------";
419 "-------------- cappend (from ctree above)------------------------";
420 val (pt',cuts) = cappend_form pt [3,2,1] Istate.empty (TermC.str2term "newnew");
421 if cuts = [([3, 2, 1], Res),
427 then () else error "ctree.sml: diff:behav. in cappend_form";
428 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "newnew" andalso
429 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
430 UnparseC.term (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
431 then () else error "ctree.sml: diff:behav. in cappend 1";
433 val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.str2term "newform")
434 (Tac "test") (TermC.str2term "newresult",[]) Complete;
435 if cuts = [([3, 2, 1], Res), (*?????????????*)
441 then () else error "ctree.sml: diff:behav. in cappend_atomic";
445 "-------------- cappend minisubpbl -------------------------------";
446 "-------------- cappend minisubpbl -------------------------------";
447 "-------------- cappend minisubpbl -------------------------------";
448 "=====new ctree 1 miniscript with mini-subpbl ====================";
449 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
451 ("Test",["sqroot-test", "univariate", "equation", "test"],
452 ["Test", "squ-equ-test-subpbl1"]);
453 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
454 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
455 (* nxt = Add_Given "equality (x + 1 = 2)"
456 (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
459 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
461 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
462 (* (writeln o (I_Model.to_string ctxt)) (get_obj g_pbl pt (fst p));
464 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
465 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
466 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
467 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
468 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
470 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
472 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.str2term "x + 1 = 2");
473 val form = get_obj g_form pt (fst p);
474 val (res,_) = get_obj g_result pt (fst p);
475 if UnparseC.term form = "x + 1 = 2" andalso res = TermC.empty then () else
476 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
477 if not (existpt ((lev_on o fst) p) pt) then () else
478 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
480 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
483 cappend_atomic pt (fst p) Istate.empty (TermC.str2term "x + 1 = 2")
484 Empty_Tac (TermC.str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
485 val form = get_obj g_form pt (fst p);
486 val (res,_) = get_obj g_result pt (fst p);
487 if UnparseC.term form = "x + 1 = 2" andalso UnparseC.term res = "x + 1 + -1 * 2 = 0"
488 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
489 if not (existpt ((lev_on o fst) p) pt) then () else
490 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
492 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
495 cappend_atomic pt (fst p) Istate.empty (TermC.str2term "x + 1 + -1 * 2 = 0")
496 Empty_Tac (TermC.str2term "-1 + x = 0",[]) Incomplete;
497 val form = get_obj g_form pt (fst p);
498 val (res,_) = get_obj g_result pt (fst p);
499 if UnparseC.term form = "x + 1 + -1 * 2 = 0" andalso UnparseC.term res = "-1 + x = 0"
500 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
501 if not (existpt ((lev_on o fst) p) pt) then () else
502 error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
505 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
507 val (pt,cuts) = cappend_problem pt (fst p) Istate.empty Formalise.empty ([],References.empty,TermC.empty, ContextC.empty);
508 if is_pblobj (get_obj I pt (fst p)) then () else
509 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
510 if not (existpt ((lev_on o fst) p) pt) then () else
511 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
513 (* ...complete calchead skipped...*)
515 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
516 val p = ([3, 1], Frm);
517 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.str2term "-1 + x = 0");
518 val form = get_obj g_form pt (fst p);
519 val (res,_) = get_obj g_result pt (fst p);
520 if UnparseC.term form = "-1 + x = 0" andalso res = TermC.empty then () else
521 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
522 if not (existpt ((lev_on o fst) p) pt) then () else
523 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
525 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
526 val p = ([3, 1], Res);
528 cappend_atomic pt (fst p) Istate.empty (TermC.str2term "-1 + x = 0")
529 Empty_Tac (TermC.str2term "x = 0 + -1 * -1",[]) Incomplete;
530 val form = get_obj g_form pt (fst p);
531 val (res,_) = get_obj g_result pt (fst p);
532 if UnparseC.term form = "-1 + x = 0" andalso UnparseC.term res = "x = 0 + -1 * -1" then()
533 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
534 if not (existpt ((lev_on o fst) p) pt) then () else
535 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
537 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
538 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
539 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
540 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
541 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
542 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
544 WN050225 intermed. outcommented---*)
546 "=====new ctree 3 ================================================";
547 "=====new ctree 3 ================================================";
548 "=====new ctree 3 ================================================";
551 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
552 ("Test", ["sqroot-test", "univariate", "equation", "test"],
553 ["Test", "squ-equ-test-subpbl1"]))];
554 Iterator 1; moveActiveRoot 1;
555 autoCalculate 1 CompleteCalc;
557 val ((pt,_),_) = get_calc 1;
558 Test_Tool.show_pt pt;
560 "-------------- move_dn ------------------------------------------";
561 "-------------- move_dn ------------------------------------------";
562 "-------------- move_dn ------------------------------------------";
563 val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);
564 val p = move_dn [] pt p (*-> ([1],Res)*);
565 val p = move_dn [] pt p (*-> ([2],Res)*);
566 val p = move_dn [] pt p (*-> ([3],Pbl)*);
567 val p = move_dn [] pt p (*-> ([3,1],Frm)*);
568 val p = move_dn [] pt p (*-> ([3,1],Res)*);
569 val p = move_dn [] pt p (*-> ([3,2],Res)*);
570 val p = move_dn [] pt p (*-> ([3],Res)*);
571 (* UnparseC.term (get_obj g_res pt [3]);
572 UnparseC.term (get_obj g_form pt [4]);
574 val p = move_dn [] pt p (*-> ([4],Res)*);
575 val p = move_dn [] pt p (*-> ([],Res)*);
577 val p = (move_dn [] pt p) handle e => print_exn_G e;
578 Exception PTREE end of calculation*)
580 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
582 "-------------- move_dn: Frm -> Res ------------------------------";
583 "-------------- move_dn: Frm -> Res ------------------------------";
584 "-------------- move_dn: Frm -> Res ------------------------------";
586 CalcTree (*start of calculation, return No.1*)
587 [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
589 ["LINEAR", "univariate", "equation", "test"],
590 ["Test", "solve_linear"]))];
591 Iterator 1; moveActiveRoot 1;
592 autoCalculate 1 CompleteCalcHead;
593 autoCalculate 1 (Steps 1);
594 refFormula 1 (get_pos 1 1);
598 if get_pos 1 1 = ([1], Frm) then ()
599 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
600 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
602 autoCalculate 1 (Steps 1);
603 refFormula 1 (get_pos 1 1);
605 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
606 if get_pos 1 1 = ([1], Res) then ()
607 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
608 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
611 "-------------- move_up ------------------------------------------";
612 "-------------- move_up ------------------------------------------";
613 "-------------- move_up ------------------------------------------";
614 val p = move_up [] pt ([],Res); (*-> ([4],Res)*)
615 val p = move_up [] pt p; (*-> ([3],Res)*)
616 val p = move_up [] pt p; (*-> ([3,2],Res)*)
617 val p = move_up [] pt p; (*-> ([3,1],Res)*)
618 val p = move_up [] pt p; (*-> ([3,1],Frm)*)
619 val p = move_up [] pt p; (*-> ([3],Pbl)*)
620 val p = move_up [] pt p; (*-> ([2],Res)*)
621 val p = move_up [] pt p; (*-> ([1],Res)*)
622 val p = move_up [] pt p; (*-> ([1],Frm)*)
623 val p = move_up [] pt p; (*-> ([],Pbl)*)
624 (*val p = (move_up [] pt p) handle e => print_exn_G e;
625 Exception PTREE begin of calculation*)
627 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
629 "------ move into detail -----------------------------------------";
630 "------ move into detail -----------------------------------------";
631 "------ move into detail -----------------------------------------";
633 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
634 ("Test", ["sqroot-test", "univariate", "equation", "test"],
635 ["Test", "squ-equ-test-subpbl1"]))];
636 Iterator 1; moveActiveRoot 1;
637 autoCalculate 1 CompleteCalc;
642 refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
644 interSteps 1 ([2],Res);
646 val ((pt,_),_) = get_calc 1; Test_Tool.show_pt pt;
649 val p = move_up [] pt p; (*([2, 6], Res)*);
650 val p = movelevel_up [] pt p;(*([2], Frm)*);
651 val p = move_dn [] pt p; (*([2, 1], Frm)*);
652 val p = move_dn [] pt p; (*([2, 1], Res)*);
653 val p = move_dn [] pt p; (*([2, 2], Res)*);
654 val p = move_dn [] pt p; (*([2, 3], Res)*);
655 val p = move_dn [] pt p; (*([2, 4], Res)*);
656 val p = move_dn [] pt p; (*([2, 5], Res)*);
657 val p = move_dn [] pt p; (*([2, 6], Res)*);
658 if p = ([2, 6], Res) then()
659 else error "ctree.sml: diff.behav. in move into detail";
661 "=====new ctree 3a ===============================================";
662 "=====new ctree 3a ===============================================";
663 "=====new ctree 3a ===============================================";
665 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
666 ("Test", ["sqroot-test", "univariate", "equation", "test"],
667 ["Test", "squ-equ-test-subpbl1"]))];
668 Iterator 1; moveActiveRoot 1;
669 autoCalculate 1 CompleteCalcHead;
670 autoCalculate 1 (Steps 1);
671 autoCalculate 1 (Steps 1);
672 autoCalculate 1 (Steps 1);
673 val ((pt,_),_) = get_calc 1;
674 val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
675 val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
676 val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
677 (*val p = move_dn [] pt ([2], Res) ->Exception- PTREE "[] not complete"*);
679 moveDown 1 ([],Pbl) (*-> ([1], Frm)*);
680 moveDown 1 ([1],Frm) (*-> ([1],Res)*);
681 moveDown 1 ([1],Res) (*-> ([2],Res)*);
682 moveDown 1 ([2],Res) (*-> pos does not exist*);
684 get_obj g_ostate pt [1];
685 Test_Tool.show_pt pt;
688 "-------------- move_dn in Incomplete ctree ----------------------";
689 "-------------- move_dn in Incomplete ctree ----------------------";
690 "-------------- move_dn in Incomplete ctree ----------------------";
694 "=====new ctree 4: crooked by cut_level_'_ =======================";
695 "=====new ctree 4: crooked by cut_level_'_ =======================";
696 "=====new ctree 4: crooked by cut_level_'_ =======================";
699 [(["equality (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)",
700 "solveFor x", "solutions L"],
701 ("RatEq",["univariate", "equation"],["no_met"]))];
702 Iterator 1; moveActiveRoot 1;
703 autoCalculate 1 CompleteCalc;
705 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
706 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
707 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
708 getTactic 1 ([4,1],Res);(*Rewrite all_left*)
709 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
710 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
712 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
713 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
714 moveActiveFormula 1 ([3],Res)(*3.1.*);
715 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
716 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Program Stepwise t_=*);
718 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
719 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
721 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
722 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
723 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
724 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
726 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
727 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
728 val ((pt,_),_) = get_calc 1;
729 writeln(pr_ctree pr_short pt);
730 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
731 ###########################################################################*)
732 val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
733 writeln(pr_ctree pr_short pt);
736 "-------------- ME_Misc.get_interval from ctree: incremental development--";
737 "-------------- ME_Misc.get_interval from ctree: incremental development--";
738 "-------------- ME_Misc.get_interval from ctree: incremental development--";
739 "--- level 1: get pos from start b to end p ----------------------";
740 "--- level 1: get pos from start b to end p ----------------------";
741 "--- level 1: get pos from start b to end p ----------------------";
742 (******************************************************************)
743 (**) val SAVE_get_trace = get_trace; (**)
744 (******************************************************************)
745 (*'getnds' below is structured as such:*)
746 fun www _ [x] = "l+r-margin"
747 | www true [x1,x2] = "l-margin, r-margin"
748 | www _ [x1,x2] = "intern, r-margin"
749 | www true (x::(xs as _::_)) = "l-margin " ^ www false xs
750 | www _ (x::(xs as _::_)) = "intern " ^ www false xs;
751 www true [1,2,3,4,5];
752 (*val it = "from intern intern intern to" : string*)
754 (*val it = "from to" : string*)
756 (*val it = "from+to" : string*)
759 (*specific values of hd of pos p,q for simple handling take_fromto,
760 from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
761 ... can be used even for positions _below_ p or q*)
762 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
763 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
764 (*analoguous for tl*)
765 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
766 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
768 (*see modspec.sml#pt_form
769 fun pt_form (PrfObj {form,...}) = UnparseC.term form
770 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
771 let val (dI, pI, _) = get_somespec' spec spec'
772 val {cas,...} = Problem.from_store pI
774 NONE => UnparseC.term (pblterm dI pI)
775 | SOME t => UnparseC.term (subst_atomic (mk_env probl) t)
778 (*.get an 'interval' from ctree down to a certain level
779 by 'take_fromto children' of the nodes with specific 'from' and 'to';
780 'i > 0' suppresses output during recursive descent towards 'from'
781 b: the 'from' incremented to the actual pos
782 p,q: specific 'from','to' for simple use of 'take_fromto'*)
783 fun getnd i (b,p) q (Nd (po, nds)) =
784 (if i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
786 @ (writeln("getnd : b="^(ints2str' b)^", p="^
787 (ints2str' p)^", q="^(ints2str' q));
789 getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
790 (take_fromto (hdp p) (hdq q) nds))
792 and getnds _ _ _ _ [] = [] (*no children*)
793 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
794 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
795 (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
796 ", q="^ ints2str' q);
797 (getnd i ( b, p ) [99999] n1) @
798 (getnd ~99999 (lev_on b,[0]) q n2))
799 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
800 (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
801 ", q="^ ints2str' q);
802 (getnd i ( b,[0]) [99999] n1) @
803 (getnd ~99999 (lev_on b,[0]) q n2))
804 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
805 (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
806 ", q="^ ints2str' q);
807 (getnd i ( b, p ) [99999] nd) @
808 (getnds ~99999 false (lev_on b,[0]) q nds))
809 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
810 (getnd i ( b,[0]) [99999] nd) @
811 (getnds ~99999 false (lev_on b,[0]) q nds);
813 (*get an 'interval from to' from a ctree as 'intervals f t' of respective nodes
814 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
815 (1) the 'f' are given
816 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
817 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
819 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
820 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
821 the 'f' and 't' are set by hdp,... *)
822 fun get_trace pt p q =
823 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
824 (take_fromto (hdp p) (hdq q) (children pt));
827 writeln(pr_ctree pr_short pt);
829 case get_trace pt [1,3] [4,1,1] of
830 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
831 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1a";
832 case get_trace pt [2] [4,3,2] of
833 [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
834 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1b";
835 case get_trace pt [1,4] [4,3,1] of
836 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
837 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1c";
840 (*========== inhibit exn AK110719 ==============================================
841 case get_trace pt [4,2] [5] of
842 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
843 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
844 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
845 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1d";
846 ========== inhibit exn AK110719 ==============================================*)
848 case get_trace pt [] [4,4,2] of
849 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
850 [4,3],[4,3,1],[4,3,2]] => ()
851 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1e";
853 (*========== inhibit exn AK110719 ==============================================
854 case get_trace pt [] [] of
855 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
856 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
857 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1f";
858 case get_trace pt [4,3] [4,3] of
859 [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
860 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1g";
861 ========== inhibit exn AK110719 ==============================================*)
863 "--- level 2: get pos' from start b to end p ---------------------";
864 "--- level 2: get pos' from start b to end p ---------------------";
865 "--- level 2: get pos' from start b to end p ---------------------";
866 (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
867 development stopped in favour of move_dn, see ME_Misc.get_interval
868 actually used (inefficient) version with move_dn: see modspec.sml
871 case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
872 [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
873 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1b";
874 case get_trace pt ([],Pbl) ([],Res) of
875 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
876 [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
877 | _ => error "diff.behav.in ctree.sml: ME_Misc.get_interval lev 1e";
880 (******************************************************************)
881 (**) val get_trace = SAVE_get_trace; (**)
882 (******************************************************************)
884 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
885 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
886 "-------------- ME_Misc.pt_extract form, tac, asm<>[] --------------------";
887 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Res));
888 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
889 ("(3 + -1 * x + x \<up> 2) * x = 1 * (9 * x + -6 * x \<up> 2 + x \<up> 3)",
892 ["normalise", "polynomial", "univariate", "equation"]),
893 ["x \<noteq> 0", "9 * x + -6 * x \<up> 2 + x \<up> 3 \<noteq> 0"]) => ()
894 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract asm<>[]";
895 (*WN060717 unintentionally changed some rls/ord while
896 completing knowl. for thes2file...
898 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
899 ((*"(3 + (-1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))",
902 ["normalise", "polynomial", "univariate", "equation"]),
903 ["9 * x + (x \<up> 3 + -6 * x \<up> 2) ~= 0"]) => ()
904 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract asm<>[]";
906 .... but it became even better*)
910 "=====new ctree 5 minisubpbl =====================================";
911 "=====new ctree 5 minisubpbl =====================================";
912 "=====new ctree 5 minisubpbl =====================================";
914 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
915 ("Test", ["sqroot-test", "univariate", "equation", "test"],
916 ["Test", "squ-equ-test-subpbl1"]))];
917 Iterator 1; moveActiveRoot 1;
918 autoCalculate 1 CompleteCalc;
919 val ((pt,_),_) = get_calc 1;
920 Test_Tool.show_pt pt;
922 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
923 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
924 "-------------- ME_Misc.pt_extract form, tac, asm ------------------------";
925 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract (pt, ([], Frm));
926 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
927 ("solve (x + 1 = 2, x)",
928 Apply_Method ["Test", "squ-equ-test-subpbl1"],
930 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([], Pbl)";
932 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Frm));
933 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
934 ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
935 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([1], Frm)";
937 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
938 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
939 ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
940 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([1], Res)";
942 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([2], Res));
943 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
945 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
947 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([2], Res)";
949 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Pbl));
950 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
951 ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
952 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3], Pbl)";
954 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,1], Frm));
955 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
956 ("-1 + x = 0", Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), []) => ()
957 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,1], Frm)";
959 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,1], Res));
960 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
961 ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
962 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,1], Res)";
964 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3,2], Res));
965 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
966 ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],
968 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3,2], Res)";
970 (*========== inhibit exn AK110719 ==============================================
971 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([3], Res));
972 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
973 ("[x = 1]", Check_elementwise "Assumptions", []) => ()
974 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([3], Res)";
976 val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([4], Res));
977 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
979 Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
981 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([4], Res)";
983 val (Form form, tac, asm) = ME_Misc.pt_extract (pt, ([], Res));
984 case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
985 ("[x = 1]", NONE, []) => ()
986 | _ => error "diff.behav.in ctree.sml: ME_Misc.pt_extract ([], Res)";
987 ========== inhibit exn AK110719 ==============================================*)
989 "=====new ctree 6 minisubpbl intersteps ==========================";
990 "=====new ctree 6 minisubpbl intersteps ==========================";
991 "=====new ctree 6 minisubpbl intersteps ==========================";
993 CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
994 ("Test", ["sqroot-test", "univariate", "equation", "test"],
995 ["Test", "squ-equ-test-subpbl1"]))];
996 Iterator 1; moveActiveRoot 1;
997 autoCalculate 1 CompleteCalc;
998 interSteps 1 ([2],Res);
999 interSteps 1 ([3,2],Res);
1000 val ((pt,_),_) = get_calc 1;
1001 Test_Tool.show_pt pt;
1003 (**##############################################################**)
1004 "-------------- get_allpos' new ----------------------------------";
1005 "-------------- get_allpos' new ----------------------------------";
1006 "-------------- get_allpos' new ----------------------------------";
1008 (*default_print_depth 99;*)
1009 val cuts = get_allp [] ([], ([],Frm)) pt;
1010 (*default_print_depth 3;*)
1012 [(*never returns the first pos'*)
1015 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1016 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1019 ([3, 1], Frm), ([3, 1], Res),
1020 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1024 ([], Res)] then () else
1025 error "ctree.sml diff.behav. get_allp new []";
1027 (*default_print_depth 99;*)
1028 val cuts2 = get_allps [] [1] (children pt);
1029 (*default_print_depth 3;*)
1030 if cuts = cuts2 @ [([], Res)] then () else
1031 error "ctree.sml diff.behav. get_allps new []";
1033 "---(3) on S(606)..S(608)--------";
1034 "--- nd [2] with 6 children---------------------------------";
1035 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
1037 [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1038 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1039 ([2], Res)] then () else
1040 error "ctree.sml diff.behav. get_allp new [2]";
1042 val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
1043 if cuts = cuts2 @ [([2], Res)] then () else
1044 error "ctree.sml diff.behav. get_allps new [2]";
1047 "---(4) on S(606)..S(608)--------";
1048 "--- nd [3] subproblem--------------------------------------";
1049 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
1053 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1055 ([3], Res)] then () else
1056 error "ctree.sml diff.behav. get_allp new [3]";
1058 val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
1059 if cuts = cuts2 @ [([3], Res)] then () else
1060 error "ctree.sml diff.behav. get_allps new [3]";
1062 "--- nd [3,2] with 2 children--------------------------------";
1063 val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
1065 [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1066 ([3, 2], Res)] then () else
1067 error "ctree.sml diff.behav. get_allp new [3,2]";
1069 val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
1070 if cuts = cuts2 @ [([3, 2], Res)] then () else
1071 error "ctree.sml diff.behav. get_allps new [3,2]";
1073 "---(5a) on S(606)..S(608)--------";
1074 "--- nd [3,2,1] with 0 children------------------------------";
1075 val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
1078 error "ctree.sml diff.behav. get_allp new [3,2,1]";
1080 val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
1081 if cuts = cuts2 @ [] then () else
1082 error "ctree.sml diff.behav. get_allps new [3,2,1]";
1085 (**#################################################################**)
1086 "-------------- cut_tree new (from ctree above)-------------------";
1087 "-------------- cut_tree new (from ctree above)-------------------";
1088 "-------------- cut_tree new (from ctree above)-------------------";
1089 Test_Tool.show_pt pt;
1090 val b = get_obj g_branch pt [];
1091 if b = TransitiveB then () else
1092 error ("ctree.sml diff.behav. in [] branch="^branch2str b);
1093 val b = get_obj g_branch pt [3];
1094 if b = TransitiveB then () else
1095 error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
1097 "---(2) on S(606)..S(608)--------";
1098 val (pt', cuts) = cut_tree pt ([1],Res);
1099 (*default_print_depth 99;*)
1101 (*default_print_depth 3;*)
1102 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1103 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1104 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1105 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1106 ([], Res)] then () else
1107 error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1110 "---(3) on S(606)..S(608)--------";
1111 val (pt', cuts) = cut_tree pt ([2],Res);
1112 (*default_print_depth 99;*)
1114 (*default_print_depth 3;*)
1115 if cuts = [(*preceding step on WS was ([1]),Res*)
1116 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1117 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1122 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1127 else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1129 "---(4) on S(606)..S(608)--------";
1130 val (pt', cuts) = cut_tree pt ([3],Pbl);
1131 (*default_print_depth 99;*)
1133 (*default_print_depth 3;*)
1134 if cuts = [([3], Pbl),
1135 ([3, 1], Frm), ([3, 1], Res),
1136 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1141 then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1143 "---(5a) on S(606)..S(608) cut_tree --------";
1144 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1145 (*default_print_depth 99;*)
1147 (*default_print_depth 1;*)
1148 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),([],Res)] then ()
1149 else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1150 Test_Tool.show_pt pt';
1153 "-------------- cappend on complete ctree from above -------------";
1154 "-------------- cappend on complete ctree from above -------------";
1155 "-------------- cappend on complete ctree from above -------------";
1156 Test_Tool.show_pt pt;
1158 "---(2) on S(606)..S(608)--------";
1159 (*========== inhibit exn AK110726 ==============================================
1160 (* ERROR: Can't unify istate to istate * Proof.context *)
1161 val (pt', cuts) = cappend_atomic pt [1] Istate.empty (TermC.str2term "Inform[1]")
1162 (Tac "test") (TermC.str2term "Inres[1]",[]) Complete;
1164 (*default_print_depth 99;*)
1166 (*default_print_depth 3;*)
1167 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1168 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1169 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1170 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1172 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1174 val afterins = get_allp [] ([], ([],Frm)) pt';
1175 (*default_print_depth 99;*)
1177 (*default_print_depth 3;*)
1178 if afterins = [([1], Frm), ([1], Res)] then()
1179 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1180 Test_Tool.show_pt pt';
1181 "---(3) on S(606)..S(608)--------";
1182 Test_Tool.show_pt pt;
1183 val (pt', cuts) = cappend_atomic pt [2] Istate.empty (TermC.str2term "Inform[2]")
1184 (Tac "test") (TermC.str2term "Inres[2]",[]) Complete;
1185 (*default_print_depth 99;*)
1187 (*default_print_depth 3;*)
1189 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1190 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1191 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1192 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1194 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1197 val afterins = get_allp [] ([], ([],Frm)) pt';
1198 (*default_print_depth 99;*)
1200 (*default_print_depth 3;*)
1202 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)]
1204 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1205 Test_Tool.show_pt pt';
1209 val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
1210 val p = move_dn [] pt' p (*-> ([1],Res)*);
1211 val p = move_dn [] pt' p (*-> ([2],Frm)*);
1212 val p = move_dn [] pt' p (*-> ([2],Res)*);
1214 UnparseC.term (get_obj g_form pt' [2]);
1215 UnparseC.term (get_obj g_res pt' [2]);
1216 ostate2str (get_obj g_ostate pt' [2]);
1219 "---(4) on S(606)..S(608)--------";
1220 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],References.empty)
1221 ([],References.empty, TermC.str2term "Inhead[3]", ContextC.empty);
1222 (*default_print_depth 99;*)
1224 (*default_print_depth 3;*)
1225 if cuts = [([3], Pbl),
1226 ([3, 1], Frm), ([3, 1], Res),
1227 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1229 ([3], Res), ([4], Res),
1230 ([], Res)] then ()else
1231 error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1232 val afterins = get_allp [] ([], ([],Frm)) pt';
1233 (*default_print_depth 99;*)
1235 (*default_print_depth 3;*)
1237 [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1238 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
1239 ([3], Pbl)] then () else
1240 error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
1241 (* use"systest/ctree.sml";
1245 "---(6-1) on S(606)..S(608)--------";
1246 val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (TermC.str2term "Inform[3,1]")
1247 (Tac "test") (TermC.str2term "Inres[3,1]",[]) Complete;
1248 (*default_print_depth 99;*)
1250 (*default_print_depth 3;*)
1251 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1253 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
1254 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
1256 val afterins = get_allp [] ([], ([],Frm)) pt';
1257 (*default_print_depth 99;*)
1259 (*default_print_depth 3;*)
1260 if afterins = [([1], Frm), ([1], Res),
1261 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1262 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1265 ([3, 1], Frm), ([3, 1], Res)] then () else
1266 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1268 if UnparseC.term (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
1269 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1271 "---(6) on S(606)..S(608)--------";
1272 val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (TermC.str2term "Inform[3,2]")
1273 (Tac "test") (TermC.str2term "Inres[3,2]",[]) Complete;
1274 (*default_print_depth 99;*)
1276 (*default_print_depth 3;*)
1277 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else
1278 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1279 val afterins = get_allp [] ([], ([],Frm)) pt';
1280 (*default_print_depth 99;*)
1282 (*default_print_depth 3;*)
1283 if afterins = [([1], Frm), ([1], Res),
1284 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1285 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1288 ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
1290 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1292 if UnparseC.term (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
1293 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
1295 "---(6++) on S(606)..S(608)--------";
1297 val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.str2term "Inform[3,2,1]")
1298 (Tac "test") (TermC.str2term "Inres[3,2,1]",[]) Complete;
1299 (*default_print_depth 99;*)
1301 (*default_print_depth 1;*)
1302 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)]
1304 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1305 val afterins = get_allp [] ([], ([],Frm)) pt';
1306 (*default_print_depth 99;*)
1308 (*default_print_depth 3;*)
1309 if afterins = [([1], Frm), ([1], Res),
1310 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1311 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1314 ([3, 1], Frm), ([3, 1], Res),
1315 ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
1316 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
1317 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
1318 error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
1320 Test_Tool.show_pt pt';
1321 Test_Tool.show_pt pt;
1323 ========== inhibit exn AK110726 ==============================================*)
1324 "-------------- repl_app------------------------------------------";
1325 "-------------- repl_app------------------------------------------";
1326 "-------------- repl_app------------------------------------------";
1328 > repl [1,2,3] 2 22222;
1329 val it = [1,22222,3] : int list
1330 > repl_app [1,2,3,4] 5 5555;
1331 val it = [1,2,3,4,5555] : int list
1332 > repl_app [1,2,3] 2 22222;
1333 val it = [1,22222,3] : int list
1334 > repl_app [1] 2 22222 ;
1335 val it = [1,22222] : int list