sml-050303a-inter-cappend: intermediate state in work in error in cappend [3,2,1]
S(617)
1.1 --- a/src/sml/ME/ctree.sml Thu Mar 03 00:23:21 2005 +0100
1.2 +++ b/src/sml/ME/ctree.sml Thu Mar 03 17:54:09 2005 +0100
1.3 @@ -851,7 +851,8 @@
1.4 fun g_cell (PblObj {cell = c,...}) = c
1.5 | g_cell (PrfObj {cell = c,...}) = c;
1.6 fun g_form (PrfObj {form = f,...}) = f
1.7 - | g_form _ = raise PTREE "g_form not for PblObj";
1.8 + | g_form (PblObj {origin=(_,_,f),...}) = f;
1.9 +(* | g_form _ = raise PTREE "g_form not for PblObj";*)
1.10 fun g_origin (PblObj {origin = ori,...}) = ori
1.11 | g_origin _ = raise PTREE "g_origin not for PrfObj";
1.12 fun g_fmz (PblObj {fmz = f,...}) = f
2.1 --- a/src/sml/ME/ctreeNEW.sml Thu Mar 03 00:23:21 2005 +0100
2.2 +++ b/src/sml/ME/ctreeNEW.sml Thu Mar 03 17:54:09 2005 +0100
2.3 @@ -83,36 +83,6 @@
2.4 pos' list) * : the pos's cut
2.5 bool : cutting shall be continued on the higher level(s)
2.6 *)
2.7 -
2.8 -(* val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, pos);
2.9 - val (cuts, P, pt as Nd (b,bs), (p::[])) = ([], [], pt, [2]);
2.10 - *)
2.11 -print_depth 99;
2.12 -(**############# 2nd get_allp/s/ ######################################**)
2.13 -fun cut_bottom (pt:ptree) (P, p) (Nd (b, bs)) =
2.14 - let (*divide level into 3 parts...*)
2.15 - val keep = take (p - 1, bs)
2.16 - val pt' as Nd (_,bs') = nth p bs
2.17 - (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
2.18 - val (tail, tp) = (takerest (p, bs),
2.19 - if null (takerest (p, bs)) then 0 else p + 1)
2.20 - val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p]));
2.21 - val (children, cuts) =
2.22 - if test_trans b
2.23 - then (keep,
2.24 - (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
2.25 - @ (get_allp [] (P @ [p], (P, Frm)) pt')
2.26 - @ (get_allps [] (P @ [p+1]) tail))
2.27 - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
2.28 - get_allps [] (P @ [p] @ [1]) bs')
2.29 - val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b));
2.30 - val (parent, cuts) =
2.31 - if cutlevup b
2.32 - then (Nd (del_res b, children),
2.33 - cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2.34 - else (Nd (b, children), cuts)
2.35 - in ((parent, cuts:pos' list), cutlevup b) end;
2.36 -print_depth 3;
2.37 (**############# 2nd get_allp finished############################**)
2.38 fun cut_bottom (pt:ptree) (P, p) (Nd (b, bs)) =
2.39 let (*divide level into 3 parts...*)
2.40 @@ -121,7 +91,6 @@
2.41 (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
2.42 val (tail, tp) = (takerest (p, bs),
2.43 if null (takerest (p, bs)) then 0 else p + 1)
2.44 - val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p]));
2.45 val (children, cuts) =
2.46 if test_trans b
2.47 then (keep,
2.48 @@ -130,55 +99,83 @@
2.49 @ (get_allps [] (P @ [p+1]) tail))
2.50 else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
2.51 get_allp [] (P @ [p], (P, Frm)) pt')
2.52 - val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b));
2.53 - val (parent, cuts) =
2.54 + val (pt'', cuts) =
2.55 if cutlevup b
2.56 then (Nd (del_res b, children),
2.57 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2.58 else (Nd (b, children), cuts)
2.59 - in ((parent, cuts:pos' list), cutlevup b) end;
2.60 + val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
2.61 + ", Nd=.............................................")
2.62 + val _= show_pt pt''
2.63 + val _= writeln("####cut_bottom res="^
2.64 + term2str (fst (get_obj g_result pt'' [])))
2.65 + val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
2.66 + ", cuts="^pos's2str cuts)
2.67 + in ((pt'', cuts:pos' list), cutlevup b) end;
2.68 print_depth 3;
2.69 (**######################################################################**);
2.70 -(**############# start cut_levup ########################################**)
2.71 -fun cut_levup clevup (pt:ptree) (P, p) (Nd (b, bs)) =
2.72 +(*.go all levels from the bottom of 'pos' up to the root,
2.73 + on each level compose the children of a node and accumulate the cut Nds
2.74 +args
2.75 + pos' list -> : for accumulation
2.76 + bool -> : cutting shall be continued on the higher level(s)
2.77 + ptree -> : the whole ptree for 'get_nd pt P' on each level
2.78 + ptree -> : the Nd from the lower level for insertion at path
2.79 + pos * posel -> : pos=path split for convenience
2.80 + ptree -> : Nd the children of are under consideration on this call
2.81 +returns :
2.82 + ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
2.83 +.*)
2.84 +(*WN050225 neglects the recursive structure of the ptree*)
2.85 +print_depth 99;
2.86 +fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
2.87 let (*divide level into 3 parts...*)
2.88 val keep = take (p - 1, bs)
2.89 - val pt' as Nd (_,bs') = nth p bs
2.90 - (*^^^^^_here_ will be 'insert'ed by 'append_..'*)
2.91 + (*val pt' comes as argument*)
2.92 val (tail, tp) = (takerest (p, bs),
2.93 if null (takerest (p, bs)) then 0 else p + 1)
2.94 - val _= writeln("###cut_bottom: call get_allps with"^pos2str (P @ [p]));
2.95 - val (children, cuts) =
2.96 - if test_trans b
2.97 - then (keep,
2.98 - (if is_pblnd pt' then [(P @ [p], Pbl)] else [])
2.99 - @ (get_allp [] (P @ [p], (P, Frm)) pt')
2.100 - @ (get_allps [] (P @ [p+1]) tail))
2.101 - else (keep @ [(*'insert'ed by 'append_..'*)] @ tail,
2.102 - get_allps [] (P @ [p] @ [1]) bs')
2.103 - val _= writeln("###cut_bottom: cutlevup="^bool2str (cutlevup b));
2.104 - val (parent, cuts) =
2.105 + val (children, cuts') =
2.106 + if clevup
2.107 + then (keep, get_allps [] (P @ [p+1]) tail)
2.108 + else (keep @ [pt'] @ tail, [])
2.109 + val (pt'', cuts') =
2.110 if cutlevup b
2.111 then (Nd (del_res b, children),
2.112 - cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2.113 - else (Nd (b, children), cuts)
2.114 - in (parent, cuts:pos' list) end;
2.115 + cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
2.116 + else (Nd (b, children), cuts')
2.117 + val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
2.118 + ", Nd=.............................................")
2.119 + val _= show_pt pt''
2.120 + val _= writeln("#####cut_levup res="^
2.121 + term2str (fst (get_obj g_result pt'' [])))
2.122 + val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
2.123 + ", cuts="^pos's2str cuts)
2.124 + in if null P then (pt'', (cuts @ cuts'):pos' list)
2.125 + else let val (P, p) = split_last P
2.126 + in cut_levup (cuts @ cuts') clevup pt pt'' (P, p) (get_nd pt P)
2.127 + end
2.128 + end;
2.129 print_depth 3;
2.130 (**######################################################################**);
2.131 (* use"ME/ctreeNEW.sml";
2.132 use"ctreeNEW.sml";
2.133 *)
2.134 +print_depth 99;
2.135 fun cut_tree pt (pos,_) =
2.136 - let val (P, p) = split_last pos;
2.137 + let val _= writeln("### cut_tree pt 1")
2.138 + val (P, p) = split_last pos
2.139 + val _= writeln("### cut_tree pt 2")
2.140 val ((pt', cuts), clevup) = cut_bottom pt (P, p) (get_nd pt P)
2.141 -(* val ((pt', cuts), clevup) = if null P then ((pt', cuts),[]) else
2.142 - cut_levup clevup pt
2.143 -*)
2.144 - in (pt', cuts) end;
2.145 + (* pt' is the updated parent of the Nd to cappend_..*)
2.146 + in if null P then (pt', cuts)
2.147 + else let val _= writeln("### cut_tree pt 3")
2.148 + val (P, p) = split_last P
2.149 + val _= writeln("### cut_tree pt 4")
2.150 + in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
2.151 + end
2.152 + end;
2.153 +print_depth 3;
2.154
2.155 -print_depth 99;
2.156 -cut_tree;
2.157 -print_depth 3;
2.158
2.159
2.160 (*######## eval from here ##########################################**)
2.161 @@ -186,21 +183,23 @@
2.162 (*######## eval from here ##########################################**)
2.163
2.164 fun append_atomic p l f r f' s pt =
2.165 - let val _= writeln("###append_atomic: pos ="^pos2str p);
2.166 - val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.167 - then (*after Take*)
2.168 - ((fst (get_obj g_loc pt p), Some l),
2.169 - get_obj g_form pt p)
2.170 -(*040223 else ((Some l, None), f)*)
2.171 - else ((None, Some l), f)
2.172 - in insert (PrfObj {cell = [(*3.00. unused*)],
2.173 - form = f,
2.174 - tac = r,
2.175 - loc = iss,
2.176 - branch= NoBranch,
2.177 - result= f',
2.178 - ostate= s}) pt p end;
2.179 -
2.180 + let val _= writeln("##append_atomic: pos ="^pos2str p^
2.181 + ", Nd=.............................................")
2.182 + val _= show_pt pt
2.183 + val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
2.184 + then (*after Take*)
2.185 + ((fst (get_obj g_loc pt p), Some l),
2.186 + get_obj g_form pt p)
2.187 + (*040223 else ((Some l, None), f)*)
2.188 + else ((None, Some l), f)
2.189 + in insert (PrfObj {cell = [(*3.00. unused*)],
2.190 + form = f,
2.191 + tac = r,
2.192 + loc = iss,
2.193 + branch= NoBranch,
2.194 + result= f',
2.195 + ostate= s}) pt p end;
2.196 +
2.197 (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
2.198 detail - generate - cappend: inserted, not appended !!!
2.199
2.200 @@ -214,6 +213,12 @@
2.201 (writeln("###cappend_atomic: pos ="^pos2str p);
2.202 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
2.203 );
2.204 +fun cappend_atomic pt p loc f r f' s =
2.205 + let val _= writeln("#cappend_atomic: pos ="^pos2str p)
2.206 + val (pt',c) = cut_tree pt (p,Frm)
2.207 + val _= writeln("#cappend_atomic: after cut")
2.208 + val pt'' = append_atomic p loc f r f' s pt'
2.209 + in (pt'',c) end;
2.210
2.211 (* called by Take *)
2.212 fun append_form p l f pt =
3.1 --- a/src/sml/ROOT.ML Thu Mar 03 00:23:21 2005 +0100
3.2 +++ b/src/sml/ROOT.ML Thu Mar 03 17:54:09 2005 +0100
3.3 @@ -159,8 +159,8 @@
3.4
3.5 cd "systest";
3.6 (*+ check kbtest/diffapp.sml for additional items in met-model*)
3.7 - (**) use"ctree.sml";
3.8 - (**)
3.9 + (** use"ctree.sml";
3.10 + **)
3.11 use"calculate.sml";
3.12 use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *);
3.13 use"root-equ.sml";
4.1 --- a/src/sml/systest/ctree.sml Thu Mar 03 00:23:21 2005 +0100
4.2 +++ b/src/sml/systest/ctree.sml Thu Mar 03 17:54:09 2005 +0100
4.3 @@ -2,7 +2,6 @@
4.4 use"systest/ctree.sml";
4.5 use"ctree.sml";
4.6 *)
4.7 -print_depth 99; cuts; print_depth 3;
4.8
4.9 "-----------------------------------------------------------------";
4.10 "=====new ptree 1 miniscript with mini-subpbl ====================";
4.11 @@ -1018,6 +1017,17 @@
4.12 if cuts = cuts2 @ [([3, 2], Res)] then () else
4.13 raise error "ctree.sml diff.behav. get_allps new [3,2]";
4.14
4.15 +"---(5a) on S(606)..S(608)--------";
4.16 +"--- nd [3,2,1] with 0 children------------------------------";
4.17 +val cuts = get_allp [] ([3,2,1], ([],Frm)) (get_nd pt [3,2,1]);
4.18 +if cuts =
4.19 + [] then () else
4.20 +raise error "ctree.sml diff.behav. get_allp new [3,2,1]";
4.21 +
4.22 +val cuts2 = get_allps [] [3,2,1,1] (children (get_nd pt [3,2,1]));
4.23 +if cuts = cuts2 @ [] then () else
4.24 +raise error "ctree.sml diff.behav. get_allps new [3,2,1]";
4.25 +
4.26
4.27 (**#################################################################**)
4.28 "-------------- cut_tree new (from ptree above)-------------------";
4.29 @@ -1062,7 +1072,6 @@
4.30 (*([],Res) because cutlevup=false*)] then () else
4.31 raise error "ctree.sml: diff.behav. cut_tree ([2],Res)";
4.32
4.33 -
4.34 "---(4) on S(606)..S(608)--------";
4.35 val (pt', cuts) = cut_tree pt ([3],Pbl);
4.36 print_depth 99;
4.37 @@ -1076,15 +1085,24 @@
4.38 ([4], Res)] then () else
4.39 raise error "ctree.sml: diff.behav. cut_tree ([3],Pbl)";
4.40
4.41 +"---(5a) on S(606)..S(608) cut_tree --------";
4.42 +val (pt', cuts) = cut_tree pt ([3,2,1],Res);
4.43 +print_depth 99;
4.44 +cuts;
4.45 +print_depth 3;
4.46 +if cuts = [] then () else
4.47 +raise error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
4.48 +show_pt pt';
4.49 +(* @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
4.50 + use"systest/ctree.sml";
4.51 + use"ctree.sml";
4.52 + *)
4.53
4.54 (**#################################################################**)
4.55
4.56 "-------------- cappend on complete ctree from above -------------";
4.57 "-------------- cappend on complete ctree from above -------------";
4.58 "-------------- cappend on complete ctree from above -------------";
4.59 -(* use"systest/ctree.sml";
4.60 - use"ctree.sml";
4.61 - *)
4.62
4.63 "---(3) on S(606)..S(608)--------";
4.64 val (pt', cuts) = cappend_atomic pt [2] e_istate (str2term "Inform[2]")
4.65 @@ -1097,12 +1115,12 @@
4.66 ([3, 1], Frm),([3, 1], Res), ([3, 2, 1], Frm), ([3, 2, 1], Res),
4.67 ([3, 2, 2], Res), ([3, 2], Res), ([3], Res), ([4], Res)] then () else
4.68 raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] cuts";
4.69 -val insrted = get_allp [] ([], ([],Frm)) pt';
4.70 +val afterins = get_allp [] ([], ([],Frm)) pt';
4.71 print_depth 99;
4.72 -insrted;
4.73 +afterins;
4.74 print_depth 3;
4.75 -if insrted = [([1], Frm), ([1], Res), ([2], Res), ([], Res)] then () else
4.76 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] insrted";
4.77 +if afterins = [([1], Frm), ([1], Res), ([2], Res), ([], Res)] then () else
4.78 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[2] afterins";
4.79 show_pt pt';
4.80
4.81 "---(4) on S(606)..S(608)--------";
4.82 @@ -1117,16 +1135,91 @@
4.83 ([3, 2], Res),
4.84 ([3], Res), ([4], Res)] then () else
4.85 raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] cuts";
4.86 -val insrted = get_allp [] ([], ([],Frm)) pt';
4.87 +val afterins = get_allp [] ([], ([],Frm)) pt';
4.88 print_depth 99;
4.89 -insrted;
4.90 +afterins;
4.91 print_depth 3;
4.92 -if insrted =
4.93 +if afterins =
4.94 [([1], Frm), ([1], Res),([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
4.95 ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res), ([2], Res),
4.96 ([3], Pbl)] then () else
4.97 -raise error "ctree.sml: diff:behav. in ccomplete pt: append_problem[3] insrted";
4.98 +raise error "ctree.sml: diff:behav.in complete pt: append_problem[3] afterins";
4.99 +(* use"systest/ctree.sml";
4.100 + use"ctree.sml";
4.101 + *)
4.102 +
4.103 +"---(6-1) on S(606)..S(608)--------";
4.104 +val (pt', cuts) = cappend_atomic pt [3,1] e_istate (str2term "Inform[3,1]")
4.105 + (Tac "test") (str2term "Inres[3,1]",[]) Complete;
4.106 +print_depth 99;
4.107 +cuts;
4.108 +print_depth 3;
4.109 +if cuts = [([3, 2, 1], Frm), ([3, 2, 1], Res), ([3, 2, 2], Res),
4.110 + ([3, 2], Res)] then () else
4.111 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] cuts";
4.112 +val afterins = get_allp [] ([], ([],Frm)) pt';
4.113 +print_depth 99;
4.114 +afterins;
4.115 +print_depth 3;
4.116 +if afterins = [([1], Frm), ([1], Res),
4.117 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
4.118 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
4.119 + ([2], Res),
4.120 + ([3], Pbl),
4.121 + ([3, 1], Frm), ([3, 1], Res)(*replaced*), (*([3, 2], Res) cut!*)
4.122 + ([3], Res)(*cutlevup=false*),
4.123 + ([4], Res),
4.124 + ([], Res)(*cutlevup=false*)] then () else
4.125 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] insrtd";
4.126 +if term2str (get_obj g_form pt' [3,1]) = "Inform [3, 1]" then () else
4.127 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,1] Inform";
4.128 +
4.129 +"---(6) on S(606)..S(608)--------";
4.130 +val (pt', cuts) = cappend_atomic pt [3,2] e_istate (str2term "Inform[3,2]")
4.131 + (Tac "test") (str2term "Inres[3,2]",[]) Complete;
4.132 +print_depth 99;
4.133 +cuts;
4.134 +print_depth 3;
4.135 +if cuts = [(*just after is: cutlevup=false in [3]*)] then () else
4.136 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] cuts";
4.137 +val afterins = get_allp [] ([], ([],Frm)) pt';
4.138 +print_depth 99;
4.139 +afterins;
4.140 +print_depth 3;
4.141 +if afterins = [([1], Frm), ([1], Res),
4.142 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
4.143 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
4.144 + ([2], Res),
4.145 + ([3], Pbl),
4.146 + ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res)(*replaced*),
4.147 + ([3], Res),
4.148 + ([4], Res), ([], Res)] then () else
4.149 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
4.150 +if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2]" then () else
4.151 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] Inform";
4.152 +
4.153 +"---(6++) on S(606)..S(608)--------";
4.154 +(**)
4.155 +val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
4.156 + (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
4.157 +print_depth 99;
4.158 +append_atomic;
4.159 +cuts;
4.160 +print_depth 3;
4.161 +if cuts = [] then () else
4.162 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
4.163 +val afterins = get_allp [] ([], ([],Frm)) pt';
4.164 +print_depth 99;
4.165 +afterins;
4.166 +print_depth 3;
4.167 +if afterins = [] then () else
4.168 +raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
4.169 +if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2, 1]" then () else
4.170 +raise error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
4.171 +(**)
4.172 show_pt pt';
4.173 +show_pt pt;
4.174 +
4.175 (* use"../systest/ctree.sml";
4.176 use"systest/ctree.sml";
4.177 use"ctree.sml";