1.1 --- a/src/sml/ME/ctreeNEW.sml Fri Feb 25 09:56:31 2005 +0100
1.2 +++ b/src/sml/ME/ctreeNEW.sml Fri Feb 25 14:41:38 2005 +0100
1.3 @@ -1,4 +1,5 @@
1.4 -(* use"ME/ctreeNEW.sml";
1.5 +(* use"../ME/ctreeNEW.sml";
1.6 + use"ME/ctreeNEW.sml";
1.7 use"ctreeNEW.sml";
1.8 *)
1.9
1.10 @@ -26,9 +27,6 @@
1.11
1.12
1.13
1.14 -(* use"ME/ctreeNEW.sml";
1.15 - use"ctreeNEW.sml";
1.16 - *)
1.17 (*----OLD-----*)
1.18 fun get_allps (cuts: pos' list) (P:pos) [] = cuts
1.19 | get_allps cuts P (pt::pts) =
1.20 @@ -66,9 +64,13 @@
1.21 (*.shall the nodes _after_ the pos to be inserted at be deleted?.*)
1.22 fun test_trans (PrfObj{branch = Transitive,...}) = true
1.23 | test_trans (PrfObj{branch = NoBranch,...}) = true
1.24 - (*| test_trans (PblObj{branch = NoBranch,...}) = true
1.25 - WN050221 for test on worksheet*)
1.26 + | test_trans (PblObj{branch = Transitive,...}) = true
1.27 + | test_trans (PblObj{branch = NoBranch,...}) = true
1.28 | test_trans _ = false;
1.29 +(*.shall cutting be continued on the higher level(s)?
1.30 + the Nd regarded will NOT be changed.*)
1.31 +fun cutlevup (PblObj _) = false (*for tests of LK0502*)
1.32 + | cutlevup _ = true;
1.33
1.34 (*cut_bottom new S(603)..(608)
1.35 cut the level at the bottom of the pos (used by cappend_...)
1.36 @@ -76,120 +78,103 @@
1.37 fn: ptree -> : the _whole_ ptree for cut_levup
1.38 pos * posel -> : the pos after split_last
1.39 ptree -> : the parent of the Nd to be cut
1.40 - ptree * pos' list: the updated ptree and the pos's cut
1.41 +return
1.42 + (ptree * : the updated ptree
1.43 + pos' list) * : the pos's cut
1.44 + bool : cutting shall be continued on the higher level(s)
1.45 *)
1.46
1.47 (* val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, pos);
1.48 val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, [2]);
1.49 *)
1.50 -(**#############before bottom..levup ####################################**)
1.51 -fun cut_bottom cuts P (Nd (b, bs)) (p::[]) =
1.52 - let (*top down divide each level into 3 parts...*)
1.53 - val keep = take (p - 1, bs)
1.54 - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*)
1.55 - val tail = takerest (p, bs)
1.56 - in if test_trans b'
1.57 - then (Nd (del_res b(*...and handle parent*), keep(*here at end*)),
1.58 - cuts
1.59 - @ (get_allpos's (P @ [p], 1) bs')
1.60 - @ (get_allpos's (P, p + 1) tail)
1.61 - @ (if g_ostate b = Incomplete then [(P,Res)] else []))
1.62 -
1.63 - else (Nd (b, keep @ [(*Nd (b',bs') 'insert'ed*)] @ tail),
1.64 - cuts
1.65 - @ (get_allpos's (P @ [p], 1) bs'))
1.66 - end
1.67 - | cut_bottom cuts P (pt as Nd (b,bs)) (p::ps) = (pt,[])
1.68 -;
1.69 -(*
1.70 - let (*top down divide each level into 3 parts...*)
1.71 - val keep = take (p - 1, bs)
1.72 - val (pt' as (Nd (b',_)), cuts') = cut_bottom cuts (P@[p]) (nth p bs) ps
1.73 - val tail = takerest (p, bs)
1.74 - in if test_trans b'
1.75 - then (Nd ((*if P=[]...del_res*)b,
1.76 - keep @ [delete_result pt' []]),
1.77 - cuts @ cuts' @ ([(*Res pt'?*)]) @ (get_allpos's tail))
1.78 - else (Nd (b, keep @ [pt'] @ tail),
1.79 - cuts @ cuts' @ ([(*Res pt'*)]))
1.80 - end
1.81 -*)
1.82 -print_depth 3;
1.83 -(**############# result constructed goOn finished ########################**)
1.84 print_depth 99;
1.85 -fun cut_bottom (pt:ptree) (P:pos, p:posel) (Nd (b, bs)) =
1.86 - let (*divide level into 3 parts...*)
1.87 - val keep = take (p - 1, bs)
1.88 - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*)
1.89 - val tail = takerest (p, bs)
1.90 - val (children, cuts) =
1.91 - if test_trans b'
1.92 - then (keep,
1.93 - (get_allpos's (P @ [p], 1) bs')
1.94 - @ (get_allpos's (P, p + 1) tail))
1.95 - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.96 - get_allpos's (P @ [p], 1) bs')
1.97 - val (parent, cuts) =
1.98 - if test_trans b
1.99 - then (Nd (del_res b, children),
1.100 - cuts @ (if g_ostate b = Incomplete then [(P,Res)] else []))
1.101 - else (Nd (b, children), cuts)
1.102 - val cutlevup = test_trans b
1.103 - in (parent, cuts:pos' list) end;
1.104 -print_depth 3;
1.105 -(**############# new get_allpos ########################################**)
1.106 -print_depth 99;
1.107 -fun cut_bottom (pt:ptree) (P:pos, p:posel) (Nd (b, bs)) =
1.108 - let (*divide level into 3 parts...*)
1.109 - val keep = take (p - 1, bs)
1.110 - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*)
1.111 - val tail = takerest (p, bs)
1.112 - val (children, cuts) =
1.113 - if test_trans b'
1.114 - then (keep,
1.115 - (get_allps [] (P @ [1]) bs')
1.116 - @ (get_allps [] (P @ [1]) tail))
1.117 - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.118 - get_allps [] (P @ [1]) bs')
1.119 - val (parent, cuts) =
1.120 - if test_trans b
1.121 - then (Nd (del_res b, children),
1.122 - cuts @ (if g_ostate b = Incomplete then [(P,Res)] else []))
1.123 - else (Nd (b, children), cuts)
1.124 - val cutlevup = test_trans b
1.125 - in (parent, cuts:pos' list) end;
1.126 -print_depth 3;
1.127 -(**############# correct call of get_allps##############################**)
1.128 -print_depth 99;
1.129 +(**############# 2nd get_allp/s/ ######################################**)
1.130 fun cut_bottom (pt:ptree) (P, p) (Nd (b, bs)) =
1.131 let (*divide level into 3 parts...*)
1.132 val keep = take (p - 1, bs)
1.133 - val Nd (b',bs') = nth p bs(*here* will be 'insert'ed by 'append_..'*)
1.134 + val pt' as Nd (_,bs') = nth p bs
1.135 + (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1.136 val (tail, tp) = (takerest (p, bs),
1.137 if null (takerest (p, bs)) then 0 else p + 1)
1.138 - val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [1]));
1.139 + val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p]));
1.140 val (children, cuts) =
1.141 - if test_trans b'
1.142 - then (keep,
1.143 - ( get_allps [] (P @ [p] @ [1]) bs') (*1 lev_dn*)
1.144 - @ (get_allps [] (P @ [p+1]) tail)) (*on level*)
1.145 + if test_trans b
1.146 + then (keep,
1.147 + (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.148 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.149 + @ (get_allps [] (P @ [p+1]) tail))
1.150 else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.151 get_allps [] (P @ [p] @ [1]) bs')
1.152 + val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b));
1.153 val (parent, cuts) =
1.154 + if cutlevup b
1.155 + then (Nd (del_res b, children),
1.156 + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.157 + else (Nd (b, children), cuts)
1.158 + in ((parent, cuts:pos' list), cutlevup b) end;
1.159 +print_depth 3;
1.160 +(**############# 2nd get_allp finished############################**)
1.161 +fun cut_bottom (pt:ptree) (P, p) (Nd (b, bs)) =
1.162 + let (*divide level into 3 parts...*)
1.163 + val keep = take (p - 1, bs)
1.164 + val pt' as Nd (_,bs') = nth p bs
1.165 + (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1.166 + val (tail, tp) = (takerest (p, bs),
1.167 + if null (takerest (p, bs)) then 0 else p + 1)
1.168 + val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p]));
1.169 + val (children, cuts) =
1.170 if test_trans b
1.171 + then (keep,
1.172 + (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.173 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.174 + @ (get_allps [] (P @ [p+1]) tail))
1.175 + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.176 + get_allp [] (P @ [p], (P, Frm)) pt')
1.177 + val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b));
1.178 + val (parent, cuts) =
1.179 + if cutlevup b
1.180 then (Nd (del_res b, children),
1.181 - cuts @ (if g_ostate b = Incomplete then [(P,Res)] else []))
1.182 + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.183 else (Nd (b, children), cuts)
1.184 - val cutlevup = test_trans b
1.185 + in ((parent, cuts:pos' list), cutlevup b) end;
1.186 +print_depth 3;
1.187 +(**######################################################################**);
1.188 +(**############# start cut_levup ########################################**)
1.189 +fun cut_levup clevup (pt:ptree) (P, p) (Nd (b, bs)) =
1.190 + let (*divide level into 3 parts...*)
1.191 + val keep = take (p - 1, bs)
1.192 + val pt' as Nd (_,bs') = nth p bs
1.193 + (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
1.194 + val (tail, tp) = (takerest (p, bs),
1.195 + if null (takerest (p, bs)) then 0 else p + 1)
1.196 + val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p]));
1.197 + val (children, cuts) =
1.198 + if test_trans b
1.199 + then (keep,
1.200 + (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
1.201 + @ (get_allp [] (P @ [p], (P, Frm)) pt')
1.202 + @ (get_allps [] (P @ [p+1]) tail))
1.203 + else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
1.204 + get_allps [] (P @ [p] @ [1]) bs')
1.205 + val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b));
1.206 + val (parent, cuts) =
1.207 + if cutlevup b
1.208 + then (Nd (del_res b, children),
1.209 + cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.210 + else (Nd (b, children), cuts)
1.211 in (parent, cuts:pos' list) end;
1.212 print_depth 3;
1.213 (**######################################################################**);
1.214 -
1.215 -
1.216 +(* use"ME/ctreeNEW.sml";
1.217 + use"ctreeNEW.sml";
1.218 + *)
1.219 fun cut_tree pt (pos,_) =
1.220 let val (P, p) = split_last pos;
1.221 - val (pt, cuts) = cut_bottom pt (P, p) (get_nd pt P)
1.222 - in (pt, cuts) end;
1.223 + val ((pt', cuts), clevup) = cut_bottom pt (P, p) (get_nd pt P)
1.224 +(* val ((pt', cuts), clevup) = if null P then ((pt', cuts),[]) else
1.225 + cut_levup clevup pt
1.226 +*)
1.227 + in (pt', cuts) end;
1.228
1.229 print_depth 99;
1.230 cut_tree;
2.1 --- a/src/sml/ME/modspec.sml Fri Feb 25 09:56:31 2005 +0100
2.2 +++ b/src/sml/ME/modspec.sml Fri Feb 25 14:41:38 2005 +0100
2.3 @@ -1895,5 +1895,6 @@
2.4 fun posforms2str pfs = (strs2str' o (map (curry op ^ "\n")) o
2.5 (map posform2str)) pfs;
2.6
2.7 +(*WN050225 omits the last step, if pt is incomplete*)
2.8 fun show_pt pt =
2.9 writeln (posforms2str (get_interval ([],Frm) ([],Res) 99999 pt));
3.1 --- a/src/sml/systest/ctree.sml Fri Feb 25 09:56:31 2005 +0100
3.2 +++ b/src/sml/systest/ctree.sml Fri Feb 25 14:41:38 2005 +0100
3.3 @@ -2,6 +2,7 @@
3.4 use"systest/ctree.sml";
3.5 use"ctree.sml";
3.6 *)
3.7 +print_depth 99; cuts; print_depth 3;
3.8
3.9 "-----------------------------------------------------------------";
3.10 "=====new ptree 1 miniscript with mini-subpbl ====================";
3.11 @@ -348,22 +349,20 @@
3.12 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
3.13 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
3.14 "-------------- cut_tree (intermedi.ptree: 3rd level)-------------";
3.15 -
3.16 +(*WN050225 intermed. outcommented
3.17 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
3.18 if cuts = [([3, 2, 1], Res),
3.19 ([3, 2, 2], Res),
3.20 ([3, 2], Res),
3.21 ([3], Res),
3.22 - ([4], Res),
3.23 - ([], Res)]
3.24 + ([4], Res)]
3.25 then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 1";
3.26
3.27 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
3.28 if cuts = [([3, 2, 2], Res),
3.29 ([3, 2], Res),
3.30 ([3], Res),
3.31 - ([4], Res),
3.32 - ([], Res)]
3.33 + ([4], Res)]
3.34 then () else raise error "ctree.sml: diff:behav. in cut_tree 3rd level 2";
3.35
3.36
3.37 @@ -495,6 +494,7 @@
3.38 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
3.39 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
3.40
3.41 +WN050225 intermed. outcommented---*)
3.42
3.43 "=====new ptree 3 ================================================";
3.44 "=====new ptree 3 ================================================";
3.45 @@ -949,7 +949,7 @@
3.46 val ((pt,_),_) = get_calc 1;
3.47 show_pt pt;
3.48
3.49 -(**##############################################################(**)
3.50 +(**##############################################################**)
3.51 "-------------- get_allpos' new ----------------------------------";
3.52 "-------------- get_allpos' new ----------------------------------";
3.53 "-------------- get_allpos' new ----------------------------------";
3.54 @@ -978,6 +978,7 @@
3.55 if cuts = cuts2 @ [([], Res)] then () else
3.56 raise error "ctree.sml diff.behav. get_allps new []";
3.57
3.58 +"---(3) on S(606)..S(608)--------";
3.59 "--- nd [2] with 6 children---------------------------------";
3.60 val cuts = get_allp [] ([2], ([],Frm)) (get_nd pt [2]);
3.61 if cuts =
3.62 @@ -991,6 +992,7 @@
3.63 raise error "ctree.sml diff.behav. get_allps new [2]";
3.64
3.65
3.66 +"---(4) on S(606)..S(608)--------";
3.67 "--- nd [3] subproblem--------------------------------------";
3.68 val cuts = get_allp [] ([3], ([],Frm)) (get_nd pt [3]);
3.69 if cuts =
3.70 @@ -1022,17 +1024,118 @@
3.71 "-------------- cut_tree new (from ptree above)-------------------";
3.72 "-------------- cut_tree new (from ptree above)-------------------";
3.73 show_pt pt;
3.74 -(* print_depth 99; cuts; print_depth 3;
3.75 - print_depth 99; get_allpos's (P@[p], 0) bs'; print_depth 3;
3.76 - print_depth 99; get_allpos's (P,p+1) tail; print_depth 3;
3.77 - *)
3.78 +val b = get_obj g_branch pt [];
3.79 +if b = TransitiveB then () else
3.80 +raise error ("ctree.sml diff.behav. in [] branch="^branch2str b);
3.81 +val b = get_obj g_branch pt [3];
3.82 +if b = TransitiveB then () else
3.83 +raise error ("ctree.sml diff.behav. in [3] branch="^branch2str b);
3.84 +
3.85 +"---(2) on S(606)..S(608)--------";
3.86 +val (pt', cuts) = cut_tree pt ([1],Res);
3.87 +print_depth 99;
3.88 +cuts;
3.89 +print_depth 3;
3.90 +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
3.91 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
3.92 + ([3, 1], Frm), ([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
3.93 + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res)] then () else
3.94 +raise error "ctree.sml: diff.behav. cut_tree ([1],Res)";
3.95 +
3.96 +
3.97 +"---(3) on S(606)..S(608)--------";
3.98 val (pt', cuts) = cut_tree pt ([2],Res);
3.99 print_depth 99;
3.100 cuts;
3.101 print_depth 3;
3.102 -if cuts = []
3.103 -then () else raise error "ctree.sml: diff.behav. cut_tree ([2],Res)";
3.104 +if cuts = [(*preceding step on WS was ([1]),Res*)
3.105 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
3.106 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
3.107 + ([2], Res),
3.108 + ([3], Pbl),
3.109 + ([3, 1], Frm),
3.110 + ([3, 1], Res),
3.111 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
3.112 + ([3, 2], Res),
3.113 + ([3], Res),
3.114 + ([4], Res)
3.115 + (*([],Res) because cutlevup=false*)] then () else
3.116 +raise error "ctree.sml: diff.behav. cut_tree ([2],Res)";
3.117
3.118 +
3.119 +"---(4) on S(606)..S(608)--------";
3.120 +val (pt', cuts) = cut_tree pt ([3],Pbl);
3.121 +print_depth 99;
3.122 +cuts;
3.123 +print_depth 3;
3.124 +if cuts = [([3], Pbl),
3.125 + ([3, 1], Frm), ([3, 1], Res),
3.126 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
3.127 + ([3, 2], Res),
3.128 + ([3], Res),
3.129 + ([4], Res)] then () else
3.130 +raise error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
3.131 +
3.132 +
3.133 +(**#################################################################**)
3.134 +
3.135 +"-------------- cappend on complete ctree from above -------------";
3.136 +"-------------- cappend on complete ctree from above -------------";
3.137 +"-------------- cappend on complete ctree from above -------------";
3.138 +(* use"systest/ctree.sml";
3.139 + use"ctree.sml";
3.140 + *)
3.141 +
3.142 +"---(3) on S(606)..S(608)--------";
3.143 +val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
3.144 + (Tac "test") (str2term "Inres[2]",[]) Complete;
3.145 +print_depth 99;
3.146 +cuts;
3.147 +print_depth 3;
3.148 +if cuts = [([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
3.149 + ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res), ([3], Pbl),
3.150 + ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
3.151 + ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res)] then () else
3.152 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] cuts";
3.153 +val insrted = get_allp [] ([], ([],Frm)) pt';
3.154 +print_depth 99;
3.155 +insrted;
3.156 +print_depth 3;
3.157 +if insrted = [([1], Frm), ([1], Res), ([2], Res), ([], Res)] then () else
3.158 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] insrted";
3.159 +show_pt pt';
3.160 +
3.161 +"---(4) on S(606)..S(608)--------";
3.162 +val (pt', cuts) = cappend_problem pt [3] e_istate ([],e_spec)
3.163 + ([],e_spec, str2term "Inhead[3]");
3.164 +print_depth 99;
3.165 +cuts;
3.166 +print_depth 3;
3.167 +if cuts = [([3], Pbl),
3.168 + ([3, 1], Frm), ([3, 1], Res),
3.169 + ([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
3.170 + ([3, 2], Res),
3.171 + ([3], Res), ([4], Res)] then () else
3.172 +raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
3.173 +val insrted = get_allp [] ([], ([],Frm)) pt';
3.174 +print_depth 99;
3.175 +insrted;
3.176 +print_depth 3;
3.177 +if insrted =
3.178 + [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
3.179 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
3.180 + ([3], Pbl)] then () else
3.181 +raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] insrted";
3.182 +show_pt pt';
3.183 +(* use"../systest/ctree.sml";
3.184 + use"systest/ctree.sml";
3.185 + use"ctree.sml";
3.186 + *)
3.187 +
3.188 +
3.189 +
3.190 +
3.191 +(*
3.192 val (res,asm) = get_obj g_result pt' [2];
3.193 if res = e_term (*WN050219 done by cut_level*) then () else
3.194 raise error "ctree.sml: diff:behav. in cut_tree 1aa";
3.195 @@ -1050,5 +1153,4 @@
3.196 ([1], Frm),
3.197 ([1], Res)] then () else
3.198 raise error "ctree.sml: diff:behav. in cut_tree 1ad";
3.199 -(**)#################################################################**)
3.200 -
3.201 +*)
3.202 \ No newline at end of file