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 -------------------------------------";
14 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
15 "-------------- check positions in miniscript --------------------";
16 "-------------- get_allpos' (from ptree above)--------------------";
17 "-------------- cut_level (from ptree above)----------------------";
18 "-------------- cut_tree (from ptree above)-----------------------";
19 "=====new ptree 1a miniscript with mini-subpbl ===================";
20 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
21 "=====new ptree 2 miniscript with mini-subpbl ====================";
22 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
23 "-------------- cappend (from ptree above)------------------------";
24 "-------------- cappend minisubpbl -------------------------------";
25 "=====new ptree 3 ================================================";
26 "-------------- move_dn ------------------------------------------";
27 "-------------- move_dn: Frm -> Res ------------------------------";
28 "-------------- move_up ------------------------------------------";
29 "------ move into detail -----------------------------------------";
30 "=====new ptree 3a ===============================================";
31 "-------------- move_dn in Incomplete ctree ----------------------";
32 "=====new ptree 4: crooked by cut_level_'_ =======================";
33 (*############## development stopped 0501 ########################*)
34 (******************************************************************)
35 (* val SAVE_get_trace = get_trace; *)
36 (******************************************************************)
37 "-------------- get_interval from ctree: incremental development--";
38 (******************************************************************)
39 (* val get_trace = SAVE_get_trace; *)
40 (******************************************************************)
41 (*############## development stopped 0501 ########################*)
42 "=====new ptree 4 ratequation ====================================";
43 "-------------- pt_extract form, tac, asm<>[] --------------------";
44 "=====new ptree 5 minisubpbl =====================================";
45 "-------------- pt_extract form, tac, asm ------------------------";
46 "=====new ptree 6 minisubpbl intersteps ==========================";
47 "-------------- get_allpos' new ----------------------------------";
48 "-------------- cut_tree new (from ptree above)-------------------";
49 "-----------------------------------------------------------------";
50 "-----------------------------------------------------------------";
51 "-----------------------------------------------------------------";
54 "-------------- fun get_ctxt -------------------------------------";
55 "-------------- fun get_ctxt -------------------------------------";
56 "-------------- fun get_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";
68 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
69 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
70 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
72 val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
73 val ctxt = get_obj g_ctxt pt [];
74 if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
75 val pt = update_ctxt pt [] (ProofContext.init_global @{theory "Isac"});
76 if (get_obj g_ctxt pt [] |> ProofContext.theory_of |> Context.theory_name) = "Isac"
77 then () else error "--- fun update_ctxt, fun g_ctxt changed";
79 "-------------- check positions in miniscript --------------------";
80 "-------------- check positions in miniscript --------------------";
81 "-------------- check positions in miniscript --------------------";
82 val fmz = ["equality (x+1=(2::real))",
83 "solveFor x","solutions L"];
85 ("Test",["sqroot-test","univariate","equation","test"],
86 ["Test","squ-equ-test-subpbl1"]);
87 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
89 (* nxt = Add_Given "equality (x + 1 = 2)"
90 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
96 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 "ctree.sml-------------- get_allpos' new ------------------------\"";
102 val (PP, pp) = split_last [1];
103 val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);
105 val cuts = get_allp [] ([], ([],Frm)) pt;
106 val cuts2 = get_allps [] [1] (children pt);
107 "ctree.sml-------------- cut_tree new (from ptree above)----------";
108 val (pt', cuts) = cut_tree pt ([1],Frm);
109 "ctree.sml-------------- cappend on complete ctree from above ----";
110 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
111 "----------------------------------------------------------------/";
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 (*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 (*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
133 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
134 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
135 else error "new behaviour in test: miniscript with mini-subpbl";
139 "-------------- get_allpos' (from ptree above)--------------------";
140 "-------------- get_allpos' (from ptree above)--------------------";
141 "-------------- get_allpos' (from ptree above)--------------------";
142 if get_allpos' ([], 1) pt =
154 then () else error "ctree.sml: diff:behav. in get_allpos' 1";
156 if get_allpos's ([], 1) (children pt) =
166 then () else error "ctree.sml: diff:behav. in get_allpos' 2";
168 if get_allpos's ([], 2) (takerest (1, children pt)) =
176 then () else error "ctree.sml: diff:behav. in get_allpos' 3";
178 if get_allpos's ([], 3) (takerest (2, children pt)) =
185 then () else error "ctree.sml: diff:behav. in get_allpos' 4";
187 if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
191 then () else error "ctree.sml: diff:behav. in get_allpos' 5";
193 if get_allpos' ([3], 1) (nth 3 (children pt)) =
199 then () else error "ctree.sml: diff:behav. in get_allpos' 6";
206 "-------------- cut_level (from ptree above)----------------------";
207 "-------------- cut_level (from ptree above)----------------------";
208 "-------------- cut_level (from ptree above)----------------------";
211 print_depth 99; cuts; print_depth 3;
213 (*if cuts = [([2], Res),
220 then () else error "ctree.sml: diff:behav. in cut_level 1a";
221 val (res,asm) = get_obj g_result pt' [2];
222 if res = e_term andalso asm = [] then () else
223 error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
224 if not (existpt [2] pt') then () else
225 error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
227 val (res,asm) = get_obj g_result pt' [];
229 (*============ inhibit exn AK110726 ==============================================
230 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
231 error "ctree.sml: diff:behav. in cut_level 1ab";
232 ============ inhibit exn AK110726 ==============================================*)
233 (*============ inhibit exn AK110726 ==============================================
234 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
238 ([2], Res),(*, e_term in cut_tree!!!*)
239 ([], Res)] then () else
240 error "ctree.sml: diff:behav. in cut_level 1b";
241 ============ inhibit exn AK110726 ==============================================*)
243 val (pt',cuts) = cut_level [] [] pt ([2],Res);
244 if cuts = [([3], Frm),
250 then () else error "ctree.sml: diff:behav. in cut_level 2a";
252 if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
253 then () else error "ctree.sml: diff:behav. in cut_level 2b";
255 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
256 if cuts = [([3, 1], Res), ([3, 2], Res)]
257 then () else error "ctree.sml: diff:behav. in cut_level 3a";
258 if pr_ptree 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"
259 then () else error "ctree.sml: diff:behav. in cut_level 3b";
261 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
262 if cuts = [([3, 2], Res)]
263 then () else error "ctree.sml: diff:behav. in cut_level 4a";
264 if pr_ptree 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"
265 then () else error "ctree.sml: diff:behav. in cut_level 4b";
268 "-------------- cut_tree (from ptree above)-----------------------";
269 "-------------- cut_tree (from ptree above)-----------------------";
270 "-------------- cut_tree (from ptree above)-----------------------";
271 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
273 (*============ inhibit exn AK110726 ==============================================
274 if cuts = [([2], Res),
282 then () else error "ctree.sml: diff:behav. in cut_tree 1a";
284 val (res,asm) = get_obj g_result pt' [2];
285 ============ inhibit exn AK110726 ==============================================*)
287 if res = e_term (*WN050219 done by cut_level*) then () else
288 error "ctree.sml: diff:behav. in cut_tree 1aa";
290 (*============ inhibit exn AK110726 ==============================================
291 val form = get_obj g_form pt' [2];
292 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
293 error "ctree.sml: diff:behav. in cut_tree 1ab";
294 ============ inhibit exn AK110726 ==============================================*)
296 (* get_obj g_form pt' [2];
297 (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"
298 raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)
299 "~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)
301 val (res,asm) = get_obj g_result pt' [];
302 if res = e_term (*WN050219 done by cut_tree*) then () else
303 error "ctree.sml: diff:behav. in cut_tree 1ac";
305 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
308 ([1], Res)] then () else
309 error "ctree.sml: diff:behav. in cut_tree 1ad";
311 val (pt', cuts) = cut_tree pt ([2],Res);
312 (*============ inhibit exn AK110726 ==============================================
313 if cuts = [([3], Frm),
320 then () else error "ctree.sml: diff:behav. in cut_tree 2";
321 ============ inhibit exn AK110726 ==============================================*)
323 val (pt', cuts) = cut_tree pt ([3,1],Frm);
324 (*============ inhibit exn AK110726 ==============================================
325 if cuts = [([3, 1], Res),
330 then () else error "ctree.sml: diff:behav. in cut_tree 3";
331 ============ inhibit exn AK110726 ==============================================*)
333 val (pt', cuts) = cut_tree pt ([3,1],Res);
334 if cuts = [([3, 2], Res),
338 then () else error "ctree.sml: diff:behav. in cut_tree 4";
340 "=====new ptree 1a miniscript with mini-subpbl ===================";
341 "=====new ptree 1a miniscript with mini-subpbl ===================";
342 "=====new ptree 1a miniscript with mini-subpbl ===================";
343 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
345 ("Test",["sqroot-test","univariate","equation","test"],
346 ["Test","squ-equ-test-subpbl1"]);
347 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
353 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
354 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
358 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
359 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
360 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
362 val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
363 if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
364 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
366 val (pt', cuts) = cut_tree pt ([1],Frm);
368 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
371 val pos as ([p],_) = ([1],Frm);
372 val pt as Nd (b,_) = pt;
377 print_depth 99;cuts;print_depth 3;
378 print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
379 ####################################################################*)
383 "=====new ptree 2 miniscript with mini-subpbl ====================";
384 "=====new ptree 2 miniscript with mini-subpbl ====================";
385 "=====new ptree 2 miniscript with mini-subpbl ====================";
387 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
388 ("Test", ["sqroot-test","univariate","equation","test"],
389 ["Test","squ-equ-test-subpbl1"]))];
390 Iterator 1; moveActiveRoot 1;
391 autoCalculate 1 CompleteCalc;
393 interSteps 1 ([3,2],Res);
395 val ((pt,_),_) = get_calc 1;
398 if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
399 else error "mini-subpbl interSteps broken";
401 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
402 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
403 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
404 (*WN050225 intermed. outcommented
405 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
406 if cuts = [([3, 2, 1], Res),
411 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
413 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
414 if cuts = [([3, 2, 2], Res),
418 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
421 "-------------- cappend (from ptree above)------------------------";
422 "-------------- cappend (from ptree above)------------------------";
423 "-------------- cappend (from ptree above)------------------------";
424 val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
425 if cuts = [([3, 2, 1], Res),
431 then () else error "ctree.sml: diff:behav. in cappend_form";
432 if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
433 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
434 term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
435 then () else error "ctree.sml: diff:behav. in cappend 1";
437 val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
438 (Tac "test") (str2term "newresult",[]) Complete;
439 if cuts = [([3, 2, 1], Res), (*?????????????*)
445 then () else error "ctree.sml: diff:behav. in cappend_atomic";
449 "-------------- cappend minisubpbl -------------------------------";
450 "-------------- cappend minisubpbl -------------------------------";
451 "-------------- cappend minisubpbl -------------------------------";
452 "=====new ptree 1 miniscript with mini-subpbl ====================";
453 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
455 ("Test",["sqroot-test","univariate","equation","test"],
456 ["Test","squ-equ-test-subpbl1"]);
457 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
459 (* nxt = Add_Given "equality (x + 1 = 2)"
460 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
462 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
463 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
465 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
466 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
468 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
471 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
472 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
474 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
476 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
477 val form = get_obj g_form pt (fst p);
478 val (res,_) = get_obj g_result pt (fst p);
479 if term2str form = "x + 1 = 2" andalso res = e_term then () else
480 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
481 if not (existpt ((lev_on o fst) p) pt) then () else
482 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
484 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
487 cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
488 Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
489 val form = get_obj g_form pt (fst p);
490 val (res,_) = get_obj g_result pt (fst p);
491 if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
492 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
493 if not (existpt ((lev_on o fst) p) pt) then () else
494 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
496 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
499 cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
500 Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
501 val form = get_obj g_form pt (fst p);
502 val (res,_) = get_obj g_result pt (fst p);
503 if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
504 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
505 if not (existpt ((lev_on o fst) p) pt) then () else
506 error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
509 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
511 val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
512 if is_pblobj (get_obj I pt (fst p)) then () else
513 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
514 if not (existpt ((lev_on o fst) p) pt) then () else
515 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
517 (* ...complete calchead skipped...*)
519 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
520 val p = ([3, 1], Frm);
521 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
522 val form = get_obj g_form pt (fst p);
523 val (res,_) = get_obj g_result pt (fst p);
524 if term2str form = "-1 + x = 0" andalso res = e_term then () else
525 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
526 if not (existpt ((lev_on o fst) p) pt) then () else
527 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
529 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
530 val p = ([3, 1], Res);
532 cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
533 Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
534 val form = get_obj g_form pt (fst p);
535 val (res,_) = get_obj g_result pt (fst p);
536 if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
537 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
538 if not (existpt ((lev_on o fst) p) pt) then () else
539 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
541 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
542 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
543 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
544 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
545 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
546 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
548 WN050225 intermed. outcommented---*)
550 "=====new ptree 3 ================================================";
551 "=====new ptree 3 ================================================";
552 "=====new ptree 3 ================================================";
555 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
556 ("Test", ["sqroot-test","univariate","equation","test"],
557 ["Test","squ-equ-test-subpbl1"]))];
558 Iterator 1; moveActiveRoot 1;
559 autoCalculate 1 CompleteCalc;
561 val ((pt,_),_) = get_calc 1;
564 "-------------- move_dn ------------------------------------------";
565 "-------------- move_dn ------------------------------------------";
566 "-------------- move_dn ------------------------------------------";
567 val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);
568 val p = move_dn [] pt p (*-> ([1],Res)*);
569 val p = move_dn [] pt p (*-> ([2],Res)*);
570 val p = move_dn [] pt p (*-> ([3],Pbl)*);
571 val p = move_dn [] pt p (*-> ([3,1],Frm)*);
572 val p = move_dn [] pt p (*-> ([3,1],Res)*);
573 val p = move_dn [] pt p (*-> ([3,2],Res)*);
574 val p = move_dn [] pt p (*-> ([3],Res)*);
575 (* term2str (get_obj g_res pt [3]);
576 term2str (get_obj g_form pt [4]);
578 val p = move_dn [] pt p (*-> ([4],Res)*);
579 val p = move_dn [] pt p (*-> ([],Res)*);
581 val p = (move_dn [] pt p) handle e => print_exn_G e;
582 Exception PTREE end of calculation*)
584 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
586 "-------------- move_dn: Frm -> Res ------------------------------";
587 "-------------- move_dn: Frm -> Res ------------------------------";
588 "-------------- move_dn: Frm -> Res ------------------------------";
590 CalcTree (*start of calculation, return No.1*)
591 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
593 ["linear","univariate","equation","test"],
594 ["Test","solve_linear"]))];
595 Iterator 1; moveActiveRoot 1;
596 autoCalculate 1 CompleteCalcHead;
597 autoCalculate 1 (Step 1);
598 refFormula 1 (get_pos 1 1);
602 if get_pos 1 1 = ([1], Frm) then ()
603 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
604 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
606 autoCalculate 1 (Step 1);
607 refFormula 1 (get_pos 1 1);
609 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
610 if get_pos 1 1 = ([1], Res) then ()
611 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
612 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
615 "-------------- move_up ------------------------------------------";
616 "-------------- move_up ------------------------------------------";
617 "-------------- move_up ------------------------------------------";
618 val p = move_up [] pt ([],Res); (*-> ([4],Res)*)
619 val p = move_up [] pt p; (*-> ([3],Res)*)
620 val p = move_up [] pt p; (*-> ([3,2],Res)*)
621 val p = move_up [] pt p; (*-> ([3,1],Res)*)
622 val p = move_up [] pt p; (*-> ([3,1],Frm)*)
623 val p = move_up [] pt p; (*-> ([3],Pbl)*)
624 val p = move_up [] pt p; (*-> ([2],Res)*)
625 val p = move_up [] pt p; (*-> ([1],Res)*)
626 val p = move_up [] pt p; (*-> ([1],Frm)*)
627 val p = move_up [] pt p; (*-> ([],Pbl)*)
628 (*val p = (move_up [] pt p) handle e => print_exn_G e;
629 Exception PTREE begin of calculation*)
631 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
633 "------ move into detail -----------------------------------------";
634 "------ move into detail -----------------------------------------";
635 "------ move into detail -----------------------------------------";
637 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
638 ("Test", ["sqroot-test","univariate","equation","test"],
639 ["Test","squ-equ-test-subpbl1"]))];
640 Iterator 1; moveActiveRoot 1;
641 autoCalculate 1 CompleteCalc;
646 refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
648 interSteps 1 ([2],Res);
650 val ((pt,_),_) = get_calc 1; show_pt pt;
653 val p = move_up [] pt p; (*([2, 6], Res)*);
654 val p = movelevel_up [] pt p;(*([2], Frm)*);
655 val p = move_dn [] pt p; (*([2, 1], Frm)*);
656 val p = move_dn [] pt p; (*([2, 1], Res)*);
657 val p = move_dn [] pt p; (*([2, 2], Res)*);
658 val p = move_dn [] pt p; (*([2, 3], Res)*);
659 val p = move_dn [] pt p; (*([2, 4], Res)*);
660 val p = move_dn [] pt p; (*([2, 5], Res)*);
661 val p = move_dn [] pt p; (*([2, 6], Res)*);
662 if p = ([2, 6], Res) then()
663 else error "ctree.sml: diff.behav. in move into detail";
665 "=====new ptree 3a ===============================================";
666 "=====new ptree 3a ===============================================";
667 "=====new ptree 3a ===============================================";
669 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
670 ("Test", ["sqroot-test","univariate","equation","test"],
671 ["Test","squ-equ-test-subpbl1"]))];
672 Iterator 1; moveActiveRoot 1;
673 autoCalculate 1 CompleteCalcHead;
674 autoCalculate 1 (Step 1);
675 autoCalculate 1 (Step 1);
676 autoCalculate 1 (Step 1);
677 val ((pt,_),_) = get_calc 1;
678 val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
679 val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
680 val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
681 (*val p = move_dn [] pt ([2], Res) ->Exception- PTREE "[] not complete"*);
683 moveDown 1 ([],Pbl) (*-> ([1], Frm)*);
684 moveDown 1 ([1],Frm) (*-> ([1],Res)*);
685 moveDown 1 ([1],Res) (*-> ([2],Res)*);
686 moveDown 1 ([2],Res) (*-> pos does not exist*);
688 get_obj g_ostate pt [1];
692 "-------------- move_dn in Incomplete ctree ----------------------";
693 "-------------- move_dn in Incomplete ctree ----------------------";
694 "-------------- move_dn in Incomplete ctree ----------------------";
698 "=====new ptree 4: crooked by cut_level_'_ =======================";
699 "=====new ptree 4: crooked by cut_level_'_ =======================";
700 "=====new ptree 4: crooked by cut_level_'_ =======================";
703 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
704 "solveFor x","solutions L"],
705 ("RatEq",["univariate","equation"],["no_met"]))];
706 Iterator 1; moveActiveRoot 1;
707 autoCalculate 1 CompleteCalc;
709 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
710 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
711 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
712 getTactic 1 ([4,1],Res);(*Rewrite all_left*)
713 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
714 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
716 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
717 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
718 moveActiveFormula 1 ([3],Res)(*3.1.*);
719 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
720 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
722 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
723 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
725 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
726 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
727 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
728 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
730 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
731 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
732 val ((pt,_),_) = get_calc 1;
733 writeln(pr_ptree pr_short pt);
734 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
735 ###########################################################################*)
736 val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
737 writeln(pr_ptree pr_short pt);
743 "-------------- get_interval from ctree: incremental development--";
744 "-------------- get_interval from ctree: incremental development--";
745 "-------------- get_interval from ctree: incremental development--";
746 "--- level 1: get pos from start b to end p ----------------------";
747 "--- level 1: get pos from start b to end p ----------------------";
748 "--- level 1: get pos from start b to end p ----------------------";
749 (******************************************************************)
750 (**) val SAVE_get_trace = get_trace; (**)
751 (******************************************************************)
752 (*'getnds' below is structured as such:*)
753 fun www _ [x] = "l+r-margin"
754 | www true [x1,x2] = "l-margin, r-margin"
755 | www _ [x1,x2] = "intern, r-margin"
756 | www true (x::(xs as _::_)) = "l-margin " ^ www false xs
757 | www _ (x::(xs as _::_)) = "intern " ^ www false xs;
758 www true [1,2,3,4,5];
759 (*val it = "from intern intern intern to" : string*)
761 (*val it = "from to" : string*)
763 (*val it = "from+to" : string*)
766 (*specific values of hd of pos p,q for simple handling take_fromto,
767 from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
768 ... can be used even for positions _below_ p or q*)
769 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
770 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
771 (*analoguous for tl*)
772 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
773 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
775 (*see modspec.sml#pt_form
776 fun pt_form (PrfObj {form,...}) = term2str form
777 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
778 let val (dI, pI, _) = get_somespec' spec spec'
779 val {cas,...} = get_pbt pI
781 NONE => term2str (pblterm dI pI)
782 | SOME t => term2str (subst_atomic (mk_env probl) t)
785 (*.get an 'interval' from ptree down to a certain level
786 by 'take_fromto children' of the nodes with specific 'from' and 'to';
787 'i > 0' suppresses output during recursive descent towards 'from'
788 b: the 'from' incremented to the actual pos
789 p,q: specific 'from','to' for simple use of 'take_fromto'*)
790 fun getnd i (b,p) q (Nd (po, nds)) =
791 (if i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
793 @ (writeln("getnd : b="^(ints2str' b)^", p="^
794 (ints2str' p)^", q="^(ints2str' q));
796 getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
797 (take_fromto (hdp p) (hdq q) nds))
799 and getnds _ _ _ _ [] = [] (*no children*)
800 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
801 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
802 (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
803 ", q="^ ints2str' q);
804 (getnd i ( b, p ) [99999] n1) @
805 (getnd ~99999 (lev_on b,[0]) q n2))
806 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
807 (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
808 ", q="^ ints2str' q);
809 (getnd i ( b,[0]) [99999] n1) @
810 (getnd ~99999 (lev_on b,[0]) q n2))
811 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
812 (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
813 ", q="^ ints2str' q);
814 (getnd i ( b, p ) [99999] nd) @
815 (getnds ~99999 false (lev_on b,[0]) q nds))
816 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
817 (getnd i ( b,[0]) [99999] nd) @
818 (getnds ~99999 false (lev_on b,[0]) q nds);
820 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
821 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
822 (1) the 'f' are given
823 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
824 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
826 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
827 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
828 the 'f' and 't' are set by hdp,... *)
829 fun get_trace pt p q =
830 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
831 (take_fromto (hdp p) (hdq q) (children pt));
834 writeln(pr_ptree pr_short pt);
836 case get_trace pt [1,3] [4,1,1] of
837 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
838 | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
839 case get_trace pt [2] [4,3,2] of
840 [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
841 | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
842 case get_trace pt [1,4] [4,3,1] of
843 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
844 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
847 (*========== inhibit exn AK110719 ==============================================
848 case get_trace pt [4,2] [5] of
849 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
850 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
851 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
852 | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
853 ========== inhibit exn AK110719 ==============================================*)
855 case get_trace pt [] [4,4,2] of
856 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
857 [4,3],[4,3,1],[4,3,2]] => ()
858 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
860 (*========== inhibit exn AK110719 ==============================================
861 case get_trace pt [] [] of
862 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
863 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
864 | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
865 case get_trace pt [4,3] [4,3] of
866 [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
867 | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
868 ========== inhibit exn AK110719 ==============================================*)
870 "--- level 2: get pos' from start b to end p ---------------------";
871 "--- level 2: get pos' from start b to end p ---------------------";
872 "--- level 2: get pos' from start b to end p ---------------------";
873 (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
874 development stopped in favour of move_dn, see get_interval
875 actually used (inefficient) version with move_dn: see modspec.sml
878 case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
879 [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
880 | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
881 case get_trace pt ([],Pbl) ([],Res) of
882 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
883 [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
884 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
887 (******************************************************************)
888 (**) val get_trace = SAVE_get_trace; (**)
889 (******************************************************************)
892 "=====new ptree 4 ratequation ====================================";
893 "=====new ptree 4 ratequation ====================================";
894 "=====new ptree 4 ratequation ====================================";
897 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
898 "solveFor x","solutions L"],
899 ("RatEq",["univariate","equation"],["no_met"]))];
900 Iterator 1; moveActiveRoot 1;
901 autoCalculate 1 CompleteCalc;
902 val ((pt,_),_) = get_calc 1;
906 "-------------- pt_extract form, tac, asm<>[] --------------------";
907 "-------------- pt_extract form, tac, asm<>[] --------------------";
908 "-------------- pt_extract form, tac, asm<>[] --------------------";
909 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
910 case (term2str form, tac, terms2strs asm) of
911 ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
914 ["normalize", "polynomial", "univariate", "equation"]),
915 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
916 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
917 (*WN060717 unintentionally changed some rls/ord while
918 completing knowl. for thes2file...
920 case (term2str form, tac, terms2strs asm) of
921 ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
924 ["normalize", "polynomial", "univariate", "equation"]),
925 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
926 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
928 .... but it became even better*)
932 "=====new ptree 5 minisubpbl =====================================";
933 "=====new ptree 5 minisubpbl =====================================";
934 "=====new ptree 5 minisubpbl =====================================";
936 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
937 ("Test", ["sqroot-test","univariate","equation","test"],
938 ["Test","squ-equ-test-subpbl1"]))];
939 Iterator 1; moveActiveRoot 1;
940 autoCalculate 1 CompleteCalc;
941 val ((pt,_),_) = get_calc 1;
944 "-------------- pt_extract form, tac, asm ------------------------";
945 "-------------- pt_extract form, tac, asm ------------------------";
946 "-------------- pt_extract form, tac, asm ------------------------";
947 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
948 case (term2str form, tac, terms2strs asm) of
949 ("solve (x + 1 = 2, x)",
950 Apply_Method ["Test", "squ-equ-test-subpbl1"],
952 | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
954 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
955 case (term2str form, tac, terms2strs asm) of
956 ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
957 | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
959 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
960 case (term2str form, tac, terms2strs asm) of
961 ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
962 | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
964 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
965 case (term2str form, tac, terms2strs asm) of
967 Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
969 | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
971 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
972 case (term2str form, tac, terms2strs asm) of
973 ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
974 | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
976 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
977 case (term2str form, tac, terms2strs asm) of
978 ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
979 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
981 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
982 case (term2str form, tac, terms2strs asm) of
983 ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
984 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
986 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
987 case (term2str form, tac, terms2strs asm) of
988 ("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],
990 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
992 (*========== inhibit exn AK110719 ==============================================
993 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
994 case (term2str form, tac, terms2strs asm) of
995 ("[x = 1]", Check_elementwise "Assumptions", []) => ()
996 | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
998 val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
999 case (term2str form, tac, terms2strs asm) of
1001 Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
1003 | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
1005 val (Form form, tac, asm) = pt_extract (pt, ([], Res));
1006 case (term2str form, tac, terms2strs asm) of
1007 ("[x = 1]", NONE, []) => ()
1008 | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
1009 ========== inhibit exn AK110719 ==============================================*)
1011 "=====new ptree 6 minisubpbl intersteps ==========================";
1012 "=====new ptree 6 minisubpbl intersteps ==========================";
1013 "=====new ptree 6 minisubpbl intersteps ==========================";
1015 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1016 ("Test", ["sqroot-test","univariate","equation","test"],
1017 ["Test","squ-equ-test-subpbl1"]))];
1018 Iterator 1; moveActiveRoot 1;
1019 autoCalculate 1 CompleteCalc;
1020 interSteps 1 ([2],Res);
1021 interSteps 1 ([3,2],Res);
1022 val ((pt,_),_) = get_calc 1;
1025 (**##############################################################**)
1026 "-------------- get_allpos' new ----------------------------------";
1027 "-------------- get_allpos' new ----------------------------------";
1028 "-------------- get_allpos' new ----------------------------------";
1031 val cuts = get_allp [] ([], ([],Frm)) pt;
1034 [(*never returns the first pos'*)
1037 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1038 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1041 ([3, 1], Frm), ([3, 1], Res),
1042 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1046 ([], Res)] then () else
1047 error "ctree.sml diff.behav. get_allp new []";
1050 val cuts2 = get_allps [] [1] (children pt);
1052 if cuts = cuts2 @ [([], Res)] then () else
1053 error "ctree.sml diff.behav. get_allps new []";
1055 "---(3) on S(606)..S(608)--------";
1056 "--- nd [2] with 6 children---------------------------------";
1057 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
1059 [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1060 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1061 ([2], Res)] then () else
1062 error "ctree.sml diff.behav. get_allp new [2]";
1064 val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
1065 if cuts = cuts2 @ [([2], Res)] then () else
1066 error "ctree.sml diff.behav. get_allps new [2]";
1069 "---(4) on S(606)..S(608)--------";
1070 "--- nd [3] subproblem--------------------------------------";
1071 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
1075 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1077 ([3], Res)] then () else
1078 error "ctree.sml diff.behav. get_allp new [3]";
1080 val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
1081 if cuts = cuts2 @ [([3], Res)] then () else
1082 error "ctree.sml diff.behav. get_allps new [3]";
1084 "--- nd [3,2] with 2 children--------------------------------";
1085 val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
1087 [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1088 ([3, 2], Res)] then () else
1089 error "ctree.sml diff.behav. get_allp new [3,2]";
1091 val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
1092 if cuts = cuts2 @ [([3, 2], Res)] then () else
1093 error "ctree.sml diff.behav. get_allps new [3,2]";
1095 "---(5a) on S(606)..S(608)--------";
1096 "--- nd [3,2,1] with 0 children------------------------------";
1097 val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
1100 error "ctree.sml diff.behav. get_allp new [3,2,1]";
1102 val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
1103 if cuts = cuts2 @ [] then () else
1104 error "ctree.sml diff.behav. get_allps new [3,2,1]";
1107 (**#################################################################**)
1108 "-------------- cut_tree new (from ptree above)-------------------";
1109 "-------------- cut_tree new (from ptree above)-------------------";
1110 "-------------- cut_tree new (from ptree above)-------------------";
1112 val b = get_obj g_branch pt [];
1113 if b = TransitiveB then () else
1114 error ("ctree.sml diff.behav. in [] branch="^branch2str b);
1115 val b = get_obj g_branch pt [3];
1116 if b = TransitiveB then () else
1117 error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
1119 "---(2) on S(606)..S(608)--------";
1120 val (pt', cuts) = cut_tree pt ([1],Res);
1124 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1125 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1126 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1127 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1128 (*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
1129 error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1132 "---(3) on S(606)..S(608)--------";
1133 val (pt', cuts) = cut_tree pt ([2],Res);
1137 if cuts = [(*preceding step on WS was ([1]),Res*)
1138 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1139 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1144 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1148 (*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
1149 else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1151 "---(4) on S(606)..S(608)--------";
1152 val (pt', cuts) = cut_tree pt ([3],Pbl);
1156 if cuts = [([3], Pbl),
1157 ([3, 1], Frm), ([3, 1], Res),
1158 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1162 (*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
1163 then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1165 "---(5a) on S(606)..S(608) cut_tree --------";
1166 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1170 if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1171 (*WN060727 added after replacing cutlevup by test_trans:*)
1172 ([3], Res), ([4], Res),([],Res)] then ()
1173 else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1177 "-------------- cappend on complete ctree from above -------------";
1178 "-------------- cappend on complete ctree from above -------------";
1179 "-------------- cappend on complete ctree from above -------------";
1182 "---(2) on S(606)..S(608)--------";
1183 (*========== inhibit exn AK110726 ==============================================
1184 (* ERROR: Can't unify istate to istate * Proof.context *)
1185 val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
1186 (Tac "test") (str2term "Inres[1]",[]) Complete;
1191 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1192 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1193 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1194 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1195 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1196 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1198 val afterins = get_allp [] ([], ([],Frm)) pt';
1202 if afterins = [([1], Frm), ([1], Res)
1203 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
1204 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1206 "---(3) on S(606)..S(608)--------";
1208 val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
1209 (Tac "test") (str2term "Inres[2]",[]) Complete;
1214 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1215 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1216 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1217 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1218 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1219 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1222 val afterins = get_allp [] ([], ([],Frm)) pt';
1227 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
1228 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
1230 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1235 val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
1236 val p = move_dn [] pt' p (*-> ([1],Res)*);
1237 val p = move_dn [] pt' p (*-> ([2],Frm)*);
1238 val p = move_dn [] pt' p (*-> ([2],Res)*);
1240 term2str (get_obj g_form pt' [2]);
1241 term2str (get_obj g_res pt' [2]);
1242 ostate2str (get_obj g_ostate pt' [2]);
1245 "---(4) on S(606)..S(608)--------";
1246 val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
1247 ([],e_spec, str2term "Inhead[3]");
1251 if cuts = [([3], Pbl),
1252 ([3, 1], Frm), ([3, 1], Res),
1253 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1255 ([3], Res), ([4], Res),
1256 (*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
1257 error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1258 val afterins = get_allp [] ([], ([],Frm)) pt';
1263 [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1264 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
1265 ([3], Pbl)] then () else
1266 error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
1267 (* use"systest/ctree.sml";
1271 "---(6-1) on S(606)..S(608)--------";
1272 val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
1273 (Tac "test") (str2term "Inres[3,1]",[]) Complete;
1277 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1279 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
1280 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
1282 val afterins = get_allp [] ([], ([],Frm)) pt';
1286 (*WN060727 replaced after overwriting cutlevup by test_trans
1287 if afterins = [([1], Frm), ([1], Res),
1288 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1289 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1292 ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
1293 ([3], Res)(*cutlevup=false*),
1295 ([], Res)(*cutlevup=false*)] then () else
1296 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1298 if afterins = [([1], Frm), ([1], Res),
1299 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1300 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1303 ([3, 1], Frm), ([3, 1], Res)] then () else
1304 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1306 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
1307 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1309 "---(6) on S(606)..S(608)--------";
1310 val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
1311 (Tac "test") (str2term "Inres[3,2]",[]) Complete;
1315 if cuts = [(*just after is: cutlevup=false in [3]*)
1316 (*WN060727 after test_trans instead cutlevup added:*)
1317 ([3], Res), ([4], Res), ([], Res)] then () else
1318 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1319 val afterins = get_allp [] ([], ([],Frm)) pt';
1323 (*WN060727 replaced after overwriting cutlevup by test_trans
1324 if afterins = [([1], Frm), ([1], Res),
1325 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1326 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1329 ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res),
1331 ([4], Res), ([], Res)] then () else
1332 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1334 if afterins = [([1], Frm), ([1], Res),
1335 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1336 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1339 ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
1341 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1343 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
1344 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
1346 "---(6++) on S(606)..S(608)--------";
1348 val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
1349 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
1353 if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1354 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
1356 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1357 val afterins = get_allp [] ([], ([],Frm)) pt';
1361 if afterins = [([1], Frm), ([1], Res),
1362 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1363 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1366 ([3, 1], Frm), ([3, 1], Res),
1367 ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
1368 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
1369 if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
1370 error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
1375 ========== inhibit exn AK110726 ==============================================*)