64 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
64 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
65 (get_ctxt pt p) |
65 (get_ctxt pt p) |
66 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj"; |
66 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj"; |
67 |
67 |
68 val pt = EmptyPtree; |
68 val pt = EmptyPtree; |
69 val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term, e_ctxt) pt; |
69 val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], e_spec, e_term, ContextC.empty) pt; |
70 val ctxt = get_obj g_ctxt pt []; |
70 val ctxt = get_obj g_ctxt pt []; |
71 if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed"; |
71 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed"; |
72 |
72 |
73 "-------------- check positions in miniscript --------------------"; |
73 "-------------- check positions in miniscript --------------------"; |
74 "-------------- check positions in miniscript --------------------"; |
74 "-------------- check positions in miniscript --------------------"; |
75 "-------------- check positions in miniscript --------------------"; |
75 "-------------- check positions in miniscript --------------------"; |
76 val fmz = ["equality (x+1=(2::real))", |
76 val fmz = ["equality (x+1=(2::real))", |
99 val cuts = get_allp [] ([], ([],Frm)) pt; |
99 val cuts = get_allp [] ([], ([],Frm)) pt; |
100 val cuts2 = get_allps [] [1] (children pt); |
100 val cuts2 = get_allps [] [1] (children pt); |
101 "ctree.sml-------------- cut_tree new (from ctree above)----------"; |
101 "ctree.sml-------------- cut_tree new (from ctree above)----------"; |
102 val (pt', cuts) = cut_tree pt ([1],Frm); |
102 val (pt', cuts) = cut_tree pt ([1],Frm); |
103 "ctree.sml-------------- cappend on complete ctree from above ----"; |
103 "ctree.sml-------------- cappend on complete ctree from above ----"; |
104 val (pt', cuts) = cappend_form pt [1] (e_istate, e_ctxt) (str2term "Inform[1]"); |
104 val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (str2term "Inform[1]"); |
105 "----------------------------------------------------------------/"; |
105 "----------------------------------------------------------------/"; |
106 |
106 |
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*); |
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*); |
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*); |
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*); |
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*); |
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*); |
428 if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso |
428 if term2str (get_obj g_form pt' [3,2,1]) = "newnew" andalso |
429 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso |
429 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso |
430 term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty" |
430 term2str (fst (get_obj g_result pt' [3,2,1])) = "??.empty" |
431 then () else error "ctree.sml: diff:behav. in cappend 1"; |
431 then () else error "ctree.sml: diff:behav. in cappend 1"; |
432 |
432 |
433 val (pt',cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "newform") |
433 val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (str2term "newform") |
434 (Tac "test") (str2term "newresult",[]) Complete; |
434 (Tac "test") (str2term "newresult",[]) Complete; |
435 if cuts = [([3, 2, 1], Res), (*?????????????*) |
435 if cuts = [([3, 2, 1], Res), (*?????????????*) |
436 ([3, 2, 2], Res), |
436 ([3, 2, 2], Res), |
437 ([3, 2], Res), |
437 ([3, 2], Res), |
438 ([3], Res), |
438 ([3], Res), |
467 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped |
467 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped |
468 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*) |
468 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*) |
469 |
469 |
470 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*); |
470 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*); |
471 val p = ([1], Frm); |
471 val p = ([1], Frm); |
472 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "x + 1 = 2"); |
472 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (str2term "x + 1 = 2"); |
473 val form = get_obj g_form pt (fst p); |
473 val form = get_obj g_form pt (fst p); |
474 val (res,_) = get_obj g_result pt (fst p); |
474 val (res,_) = get_obj g_result pt (fst p); |
475 if term2str form = "x + 1 = 2" andalso res = e_term then () else |
475 if term2str form = "x + 1 = 2" andalso res = e_term then () else |
476 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)"; |
476 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)"; |
477 if not (existpt ((lev_on o fst) p) pt) then () else |
477 if not (existpt ((lev_on o fst) p) pt) then () else |
478 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt"; |
478 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt"; |
479 |
479 |
480 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*); |
480 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*); |
481 val p = ([1], Res); |
481 val p = ([1], Res); |
482 val (pt,cuts) = |
482 val (pt,cuts) = |
483 cappend_atomic pt (fst p) e_istate (str2term "x + 1 = 2") |
483 cappend_atomic pt (fst p) Istate.empty (str2term "x + 1 = 2") |
484 Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete; |
484 Empty_Tac (str2term "x + 1 + -1 * 2 = 0",[]) Incomplete; |
485 val form = get_obj g_form pt (fst p); |
485 val form = get_obj g_form pt (fst p); |
486 val (res,_) = get_obj g_result pt (fst p); |
486 val (res,_) = get_obj g_result pt (fst p); |
487 if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0" |
487 if term2str form = "x + 1 = 2" andalso term2str res = "x + 1 + -1 * 2 = 0" |
488 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)"; |
488 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)"; |
490 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt"; |
490 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt"; |
491 |
491 |
492 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*); |
492 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*); |
493 val p = ([2], Res); |
493 val p = ([2], Res); |
494 val (pt,cuts) = |
494 val (pt,cuts) = |
495 cappend_atomic pt (fst p) e_istate (str2term "x + 1 + -1 * 2 = 0") |
495 cappend_atomic pt (fst p) Istate.empty (str2term "x + 1 + -1 * 2 = 0") |
496 Empty_Tac (str2term "-1 + x = 0",[]) Incomplete; |
496 Empty_Tac (str2term "-1 + x = 0",[]) Incomplete; |
497 val form = get_obj g_form pt (fst p); |
497 val form = get_obj g_form pt (fst p); |
498 val (res,_) = get_obj g_result pt (fst p); |
498 val (res,_) = get_obj g_result pt (fst p); |
499 if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0" |
499 if term2str form = "x + 1 + -1 * 2 = 0" andalso term2str res = "-1 + x = 0" |
500 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)"; |
500 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)"; |
502 error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt"; |
502 error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res) nxt"; |
503 |
503 |
504 |
504 |
505 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*) |
505 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*) |
506 val p = ([3], Pbl); |
506 val p = ([3], Pbl); |
507 val (pt,cuts) = cappend_problem pt (fst p) e_istate e_fmz ([],e_spec,e_term, e_ctxt); |
507 val (pt,cuts) = cappend_problem pt (fst p) Istate.empty e_fmz ([],e_spec,e_term, ContextC.empty); |
508 if is_pblobj (get_obj I pt (fst p)) then () else |
508 if is_pblobj (get_obj I pt (fst p)) then () else |
509 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)"; |
509 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)"; |
510 if not (existpt ((lev_on o fst) p) pt) then () else |
510 if not (existpt ((lev_on o fst) p) pt) then () else |
511 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt"; |
511 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl) nxt"; |
512 |
512 |
513 (* ...complete calchead skipped...*) |
513 (* ...complete calchead skipped...*) |
514 |
514 |
515 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*); |
515 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*); |
516 val p = ([3, 1], Frm); |
516 val p = ([3, 1], Frm); |
517 val (pt,cuts) = cappend_form pt (fst p) e_istate (str2term "-1 + x = 0"); |
517 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (str2term "-1 + x = 0"); |
518 val form = get_obj g_form pt (fst p); |
518 val form = get_obj g_form pt (fst p); |
519 val (res,_) = get_obj g_result pt (fst p); |
519 val (res,_) = get_obj g_result pt (fst p); |
520 if term2str form = "-1 + x = 0" andalso res = e_term then () else |
520 if term2str form = "-1 + x = 0" andalso res = e_term then () else |
521 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)"; |
521 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)"; |
522 if not (existpt ((lev_on o fst) p) pt) then () else |
522 if not (existpt ((lev_on o fst) p) pt) then () else |
523 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt"; |
523 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt"; |
524 |
524 |
525 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*) |
525 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*) |
526 val p = ([3, 1], Res); |
526 val p = ([3, 1], Res); |
527 val (pt,cuts) = |
527 val (pt,cuts) = |
528 cappend_atomic pt (fst p) e_istate (str2term "-1 + x = 0") |
528 cappend_atomic pt (fst p) Istate.empty (str2term "-1 + x = 0") |
529 Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete; |
529 Empty_Tac (str2term "x = 0 + -1 * -1",[]) Incomplete; |
530 val form = get_obj g_form pt (fst p); |
530 val form = get_obj g_form pt (fst p); |
531 val (res,_) = get_obj g_result pt (fst p); |
531 val (res,_) = get_obj g_result pt (fst p); |
532 if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then() |
532 if term2str form = "-1 + x = 0" andalso term2str res = "x = 0 + -1 * -1" then() |
533 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)"; |
533 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)"; |
1215 term2str (get_obj g_res pt' [2]); |
1215 term2str (get_obj g_res pt' [2]); |
1216 ostate2str (get_obj g_ostate pt' [2]); |
1216 ostate2str (get_obj g_ostate pt' [2]); |
1217 *) |
1217 *) |
1218 |
1218 |
1219 "---(4) on S(606)..S(608)--------"; |
1219 "---(4) on S(606)..S(608)--------"; |
1220 val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec) |
1220 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],e_spec) |
1221 ([],e_spec, str2term "Inhead[3]", e_ctxt); |
1221 ([],e_spec, str2term "Inhead[3]", ContextC.empty); |
1222 (*default_print_depth 99;*) |
1222 (*default_print_depth 99;*) |
1223 cuts; |
1223 cuts; |
1224 (*default_print_depth 3;*) |
1224 (*default_print_depth 3;*) |
1225 if cuts = [([3], Pbl), |
1225 if cuts = [([3], Pbl), |
1226 ([3, 1], Frm), ([3, 1], Res), |
1226 ([3, 1], Frm), ([3, 1], Res), |
1241 (* use"systest/ctree.sml"; |
1241 (* use"systest/ctree.sml"; |
1242 use"ctree.sml"; |
1242 use"ctree.sml"; |
1243 *) |
1243 *) |
1244 |
1244 |
1245 "---(6-1) on S(606)..S(608)--------"; |
1245 "---(6-1) on S(606)..S(608)--------"; |
1246 val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]") |
1246 val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (str2term "Inform[3,1]") |
1247 (Tac "test") (str2term "Inres[3,1]",[]) Complete; |
1247 (Tac "test") (str2term "Inres[3,1]",[]) Complete; |
1248 (*default_print_depth 99;*) |
1248 (*default_print_depth 99;*) |
1249 cuts; |
1249 cuts; |
1250 (*default_print_depth 3;*) |
1250 (*default_print_depth 3;*) |
1251 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), |
1251 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), |
1267 |
1267 |
1268 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else |
1268 if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else |
1269 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform"; |
1269 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform"; |
1270 |
1270 |
1271 "---(6) on S(606)..S(608)--------"; |
1271 "---(6) on S(606)..S(608)--------"; |
1272 val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]") |
1272 val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (str2term "Inform[3,2]") |
1273 (Tac "test") (str2term "Inres[3,2]",[]) Complete; |
1273 (Tac "test") (str2term "Inres[3,2]",[]) Complete; |
1274 (*default_print_depth 99;*) |
1274 (*default_print_depth 99;*) |
1275 cuts; |
1275 cuts; |
1276 (*default_print_depth 3;*) |
1276 (*default_print_depth 3;*) |
1277 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else |
1277 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else |
1292 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else |
1292 if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else |
1293 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform"; |
1293 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform"; |
1294 |
1294 |
1295 "---(6++) on S(606)..S(608)--------"; |
1295 "---(6++) on S(606)..S(608)--------"; |
1296 (**) |
1296 (**) |
1297 val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]") |
1297 val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (str2term "Inform[3,2,1]") |
1298 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete; |
1298 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete; |
1299 (*default_print_depth 99;*) |
1299 (*default_print_depth 99;*) |
1300 cuts; |
1300 cuts; |
1301 (*default_print_depth 1;*) |
1301 (*default_print_depth 1;*) |
1302 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] |
1302 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] |