1.1 --- a/src/sml/ME/ctree.sml Sat Mar 05 17:26:21 2005 +0100
1.2 +++ b/src/sml/ME/ctree.sml Sat Mar 05 18:08:56 2005 +0100
1.3 @@ -3,7 +3,7 @@
1.4 use"ctree.sml";
1.5 W.N.26.10.99
1.6
1.7 -writeln (pr_ptree pr_short pt);
1.8 +writeln (pr_ptree pr_short pt);
1.9
1.10 val Nd ( _, ns) = pt;
1.11
1.12 @@ -1220,7 +1220,7 @@
1.13 fun update_oris pt pos x = appl_obj (repl_oris x) pt pos;
1.14 fun update_orispec pt pos x = appl_obj (repl_orispec x) pt pos;
1.15
1.16 - (*done by append_* !! 3.5.02*)
1.17 + (*done by append_* !! 3.5.02; ununsed WN050305 thus outcommented
1.18 fun update_loc pt (p,_) (ScrState ([],[],None,
1.19 Const ("empty",_),Sundef,false)) =
1.20 appl_obj (repl_loc (None,None)) pt p
1.21 @@ -1230,7 +1230,8 @@
1.22
1.23 | update_loc pt (p,_) x =
1.24 let val (_,lres) = get_obj g_loc pt p
1.25 - in appl_obj (repl_loc (Some x,lres)) pt p end;
1.26 + in appl_obj (repl_loc (Some x,lres)) pt p end;-------------*)
1.27 +
1.28 (*WN050305 for handling cut_tree in cappend_atomic -- TODO redesign !*)
1.29 fun update_loc' pt p iss = appl_obj (repl_loc iss) pt p;
1.30
1.31 @@ -1597,10 +1598,10 @@
1.32 fun get_allpos' (_:pos, _:posel) EmptyPtree = ([]:pos' list)
1.33 | get_allpos' (p, 1) (Nd (b, bs)) = (*p is pos of Nd*)
1.34 if g_ostate b = Incomplete
1.35 - then (writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);
1.36 + then ((*writeln("get_allpos' (p, 1) Incomplete: p="^ints2str' p);*)
1.37 [(p,Frm)] @ (get_allpos's (p, 1) bs)
1.38 )
1.39 - else (writeln("get_allpos' (p, 1) else: p="^ints2str' p);
1.40 + else ((*writeln("get_allpos' (p, 1) else: p="^ints2str' p);*)
1.41 [(p,Frm)] @ (get_allpos's (p, 1) bs) @ [(p,Res)]
1.42 )
1.43 (*WN041020 here we assume what is presented on the worksheet ?!*)
1.44 @@ -1691,7 +1692,7 @@
1.45 then [] else [([], Res)])) end;
1.46
1.47
1.48 -(*########/ inserted from ctreeNEW.sml \#################################(**)
1.49 +(*########/ inserted from ctreeNEW.sml \#################################**)
1.50
1.51 (*.get all positions in a ptree until ([],Res) or ostate=Incomplete
1.52 val get_allp = fn :
1.53 @@ -1840,10 +1841,10 @@
1.54 end
1.55 end;
1.56 print_depth 3;
1.57 -(**)########\ inserted from ctreeNEW.sml /#################################**)
1.58 +(*########\ inserted from ctreeNEW.sml /#################################**)
1.59
1.60 fun append_atomic p l f r f' s pt =
1.61 - let (**)val _= writeln("#@append_atomic: pos ="^pos2str p)(**)
1.62 + let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**)
1.63 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.64 then (*after Take*)
1.65 ((fst (get_obj g_loc pt p), Some l),
1.66 @@ -1868,31 +1869,10 @@
1.67 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1.68 (f',asm),Complete);
1.69 *)
1.70 -(writeln("##@cappend_atomic: pos ="^pos2str p);
1.71 +((*writeln("##@cappend_atomic: pos ="^pos2str p);*)
1.72 apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.73 );
1.74 -fun cappend_atomic pt p loc f r f' s =
1.75 -let val _= writeln("##@cappend_atomic: pos ="^pos2str p);
1.76 - val _= writeln("##@cappend_atomic arg loc ="^istate2str loc);
1.77 - val _= if existpt p pt
1.78 - then writeln("##@cappend_atomic before cut_ loc ="^
1.79 - istates2str (get_obj g_loc pt p))
1.80 - else writeln("##@cappend_atomic pos not existent before cut_");
1.81 - val (pt', cs) = cut_tree pt (p,Frm);
1.82 - val _= if existpt p pt'
1.83 - then writeln("##@cappend_atomic after cut_ loc ="^
1.84 - istates2str (get_obj g_loc pt' p))
1.85 - else writeln("##@cappend_atomic pos not existent after cut_");
1.86 - val pt'' = append_atomic p loc f r f' s pt';
1.87 - val _= writeln("##@cappend_atomic after append: loc ="^
1.88 - istates2str (get_obj g_loc pt'' p));
1.89 -in (pt'', cs) end;
1.90 -
1.91 -fun cappend_atomic pt p loc f r f' s =
1.92 -let val (pt', cs) = cut_tree pt (p,Frm)
1.93 - val pt'' = append_atomic p loc f r f' s pt'
1.94 -in (pt'', cs) end;
1.95 -
1.96 +(*TODO.WN050305 redesign the handling of istates*)
1.97 fun cappend_atomic pt p ist_res f r f' s =
1.98 if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.99 then (*after Take: transfer Frm and respective istate*)
1.100 @@ -1907,7 +1887,7 @@
1.101
1.102 (* called by Take *)
1.103 fun append_form p l f pt =
1.104 -(writeln("##@append_form: pos ="^pos2str p);
1.105 +((*writeln("##@append_form: pos ="^pos2str p);*)
1.106 insert (PrfObj {cell = [(*3.00. unused*)],
1.107 form = (*if existpt p pt
1.108 andalso get_obj g_tac pt p = Empty_Tac
1.109 @@ -1923,22 +1903,22 @@
1.110 val (p,loc,f) = (fst p, e_istate, str2term "-1 + x = 0");
1.111 *)
1.112 fun cappend_form pt p loc f =
1.113 -(writeln("##@cappend_form: pos ="^pos2str p);
1.114 +((*writeln("##@cappend_form: pos ="^pos2str p);*)
1.115 apfst (append_form p loc f) (cut_tree pt (p,Frm))
1.116 );
1.117 fun cappend_form pt p loc f =
1.118 -let val _= writeln("##@cappend_form: pos ="^pos2str p)
1.119 - val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)
1.120 +let (*val _= writeln("##@cappend_form: pos ="^pos2str p)
1.121 + val _= writeln("##@cappend_form before cut_tree: loc ="^istate2str loc)*)
1.122 val (pt', cs) = cut_tree pt (p,Frm)
1.123 val pt'' = append_form p loc f pt'
1.124 - val _= writeln("##@cappend_form after append: loc ="^
1.125 - istates2str (get_obj g_loc pt'' p))
1.126 + (*val _= writeln("##@cappend_form after append: loc ="^
1.127 + istates2str (get_obj g_loc pt'' p))*)
1.128 in (pt'', cs) end;
1.129
1.130
1.131
1.132 fun append_result pt p l f s =
1.133 -(writeln("##@append_result: pos ="^pos2str p);
1.134 +((*writeln("##@append_result: pos ="^pos2str p);*)
1.135 (appl_obj (repl_result (fst (get_obj g_loc pt p),
1.136 Some l) f s) pt p, [])
1.137 );
1.138 @@ -1946,7 +1926,7 @@
1.139
1.140 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1.141 fun append_parent p l f r b pt =
1.142 - let val _= writeln("###append_parent: pos ="^pos2str p);
1.143 + let (*val _= writeln("###append_parent: pos ="^pos2str p);*)
1.144 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.145 then ((fst (get_obj g_loc pt p), Some l),
1.146 get_obj g_form pt p)
1.147 @@ -1960,13 +1940,13 @@
1.148 result= (e_term,[]),
1.149 ostate= Incomplete}) pt p end;
1.150 fun cappend_parent pt p loc f r b =
1.151 -(writeln("###cappend_parent: pos ="^pos2str p);
1.152 +((*writeln("###cappend_parent: pos ="^pos2str p);*)
1.153 apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
1.154 );
1.155
1.156
1.157 fun append_problem [] l fmz (strs,spec,hdf) _ =
1.158 -(writeln("###append_problem: pos = []");
1.159 +((*writeln("###append_problem: pos = []");*)
1.160 (Nd (PblObj
1.161 {cell = [(*3.00. unused*)],
1.162 origin= (strs,spec,hdf),
1.163 @@ -1981,7 +1961,7 @@
1.164 ostate= Incomplete},[]))
1.165 )
1.166 | append_problem p l fmz (strs,spec,hdf) pt =
1.167 -(writeln("###append_problem: pos ="^pos2str p);
1.168 +((*writeln("###append_problem: pos ="^pos2str p);*)
1.169 insert (PblObj
1.170 {cell = [(*3.00. unused*)],
1.171 origin= (strs,spec,hdf),
1.172 @@ -1996,11 +1976,11 @@
1.173 ostate= Incomplete}) pt p
1.174 );
1.175 fun cappend_problem _ [] loc fmz ori =
1.176 -(writeln("###cappend_problem: pos = []");
1.177 +((*writeln("###cappend_problem: pos = []");*)
1.178 (append_problem [] loc fmz ori EmptyPtree,[])
1.179 )
1.180 | cappend_problem pt p loc fmz ori =
1.181 -(writeln("###cappend_problem: pos ="^pos2str p);
1.182 +((*writeln("###cappend_problem: pos ="^pos2str p);*)
1.183 apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
1.184 );
1.185