1.1 --- a/src/sml/ME/ctreeNEW.sml Thu Mar 03 17:54:09 2005 +0100
1.2 +++ b/src/sml/ME/ctreeNEW.sml Thu Mar 03 18:53:00 2005 +0100
1.3 @@ -104,13 +104,13 @@
1.4 then (Nd (del_res b, children),
1.5 cuts @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.6 else (Nd (b, children), cuts)
1.7 - val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
1.8 + (*val _= writeln("####cut_bottom (P, p)="^pos2str (P @ [p])^
1.9 ", Nd=.............................................")
1.10 val _= show_pt pt''
1.11 - val _= writeln("####cut_bottom res="^
1.12 - term2str (fst (get_obj g_result pt'' [])))
1.13 + val _= writeln("####cut_bottom form='"^
1.14 + term2str (get_obj g_form pt'' []))
1.15 val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
1.16 - ", cuts="^pos's2str cuts)
1.17 + ", cuts="^pos's2str cuts)*)
1.18 in ((pt'', cuts:pos' list), cutlevup b) end;
1.19 print_depth 3;
1.20 (**######################################################################**);
1.21 @@ -126,33 +126,36 @@
1.22 returns :
1.23 ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
1.24 .*)
1.25 -(*WN050225 neglects the recursive structure of the ptree*)
1.26 print_depth 99;
1.27 fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
1.28 let (*divide level into 3 parts...*)
1.29 val keep = take (p - 1, bs)
1.30 - (*val pt' comes as argument*)
1.31 + (*val pt' comes as argument from below*)
1.32 val (tail, tp) = (takerest (p, bs),
1.33 if null (takerest (p, bs)) then 0 else p + 1)
1.34 val (children, cuts') =
1.35 if clevup
1.36 - then (keep, get_allps [] (P @ [p+1]) tail)
1.37 + then (keep @ [pt'], get_allps [] (P @ [p+1]) tail)
1.38 else (keep @ [pt'] @ tail, [])
1.39 + val clevup' = if clevup then cutlevup b else false
1.40 + (*the first Nd with false stops cutting on all levels above*)
1.41 val (pt'', cuts') =
1.42 - if cutlevup b
1.43 + if clevup'
1.44 then (Nd (del_res b, children),
1.45 cuts' @ (if g_ostate b = Incomplete then [] else [(P,Res)]))
1.46 else (Nd (b, children), cuts')
1.47 + (*val _= writeln("#####cut_levup clevup= "^bool2str clevup)
1.48 + val _= writeln("#####cut_levup cutlevup b= "^bool2str (cutlevup b))
1.49 val _= writeln("#####cut_levup (P, p)="^pos2str (P @ [p])^
1.50 ", Nd=.............................................")
1.51 val _= show_pt pt''
1.52 - val _= writeln("#####cut_levup res="^
1.53 - term2str (fst (get_obj g_result pt'' [])))
1.54 + val _= writeln("#####cut_levup form='"^
1.55 + term2str (get_obj g_form pt'' []))
1.56 val _= writeln("#####cut_levup cuts#="^string_of_int (length cuts)^
1.57 - ", cuts="^pos's2str cuts)
1.58 + ", cuts="^pos's2str cuts)*)
1.59 in if null P then (pt'', (cuts @ cuts'):pos' list)
1.60 else let val (P, p) = split_last P
1.61 - in cut_levup (cuts @ cuts') clevup pt pt'' (P, p) (get_nd pt P)
1.62 + in cut_levup (cuts @ cuts') clevup' pt pt'' (P, p) (get_nd pt P)
1.63 end
1.64 end;
1.65 print_depth 3;
1.66 @@ -162,15 +165,11 @@
1.67 *)
1.68 print_depth 99;
1.69 fun cut_tree pt (pos,_) =
1.70 - let val _= writeln("### cut_tree pt 1")
1.71 - val (P, p) = split_last pos
1.72 - val _= writeln("### cut_tree pt 2")
1.73 + let val (P, p) = split_last pos
1.74 val ((pt', cuts), clevup) = cut_bottom pt (P, p) (get_nd pt P)
1.75 (* pt' is the updated parent of the Nd to cappend_..*)
1.76 in if null P then (pt', cuts)
1.77 - else let val _= writeln("### cut_tree pt 3")
1.78 - val (P, p) = split_last P
1.79 - val _= writeln("### cut_tree pt 4")
1.80 + else let val (P, p) = split_last P
1.81 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
1.82 end
1.83 end;
1.84 @@ -183,9 +182,9 @@
1.85 (*######## eval from here ##########################################**)
1.86
1.87 fun append_atomic p l f r f' s pt =
1.88 - let val _= writeln("##append_atomic: pos ="^pos2str p^
1.89 + let (*val _= writeln("##append_atomic: pos ="^pos2str p^
1.90 ", Nd=.............................................")
1.91 - val _= show_pt pt
1.92 + val _= show_pt pt*)
1.93 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.94 then (*after Take*)
1.95 ((fst (get_obj g_loc pt p), Some l),
1.96 @@ -206,23 +205,23 @@
1.97 cut decided in applicable_in !?!
1.98 *)
1.99 fun cappend_atomic pt p loc f r f' s =
1.100 -(* val (pt, p, loc, f, r, f', s) =
1.101 - (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1.102 - (f',asm),Complete);
1.103 - *)
1.104 -(writeln("###cappend_atomic: pos ="^pos2str p);
1.105 - apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.106 -);
1.107 -fun cappend_atomic pt p loc f r f' s =
1.108 let val _= writeln("#cappend_atomic: pos ="^pos2str p)
1.109 val (pt',c) = cut_tree pt (p,Frm)
1.110 val _= writeln("#cappend_atomic: after cut")
1.111 val pt'' = append_atomic p loc f r f' s pt'
1.112 in (pt'',c) end;
1.113 +fun cappend_atomic pt p loc f r f' s =
1.114 +(* val (pt, p, loc, f, r, f', s) =
1.115 + (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1.116 + (f',asm),Complete);
1.117 + *)
1.118 +((*writeln("###cappend_atomic: pos ="^pos2str p);*)
1.119 + apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.120 +);
1.121
1.122 (* called by Take *)
1.123 fun append_form p l f pt =
1.124 -(writeln("###append_form: pos ="^pos2str p);
1.125 +((*writeln("###append_form: pos ="^pos2str p);*)
1.126 insert (PrfObj {cell = [(*3.00. unused*)],
1.127 form = (*if existpt p pt
1.128 andalso get_obj g_tac pt p = Empty_Tac
1.129 @@ -238,14 +237,14 @@
1.130 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
1.131 *)
1.132 fun cappend_form pt p loc f =
1.133 -(writeln("###cappend_form: pos ="^pos2str p);
1.134 +((*writeln("###cappend_form: pos ="^pos2str p);*)
1.135 apfst (append_form p loc f) (cut_tree pt (p,Frm))
1.136 );
1.137
1.138
1.139
1.140 fun append_result pt p l f s =
1.141 -(writeln("###append_result: pos ="^pos2str p);
1.142 +((*writeln("###append_result: pos ="^pos2str p);*)
1.143 (appl_obj (repl_result (fst (get_obj g_loc pt p),
1.144 Some l) f s) pt p, [])
1.145 );
1.146 @@ -253,7 +252,7 @@
1.147
1.148 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1.149 fun append_parent p l f r b pt =
1.150 - let val _= writeln("###append_parent: pos ="^pos2str p);
1.151 + let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
1.152 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.153 then ((fst (get_obj g_loc pt p), Some l),
1.154 get_obj g_form pt p)
1.155 @@ -267,13 +266,13 @@
1.156 result= (e_term,[]),
1.157 ostate= Incomplete}) pt p end;
1.158 fun cappend_parent pt p loc f r b =
1.159 -(writeln("###cappend_parent: pos ="^pos2str p);
1.160 +((*writeln("###cappend_parent: pos ="^pos2str p);*)
1.161 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
1.162 );
1.163
1.164
1.165 fun append_problem [] l fmz (strs,spec,hdf) _ =
1.166 -(writeln("###append_problem: pos = []");
1.167 +((*writeln("###append_problem: pos = []");*)
1.168 (Nd (PblObj
1.169 {cell = [(*3.00. unused*)],
1.170 origin= (strs,spec,hdf),
1.171 @@ -288,7 +287,7 @@
1.172 ostate= Incomplete},[]))
1.173 )
1.174 | append_problem p l fmz (strs,spec,hdf) pt =
1.175 -(writeln("###append_problem: pos ="^pos2str p);
1.176 +((*writeln("###append_problem: pos ="^pos2str p);*)
1.177 insert (PblObj
1.178 {cell = [(*3.00. unused*)],
1.179 origin= (strs,spec,hdf),
1.180 @@ -303,16 +302,16 @@
1.181 ostate= Incomplete}) pt p
1.182 );
1.183 fun cappend_problem _ [] loc fmz ori =
1.184 -(writeln("###cappend_problem: pos = []");
1.185 +((*writeln("###cappend_problem: pos = []");*)
1.186 (append_problem [] loc fmz ori EmptyPtree,[])
1.187 )
1.188 | cappend_problem pt p loc fmz ori =
1.189 -(writeln("###cappend_problem: pos ="^pos2str p);
1.190 +((*writeln("###cappend_problem: pos ="^pos2str p);*)
1.191 apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
1.192 );
1.193
1.194
1.195 -(* use"ME/sequent.sml";
1.196 - use"sequent.sml";
1.197 +(* use"ME/ctreeNEW.sml";
1.198 + use"ctreeNEW.sml";
1.199 *)
1.200
2.1 --- a/src/sml/systest/ctree.sml Thu Mar 03 17:54:09 2005 +0100
2.2 +++ b/src/sml/systest/ctree.sml Thu Mar 03 18:53:00 2005 +0100
2.3 @@ -957,7 +957,8 @@
2.4 val cuts = get_allp [] ([], ([],Frm)) pt;
2.5 print_depth 3;
2.6 if cuts =
2.7 - [([1], Frm),
2.8 + [(*never returns the first pos'*)
2.9 + ([1], Frm),
2.10 ([1], Res),
2.11 ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res), ([2, 3], Res),
2.12 ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
2.13 @@ -1089,8 +1090,8 @@
2.14 val (pt', cuts) = cut_tree pt ([3,2,1],Res);
2.15 print_depth 99;
2.16 cuts;
2.17 -print_depth 3;
2.18 -if cuts = [] then () else
2.19 +print_depth 1;
2.20 +if cuts = [([3, 2, 2], Res), ([3, 2], Res)] then () else
2.21 raise error "ctree.sml: diff.behav. cut_tree ([3,2,1],Res)";
2.22 show_pt pt';
2.23 (* @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
2.24 @@ -1203,47 +1204,31 @@
2.25 val (pt', cuts) = cappend_atomic pt [3,2,1] e_istate (str2term "Inform[3,2,1]")
2.26 (Tac "test") (str2term "Inres[3,2,1]",[]) Complete;
2.27 print_depth 99;
2.28 -append_atomic;
2.29 cuts;
2.30 -print_depth 3;
2.31 -if cuts = [] then () else
2.32 +print_depth 1;
2.33 +if cuts = [([3, 2, 2], Res), ([3, 2], Res)] then () else
2.34 raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2,1] cuts";
2.35 val afterins = get_allp [] ([], ([],Frm)) pt';
2.36 print_depth 99;
2.37 afterins;
2.38 print_depth 3;
2.39 -if afterins = [] then () else
2.40 -raise error "ctree.sml: diff:behav. in complete pt: append_atomic[3,2] insrtd";
2.41 -if term2str (get_obj g_form pt' [3,2]) = "Inform [3, 2, 1]" then () else
2.42 +if afterins = [([1], Frm), ([1], Res),
2.43 + ([2, 1], Frm), ([2, 1], Res), ([2, 2], Res),
2.44 + ([2, 3], Res), ([2, 4], Res), ([2, 5], Res), ([2, 6], Res),
2.45 + ([2], Res),
2.46 + ([3], Pbl),
2.47 + ([3, 1], Frm), ([3, 1], Res),
2.48 + ([3, 2, 1], Frm), ([3, 2, 1], Res)] then () else
2.49 +raise error "ctree.sml: diff:behav. in complete pt: append_atom[3,2,1] insrtd";
2.50 +if term2str (get_obj g_form pt' [3,2,1]) = "Inform [3, 2, 1]" then () else
2.51 raise error "ctree.sml: diff:behav. complete pt: append_atomic[3,2,1] Inform";
2.52 -(**)
2.53 +(*
2.54 show_pt pt';
2.55 show_pt pt;
2.56 -
2.57 +*)
2.58 (* use"../systest/ctree.sml";
2.59 use"systest/ctree.sml";
2.60 use"ctree.sml";
2.61 *)
2.62
2.63
2.64 -
2.65 -
2.66 -(*
2.67 -val (res,asm) = get_obj g_result pt' [2];
2.68 -if res = e_term (*WN050219 done by cut_level*) then () else
2.69 -raise error "ctree.sml: diff:behav. in cut_tree 1aa";
2.70 -
2.71 -val form = get_obj g_form pt' [2];
2.72 -if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
2.73 -raise error "ctree.sml: diff:behav. in cut_tree 1ab";
2.74 -
2.75 -val (res,asm) = get_obj g_result pt' [];
2.76 -if res = e_term (*WN050219 done by cut_tree*) then () else
2.77 -raise error "ctree.sml: diff:behav. in cut_tree 1ac";
2.78 -
2.79 -if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
2.80 - [([], Frm),
2.81 - ([1], Frm),
2.82 - ([1], Res)] then () else
2.83 -raise error "ctree.sml: diff:behav. in cut_tree 1ad";
2.84 -*)
2.85 \ No newline at end of file