1.1 --- a/src/sml/ME/ctree.sml Fri Feb 18 17:56:07 2005 +0100
1.2 +++ b/src/sml/ME/ctree.sml Sat Feb 19 18:57:29 2005 +0100
1.3 @@ -152,6 +152,7 @@
1.4
1.5 type posel = int; (* roundabout for (some of) nice signatures *)
1.6 type pos = posel list;
1.7 +val pos2str = ints2str';
1.8 datatype pos_ =
1.9 Pbl (*PblObj-position: problem-type*)
1.10 | Met (*PblObj-position: method*)
1.11 @@ -1144,7 +1145,23 @@
1.12 PrfObj {cell=cell union cell',form=form,tac=tac,loc=loc,
1.13 branch=branch,result=result,ostate=ostate};
1.14
1.15 -
1.16 +(*WN050219 put here for interpreting code for cut_tree below...*)
1.17 +type ocalhd =
1.18 + bool * (*ALL itms+preconds true*)
1.19 + pos_ * (*model belongs to Problem | Method*)
1.20 + term * (*header: Problem... or Cas
1.21 + FIXXXME.12.03: item! for marking syntaxerrors*)
1.22 + itm list * (*model: given, find, relate*)
1.23 + ((bool * term) list) *(*model: preconds*)
1.24 + spec; (*specification*)
1.25 +val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1.26 +
1.27 +datatype ptform =
1.28 + Form of term
1.29 + | ModSpec of ocalhd;
1.30 +val e_ptform = Form e_term;
1.31 +val e_ptform' = ModSpec e_ocalhd;
1.32 +
1.33
1.34
1.35 (*.applies (snd f) to the branches at a pos if ((fst f) b),
1.36 @@ -1164,14 +1181,14 @@
1.37 fun test_trans (PrfObj{branch = Transitive,...}) = true
1.38 | test_trans (PblObj{branch = Transitive,...}) = true
1.39 | test_trans _ = false;
1.40 -(*
1.41 +(*before WN041019......
1.42 val cut_branch = (test_trans, curry take):
1.43 (ppobj -> bool) * (int -> ptree list -> ptree list);
1.44 .. formlery used for ...
1.45 -fun cut_tree _ [] = EmptyPtree
1.46 - | cut_tree pt pos =
1.47 +fun cut_tree''' _ [] = EmptyPtree
1.48 + | cut_tree''' pt pos =
1.49 let val (pt',cut) = appl_branch cut_branch pt pos
1.50 - in if cut andalso length pos > 1 then cut_tree pt' (lev_up pos)
1.51 + in if cut andalso length pos > 1 then cut_tree''' pt' (lev_up pos)
1.52 else pt' end;
1.53 *)
1.54 fun is_pblobj' pt (p:pos) =
1.55 @@ -1196,17 +1213,11 @@
1.56 let val (bs',cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
1.57 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.58
1.59 -(*.cuts the nodes at a pos' + below + after ON SAME LEVEL until 'test_trans'
1.60 - and returns the pos' cut, found by get_allpos's + possibly head;
1.61 - regards, if only Frm is present, but _NOT_ Res (*#*)
1.62 - pos' list: for collecting during descent into ptree
1.63 - pos : build up pos during descent
1.64 - ptree : to be cut ..
1.65 - pos' : ... below and after this
1.66 -.*)
1.67 +(*before WN050219*)
1.68 fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1.69 - raise PTREE "cut_level Empty _"
1.70 + raise PTREE "cut_level EmptyPtree _"
1.71 | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1.72 +
1.73 | cut_level cuts P (Nd (b, bs)) (p::[],p_) =
1.74 if test_trans b
1.75 then (Nd (b, take (p:posel, bs)),
1.76 @@ -1216,25 +1227,83 @@
1.77 (*WN041020 here we assume what is presented on the worksheet ?!*)
1.78 (get_allpos's (P, p+1) (takerest (p, bs))))
1.79 else (Nd (b, bs), cuts)
1.80 +
1.81 | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1.82 let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1.83 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.84 -(*#################################################################*)
1.85
1.86 fun delete_result pt (p:pos) =
1.87 (appl_obj (repl_result (fst (get_obj g_loc pt p), None)
1.88 (e_term,[]) Incomplete) pt p);
1.89
1.90 +
1.91 +
1.92 +(*.specialize 'take' for nodes of a ptree regarding Frm,Pbl,Met -- Res.*)
1.93 +(*WN050219 ?redesign with integrating the 'cuts' returned???*)
1.94 +fun take_nds (p:posel, bs: ptree list) Res = take (p, bs)
1.95 + | take_nds (1, b::_) p_ = [delete_result b []]
1.96 + | take_nds (p, bs: ptree list) p_ =
1.97 + (take (p-1, bs)) @ [delete_result (nth p bs) []];
1.98 +
1.99 +(*.cuts the nodes at a pos' + below + after ON SAME LEVEL until 'test_trans'
1.100 + and returns the pos' cut, found by get_allpos's + possibly head;
1.101 + regards, if only Frm is present, but _NOT_ Res (*#*)
1.102 + pos' list: for collecting during descent into ptree
1.103 + pos : build up pos during descent
1.104 + ptree : to be cut ..
1.105 + pos' : ... below and after this
1.106 +.*)
1.107 +(*WN050219 ?redesign wrt cappend_*: regard only pos .v., _NOT_ pos' ????*)
1.108 +(*#################################################################(**)
1.109 +fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
1.110 + raise PTREE "cut_level EmptyPtree _"
1.111 + | cut_level _ _ (Nd ( _, _)) ([],_) = raise PTREE "cut_level _ []"
1.112 +
1.113 + | cut_level cuts P (pt as Nd (b, bs)) (p::[],p_) =
1.114 + if test_trans b
1.115 + then (Nd (b, take_nds (p:posel, bs) p_),
1.116 + cuts @
1.117 + (if p_ = Frm andalso (*#*) g_ostate b = Complete
1.118 + then [(P@[p],Res)] else ([]:pos' list)) @
1.119 + (*WN041020 here we assume what is presented on the worksheet ?!*)
1.120 + (get_allpos's (P, p+1) (takerest (p, bs))))
1.121 + else (pt, cuts)
1.122 +
1.123 + | cut_level cuts P (Nd (b, bs)) ((p::ps),p_) =
1.124 + let val (bs',cuts') = cut_level cuts P (nth p bs) (ps, p_)
1.125 + in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
1.126 +(**)#################################################################*)
1.127 +
1.128 +(*before WN050219*)
1.129 +fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1.130 + | cut_tree pt (pos as ([p],_)) =
1.131 + let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1.132 + in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.133 + then [] else [([],Res)])) end
1.134 + | cut_tree pt (p,p_) =
1.135 + let
1.136 + fun cutfn pt cuts (p,p_) =
1.137 + let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1.138 + val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1.139 + then [] else [(lev_up p, Res)]
1.140 + in if length cuts' > 0 andalso length p > 1
1.141 + then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1.142 + else (pt',cuts @ cuts') end
1.143 + val (pt', cuts) = cutfn pt [] (p,p_)
1.144 + in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.145 + then [] else [([], Res)])) end;
1.146 (*.cuts the nodes at and after the given pos' until 'not test_trans'
1.147 returns the pos's cut .*)
1.148 -(*FIXXXME.WN0501 should change the ([*],Res) _below_ to Incomplete*)
1.149 +(*####################################################################(**)
1.150 fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1.151
1.152 | cut_tree (pt as Nd (b,_)) (pos as ([p],_)) =
1.153 let val (pt', cuts') = cut_level ([]:pos' list) [] pt pos
1.154 val (pt'', cuts'') =
1.155 if test_trans (get_obj I pt [])
1.156 - then (delete_result pt' [], cuts' @ [([],Res)])
1.157 + then (delete_result pt' [],
1.158 + cuts' @ (if get_obj g_ostate pt [] = Incomplete
1.159 + then [] else[([],Res)]))
1.160 else (pt', cuts')
1.161 in (pt'', cuts'') end
1.162
1.163 @@ -1255,33 +1324,17 @@
1.164
1.165 in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.166 then [] else [([], Res)])) end;
1.167 +(**)#################################################################*)
1.168 (*
1.169 val _= writeln("cut_tree: pos ="^pos'2str pos);
1.170 val _= writeln("cut_tree: branch="^branch2str (get_obj g_branch pt []));
1.171 val _= writeln("cut_tree: cuts' ="^pos's2str cuts');
1.172 val _= writeln("cut_tree: cuts''="^pos's2str cuts'');
1.173 *)
1.174 -fun cut_tree _ (([],_):pos') = raise PTREE "cut_tree _ ([],_)"
1.175 - | cut_tree pt (pos as ([p],_)) =
1.176 - let val (pt', cuts) = cut_level ([]:pos' list) [] pt pos
1.177 - in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.178 - then [] else [([],Res)])) end
1.179 - | cut_tree pt (p,p_) =
1.180 - let
1.181 - fun cutfn pt cuts (p,p_) =
1.182 - let val (pt', cuts') = cut_level [] (lev_up p) pt (p,p_)
1.183 - val cuts'' = if get_obj g_ostate pt (lev_up p) = Incomplete
1.184 - then [] else [(lev_up p, Res)]
1.185 - in if length cuts' > 0 andalso length p > 1
1.186 - then cutfn pt' (cuts @ cuts') (lev_up p, Frm(*-->(p,Res)*))
1.187 - else (pt',cuts @ cuts') end
1.188 - val (pt', cuts) = cutfn pt [] (p,p_)
1.189 - in (pt', cuts @ (if get_obj g_ostate pt [] = Incomplete
1.190 - then [] else [([], Res)])) end;
1.191
1.192
1.193 fun append_atomic p l f r f' s pt =
1.194 - let
1.195 + let val _= writeln("###append_atomic: pos ="^pos2str p);
1.196 val (iss, f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.197 then (*after Take*)
1.198 ((fst (get_obj g_loc pt p), Some l),
1.199 @@ -1306,10 +1359,13 @@
1.200 (pt,p,l,f,Rewrite_Set_Inst (subst2subs subs',id_rls rls'),
1.201 (f',asm),Complete);
1.202 *)
1.203 - apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm));
1.204 +(writeln("###cappend_atomic: pos ="^pos2str p);
1.205 + apfst (append_atomic p loc f r f' s) (cut_tree pt (p,Frm))
1.206 +);
1.207
1.208 (* called by Take *)
1.209 fun append_form p l f pt =
1.210 +(writeln("###append_form: pos ="^pos2str p);
1.211 insert (PrfObj {cell = [(*3.00. unused*)],
1.212 form = (*if existpt p pt
1.213 andalso get_obj g_tac pt p = Empty_Tac
1.214 @@ -1319,20 +1375,25 @@
1.215 loc = (Some l, None),
1.216 branch= NoBranch,
1.217 result= (e_term,[]),
1.218 - ostate= Incomplete}) pt p;
1.219 + ostate= Incomplete}) pt p
1.220 +);
1.221 fun cappend_form pt p loc f =
1.222 - apfst (append_form p loc f) (cut_tree pt (p,Frm));
1.223 +(writeln("###cappend_form: pos ="^pos2str p);
1.224 + apfst (append_form p loc f) (cut_tree pt (p,Frm))
1.225 +);
1.226
1.227
1.228
1.229 fun append_result pt p l f s =
1.230 +(writeln("###append_result: pos ="^pos2str p);
1.231 (appl_obj (repl_result (fst (get_obj g_loc pt p),
1.232 - Some l) f s) pt p, []);
1.233 + Some l) f s) pt p, [])
1.234 +);
1.235
1.236
1.237 (*WN041022 deprecated, still for kbtest/diffapp.sml, /systest/root-equ.sml*)
1.238 fun append_parent p l f r b pt =
1.239 - let
1.240 + let val _= writeln("###append_parent: pos ="^pos2str p);
1.241 val (ll,f) = if existpt p pt andalso get_obj g_tac pt p=Empty_Tac
1.242 then ((fst (get_obj g_loc pt p), Some l),
1.243 get_obj g_form pt p)
1.244 @@ -1346,10 +1407,13 @@
1.245 result= (e_term,[]),
1.246 ostate= Incomplete}) pt p end;
1.247 fun cappend_parent pt p loc f r b =
1.248 - apfst (append_parent p loc f r b) (cut_tree pt (p,Und));
1.249 +(writeln("###cappend_parent: pos ="^pos2str p);
1.250 + apfst (append_parent p loc f r b) (cut_tree pt (p,Und))
1.251 +);
1.252
1.253
1.254 fun append_problem [] l fmz (strs,spec,hdf) _ =
1.255 +(writeln("###append_problem: pos = []");
1.256 (Nd (PblObj
1.257 {cell = [(*3.00. unused*)],
1.258 origin= (strs,spec,hdf),
1.259 @@ -1362,7 +1426,9 @@
1.260 branch= TransitiveB,(*FIXXXXXME.27.8.03: for equations only*)
1.261 result= (e_term,[]),
1.262 ostate= Incomplete},[]))
1.263 +)
1.264 | append_problem p l fmz (strs,spec,hdf) pt =
1.265 +(writeln("###append_problem: pos ="^pos2str p);
1.266 insert (PblObj
1.267 {cell = [(*3.00. unused*)],
1.268 origin= (strs,spec,hdf),
1.269 @@ -1374,11 +1440,16 @@
1.270 loc = (Some l, None),
1.271 branch= TransitiveB,
1.272 result= (e_term,[]),
1.273 - ostate= Incomplete}) pt p;
1.274 + ostate= Incomplete}) pt p
1.275 +);
1.276 fun cappend_problem _ [] loc fmz ori =
1.277 +(writeln("###cappend_problem: pos = []");
1.278 (append_problem [] loc fmz ori EmptyPtree,[])
1.279 +)
1.280 | cappend_problem pt p loc fmz ori =
1.281 - apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm));
1.282 +(writeln("###cappend_problem: pos ="^pos2str p);
1.283 + apfst (append_problem p (loc:istate) fmz ori) (cut_tree pt (p,Frm))
1.284 +);
1.285
1.286
1.287 (* use"ME/sequent.sml";
1.288 @@ -1603,15 +1674,6 @@
1.289 in (domID, pblID, metID):spec end;
1.290
1.291 (*extract a formula or model from ptree for itms2itemppc or model2xml*)
1.292 -type ocalhd =
1.293 - bool * (*ALL itms+preconds true*)
1.294 - pos_ * (*model belongs to Problem | Method*)
1.295 - term * (*header: Problem... or Cas
1.296 - FIXXXME.12.03: item! for marking syntaxerrors*)
1.297 - itm list * (*model: given, find, relate*)
1.298 - ((bool * term) list) *(*model: preconds*)
1.299 - spec; (*specification*)
1.300 -val e_ocalhd = (false, Und, e_term, [e_itm], [(false, e_term)], e_spec);
1.301 fun preconds2str bts =
1.302 (strs2str o (map (linefeed o pair2str o
1.303 (apsnd term2str) o
1.304 @@ -1621,12 +1683,6 @@
1.305 ", "^itms2str (assoc_thy "Isac.thy") itms^
1.306 ", "^preconds2str prec^", \n"^spec2str spec^" )";
1.307
1.308 -datatype ptform =
1.309 - Form of term
1.310 - | ModSpec of ocalhd;
1.311 -val e_ptform = Form e_term;
1.312 -val e_ptform' = ModSpec e_ocalhd;
1.313 -
1.314
1.315
1.316 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj;
1.317 @@ -1791,7 +1847,7 @@
1.318 if is_pblobj (get_obj I pt p)
1.319 then (p, Pbl) else (par_pblobj pt p, Pbl);
1.320
1.321 -(*WN0502 made for interSteps; _only_ regards branch TransitiveB*)
1.322 +(*WN0502 made for interSteps; _only_ works for branch TransitiveB*)
1.323 fun lev_pred' pt (pos:pos' as (p,Res)) =
1.324 if (is_pblobj o (get_obj I pt)) p then (p,Pbl):pos' else move_up [] pt pos
1.325 | lev_pred' pt p = move_up [] pt p;
2.1 --- a/src/sml/ME/modspec.sml Fri Feb 18 17:56:07 2005 +0100
2.2 +++ b/src/sml/ME/modspec.sml Sat Feb 19 18:57:29 2005 +0100
2.3 @@ -1823,7 +1823,9 @@
2.4 (* continue with trying 'res' only*)
2.5 else get_forms (fs @ [form p nd]) (lev_on p) nds;
2.6
2.7 -(**.get an 'interval' of formulae from a ptree.**)
2.8 +(**.get an 'interval' 'from' 'to' of formulae from a ptree.**)
2.9 +(*WN050219 made robust against _'to' below or after Complete nodes
2.10 + by handling exn caused by move_dn*)
2.11 (*WN0401 this functionality belongs to ctree.sml,
2.12 but fetching a calc_head requires calculations defined in modspec.sml
2.13 transfer to ME/me.sml !!!*)
2.14 @@ -1838,6 +1840,7 @@
2.15 | Met => true
2.16 | _ => false)
2.17 | eq_pos' _ _ = false;
2.18 +(*before WN050219*)
2.19 fun get_interval (from:pos') (to:pos') level pt =
2.20 (* val (from,level) = (f,lev);
2.21 *)
2.22 @@ -1858,6 +1861,28 @@
2.23 in get_inter (c @ [(from, f)])
2.24 (move_dn [] pt from) to lev pt end
2.25 in get_inter [] from to level pt end;
2.26 +fun get_interval (from:pos') (to:pos') level pt =
2.27 +(* val (from,level) = (f,lev);
2.28 + *)
2.29 + let fun get_inter c (from:pos') (to:pos') lev pt =
2.30 +(* val (c,lev) = ([],max (level, max(lev_of from, lev_of to)));
2.31 + val (c,from) = ((c:(pos' * ptform) list) @ [(from, f)], move_dn [] pt from);
2.32 + *)
2.33 + if eq_pos' from to orelse from = ([],Res)
2.34 + (*orelse ... avoids Exception- PTREE "end of calculation" raised,
2.35 + if 'to' has values NOT generated by move_dn, see systest/me.sml
2.36 + TODO.WN0501: introduce an order on pos' and check from > to*)
2.37 + then let val (f,_,_) = pt_extract (pt, from)
2.38 + in c @ [(from, f)] end
2.39 + else
2.40 + if lev < lev_of from
2.41 + then (get_inter c (move_dn [] pt from) to lev pt)
2.42 + handle (PTREE _(*from move_dn too far*)) => c
2.43 + else let val (f,_,_) = pt_extract (pt, from)
2.44 + in (get_inter (c @ [(from, f)])
2.45 + (move_dn [] pt from) to lev pt)
2.46 + handle (PTREE _(*from move_dn too far*)) => c end
2.47 + in get_inter [] from to level pt end;
2.48
2.49
2.50 (*for tests*)
3.1 --- a/src/sml/ROOT.ML Fri Feb 18 17:56:07 2005 +0100
3.2 +++ b/src/sml/ROOT.ML Sat Feb 19 18:57:29 2005 +0100
3.3 @@ -158,8 +158,54 @@
3.4 "******* build ME & DG complete, knowledge + XML added *******";
3.5 *)
3.6
3.7 -(*=======================================================================(**)
3.8 +(*=======================================================================**)
3.9
3.10 + cd "systest";
3.11 + (*+ check kbtest/diffapp.sml for additional items in met-model*)
3.12 + (* use"ctree.sml";*)
3.13 + use"calculate.sml";
3.14 + use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *);
3.15 + use"root-equ.sml";
3.16 + use"modspec.sml";
3.17 + use"script.sml";
3.18 + (* use"script_if.sml"; missing: is_rootequation_in*)
3.19 + use"scriptnew.sml";
3.20 + use"refine.sml";
3.21 + use"subp-rooteq.sml";
3.22 + use"list_rls.sml";
3.23 + use"auto-inform.sml";
3.24 + use"tacis.sml";
3.25 + use"me.sml";
3.26 + use"interface-xml.sml";
3.27 + use"FE-interface.sml";
3.28 + (**)
3.29 + (*use"testdaten.sml"; no update after dropping 'errorBound'*)
3.30 + "******* systests complete *******";
3.31 + cd "../";
3.32 +
3.33 +
3.34 +(*----------list_rls.sml---##########FIXXXME.040311.doesnt work at other pos
3.35 + cd "systest";
3.36 + (*+ check kbtest/diffapp.sml for additional items in met-model*)
3.37 + use"FE-interface.sml";
3.38 + use"auto-inform.sml";
3.39 + use"calculate.sml";
3.40 +val me = meOLD;
3.41 + use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *)
3.42 +val me = meNEW; (*see FIXXXXXME.040216*)
3.43 + use"list_rls.sml"; ##########FIXXXME.040311.doesnt work at other pos
3.44 + use"ptree.sml";
3.45 + use"refine.sml";
3.46 + use"root-equ.sml";
3.47 + use"script.sml";
3.48 + (* use"script_if.sml"; missing: is_rootequation_in*)
3.49 + use"scriptnew.sml";
3.50 + use"subp-rooteq.sml";
3.51 + (*use"testdaten.sml"; no update after dropping 'errorBound'*)
3.52 + "******* systests complete *******";
3.53 + cd "../";
3.54 +----------------------------------------------------------------------*)
3.55 +
3.56 cd"kbtest";
3.57 use"complex.sml";
3.58 use"diff.sml";
3.59 @@ -185,51 +231,6 @@
3.60 "******* kbtests complete *******";
3.61 cd "../";
3.62
3.63 - cd "systest";
3.64 - (*+ check kbtest/diffapp.sml for additional items in met-model*)
3.65 - use"ctree.sml";
3.66 - use"calculate.sml";
3.67 - use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *);
3.68 - use"root-equ.sml";
3.69 - use"modspec.sml";
3.70 - use"script.sml";
3.71 - (* use"script_if.sml"; missing: is_rootequation_in*)
3.72 - use"scriptnew.sml";
3.73 - use"refine.sml";
3.74 - use"subp-rooteq.sml";
3.75 - use"list_rls.sml";
3.76 - use"auto-inform.sml";
3.77 - use"tacis.sml";
3.78 - use"me.sml";
3.79 - use"interface-xml.sml";
3.80 - use"FE-interface.sml";
3.81 - (**)
3.82 - (*use"testdaten.sml"; no update after dropping 'errorBound'*)
3.83 - "******* systests complete *******";
3.84 - cd "../";
3.85 -
3.86 -
3.87 -(*----------list_rls.sml---##########FIXXXME.040311.doesnt work at other pos
3.88 - cd "systest";
3.89 - (*+ check kbtest/diffapp.sml for additional items in met-model*)
3.90 - use"FE-interface.sml";
3.91 - use"auto-inform.sml";
3.92 - use"calculate.sml";
3.93 -val me = meOLD;
3.94 - use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *)
3.95 -val me = meNEW; (*see FIXXXXXME.040216*)
3.96 - use"list_rls.sml"; ##########FIXXXME.040311.doesnt work at other pos
3.97 - use"ptree.sml";
3.98 - use"refine.sml";
3.99 - use"root-equ.sml";
3.100 - use"script.sml";
3.101 - (* use"script_if.sml"; missing: is_rootequation_in*)
3.102 - use"scriptnew.sml";
3.103 - use"subp-rooteq.sml";
3.104 - (*use"testdaten.sml"; no update after dropping 'errorBound'*)
3.105 - "******* systests complete *******";
3.106 - cd "../";
3.107 -----------------------------------------------------------------------*)
3.108 (*
3.109 print_depth 3;
3.110 Compiler.Control.Print.printDepth:=15; (*4 default*)
3.111 @@ -238,6 +239,6 @@
3.112 Compiler.Control.Print.printDepth:=4; (*4 default*)
3.113
3.114 *)
3.115 -(**)=======================================================================*)
3.116 +(**=======================================================================*)
3.117
3.118 states:=[];
4.1 --- a/src/sml/systest/FE-interface.sml Fri Feb 18 17:56:07 2005 +0100
4.2 +++ b/src/sml/systest/FE-interface.sml Sat Feb 19 18:57:29 2005 +0100
4.3 @@ -1071,7 +1071,7 @@
4.4 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
4.5 raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2";
4.6
4.7 -(*WN050211 replaceFormula didn't work on second ctree*)
4.8 +(*WN050211 replaceFormula didn't work on second ctree: thus now tested...*)
4.9 CalcTree
4.10 [(["equality (x+1=2)", "solveFor x","solutions L"],
4.11 ("Test.thy",
4.12 @@ -1081,7 +1081,6 @@
4.13 moveActiveRoot 2;
4.14 autoCalculate 2 CompleteCalc;
4.15 moveActiveFormula 2 ([2],Res);
4.16 -(*-------------------------------- should work !!!! as above
4.17 replaceFormula 2 "-1 + x = 0" (*i.e. repeats input*);
4.18 (*... returns <ERROR> formula not changed </ERROR>*)
4.19
4.20 @@ -1094,7 +1093,6 @@
4.21 [([2], Res), ([3], Pbl), ([3, 1], Frm), ([3, 1], Res), ([3, 2], Res),
4.22 ([3], Res), ([4], Res), ([], Res)] then () (*nothing deleted!*) else
4.23 raise error "FE-interface.sml: diff.behav. in FORMULA:replace} right 2b";
4.24 -------------------------------------------------------------------------*)
4.25
4.26 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
4.27 "--------- replaceFormula {SOLVE:MANUAL:FORMULA:replace} other----";
4.28 @@ -1115,6 +1113,7 @@
4.29 getElementsFromTo 1 unc gen 99999 (*all levels*) false;
4.30
4.31 val ((pt,_),_) = get_calc 1;
4.32 + show_pt pt;
4.33 val p = get_pos 1 1;
4.34 val (Form f, tac, asms) = pt_extract (pt, p);
4.35 if term2str f = "x - 1 = 0" andalso p = ([2], Res) then () else
5.1 --- a/src/sml/systest/ctree.sml Fri Feb 18 17:56:07 2005 +0100
5.2 +++ b/src/sml/systest/ctree.sml Sat Feb 19 18:57:29 2005 +0100
5.3 @@ -22,6 +22,7 @@
5.4 "-------------- move_dn in Incomplete ctree ----------------------";
5.5
5.6 "=====new ptree 4: crooked by cut_level_'_ =======================";
5.7 +(*############## development stopped 0501 ########################*)
5.8 (******************************************************************)
5.9 (* val SAVE_get_trace = get_trace; *)
5.10 (******************************************************************)
5.11 @@ -29,6 +30,7 @@
5.12 (******************************************************************)
5.13 (* val get_trace = SAVE_get_trace; *)
5.14 (******************************************************************)
5.15 +(*############## development stopped 0501 ########################*)
5.16
5.17 "=====new ptree 4 ratequation ====================================";
5.18 "-------------- pt_extract form, tac, asm<>[] --------------------";
5.19 @@ -150,13 +152,20 @@
5.20 ([3], Res),
5.21 ([4], Res)]
5.22 then () else raise error "ctree.sml: diff:behav. in cut_level 1a";
5.23 +val (res,asm) = get_obj g_result pt' [2];
5.24 +if res = e_term andalso asm = [] then () else
5.25 +raise error "ctree.sml: diff:behav. in cut_level 1aa" (*WN050219*);
5.26 +
5.27 +val (res,asm) = get_obj g_result pt' [];
5.28 +if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
5.29 +raise error "ctree.sml: diff:behav. in cut_level 1ab";
5.30 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
5.31 [([], Frm),
5.32 ([1], Frm),
5.33 ([1], Res),
5.34 - ([2], Res),(*, change Res on higher levels to InComplete, delete result*)
5.35 + ([2], Res),(*, e_term in cut_tree!!!*)
5.36 ([], Res)] then () else
5.37 -raise error "ctree.sml: diff:behav. in cut_level 1b";;
5.38 +raise error "ctree.sml: diff:behav. in cut_level 1b";
5.39
5.40
5.41 val (pt',cuts) = cut_level [] [] pt ([2],Res);
5.42 @@ -167,6 +176,7 @@
5.43 ([3], Res),
5.44 ([4], Res)]
5.45 then () else raise error "ctree.sml: diff:behav. in cut_level 2a";
5.46 +
5.47 if pr_ptree pr_short pt' = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n"
5.48 then () else raise error "ctree.sml: diff:behav. in cut_level 2b";
5.49
5.50 @@ -186,7 +196,7 @@
5.51 "-------------- cut_tree (from ptree above)-----------------------";
5.52 "-------------- cut_tree (from ptree above)-----------------------";
5.53 "-------------- cut_tree (from ptree above)-----------------------";
5.54 -val (pt', cuts) = cut_tree pt ([2],Frm);
5.55 +val (pt', cuts) = cut_tree pt ([2],Frm);(*not created by move_dn -- not on WS*)
5.56 if cuts = [([2], Res),
5.57 ([3], Frm),
5.58 ([3, 1], Frm),
5.59 @@ -197,18 +207,23 @@
5.60 ([], Res)]
5.61 then () else raise error "ctree.sml: diff:behav. in cut_tree 1a";
5.62
5.63 -print_depth 99;cuts;print_depth 3;
5.64 -print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
5.65 +val (res,asm) = get_obj g_result pt' [2];
5.66 +if res = e_term (*WN050219 done by cut_level*) then () else
5.67 +raise error "ctree.sml: diff:behav. in cut_tree 1aa";
5.68
5.69 -(*
5.70 +val form = get_obj g_form pt' [2];
5.71 +if term2str form = "x + 1 + -1 * 2 = 0" (*remained !!!*) then () else
5.72 +raise error "ctree.sml: diff:behav. in cut_tree 1ab";
5.73 +
5.74 +val (res,asm) = get_obj g_result pt' [];
5.75 +if res = e_term (*WN050219 done by cut_tree*) then () else
5.76 +raise error "ctree.sml: diff:behav. in cut_tree 1ac";
5.77 +
5.78 if map fst (get_interval ([],Frm) ([],Res) 9999 pt') =
5.79 [([], Frm),
5.80 ([1], Frm),
5.81 - ([1], Res),
5.82 - ([2], Res)(*, change Res on higher levels to InComplete, delete result
5.83 - ([], Res)*)] then () else
5.84 -raise error "ctree.sml: diff:behav. in cut_tree 1aa";
5.85 -*)
5.86 + ([1], Res)] then () else
5.87 +raise error "ctree.sml: diff:behav. in cut_tree 1ad";
5.88
5.89 val (pt', cuts) = cut_tree pt ([2],Res);
5.90 if cuts = [([3], Frm),
5.91 @@ -253,15 +268,30 @@
5.92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.95 +show_pt pt;
5.96
5.97 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
5.98 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
5.99 "-------------- cut_level ( ,Frm) on Incomplete Nd ---------------";
5.100 -(*([1],Frm) is stored, ([1],Res) is not yet stored (Nd.ostate=Incomplete):...*)
5.101 +
5.102 +val (pt',cuts) = cut_level [] [3] pt ([1],Frm);(*([1],Frm) is stored*)
5.103 +if cuts = [](*([1],Res) is not yet stored (Nd.ostate=Incomplete)*)
5.104 +then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
5.105 +
5.106 val (pt', cuts) = cut_tree pt ([1],Frm);
5.107 if cuts = []
5.108 then () else raise error "ctree.sml: diff:behav. in cut_tree 4a";
5.109
5.110 +(*WN050219
5.111 +val pos as ([p],_) = ([1],Frm);
5.112 +val pt as Nd (b,_) = pt;
5.113 +
5.114 +
5.115 +show_pt pt;
5.116 +show_pt pt';
5.117 +print_depth 99;cuts;print_depth 3;
5.118 +print_depth 99;map fst (get_interval ([],Frm) ([],Res) 9999 pt');print_depth 3;
5.119 +####################################################################*)
5.120
5.121 "=====new ptree 2 miniscript with mini-subpbl ====================";
5.122 "=====new ptree 2 miniscript with mini-subpbl ====================";
5.123 @@ -274,29 +304,16 @@
5.124 ["Test","squ-equ-test-subpbl1"]))];
5.125 Iterator 1; moveActiveRoot 1;
5.126 autoCalculate 1 CompleteCalc;
5.127 - moveActiveRoot 1;
5.128 - moveActiveDown 1;
5.129 - moveActiveDown 1;
5.130 - moveActiveDown 1;
5.131 - moveActiveDown 1;
5.132 - moveActiveDown 1;
5.133 - moveActiveDown 1;
5.134 - moveActiveDown 1;
5.135 - val pp = get_pos 1 1;(*([3, 1], Frm)*)
5.136
5.137 interSteps 1 ([3,2],Res);
5.138
5.139 val ((pt,_),_) = get_calc 1;
5.140 - writeln(pr_ptree pr_short pt);
5.141 -
5.142 + show_pt pt;
5.143
5.144 "-------------- cut_tree (from 3rd level)-------------------------";
5.145 "-------------- cut_tree (from 3rd level)-------------------------";
5.146 "-------------- cut_tree (from 3rd level)-------------------------";
5.147
5.148 - val ((pt,_),_) = get_calc 1;
5.149 - writeln( pr_ptree pr_short pt);
5.150 -
5.151 val (pt', cuts) = cut_tree pt ([3,2,1],Frm);
5.152 if cuts = [([3, 2, 1], Res),
5.153 ([3, 2, 2], Res),
5.154 @@ -339,7 +356,7 @@
5.155 ([3], Res),
5.156 ([4], Res),
5.157 ([], Res)]
5.158 -then () else raise error "ctree.sml: diff:behav. in cappend_form";
5.159 +then () else raise error "ctree.sml: diff:behav. in cappend_atomic";
5.160
5.161
5.162