101 val cuts = get_allp [] ([], ([],Frm)) pt; |
101 val cuts = get_allp [] ([], ([],Frm)) pt; |
102 val cuts2 = get_allps [] [1] (children pt); |
102 val cuts2 = get_allps [] [1] (children pt); |
103 "ctree.sml-------------- cut_tree new (from ctree above)----------"; |
103 "ctree.sml-------------- cut_tree new (from ctree above)----------"; |
104 val (pt', cuts) = cut_tree pt ([1],Frm); |
104 val (pt', cuts) = cut_tree pt ([1],Frm); |
105 "ctree.sml-------------- cappend on complete ctree from above ----"; |
105 "ctree.sml-------------- cappend on complete ctree from above ----"; |
106 val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (TermC.str2term "Inform[1]"); |
106 val (pt', cuts) = cappend_form pt [1] (Istate.empty, ContextC.empty) (TermC.parse_test @{context} "Inform[1]"); |
107 "----------------------------------------------------------------/"; |
107 "----------------------------------------------------------------/"; |
108 |
108 |
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*); |
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[1]*); |
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*); |
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[1]*); |
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*); |
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[2]*); |
430 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "newnew" andalso |
430 if UnparseC.term (get_obj g_form pt' [3,2,1]) = "newnew" andalso |
431 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso |
431 get_obj g_tac pt' [3,2,1] = Empty_Tac andalso |
432 UnparseC.term (fst (get_obj g_result pt' [3,2,1])) = "??.empty" |
432 UnparseC.term (fst (get_obj g_result pt' [3,2,1])) = "??.empty" |
433 then () else error "ctree.sml: diff:behav. in cappend 1"; |
433 then () else error "ctree.sml: diff:behav. in cappend 1"; |
434 |
434 |
435 val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.str2term "newform") |
435 val (pt',cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.parse_test @{context} "newform") |
436 (Tac "test") (TermC.str2term "newresult",[]) Complete; |
436 (Tac "test") (TermC.parse_test @{context} "newresult",[]) Complete; |
437 if cuts = [([3, 2, 1], Res), (*?????????????*) |
437 if cuts = [([3, 2, 1], Res), (*?????????????*) |
438 ([3, 2, 2], Res), |
438 ([3, 2, 2], Res), |
439 ([3, 2], Res), |
439 ([3, 2], Res), |
440 ([3], Res), |
440 ([3], Res), |
441 ([4], Res), |
441 ([4], Res), |
469 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped |
469 (*###cappend_form: pos =[1] ... while calculating nxt, which pt is dropped |
470 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*) |
470 val nxt = ("Apply_Method", Apply_Method ["Test", "squ-equ-test-subpbl1"])*) |
471 |
471 |
472 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*); |
472 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[1]*); |
473 val p = ([1], Frm); |
473 val p = ([1], Frm); |
474 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.str2term "x + 1 = 2"); |
474 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 = 2"); |
475 val form = get_obj g_form pt (fst p); |
475 val form = get_obj g_form pt (fst p); |
476 val (res,_) = get_obj g_result pt (fst p); |
476 val (res,_) = get_obj g_result pt (fst p); |
477 if UnparseC.term form = "x + 1 = 2" andalso res = TermC.empty then () else |
477 if UnparseC.term form = "x + 1 = 2" andalso res = TermC.empty then () else |
478 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)"; |
478 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm)"; |
479 if not (existpt ((lev_on o fst) p) pt) then () else |
479 if not (existpt ((lev_on o fst) p) pt) then () else |
480 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt"; |
480 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Frm) nxt"; |
481 |
481 |
482 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*); |
482 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[1]*); |
483 val p = ([1], Res); |
483 val p = ([1], Res); |
484 val (pt,cuts) = |
484 val (pt,cuts) = |
485 cappend_atomic pt (fst p) Istate.empty (TermC.str2term "x + 1 = 2") |
485 cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 = 2") |
486 Empty_Tac (TermC.str2term "x + 1 + - 1 * 2 = 0",[]) Incomplete; |
486 Empty_Tac (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0",[]) Incomplete; |
487 val form = get_obj g_form pt (fst p); |
487 val form = get_obj g_form pt (fst p); |
488 val (res,_) = get_obj g_result pt (fst p); |
488 val (res,_) = get_obj g_result pt (fst p); |
489 if UnparseC.term form = "x + 1 = 2" andalso UnparseC.term res = "x + 1 + - 1 * 2 = 0" |
489 if UnparseC.term form = "x + 1 = 2" andalso UnparseC.term res = "x + 1 + - 1 * 2 = 0" |
490 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)"; |
490 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res)"; |
491 if not (existpt ((lev_on o fst) p) pt) then () else |
491 if not (existpt ((lev_on o fst) p) pt) then () else |
492 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt"; |
492 error "ctree.sml, diff.behav. cappend minisubpbl ([1],Res) nxt"; |
493 |
493 |
494 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*); |
494 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[2]*); |
495 val p = ([2], Res); |
495 val p = ([2], Res); |
496 val (pt,cuts) = |
496 val (pt,cuts) = |
497 cappend_atomic pt (fst p) Istate.empty (TermC.str2term "x + 1 + - 1 * 2 = 0") |
497 cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0") |
498 Empty_Tac (TermC.str2term "- 1 + x = 0",[]) Incomplete; |
498 Empty_Tac (TermC.parse_test @{context} "- 1 + x = 0",[]) Incomplete; |
499 val form = get_obj g_form pt (fst p); |
499 val form = get_obj g_form pt (fst p); |
500 val (res,_) = get_obj g_result pt (fst p); |
500 val (res,_) = get_obj g_result pt (fst p); |
501 if UnparseC.term form = "x + 1 + - 1 * 2 = 0" andalso UnparseC.term res = "- 1 + x = 0" |
501 if UnparseC.term form = "x + 1 + - 1 * 2 = 0" andalso UnparseC.term res = "- 1 + x = 0" |
502 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)"; |
502 then () else error "ctree.sml, diff.behav. cappend minisubpbl ([2],Res)"; |
503 if not (existpt ((lev_on o fst) p) pt) then () else |
503 if not (existpt ((lev_on o fst) p) pt) then () else |
514 |
514 |
515 (* ...complete calchead skipped...*) |
515 (* ...complete calchead skipped...*) |
516 |
516 |
517 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*); |
517 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*); |
518 val p = ([3, 1], Frm); |
518 val p = ([3, 1], Frm); |
519 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.str2term "- 1 + x = 0"); |
519 val (pt,cuts) = cappend_form pt (fst p) Istate.empty (TermC.parse_test @{context} "- 1 + x = 0"); |
520 val form = get_obj g_form pt (fst p); |
520 val form = get_obj g_form pt (fst p); |
521 val (res,_) = get_obj g_result pt (fst p); |
521 val (res,_) = get_obj g_result pt (fst p); |
522 if UnparseC.term form = "- 1 + x = 0" andalso res = TermC.empty then () else |
522 if UnparseC.term form = "- 1 + x = 0" andalso res = TermC.empty then () else |
523 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)"; |
523 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm)"; |
524 if not (existpt ((lev_on o fst) p) pt) then () else |
524 if not (existpt ((lev_on o fst) p) pt) then () else |
525 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt"; |
525 error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Frm) nxt"; |
526 |
526 |
527 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*) |
527 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_atomic: pos =[3,1]*) |
528 val p = ([3, 1], Res); |
528 val p = ([3, 1], Res); |
529 val (pt,cuts) = |
529 val (pt,cuts) = |
530 cappend_atomic pt (fst p) Istate.empty (TermC.str2term "- 1 + x = 0") |
530 cappend_atomic pt (fst p) Istate.empty (TermC.parse_test @{context} "- 1 + x = 0") |
531 Empty_Tac (TermC.str2term "x = 0 + - 1 * - 1",[]) Incomplete; |
531 Empty_Tac (TermC.parse_test @{context} "x = 0 + - 1 * - 1",[]) Incomplete; |
532 val form = get_obj g_form pt (fst p); |
532 val form = get_obj g_form pt (fst p); |
533 val (res,_) = get_obj g_result pt (fst p); |
533 val (res,_) = get_obj g_result pt (fst p); |
534 if UnparseC.term form = "- 1 + x = 0" andalso UnparseC.term res = "x = 0 + - 1 * - 1" then() |
534 if UnparseC.term form = "- 1 + x = 0" andalso UnparseC.term res = "x = 0 + - 1 * - 1" then() |
535 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)"; |
535 else error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res)"; |
536 if not (existpt ((lev_on o fst) p) pt) then () else |
536 if not (existpt ((lev_on o fst) p) pt) then () else |
1158 Test_Tool.show_pt pt; |
1158 Test_Tool.show_pt pt; |
1159 |
1159 |
1160 "---(2) on S(606)..S(608)--------"; |
1160 "---(2) on S(606)..S(608)--------"; |
1161 (*========== inhibit exn AK110726 ============================================== |
1161 (*========== inhibit exn AK110726 ============================================== |
1162 (* ERROR: Can't unify istate to istate * Proof.context *) |
1162 (* ERROR: Can't unify istate to istate * Proof.context *) |
1163 val (pt', cuts) = cappend_atomic pt [1] Istate.empty (TermC.str2term "Inform[1]") |
1163 val (pt', cuts) = cappend_atomic pt [1] Istate.empty (TermC.parse_test @{context} "Inform[1]") |
1164 (Tac "test") (TermC.str2term "Inres[1]",[]) Complete; |
1164 (Tac "test") (TermC.parse_test @{context} "Inres[1]",[]) Complete; |
1165 |
1165 |
1166 (*default_print_depth 99;*) |
1166 (*default_print_depth 99;*) |
1167 cuts; |
1167 cuts; |
1168 (*default_print_depth 3;*) |
1168 (*default_print_depth 3;*) |
1169 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), |
1169 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), |
1180 if afterins = [([1], Frm), ([1], Res)] then() |
1180 if afterins = [([1], Frm), ([1], Res)] then() |
1181 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins"; |
1181 else error "ctree.sml: diff:behav. in complete pt: append_atomic[1] afterins"; |
1182 Test_Tool.show_pt pt'; |
1182 Test_Tool.show_pt pt'; |
1183 "---(3) on S(606)..S(608)--------"; |
1183 "---(3) on S(606)..S(608)--------"; |
1184 Test_Tool.show_pt pt; |
1184 Test_Tool.show_pt pt; |
1185 val (pt', cuts) = cappend_atomic pt [2] Istate.empty (TermC.str2term "Inform[2]") |
1185 val (pt', cuts) = cappend_atomic pt [2] Istate.empty (TermC.parse_test @{context} "Inform[2]") |
1186 (Tac "test") (TermC.str2term "Inres[2]",[]) Complete; |
1186 (Tac "test") (TermC.parse_test @{context} "Inres[2]",[]) Complete; |
1187 (*default_print_depth 99;*) |
1187 (*default_print_depth 99;*) |
1188 cuts; |
1188 cuts; |
1189 (*default_print_depth 3;*) |
1189 (*default_print_depth 3;*) |
1190 |
1190 |
1191 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), |
1191 if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), |
1218 ostate2str (get_obj g_ostate pt' [2]); |
1218 ostate2str (get_obj g_ostate pt' [2]); |
1219 *) |
1219 *) |
1220 |
1220 |
1221 "---(4) on S(606)..S(608)--------"; |
1221 "---(4) on S(606)..S(608)--------"; |
1222 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],References.empty) |
1222 val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],References.empty) |
1223 ([],References.empty, TermC.str2term "Inhead[3]", ContextC.empty); |
1223 ([],References.empty, TermC.parse_test @{context} "Inhead[3]", ContextC.empty); |
1224 (*default_print_depth 99;*) |
1224 (*default_print_depth 99;*) |
1225 cuts; |
1225 cuts; |
1226 (*default_print_depth 3;*) |
1226 (*default_print_depth 3;*) |
1227 if cuts = [([3], Pbl), |
1227 if cuts = [([3], Pbl), |
1228 ([3, 1], Frm), ([3, 1], Res), |
1228 ([3, 1], Frm), ([3, 1], Res), |
1243 (* use"systest/ctree.sml"; |
1243 (* use"systest/ctree.sml"; |
1244 use"ctree.sml"; |
1244 use"ctree.sml"; |
1245 *) |
1245 *) |
1246 |
1246 |
1247 "---(6- 1) on S(606)..S(608)--------"; |
1247 "---(6- 1) on S(606)..S(608)--------"; |
1248 val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (TermC.str2term "Inform[3,1]") |
1248 val (pt', cuts) = cappend_atomic pt [3,1] Istate.empty (TermC.parse_test @{context} "Inform[3,1]") |
1249 (Tac "test") (TermC.str2term "Inres[3,1]",[]) Complete; |
1249 (Tac "test") (TermC.parse_test @{context} "Inres[3,1]",[]) Complete; |
1250 (*default_print_depth 99;*) |
1250 (*default_print_depth 99;*) |
1251 cuts; |
1251 cuts; |
1252 (*default_print_depth 3;*) |
1252 (*default_print_depth 3;*) |
1253 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), |
1253 if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), |
1254 ([3, 2], Res), |
1254 ([3, 2], Res), |
1269 |
1269 |
1270 if UnparseC.term (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else |
1270 if UnparseC.term (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else |
1271 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform"; |
1271 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform"; |
1272 |
1272 |
1273 "---(6) on S(606)..S(608)--------"; |
1273 "---(6) on S(606)..S(608)--------"; |
1274 val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (TermC.str2term "Inform[3,2]") |
1274 val (pt', cuts) = cappend_atomic pt [3,2] Istate.empty (TermC.parse_test @{context} "Inform[3,2]") |
1275 (Tac "test") (TermC.str2term "Inres[3,2]",[]) Complete; |
1275 (Tac "test") (TermC.parse_test @{context} "Inres[3,2]",[]) Complete; |
1276 (*default_print_depth 99;*) |
1276 (*default_print_depth 99;*) |
1277 cuts; |
1277 cuts; |
1278 (*default_print_depth 3;*) |
1278 (*default_print_depth 3;*) |
1279 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else |
1279 if cuts = [([3], Res), ([4], Res), ([], Res)] then () else |
1280 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts"; |
1280 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts"; |
1294 if UnparseC.term (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else |
1294 if UnparseC.term (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else |
1295 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform"; |
1295 error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform"; |
1296 |
1296 |
1297 "---(6++) on S(606)..S(608)--------"; |
1297 "---(6++) on S(606)..S(608)--------"; |
1298 (**) |
1298 (**) |
1299 val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.str2term "Inform[3,2,1]") |
1299 val (pt', cuts) = cappend_atomic pt [3,2,1] Istate.empty (TermC.parse_test @{context} "Inform[3,2,1]") |
1300 (Tac "test") (TermC.str2term "Inres[3,2,1]",[]) Complete; |
1300 (Tac "test") (TermC.parse_test @{context} "Inres[3,2,1]",[]) Complete; |
1301 (*default_print_depth 99;*) |
1301 (*default_print_depth 99;*) |
1302 cuts; |
1302 cuts; |
1303 (*default_print_depth 1;*) |
1303 (*default_print_depth 1;*) |
1304 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] |
1304 if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res), ([], Res)] |
1305 then () else |
1305 then () else |