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 "-------------- subst2subs subs2subst sube2subst subte2subst -----";
50 "-----------------------------------------------------------------";
51 "-----------------------------------------------------------------";
52 "-----------------------------------------------------------------";
55 "-------------- fun get_ctxt -------------------------------------";
56 "-------------- fun get_ctxt -------------------------------------";
57 "-------------- fun get_ctxt -------------------------------------";
58 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
60 ("Test", ["sqroot-test","univariate","equation","test"],
61 ["Test","squ-equ-test-subpbl1"]);
62 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
64 handle _ => error "--- fun get_ctxt not even some ctxt found in PblObj";
65 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
67 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
69 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
70 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
71 "-------------- fun update_ctxt, fun g_ctxt ----------------------";
73 val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
74 val ctxt = get_obj g_ctxt pt [];
75 if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
76 val pt = update_ctxt pt [] (Proof_Context.init_global @{theory "Isac"});
77 if (get_obj g_ctxt pt [] |> Proof_Context.theory_of |> Context.theory_name) = "Isac"
78 then () else error "--- fun update_ctxt, fun g_ctxt changed";
80 "-------------- check positions in miniscript --------------------";
81 "-------------- check positions in miniscript --------------------";
82 "-------------- check positions in miniscript --------------------";
83 val fmz = ["equality (x+1=(2::real))",
84 "solveFor x","solutions L"];
86 ("Test",["sqroot-test","univariate","equation","test"],
87 ["Test","squ-equ-test-subpbl1"]);
88 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 (* nxt = Add_Given "equality (x + 1 = 2)"
91 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
94 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
97 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
102 "ctree.sml-------------- get_allpos' new ------------------------\"";
103 val (PP, pp) = split_last [1];
104 val ((pt', cuts), clevup) = cut_bottom (PP, pp) (get_nd pt PP);
106 val cuts = get_allp [] ([], ([],Frm)) pt;
107 val cuts2 = get_allps [] [1] (children pt);
108 "ctree.sml-------------- cut_tree new (from ptree above)----------";
109 val (pt', cuts) = cut_tree pt ([1],Frm);
110 "ctree.sml-------------- cappend on complete ctree from above ----";
111 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]");
112 "----------------------------------------------------------------/";
114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*);
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*);
116 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*);
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_problem: pos =[3]*);
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 (*val nxt = ("Add_Given", Add_Given "equality (-1 + x = 0)").....*)
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
126 (*val nxt = ("Apply_Method", Apply_Method ["Test", "solve_linear"])*)
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
134 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
135 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
136 else error "new behaviour in test: miniscript with mini-subpbl";
140 "-------------- get_allpos' (from ptree above)--------------------";
141 "-------------- get_allpos' (from ptree above)--------------------";
142 "-------------- get_allpos' (from ptree above)--------------------";
143 if get_allpos' ([], 1) pt =
155 then () else error "ctree.sml: diff:behav. in get_allpos' 1";
157 if get_allpos's ([], 1) (children pt) =
167 then () else error "ctree.sml: diff:behav. in get_allpos' 2";
169 if get_allpos's ([], 2) (takerest (1, children pt)) =
177 then () else error "ctree.sml: diff:behav. in get_allpos' 3";
179 if get_allpos's ([], 3) (takerest (2, children pt)) =
186 then () else error "ctree.sml: diff:behav. in get_allpos' 4";
188 if get_allpos's ([3], 1) (children (nth 3 (children pt))) =
192 then () else error "ctree.sml: diff:behav. in get_allpos' 5";
194 if get_allpos' ([3], 1) (nth 3 (children pt)) =
200 then () else error "ctree.sml: diff:behav. in get_allpos' 6";
207 "-------------- cut_level (from ptree above)----------------------";
208 "-------------- cut_level (from ptree above)----------------------";
209 "-------------- cut_level (from ptree above)----------------------";
212 default_print_depth 99; cuts; default_print_depth 3;
214 (*if cuts = [([2], Res),
221 then () else error "ctree.sml: diff:behav. in cut_level 1a";
222 val (res,asm) = get_obj g_result pt' [2];
223 if res = e_term andalso asm = [] then () else
224 error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
225 if not (existpt [2] pt') then () else
226 error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
228 val (res,asm) = get_obj g_result pt' [];
230 (*============ inhibit exn AK110726 ==============================================
231 if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
232 error "ctree.sml: diff:behav. in cut_level 1ab";
233 ============ inhibit exn AK110726 ==============================================*)
234 (*============ inhibit exn AK110726 ==============================================
235 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
239 ([2], Res),(*, e_term in cut_tree!!!*)
240 ([], Res)] then () else
241 error "ctree.sml: diff:behav. in cut_level 1b";
242 ============ inhibit exn AK110726 ==============================================*)
244 val (pt',cuts) = cut_level [] [] pt ([2],Res);
245 if cuts = [([3], Frm),
251 then () else error "ctree.sml: diff:behav. in cut_level 2a";
253 if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
254 then () else error "ctree.sml: diff:behav. in cut_level 2b";
256 val (pt',cuts) = cut_level [] [3] pt ([3,1],Frm);
257 if cuts = [([3, 1], Res), ([3, 2], Res)]
258 then () else error "ctree.sml: diff:behav. in cut_level 3a";
259 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"
260 then () else error "ctree.sml: diff:behav. in cut_level 3b";
262 val (pt',cuts) = cut_level [] [3] pt ([3,1],Res);
263 if cuts = [([3, 2], Res)]
264 then () else error "ctree.sml: diff:behav. in cut_level 4a";
265 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"
266 then () else error "ctree.sml: diff:behav. in cut_level 4b";
269 "-------------- cut_tree (from ptree above)-----------------------";
270 "-------------- cut_tree (from ptree above)-----------------------";
271 "-------------- cut_tree (from ptree above)-----------------------";
272 val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
274 (*============ inhibit exn AK110726 ==============================================
275 if cuts = [([2], Res),
283 then () else error "ctree.sml: diff:behav. in cut_tree 1a";
285 val (res,asm) = get_obj g_result pt' [2];
286 ============ inhibit exn AK110726 ==============================================*)
288 if res = e_term (*WN050219 done by cut_level*) then () else
289 error "ctree.sml: diff:behav. in cut_tree 1aa";
291 (*============ inhibit exn AK110726 ==============================================
292 val form = get_obj g_form pt' [2];
293 if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
294 error "ctree.sml: diff:behav. in cut_tree 1ab";
295 ============ inhibit exn AK110726 ==============================================*)
297 (* get_obj g_form pt' [2];
298 (* ERROR: exception PTREE "get_obj: pos = [2] does not exist"
299 raised (line 908 /src/Tools/isac/Interpret/ctree.sml")*)*)
300 "~~~~~ fun get_obj, args:"; val (f, (Nd (b, bs)) ,(p::ps)) = (g_form, pt', [2]);*)
302 val (res,asm) = get_obj g_result pt' [];
303 if res = e_term (*WN050219 done by cut_tree*) then () else
304 error "ctree.sml: diff:behav. in cut_tree 1ac";
306 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
309 ([1], Res)] then () else
310 error "ctree.sml: diff:behav. in cut_tree 1ad";
312 val (pt', cuts) = cut_tree pt ([2],Res);
313 (*============ inhibit exn AK110726 ==============================================
314 if cuts = [([3], Frm),
321 then () else error "ctree.sml: diff:behav. in cut_tree 2";
322 ============ inhibit exn AK110726 ==============================================*)
324 val (pt', cuts) = cut_tree pt ([3,1],Frm);
325 (*============ inhibit exn AK110726 ==============================================
326 if cuts = [([3, 1], Res),
331 then () else error "ctree.sml: diff:behav. in cut_tree 3";
332 ============ inhibit exn AK110726 ==============================================*)
334 val (pt', cuts) = cut_tree pt ([3,1],Res);
335 if cuts = [([3, 2], Res),
339 then () else error "ctree.sml: diff:behav. in cut_tree 4";
341 "=====new ptree 1a miniscript with mini-subpbl ===================";
342 "=====new ptree 1a miniscript with mini-subpbl ===================";
343 "=====new ptree 1a miniscript with mini-subpbl ===================";
344 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
346 ("Test",["sqroot-test","univariate","equation","test"],
347 ["Test","squ-equ-test-subpbl1"]);
348 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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;
356 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
359 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
360 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
361 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
363 val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
364 if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
365 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
367 val (pt', cuts) = cut_tree pt ([1],Frm);
369 then () else error "ctree.sml: diff:behav. in cut_tree 4a";
372 val pos as ([p],_) = ([1],Frm);
373 val pt as Nd (b,_) = pt;
378 default_print_depth 99;cuts;default_print_depth 3;
379 default_print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');default_print_depth 3;
380 ####################################################################*)
384 "=====new ptree 2 miniscript with mini-subpbl ====================";
385 "=====new ptree 2 miniscript with mini-subpbl ====================";
386 "=====new ptree 2 miniscript with mini-subpbl ====================";
388 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
389 ("Test", ["sqroot-test","univariate","equation","test"],
390 ["Test","squ-equ-test-subpbl1"]))];
391 Iterator 1; moveActiveRoot 1;
392 autoCalculate' 1 CompleteCalc;
394 interSteps 1 ([3,2],Res);
396 val ((pt,_),_) = get_calc 1;
399 if (term2str o fst) (get_obj g_result pt [3,2,1]) = "x = 0 + 1" then ()
400 else error "mini-subpbl interSteps broken";
402 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
403 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
404 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
405 (*WN050225 intermed. outcommented
406 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
407 if cuts = [([3, 2, 1], Res),
412 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
414 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
415 if cuts = [([3, 2, 2], Res),
419 then () else error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
422 "-------------- cappend (from ptree above)------------------------";
423 "-------------- cappend (from ptree above)------------------------";
424 "-------------- cappend (from ptree above)------------------------";
425 val (pt',cuts) = cappend_form pt [3,2,1] e_istate (str2term "newnew");
426 if cuts = [([3, 2, 1], Res),
432 then () else error "ctree.sml: diff:behav. in cappend_form";
433 if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso
434 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso
435 term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty"
436 then () else error "ctree.sml: diff:behav. in cappend 1";
438 val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform")
439 (Tac "test") (str2term "newresult",[]) Complete;
440 if cuts = [([3, 2, 1], Res), (*?????????????*)
446 then () else error "ctree.sml: diff:behav. in cappend_atomic";
450 "-------------- cappend minisubpbl -------------------------------";
451 "-------------- cappend minisubpbl -------------------------------";
452 "-------------- cappend minisubpbl -------------------------------";
453 "=====new ptree 1 miniscript with mini-subpbl ====================";
454 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
456 ("Test",["sqroot-test","univariate","equation","test"],
457 ["Test","squ-equ-test-subpbl1"]);
458 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
459 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
460 (* nxt = Add_Given "equality (x + 1 = 2)"
461 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
463 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
464 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
466 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
467 (* (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));
469 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
471 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
472 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped
473 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*)
475 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*);
477 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2");
478 val form = get_obj g_form pt (fst p);
479 val (res,_) = get_obj g_result pt (fst p);
480 if term2str form = "x + 1 = 2" andalso res = e_term then () else
481 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)";
482 if not (existpt ((lev_on o fst) p) pt) then () else
483 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt";
485 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*);
488 cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2")
489 Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete;
490 val form = get_obj g_form pt (fst p);
491 val (res,_) = get_obj g_result pt (fst p);
492 if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0"
493 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)";
494 if not (existpt ((lev_on o fst) p) pt) then () else
495 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt";
497 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*);
500 cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0")
501 Empty_Tac (str2term "-1 + x = 0",[]) Incomplete;
502 val form = get_obj g_form pt (fst p);
503 val (res,_) = get_obj g_result pt (fst p);
504 if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0"
505 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)";
506 if not (existpt ((lev_on o fst) p) pt) then () else
507 error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt";
510 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
512 val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term);
513 if is_pblobj (get_obj I pt (fst p)) then () else
514 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
515 if not (existpt ((lev_on o fst) p) pt) then () else
516 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt";
518 (* ...complete calchead skipped...*)
520 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
521 val p = ([3, 1], Frm);
522 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0");
523 val form = get_obj g_form pt (fst p);
524 val (res,_) = get_obj g_result pt (fst p);
525 if term2str form = "-1 + x = 0" andalso res = e_term then () else
526 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)";
527 if not (existpt ((lev_on o fst) p) pt) then () else
528 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt";
530 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*)
531 val p = ([3, 1], Res);
533 cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0")
534 Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete;
535 val form = get_obj g_form pt (fst p);
536 val (res,_) = get_obj g_result pt (fst p);
537 if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then()
538 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)";
539 if not (existpt ((lev_on o fst) p) pt) then () else
540 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
542 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
543 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
544 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
545 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
546 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
547 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
549 WN050225 intermed. outcommented---*)
551 "=====new ptree 3 ================================================";
552 "=====new ptree 3 ================================================";
553 "=====new ptree 3 ================================================";
556 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
557 ("Test", ["sqroot-test","univariate","equation","test"],
558 ["Test","squ-equ-test-subpbl1"]))];
559 Iterator 1; moveActiveRoot 1;
560 autoCalculate' 1 CompleteCalc;
562 val ((pt,_),_) = get_calc 1;
565 "-------------- move_dn ------------------------------------------";
566 "-------------- move_dn ------------------------------------------";
567 "-------------- move_dn ------------------------------------------";
568 val p = move_dn [] pt ([],Pbl) (*-> ([1],Frm)*);
569 val p = move_dn [] pt p (*-> ([1],Res)*);
570 val p = move_dn [] pt p (*-> ([2],Res)*);
571 val p = move_dn [] pt p (*-> ([3],Pbl)*);
572 val p = move_dn [] pt p (*-> ([3,1],Frm)*);
573 val p = move_dn [] pt p (*-> ([3,1],Res)*);
574 val p = move_dn [] pt p (*-> ([3,2],Res)*);
575 val p = move_dn [] pt p (*-> ([3],Res)*);
576 (* term2str (get_obj g_res pt [3]);
577 term2str (get_obj g_form pt [4]);
579 val p = move_dn [] pt p (*-> ([4],Res)*);
580 val p = move_dn [] pt p (*-> ([],Res)*);
582 val p = (move_dn [] pt p) handle e => print_exn_G e;
583 Exception PTREE end of calculation*)
585 if p=([],Res) then () else error "ctree.sml: diff:behav. in move_dn";
587 "-------------- move_dn: Frm -> Res ------------------------------";
588 "-------------- move_dn: Frm -> Res ------------------------------";
589 "-------------- move_dn: Frm -> Res ------------------------------";
591 CalcTree (*start of calculation, return No.1*)
592 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
594 ["LINEAR","univariate","equation","test"],
595 ["Test","solve_linear"]))];
596 Iterator 1; moveActiveRoot 1;
597 autoCalculate' 1 CompleteCalcHead;
598 autoCalculate' 1 (Step 1);
599 refFormula 1 (get_pos 1 1);
603 if get_pos 1 1 = ([1], Frm) then ()
604 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
605 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
607 autoCalculate' 1 (Step 1);
608 refFormula 1 (get_pos 1 1);
610 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
611 if get_pos 1 1 = ([1], Res) then ()
612 else error "ctree.sml: diff.behav. in move_dn: Frm -> Res (1)";
613 moveActiveDown 1; (*<ERROR> pos does not exist </ERROR>*)
616 "-------------- move_up ------------------------------------------";
617 "-------------- move_up ------------------------------------------";
618 "-------------- move_up ------------------------------------------";
619 val p = move_up [] pt ([],Res); (*-> ([4],Res)*)
620 val p = move_up [] pt p; (*-> ([3],Res)*)
621 val p = move_up [] pt p; (*-> ([3,2],Res)*)
622 val p = move_up [] pt p; (*-> ([3,1],Res)*)
623 val p = move_up [] pt p; (*-> ([3,1],Frm)*)
624 val p = move_up [] pt p; (*-> ([3],Pbl)*)
625 val p = move_up [] pt p; (*-> ([2],Res)*)
626 val p = move_up [] pt p; (*-> ([1],Res)*)
627 val p = move_up [] pt p; (*-> ([1],Frm)*)
628 val p = move_up [] pt p; (*-> ([],Pbl)*)
629 (*val p = (move_up [] pt p) handle e => print_exn_G e;
630 Exception PTREE begin of calculation*)
632 if p=([],Pbl) then () else error "ctree.sml: diff.behav. in move_up";
634 "------ move into detail -----------------------------------------";
635 "------ move into detail -----------------------------------------";
636 "------ move into detail -----------------------------------------";
638 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
639 ("Test", ["sqroot-test","univariate","equation","test"],
640 ["Test","squ-equ-test-subpbl1"]))];
641 Iterator 1; moveActiveRoot 1;
642 autoCalculate' 1 CompleteCalc;
647 refFormula 1 (get_pos 1 1) (* 2 Res, <ISA> -1 + x = 0 </ISA> *);
649 interSteps 1 ([2],Res);
651 val ((pt,_),_) = get_calc 1; show_pt pt;
654 val p = move_up [] pt p; (*([2, 6], Res)*);
655 val p = movelevel_up [] pt p;(*([2], Frm)*);
656 val p = move_dn [] pt p; (*([2, 1], Frm)*);
657 val p = move_dn [] pt p; (*([2, 1], Res)*);
658 val p = move_dn [] pt p; (*([2, 2], Res)*);
659 val p = move_dn [] pt p; (*([2, 3], Res)*);
660 val p = move_dn [] pt p; (*([2, 4], Res)*);
661 val p = move_dn [] pt p; (*([2, 5], Res)*);
662 val p = move_dn [] pt p; (*([2, 6], Res)*);
663 if p = ([2, 6], Res) then()
664 else error "ctree.sml: diff.behav. in move into detail";
666 "=====new ptree 3a ===============================================";
667 "=====new ptree 3a ===============================================";
668 "=====new ptree 3a ===============================================";
670 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
671 ("Test", ["sqroot-test","univariate","equation","test"],
672 ["Test","squ-equ-test-subpbl1"]))];
673 Iterator 1; moveActiveRoot 1;
674 autoCalculate' 1 CompleteCalcHead;
675 autoCalculate' 1 (Step 1);
676 autoCalculate' 1 (Step 1);
677 autoCalculate' 1 (Step 1);
678 val ((pt,_),_) = get_calc 1;
679 val p = move_dn [] pt ([],Pbl) (*-> ([1], Frm)*);
680 val p = move_dn [] pt ([1], Frm) (*-> ([1], Res)*);
681 val p = move_dn [] pt ([1], Res) (*-> ([2], Res)*);
682 (*val p = move_dn [] pt ([2], Res) ->Exception- PTREE "[] not complete"*);
684 moveDown 1 ([],Pbl) (*-> ([1], Frm)*);
685 moveDown 1 ([1],Frm) (*-> ([1],Res)*);
686 moveDown 1 ([1],Res) (*-> ([2],Res)*);
687 moveDown 1 ([2],Res) (*-> pos does not exist*);
689 get_obj g_ostate pt [1];
693 "-------------- move_dn in Incomplete ctree ----------------------";
694 "-------------- move_dn in Incomplete ctree ----------------------";
695 "-------------- move_dn in Incomplete ctree ----------------------";
699 "=====new ptree 4: crooked by cut_level_'_ =======================";
700 "=====new ptree 4: crooked by cut_level_'_ =======================";
701 "=====new ptree 4: crooked by cut_level_'_ =======================";
704 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
705 "solveFor x","solutions L"],
706 ("RatEq",["univariate","equation"],["no_met"]))];
707 Iterator 1; moveActiveRoot 1;
708 autoCalculate' 1 CompleteCalc;
710 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*)
711 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*)
712 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*)
713 getTactic 1 ([4,1],Res);(*Rewrite all_left*)
714 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*)
715 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*)
717 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
718 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*);
719 moveActiveFormula 1 ([3],Res)(*3.1.*);
720 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
721 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*);
723 moveActiveFormula 1 ([1],Res)(*1.1...1.4*);
724 interSteps 1 ([1],Res)(*..is activeFormula !?!*);
726 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*)
727 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*)
728 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*)
729 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*)
731 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*);
732 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*);
733 val ((pt,_),_) = get_calc 1;
734 writeln(pr_ptree pr_short pt);
735 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
736 ###########################################################################*)
737 val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
738 writeln(pr_ptree pr_short pt);
744 "-------------- get_interval from ctree: incremental development--";
745 "-------------- get_interval from ctree: incremental development--";
746 "-------------- get_interval from ctree: incremental development--";
747 "--- level 1: get pos from start b to end p ----------------------";
748 "--- level 1: get pos from start b to end p ----------------------";
749 "--- level 1: get pos from start b to end p ----------------------";
750 (******************************************************************)
751 (**) val SAVE_get_trace = get_trace; (**)
752 (******************************************************************)
753 (*'getnds' below is structured as such:*)
754 fun www _ [x] = "l+r-margin"
755 | www true [x1,x2] = "l-margin, r-margin"
756 | www _ [x1,x2] = "intern, r-margin"
757 | www true (x::(xs as _::_)) = "l-margin " ^ www false xs
758 | www _ (x::(xs as _::_)) = "intern " ^ www false xs;
759 www true [1,2,3,4,5];
760 (*val it = "from intern intern intern to" : string*)
762 (*val it = "from to" : string*)
764 (*val it = "from+to" : string*)
767 (*specific values of hd of pos p,q for simple handling take_fromto,
768 from-pos p, to-pos q: take_fromto (hdp p) (hdq q) (children pt) ...
769 ... can be used even for positions _below_ p or q*)
770 fun hdp [] = 1 | hdp [0] = 1 | hdp x = hd x;(*start with first*)
771 fun hdq [] = 99999 | hdq [0] = 99999 | hdq x = hd x;(*take until last*)
772 (*analoguous for tl*)
773 fun tlp [] = [0] | tlp [_] = [0] | tlp x = tl x;
774 fun tlq [] = [99999] | tlq [_] = [99999] | tlq x = tl x;
776 (*see modspec.sml#pt_form
777 fun pt_form (PrfObj {form,...}) = term2str form
778 | pt_form (PblObj {probl,spec,origin=(_,spec',_),...}) =
779 let val (dI, pI, _) = get_somespec' spec spec'
780 val {cas,...} = get_pbt pI
782 NONE => term2str (pblterm dI pI)
783 | SOME t => term2str (subst_atomic (mk_env probl) t)
786 (*.get an 'interval' from ptree down to a certain level
787 by 'take_fromto children' of the nodes with specific 'from' and 'to';
788 'i > 0' suppresses output during recursive descent towards 'from'
789 b: the 'from' incremented to the actual pos
790 p,q: specific 'from','to' for simple use of 'take_fromto'*)
791 fun getnd i (b,p) q (Nd (po, nds)) =
792 (if i <= 0 then [(*[(b, pt_form po)]*) (**)[b](**)] else [])
794 @ (writeln("getnd : b="^(ints2str' b)^", p="^
795 (ints2str' p)^", q="^(ints2str' q));
797 getnds (i-1) true (b@[hdp p], tlp p) (tlq q)
798 (take_fromto (hdp p) (hdq q) nds))
800 and getnds _ _ _ _ [] = [] (*no children*)
801 | getnds i _ (b,p) q [nd] = (getnd i (b,p) q nd) (*l+r-margin*)
802 | getnds i true (b,p) q [n1, n2] = (*l-margin, r-margin*)
803 (writeln("getnds3: b="^ ints2str' b ^", p="^ ints2str' p ^
804 ", q="^ ints2str' q);
805 (getnd i ( b, p ) [99999] n1) @
806 (getnd ~99999 (lev_on b,[0]) q n2))
807 | getnds i _ (b,p) q [n1, n2] = (*intern, r-margin*)
808 (writeln("getnds4: b="^ ints2str' b ^", p="^ ints2str' p ^
809 ", q="^ ints2str' q);
810 (getnd i ( b,[0]) [99999] n1) @
811 (getnd ~99999 (lev_on b,[0]) q n2))
812 | getnds i true (b,p) q (nd::(nds as _::_)) = (*l-margin, intern*)
813 (writeln("getnds5: b="^ ints2str' b ^", p="^ ints2str' p ^
814 ", q="^ ints2str' q);
815 (getnd i ( b, p ) [99999] nd) @
816 (getnds ~99999 false (lev_on b,[0]) q nds))
817 | getnds i _ (b,p) q (nd::(nds as _::_)) = (*intern, ...*)
818 (getnd i ( b,[0]) [99999] nd) @
819 (getnds ~99999 false (lev_on b,[0]) q nds);
821 (*get an 'interval from to' from a ptree as 'intervals f t' of respective nodes
822 where 'from' are pos, i.e. a key as int list, 'f' an int (to,t analoguous)
823 (1) the 'f' are given
824 (1a) by 'from' if 'f' = the respective element of 'from' (left margin)
825 (1b) -inifinity, if 'f' > the respective element of 'from' (internal node)
827 (2a) by 'to' if 't' = the respective element of 'to' (right margin)
828 (2b) inifinity, if 't' < the respective element of 'to (internal node)'
829 the 'f' and 't' are set by hdp,... *)
830 fun get_trace pt p q =
831 (flat o (getnds ((length p) -1) true ([hdp p], tlp p) (tlq q)))
832 (take_fromto (hdp p) (hdq q) (children pt));
835 writeln(pr_ptree pr_short pt);
837 case get_trace pt [1,3] [4,1,1] of
838 [[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1]] => ()
839 | _ => error "diff.behav.in ctree.sml: get_interval lev 1a";
840 case get_trace pt [2] [4,3,2] of
841 [[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1],[4,3,2]] => ()
842 | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
843 case get_trace pt [1,4] [4,3,1] of
844 [[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],[4,3],[4,3,1]] => ()
845 | _ => error "diff.behav.in ctree.sml: get_interval lev 1c";
848 (*========== inhibit exn AK110719 ==============================================
849 case get_trace pt [4,2] [5] of
850 (*[([4,2],_),([4,3],_),([4,4],_),([4,4,1],_),([4,4,2],_),([4,4,3],_),
851 ([4,4,4],_),([4,4,5],_),([5],_)] => () ..with pt_form*)
852 [[4,2],[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]]=>()
853 | _ => error "diff.behav.in ctree.sml: get_interval lev 1d";
854 ========== inhibit exn AK110719 ==============================================*)
856 case get_trace pt [] [4,4,2] of
857 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
858 [4,3],[4,3,1],[4,3,2]] => ()
859 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
861 (*========== inhibit exn AK110719 ==============================================
862 case get_trace pt [] [] of
863 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,1,1],[4,2],
864 [4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5],[5]] => ()
865 | _ => error "diff.behav.in ctree.sml: get_interval lev 1f";
866 case get_trace pt [4,3] [4,3] of
867 [[4,3],[4,3,1],[4,3,2],[4,3,3],[4,3,4],[4,3,5]] => ()
868 | _ => error "diff.behav.in ctree.sml: get_interval lev 1g";
869 ========== inhibit exn AK110719 ==============================================*)
871 "--- level 2: get pos' from start b to end p ---------------------";
872 "--- level 2: get pos' from start b to end p ---------------------";
873 "--- level 2: get pos' from start b to end p ---------------------";
874 (*idea: pos_ is _ONLY_ relevant exactly at (endpoint of) from, to
875 development stopped in favour of move_dn, see get_interval
876 actually used (inefficient) version with move_dn: see modspec.sml
879 case get_trace pt ([1,4],Res) ([4,4,1],Frm) of
880 [[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],[4,4],[4,4,1]] => ()
881 | _ => error "diff.behav.in ctree.sml: get_interval lev 1b";
882 case get_trace pt ([],Pbl) ([],Res) of
883 [[1],[1,1],[1,2],[1,3],[1,4],[2],[3],[4],[4,1],[4,2],[4,2,1],[4,3],
884 [4,4],[4,4,1],[4,4,2],[4,4,3],[4,4,4],[4,4,5],[5]] => ()
885 | _ => error "diff.behav.in ctree.sml: get_interval lev 1e";
888 (******************************************************************)
889 (**) val get_trace = SAVE_get_trace; (**)
890 (******************************************************************)
893 "=====new ptree 4 ratequation ====================================";
894 "=====new ptree 4 ratequation ====================================";
895 "=====new ptree 4 ratequation ====================================";
898 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)",
899 "solveFor x","solutions L"],
900 ("RatEq",["univariate","equation"],["no_met"]))];
901 Iterator 1; moveActiveRoot 1;
902 autoCalculate' 1 CompleteCalc;
903 val ((pt,_),_) = get_calc 1;
905 val (Form f, tac, asms) = pt_extract (pt, p);
906 (*============ inhibit exn WN120316 ==============================================
907 if term2str f = "[x = 6 / 5]" andalso p = ([], Res) then ()
908 else error "after ===new ptree 4 ratequation ===";
909 (*WN120317.TODO dropped rateq*)
910 ============ inhibit exn WN120316 ==============================================*)
911 if p = ([], Res) andalso term2str f = "[]" (*see WN120317.TODO dropped rateq*)
912 andalso asms = [] (*STRANGE!, compare test --- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 ...*)
913 then () else error "after ===new ptree 4 ratequation ===";
916 "-------------- pt_extract form, tac, asm<>[] --------------------";
917 "-------------- pt_extract form, tac, asm<>[] --------------------";
918 "-------------- pt_extract form, tac, asm<>[] --------------------";
919 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
920 case (term2str form, tac, terms2strs asm) of
921 ("(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)",
924 ["normalize", "polynomial", "univariate", "equation"]),
925 ["9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0"]) => ()
926 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
927 (*WN060717 unintentionally changed some rls/ord while
928 completing knowl. for thes2file...
930 case (term2str form, tac, terms2strs asm) of
931 ((*"(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))",
934 ["normalize", "polynomial", "univariate", "equation"]),
935 ["9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0"]) => ()
936 | _ => error "diff.behav.in ctree.sml: pt_extract asm<>[]";
938 .... but it became even better*)
942 "=====new ptree 5 minisubpbl =====================================";
943 "=====new ptree 5 minisubpbl =====================================";
944 "=====new ptree 5 minisubpbl =====================================";
946 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
947 ("Test", ["sqroot-test","univariate","equation","test"],
948 ["Test","squ-equ-test-subpbl1"]))];
949 Iterator 1; moveActiveRoot 1;
950 autoCalculate' 1 CompleteCalc;
951 val ((pt,_),_) = get_calc 1;
954 "-------------- pt_extract form, tac, asm ------------------------";
955 "-------------- pt_extract form, tac, asm ------------------------";
956 "-------------- pt_extract form, tac, asm ------------------------";
957 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([], Frm));
958 case (term2str form, tac, terms2strs asm) of
959 ("solve (x + 1 = 2, x)",
960 Apply_Method ["Test", "squ-equ-test-subpbl1"],
962 | _ => error "diff.behav.in ctree.sml: pt_extract ([], Pbl)";
964 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Frm));
965 case (term2str form, tac, terms2strs asm) of
966 ("x + 1 = 2", Rewrite_Set "norm_equation", []) => ()
967 | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Frm)";
969 val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));
970 case (term2str form, tac, terms2strs asm) of
971 ("x + 1 + -1 * 2 = 0", Rewrite_Set "Test_simplify", []) => ()
972 | _ => error "diff.behav.in ctree.sml: pt_extract ([1], Res)";
974 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
975 case (term2str form, tac, terms2strs asm) of
977 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
979 | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
981 val (ModSpec (_,_,form,_,_,_), SOME tac, asm) = pt_extract (pt, ([3], Pbl));
982 case (term2str form, tac, terms2strs asm) of
983 ("solve (-1 + x = 0, x)", Apply_Method ["Test", "solve_linear"], []) => ()
984 | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Pbl)";
986 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Frm));
987 case (term2str form, tac, terms2strs asm) of
988 ("-1 + x = 0", Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), []) => ()
989 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Frm)";
991 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,1], Res));
992 case (term2str form, tac, terms2strs asm) of
993 ("x = 0 + -1 * -1", Rewrite_Set "Test_simplify", []) => ()
994 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,1], Res)";
996 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
997 case (term2str form, tac, terms2strs asm) of
998 ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],
1000 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
1002 (*========== inhibit exn AK110719 ==============================================
1003 val (Form form, SOME tac, asm) = pt_extract (pt, ([3], Res));
1004 case (term2str form, tac, terms2strs asm) of
1005 ("[x = 1]", Check_elementwise "Assumptions", []) => ()
1006 | _ => error "diff.behav.in ctree.sml: pt_extract ([3], Res)";
1008 val (Form form, SOME tac, asm) = pt_extract (pt, ([4], Res));
1009 case (term2str form, tac, terms2strs asm) of
1011 Check_Postcond ["sqroot-test", "univariate", "equation", "test"],
1013 | _ => error "diff.behav.in ctree.sml: pt_extract ([4], Res)";
1015 val (Form form, tac, asm) = pt_extract (pt, ([], Res));
1016 case (term2str form, tac, terms2strs asm) of
1017 ("[x = 1]", NONE, []) => ()
1018 | _ => error "diff.behav.in ctree.sml: pt_extract ([], Res)";
1019 ========== inhibit exn AK110719 ==============================================*)
1021 "=====new ptree 6 minisubpbl intersteps ==========================";
1022 "=====new ptree 6 minisubpbl intersteps ==========================";
1023 "=====new ptree 6 minisubpbl intersteps ==========================";
1025 CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1026 ("Test", ["sqroot-test","univariate","equation","test"],
1027 ["Test","squ-equ-test-subpbl1"]))];
1028 Iterator 1; moveActiveRoot 1;
1029 autoCalculate' 1 CompleteCalc;
1030 interSteps 1 ([2],Res);
1031 interSteps 1 ([3,2],Res);
1032 val ((pt,_),_) = get_calc 1;
1035 (**##############################################################**)
1036 "-------------- get_allpos' new ----------------------------------";
1037 "-------------- get_allpos' new ----------------------------------";
1038 "-------------- get_allpos' new ----------------------------------";
1040 default_print_depth 99;
1041 val cuts = get_allp [] ([], ([],Frm)) pt;
1042 default_print_depth 3;
1044 [(*never returns the first pos'*)
1047 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1048 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1051 ([3, 1], Frm), ([3, 1], Res),
1052 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1056 ([], Res)] then () else
1057 error "ctree.sml diff.behav. get_allp new []";
1059 default_print_depth 99;
1060 val cuts2 = get_allps [] [1] (children pt);
1061 default_print_depth 3;
1062 if cuts = cuts2 @ [([], Res)] then () else
1063 error "ctree.sml diff.behav. get_allps new []";
1065 "---(3) on S(606)..S(608)--------";
1066 "--- nd [2] with 6 children---------------------------------";
1067 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
1069 [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1070 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1071 ([2], Res)] then () else
1072 error "ctree.sml diff.behav. get_allp new [2]";
1074 val cuts2 = get_allps [] [2,1] (children (get_nd pt [2]));
1075 if cuts = cuts2 @ [([2], Res)] then () else
1076 error "ctree.sml diff.behav. get_allps new [2]";
1079 "---(4) on S(606)..S(608)--------";
1080 "--- nd [3] subproblem--------------------------------------";
1081 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
1085 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1087 ([3], Res)] then () else
1088 error "ctree.sml diff.behav. get_allp new [3]";
1090 val cuts2 = get_allps [] [3,1] (children (get_nd pt [3]));
1091 if cuts = cuts2 @ [([3], Res)] then () else
1092 error "ctree.sml diff.behav. get_allps new [3]";
1094 "--- nd [3,2] with 2 children--------------------------------";
1095 val cuts = get_allp [] ([3,2], ([],Frm)) (get_nd pt [3,2]);
1097 [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1098 ([3, 2], Res)] then () else
1099 error "ctree.sml diff.behav. get_allp new [3,2]";
1101 val cuts2 = get_allps [] [3,2,1] (children (get_nd pt [3,2]));
1102 if cuts = cuts2 @ [([3, 2], Res)] then () else
1103 error "ctree.sml diff.behav. get_allps new [3,2]";
1105 "---(5a) on S(606)..S(608)--------";
1106 "--- nd [3,2,1] with 0 children------------------------------";
1107 val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
1110 error "ctree.sml diff.behav. get_allp new [3,2,1]";
1112 val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
1113 if cuts = cuts2 @ [] then () else
1114 error "ctree.sml diff.behav. get_allps new [3,2,1]";
1117 (**#################################################################**)
1118 "-------------- cut_tree new (from ptree above)-------------------";
1119 "-------------- cut_tree new (from ptree above)-------------------";
1120 "-------------- cut_tree new (from ptree above)-------------------";
1122 val b = get_obj g_branch pt [];
1123 if b = TransitiveB then () else
1124 error ("ctree.sml diff.behav. in [] branch="^branch2str b);
1125 val b = get_obj g_branch pt [3];
1126 if b = TransitiveB then () else
1127 error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
1129 "---(2) on S(606)..S(608)--------";
1130 val (pt', cuts) = cut_tree pt ([1],Res);
1131 default_print_depth 99;
1133 default_print_depth 3;
1134 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1135 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1136 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1137 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1138 (*WN060727 after replacing cutlevup by test_trans:*)([], Res)] then () else
1139 error "ctree.sml: diff.behav. cut_tree ([1],Res)";
1142 "---(3) on S(606)..S(608)--------";
1143 val (pt', cuts) = cut_tree pt ([2],Res);
1144 default_print_depth 99;
1146 default_print_depth 3;
1147 if cuts = [(*preceding step on WS was ([1]),Res*)
1148 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1149 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1154 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1158 (*WN060727 added after replacing cutlevup by test_trans:*)([],Res)] then ()
1159 else error "ctree.sml: diff.behav. cut_tree ([2],Res)";
1161 "---(4) on S(606)..S(608)--------";
1162 val (pt', cuts) = cut_tree pt ([3],Pbl);
1163 default_print_depth 99;
1165 default_print_depth 3;
1166 if cuts = [([3], Pbl),
1167 ([3, 1], Frm), ([3, 1], Res),
1168 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1172 (*WN060727 added after replacing cutlevup by test_trans:*)([], Res)]
1173 then () else error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
1175 "---(5a) on S(606)..S(608) cut_tree --------";
1176 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
1177 default_print_depth 99;
1179 default_print_depth 1;
1180 if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1181 (*WN060727 added after replacing cutlevup by test_trans:*)
1182 ([3], Res), ([4], Res),([],Res)] then ()
1183 else error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
1187 "-------------- cappend on complete ctree from above -------------";
1188 "-------------- cappend on complete ctree from above -------------";
1189 "-------------- cappend on complete ctree from above -------------";
1192 "---(2) on S(606)..S(608)--------";
1193 (*========== inhibit exn AK110726 ==============================================
1194 (* ERROR: Can't unify istate to istate * Proof.context *)
1195 val (pt', cuts) = cappend_atomic pt [1] e_istate (str2term "Inform[1]")
1196 (Tac "test") (str2term "Inres[1]",[]) Complete;
1198 default_print_depth 99;
1200 default_print_depth 3;
1201 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1202 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1203 ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1204 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1205 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1206 else error "ctree.sml: diff:behav. in complete pt:append_atomic[1] cuts";
1208 val afterins = get_allp [] ([], ([],Frm)) pt';
1209 default_print_depth 99;
1211 default_print_depth 3;
1212 if afterins = [([1], Frm), ([1], Res)
1213 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)] then()
1214 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins";
1216 "---(3) on S(606)..S(608)--------";
1218 val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
1219 (Tac "test") (str2term "Inres[2]",[]) Complete;
1220 default_print_depth 99;
1222 default_print_depth 3;
1224 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
1225 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
1226 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
1227 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res),
1228 (*WN060727 added after replacing cutlevup by test_trans:*) ([], Res)] then ()
1229 else error "ctree.sml: diff:behav.in complete pt: append_atomic[2] cuts";
1232 val afterins = get_allp [] ([], ([],Frm)) pt';
1233 default_print_depth 99;
1235 default_print_depth 3;
1237 if afterins = [([1], Frm), ([1], Res), ([2], Frm), ([2], Res)
1238 (*, WN060727 removed after replacing cutlevup by test_trans:([], Res)*)]
1240 error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
1245 val p = move_dn [] pt' ([],Pbl) (*-> ([1],Frm)*);
1246 val p = move_dn [] pt' p (*-> ([1],Res)*);
1247 val p = move_dn [] pt' p (*-> ([2],Frm)*);
1248 val p = move_dn [] pt' p (*-> ([2],Res)*);
1250 term2str (get_obj g_form pt' [2]);
1251 term2str (get_obj g_res pt' [2]);
1252 ostate2str (get_obj g_ostate pt' [2]);
1255 "---(4) on S(606)..S(608)--------";
1256 val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
1257 ([],e_spec, str2term "Inhead[3]");
1258 default_print_depth 99;
1260 default_print_depth 3;
1261 if cuts = [([3], Pbl),
1262 ([3, 1], Frm), ([3, 1], Res),
1263 ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1265 ([3], Res), ([4], Res),
1266 (*WN060727 added after replacing cutlevup by test_trans*)([], Res)] then ()else
1267 error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
1268 val afterins = get_allp [] ([], ([],Frm)) pt';
1269 default_print_depth 99;
1271 default_print_depth 3;
1273 [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1274 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
1275 ([3], Pbl)] then () else
1276 error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
1277 (* use"systest/ctree.sml";
1281 "---(6-1) on S(606)..S(608)--------";
1282 val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
1283 (Tac "test") (str2term "Inres[3,1]",[]) Complete;
1284 default_print_depth 99;
1286 default_print_depth 3;
1287 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
1289 (*WN060727 added*)([3], Res), ([4], Res), ([], Res)] then () else
1290 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
1292 val afterins = get_allp [] ([], ([],Frm)) pt';
1293 default_print_depth 99;
1295 default_print_depth 3;
1296 (*WN060727 replaced after overwriting cutlevup by test_trans
1297 if afterins = [([1], Frm), ([1], Res),
1298 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1299 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1302 ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
1303 ([3], Res)(*cutlevup=false*),
1305 ([], Res)(*cutlevup=false*)] then () else
1306 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1308 if afterins = [([1], Frm), ([1], Res),
1309 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1310 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1313 ([3, 1], Frm), ([3, 1], Res)] then () else
1314 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
1316 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
1317 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
1319 "---(6) on S(606)..S(608)--------";
1320 val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
1321 (Tac "test") (str2term "Inres[3,2]",[]) Complete;
1322 default_print_depth 99;
1324 default_print_depth 3;
1325 if cuts = [(*just after is: cutlevup=false in [3]*)
1326 (*WN060727 after test_trans instead cutlevup added:*)
1327 ([3], Res), ([4], Res), ([], Res)] then () else
1328 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
1329 val afterins = get_allp [] ([], ([],Frm)) pt';
1330 default_print_depth 99;
1332 default_print_depth 3;
1333 (*WN060727 replaced after overwriting cutlevup by test_trans
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 ([4], Res), ([], Res)] then () else
1342 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1344 if afterins = [([1], Frm), ([1], Res),
1345 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1346 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1349 ([3, 1], Frm), ([3, 1], Res), ([3, 2], Frm), ([3, 2], Res)]
1351 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
1353 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
1354 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
1356 "---(6++) on S(606)..S(608)--------";
1358 val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
1359 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
1360 default_print_depth 99;
1362 default_print_depth 1;
1363 if cuts = [([3, 2, 2], Res), ([3, 2], Res),
1364 (*WN060727 {cutlevup->test_trans} added:*)([3], Res), ([4], Res), ([], Res)]
1366 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
1367 val afterins = get_allp [] ([], ([],Frm)) pt';
1368 default_print_depth 99;
1370 default_print_depth 3;
1371 if afterins = [([1], Frm), ([1], Res),
1372 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
1373 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
1376 ([3, 1], Frm), ([3, 1], Res),
1377 ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
1378 error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
1379 if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
1380 error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
1385 ========== inhibit exn AK110726 ==============================================*)
1387 "-------------- subst2subs subs2subst sube2subst subte2subst -----";
1388 "-------------- subst2subs subs2subst sube2subst subte2subst -----";
1389 "-------------- subst2subs subs2subst sube2subst subte2subst -----";
1390 val subst = [(str2term "bdv", str2term "x"), (str2term "err", str2term "0")];
1392 if ["bdv = x", "err = 0"] = subte2sube [str2term "bdv = x", str2term "err = 0"] then ()
1393 else error "subte2sube broken";
1395 subst2subs : (term * term) list -> string list;
1396 if subst2subs subst = ["(bdv, x)", "(err, 0)"] then ()
1397 else error "subst2subs broken";
1399 subst2subs' : (term * term) list -> (string * string) list;
1400 if subst2subs' subst = [("bdv", "x"), ("err", "0")] then ()
1401 else error "subst2subs' broken";
1403 subs2subst : theory -> string list -> (term * term) list;
1404 val [(i1, v1), (i2, v2)] = subs2subst thy ["(bdv, x)", "(err, 0)"];
1405 if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
1406 term2str i2 = "err" andalso term2str v2 = "0" then ()
1407 else error "subs2subst broken";
1409 sube2subst : theory -> string list -> (term * term) list;
1410 val [(i1, v1), (i2, v2)] = sube2subst thy ["bdv = x", "err = 0"];
1411 if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
1412 term2str i2 = "err" andalso term2str v2 = "0" then ()
1413 else error "sube2subst broken";
1415 sube2subte : string list -> term list;
1416 val [eq1, eq2] = sube2subte ["bdv = x", "err = 0"];
1417 if term2str eq1 = "bdv = x" andalso term2str eq2 = "err = 0" then ()
1418 else error "sube2subte broken";
1420 val [(i1, v1), (i2, v2)] = subte2subst [str2term "bdv = x", str2term "err = 0"];
1421 if term2str i1 = "bdv" andalso term2str v1 = "x" andalso
1422 term2str i2 = "err" andalso term2str v2 = "0" then ()
1423 else error "subte2subst broken";