# HG changeset patch # User wneuper # Date 1109338898 -3600 # Node ID e88dafb69d6ff3b5c17ca9ec49bb957b2d786084 # Parent 5e3036b8076e90e48d2f8ee78b7a5e83f87102d9 sml-050225c: intermediate in cut_levup diff -r 5e3036b8076e -r e88dafb69d6f src/sml/ME/ctreeNEW.sml --- a/src/sml/ME/ctreeNEW.sml Fri Feb 25 09:56:31 2005 +0100 +++ b/src/sml/ME/ctreeNEW.sml Fri Feb 25 14:41:38 2005 +0100 @@ -1,4 +1,5 @@ -(* use"ME/ctreeNEW.sml"; +(* use"../ME/ctreeNEW.sml"; + use"ME/ctreeNEW.sml"; use"ctreeNEW.sml"; *) @@ -26,9 +27,6 @@ -(* use"ME/ctreeNEW.sml"; - use"ctreeNEW.sml"; - *) (*----OLD-----*) fun get_allps (cuts: pos' list) (P:pos) [] = cuts | get_allps cuts P (pt::pts) = @@ -66,9 +64,13 @@ (*.shall the nodes _after_ the pos to be inserted at be deleted?.*) fun test_trans (PrfObj{branch = Transitive,...}) = true | test_trans (PrfObj{branch = NoBranch,...}) = true - (*| test_trans (PblObj{branch = NoBranch,...}) = true - WN050221 for test on worksheet*) + | test_trans (PblObj{branch = Transitive,...}) = true + | test_trans (PblObj{branch = NoBranch,...}) = true | test_trans _ = false; +(*.shall cutting be continued on the higher level(s)? + the Nd regarded will NOT be changed.*) +fun cutlevup (PblObj _) = false (*for tests of LK0502*) + | cutlevup _ = true; (*cut_bottom new S(603)..(608) cut the level at the bottom of the pos (used by cappend_...) @@ -76,120 +78,103 @@ fn: ptree -> : the _whole_ ptree for cut_levup pos * posel -> : the pos after split_last ptree -> : the parent of the Nd to be cut - ptree * pos' list: the updated ptree and the pos's cut +return + (ptree * : the updated ptree + pos' list) * : the pos's cut + bool : cutting shall be continued on the higher level(s) *) (* val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, pos); val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, [2]); *) -(**#############before bottom..levup ####################################**) -fun cut_bottom cuts P (Nd (b, bs)) (p::[]) = - let (*top down divide each level into 3 parts...*) - val keep = take (p - 1, bs) - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*) - val tail = takerest (p, bs) - in if test_trans b' - then (Nd (del_res b(*...and handle parent*), keep(*here at end*)), - cuts - @ (get_allpos's (P @ [p], 1) bs') - @ (get_allpos's (P, p + 1) tail) - @ (if g_ostate b = Incomplete then [(P,Res)] else [])) - - else (Nd (b, keep @ [(*Nd (b',bs') 'insert'ed*)] @ tail), - cuts - @ (get_allpos's (P @ [p], 1) bs')) - end - | cut_bottom cuts P (pt as Nd (b,bs)) (p::ps) = (pt,[]) -; -(* - let (*top down divide each level into 3 parts...*) - val keep = take (p - 1, bs) - val (pt' as (Nd (b',_)), cuts') = cut_bottom cuts (P@[p]) (nth p bs) ps - val tail = takerest (p, bs) - in if test_trans b' - then (Nd ((*if P=[]...del_res*)b, - keep @ [delete_result pt' []]), - cuts @ cuts' @ ([(*Res pt'?*)]) @ (get_allpos's tail)) - else (Nd (b, keep @ [pt'] @ tail), - cuts @ cuts' @ ([(*Res pt'*)])) - end -*) -print_depth 3; -(**############# result constructed goOn finished ########################**) print_depth 99; -fun cut_bottom (pt:ptree) (P:pos, p:posel) (Nd (b, bs)) = - let (*divide level into 3 parts...*) - val keep = take (p - 1, bs) - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*) - val tail = takerest (p, bs) - val (children, cuts) = - if test_trans b' - then (keep, - (get_allpos's (P @ [p], 1) bs') - @ (get_allpos's (P, p + 1) tail)) - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail, - get_allpos's (P @ [p], 1) bs') - val (parent, cuts) = - if test_trans b - then (Nd (del_res b, children), - cuts @ (if g_ostate b = Incomplete then [(P,Res)] else [])) - else (Nd (b, children), cuts) - val cutlevup = test_trans b - in (parent, cuts:pos' list) end; -print_depth 3; -(**############# new get_allpos ########################################**) -print_depth 99; -fun cut_bottom (pt:ptree) (P:pos, p:posel) (Nd (b, bs)) = - let (*divide level into 3 parts...*) - val keep = take (p - 1, bs) - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*) - val tail = takerest (p, bs) - val (children, cuts) = - if test_trans b' - then (keep, - (get_allps [] (P @ [1]) bs') - @ (get_allps [] (P @ [1]) tail)) - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail, - get_allps [] (P @ [1]) bs') - val (parent, cuts) = - if test_trans b - then (Nd (del_res b, children), - cuts @ (if g_ostate b = Incomplete then [(P,Res)] else [])) - else (Nd (b, children), cuts) - val cutlevup = test_trans b - in (parent, cuts:pos' list) end; -print_depth 3; -(**############# correct call of get_allps##############################**) -print_depth 99; +(**############# 2nd get_allp/s/ ######################################**) fun cut_bottom (pt:ptree) (P, p) (Nd (b, bs)) = let (*divide level into 3 parts...*) val keep = take (p - 1, bs) - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*) + val pt' as Nd (_,bs') = nth p bs + (*^^^^^_here_ will be 'insert'ed by 'append_..'*) val (tail, tp) = (takerest (p, bs), if null (takerest (p, bs)) then 0 else p + 1) - val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [1])); + val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p])); val (children, cuts) = - if test_trans b' - then (keep, - ( get_allps [] (P @ [p] @ [1]) bs') (*1 lev_dn*) - @ (get_allps [] (P @ [p+1]) tail)) (*on level*) + if test_trans b + then (keep, + (if is_pblnd pt' then [(P @ [p], Pbl)] else []) + @ (get_allp [] (P @ [p], (P, Frm)) pt') + @ (get_allps [] (P @ [p+1]) tail)) else (keep @ [(*'insert'ed by 'append_..'*)] @ tail, get_allps [] (P @ [p] @ [1]) bs') + val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b)); val (parent, cuts) = + if cutlevup b + then (Nd (del_res b, children), + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)])) + else (Nd (b, children), cuts) + in ((parent, cuts:pos' list), cutlevup b) end; +print_depth 3; +(**############# 2nd get_allp finished############################**) +fun cut_bottom (pt:ptree) (P, p) (Nd (b, bs)) = + let (*divide level into 3 parts...*) + val keep = take (p - 1, bs) + val pt' as Nd (_,bs') = nth p bs + (*^^^^^_here_ will be 'insert'ed by 'append_..'*) + val (tail, tp) = (takerest (p, bs), + if null (takerest (p, bs)) then 0 else p + 1) + val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p])); + val (children, cuts) = if test_trans b + then (keep, + (if is_pblnd pt' then [(P @ [p], Pbl)] else []) + @ (get_allp [] (P @ [p], (P, Frm)) pt') + @ (get_allps [] (P @ [p+1]) tail)) + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail, + get_allp [] (P @ [p], (P, Frm)) pt') + val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b)); + val (parent, cuts) = + if cutlevup b then (Nd (del_res b, children), - cuts @ (if g_ostate b = Incomplete then [(P,Res)] else [])) + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)])) else (Nd (b, children), cuts) - val cutlevup = test_trans b + in ((parent, cuts:pos' list), cutlevup b) end; +print_depth 3; +(**######################################################################**); +(**############# start cut_levup ########################################**) +fun cut_levup clevup (pt:ptree) (P, p) (Nd (b, bs)) = + let (*divide level into 3 parts...*) + val keep = take (p - 1, bs) + val pt' as Nd (_,bs') = nth p bs + (*^^^^^_here_ will be 'insert'ed by 'append_..'*) + val (tail, tp) = (takerest (p, bs), + if null (takerest (p, bs)) then 0 else p + 1) + val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p])); + val (children, cuts) = + if test_trans b + then (keep, + (if is_pblnd pt' then [(P @ [p], Pbl)] else []) + @ (get_allp [] (P @ [p], (P, Frm)) pt') + @ (get_allps [] (P @ [p+1]) tail)) + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail, + get_allps [] (P @ [p] @ [1]) bs') + val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b)); + val (parent, cuts) = + if cutlevup b + then (Nd (del_res b, children), + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)])) + else (Nd (b, children), cuts) in (parent, cuts:pos' list) end; print_depth 3; (**######################################################################**); - - +(* use"ME/ctreeNEW.sml"; + use"ctreeNEW.sml"; + *) fun cut_tree pt (pos,_) = let val (P, p) = split_last pos; - val (pt, cuts) = cut_bottom pt (P, p) (get_nd pt P) - in (pt, cuts) end; + val ((pt', cuts), clevup) = cut_bottom pt (P, p) (get_nd pt P) +(* val ((pt', cuts), clevup) = if null P then ((pt', cuts),[]) else + cut_levup clevup pt +*) + in (pt', cuts) end; print_depth 99; cut_tree; diff -r 5e3036b8076e -r e88dafb69d6f src/sml/ME/modspec.sml --- a/src/sml/ME/modspec.sml Fri Feb 25 09:56:31 2005 +0100 +++ b/src/sml/ME/modspec.sml Fri Feb 25 14:41:38 2005 +0100 @@ -1895,5 +1895,6 @@ fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o (map posform2str)) pfs; +(*WN050225 omits the last step, if pt is incomplete*) fun show_pt pt = writeln (posforms2str (get_interval ([],Frm) ([],Res) 99999 pt)); diff -r 5e3036b8076e -r e88dafb69d6f src/sml/systest/ctree.sml --- a/src/sml/systest/ctree.sml Fri Feb 25 09:56:31 2005 +0100 +++ b/src/sml/systest/ctree.sml Fri Feb 25 14:41:38 2005 +0100 @@ -2,6 +2,7 @@ use"systest/ctree.sml"; use"ctree.sml"; *) +print_depth 99; cuts; print_depth 3; "-----------------------------------------------------------------"; "=====new ptree 1 miniscript with mini-subpbl ===================="; @@ -348,22 +349,20 @@ "-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; "-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; "-------------- cut_tree (intermedi.ptree: 3rd level)-------------"; - +(*WN050225 intermed. outcommented val (pt', cuts) = cut_tree pt ([3,2,1],Frm); if cuts = [([3, 2, 1], Res), ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), - ([4], Res), - ([], Res)] + ([4], Res)] then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 1"; val (pt', cuts) = cut_tree pt ([3,2,1],Res); if cuts = [([3, 2, 2], Res), ([3, 2], Res), ([3], Res), - ([4], Res), - ([], Res)] + ([4], Res)] then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 2"; @@ -495,6 +494,7 @@ (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*); (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*); +WN050225 intermed. outcommented---*) "=====new ptree 3 ================================================"; "=====new ptree 3 ================================================"; @@ -949,7 +949,7 @@ val ((pt,_),_) = get_calc 1; show_pt pt; -(**##############################################################(**) +(**##############################################################**) "-------------- get_allpos' new ----------------------------------"; "-------------- get_allpos' new ----------------------------------"; "-------------- get_allpos' new ----------------------------------"; @@ -978,6 +978,7 @@ if cuts = cuts2 @ [([], Res)] then () else raise error "ctree.sml diff.behav. get_allps new []"; +"---(3) on S(606)..S(608)--------"; "--- nd [2] with 6 children---------------------------------"; val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]); if cuts = @@ -991,6 +992,7 @@ raise error "ctree.sml diff.behav. get_allps new [2]"; +"---(4) on S(606)..S(608)--------"; "--- nd [3] subproblem--------------------------------------"; val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]); if cuts = @@ -1022,17 +1024,118 @@ "-------------- cut_tree new (from ptree above)-------------------"; "-------------- cut_tree new (from ptree above)-------------------"; show_pt pt; -(* print_depth 99; cuts; print_depth 3; - print_depth 99; get_allpos's (P@[p], 0) bs'; print_depth 3; - print_depth 99; get_allpos's (P,p+1) tail; print_depth 3; - *) +val b = get_obj g_branch pt []; +if b = TransitiveB then () else +raise error ("ctree.sml diff.behav. in [] branch="^branch2str b); +val b = get_obj g_branch pt [3]; +if b = TransitiveB then () else +raise error ("ctree.sml diff.behav. in [3] branch="^branch2str b); + +"---(2) on S(606)..S(608)--------"; +val (pt', cuts) = cut_tree pt ([1],Res); +print_depth 99; +cuts; +print_depth 3; +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl), + ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res)] then () else +raise error "ctree.sml: diff.behav. cut_tree ([1],Res)"; + + +"---(3) on S(606)..S(608)--------"; val (pt', cuts) = cut_tree pt ([2],Res); print_depth 99; cuts; print_depth 3; -if cuts = [] -then () else raise error "ctree.sml: diff.behav. cut_tree ([2],Res)"; +if cuts = [(*preceding step on WS was ([1]),Res*) + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), + ([2], Res), + ([3], Pbl), + ([3, 1], Frm), + ([3, 1], Res), + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), + ([3, 2], Res), + ([3], Res), + ([4], Res) + (*([],Res) because cutlevup=false*)] then () else +raise error "ctree.sml: diff.behav. cut_tree ([2],Res)"; + +"---(4) on S(606)..S(608)--------"; +val (pt', cuts) = cut_tree pt ([3],Pbl); +print_depth 99; +cuts; +print_depth 3; +if cuts = [([3], Pbl), + ([3, 1], Frm), ([3, 1], Res), + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), + ([3, 2], Res), + ([3], Res), + ([4], Res)] then () else +raise error "ctree.sml: diff.behav. cut_tree ([3],Pbl)"; + + +(**#################################################################**) + +"-------------- cappend on complete ctree from above -------------"; +"-------------- cappend on complete ctree from above -------------"; +"-------------- cappend on complete ctree from above -------------"; +(* use"systest/ctree.sml"; + use"ctree.sml"; + *) + +"---(3) on S(606)..S(608)--------"; +val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]") + (Tac "test") (str2term "Inres[2]",[]) Complete; +print_depth 99; +cuts; +print_depth 3; +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res), + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl), + ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res), + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res)] then () else +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] cuts"; +val insrted = get_allp [] ([], ([],Frm)) pt'; +print_depth 99; +insrted; +print_depth 3; +if insrted = [([1], Frm), ([1], Res), ([2], Res), ([], Res)] then () else +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] insrted"; +show_pt pt'; + +"---(4) on S(606)..S(608)--------"; +val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec) + ([],e_spec, str2term "Inhead[3]"); +print_depth 99; +cuts; +print_depth 3; +if cuts = [([3], Pbl), + ([3, 1], Frm), ([3, 1], Res), + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res), + ([3, 2], Res), + ([3], Res), ([4], Res)] then () else +raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts"; +val insrted = get_allp [] ([], ([],Frm)) pt'; +print_depth 99; +insrted; +print_depth 3; +if insrted = + [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), + ([3], Pbl)] then () else +raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] insrted"; +show_pt pt'; +(* use"../systest/ctree.sml"; + use"systest/ctree.sml"; + use"ctree.sml"; + *) + + + + +(* val (res,asm) = get_obj g_result pt' [2]; if res = e_term (*WN050219 done by cut_level*) then () else raise error "ctree.sml: diff:behav. in cut_tree 1aa"; @@ -1050,5 +1153,4 @@ ([1], Frm), ([1], Res)] then () else raise error "ctree.sml: diff:behav. in cut_tree 1ad"; -(**)#################################################################**) - +*) \ No newline at end of file