1.1 --- a/src/sml/ME/ctree.sml	Sat Feb 19 23:34:39 2005 +0100
     1.2 +++ b/src/sml/ME/ctree.sml	Sun Feb 20 13:55:25 2005 +0100
     1.3 @@ -171,11 +171,17 @@
     1.4  	   pos : lev_on, lev_dn, lev_up, 
     1.5                   lev_onFrm, lev_dnRes (..see solve Apply_Method !) 
     1.6             pos_:
     1.7 -# generate1 sets pos_ if possible
     1.8 +# generate1 sets pos_ if possible  ...?WN0502?NOT...
     1.9  # generate1 does NOT set pos, because certain nodes can be lev_on OR lev_dn
    1.10                       exceptions: Begin/End_Trans
    1.11 -# thus generate1 called in nxt_solv (tac_ -cases); general case: 
    1.12 +# thus generate(1) called in
    1.13 +.# assy, locate_gen 
    1.14 +.# nxt_solv (tac_ -cases); general case: 
    1.15    val pos' = case pos' of (p,Res) => (lev_on p',Res) | _ => pos'
    1.16 +# WN050220, S(604):
    1.17 +  generate1...(Rewrite(f,..,res))..(pos, pos_)
    1.18 +     cappend_atomic.................pos //////  gets f+res always!!!
    1.19 +        cut_tree....................pos, pos_ 
    1.20  *)
    1.21  fun pos'2str (p,p_) = pair2str (ints2str' p, pos_2str p_);
    1.22  fun pos's2str ps = (strs2str' o (map pos'2str)) ps;
    1.23 @@ -1249,8 +1255,10 @@
    1.24     pos      : build up pos during descent 
    1.25     ptree    : to be cut ..
    1.26     pos'     : ... below and after this
    1.27 +####################################################################
    1.28 +###### WN050220: complete redesign see S(603) ######################
    1.29 +####################################################################
    1.30  .*)
    1.31 -(*WN050219 ?redesign wrt cappend_*: regard only pos .v., _NOT_ pos' ????*)
    1.32  (*##GOON with this...##############################################(**)
    1.33  fun cut_level (_:pos' list) (_:pos) EmptyPtree (_:pos') =
    1.34      raise PTREE "cut_level EmptyPtree _"

     2.1 --- a/src/sml/ME/generate.sml	Sat Feb 19 23:34:39 2005 +0100
     2.2 +++ b/src/sml/ME/generate.sml	Sun Feb 20 13:55:25 2005 +0100
     2.3 @@ -240,10 +240,12 @@
     2.4      end
     2.5  
     2.6    | generate1 thy (Apply_Method' (_,topt, is)) _ (pos as (p,p_)) pt = 
     2.7 -    (case topt of 
     2.8 +    (writeln("###generate1 Apply_Method': pos= "^pos'2str (p,p_));
     2.9 +     case topt of 
    2.10  	 Some t => 
    2.11  	 let val (pt,_) = cappend_form pt p is t
    2.12 -	 in (pos,[], EmptyMout,pt) end
    2.13 +	 in (pos,[(*WN0502: pblnd generated without children*)], EmptyMout,pt)
    2.14 +	 end
    2.15         | None => 
    2.16  	 (pos,[],EmptyMout,update_env pt p (Some is)))
    2.17  
    2.18 @@ -276,7 +278,8 @@
    2.19        pt) end
    2.20  
    2.21    | generate1 thy (Rewrite_Inst' (_,_,_,_,subs',thm',f,(f',asm))) l (p,p_) pt =
    2.22 -  let val (pt,c) = cappend_atomic pt p l f
    2.23 +  let val _= writeln("###generate1 Rewrite_Inst': pos= "^pos'2str (p,p_));
    2.24 +      val (pt,c) = cappend_atomic pt p l f
    2.25        (Rewrite_Inst (subst2subs subs',thm')) (f',asm) Complete;
    2.26        val pt = update_branch pt p TransitiveB (*040312*)
    2.27      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
    2.28 @@ -284,7 +287,8 @@
    2.29        pt) end
    2.30  
    2.31    | generate1 thy (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))) l (p,p_) pt =
    2.32 -  let val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
    2.33 +  let val _= writeln("###generate1 Rewrite': pos= "^pos'2str (p,p_))
    2.34 +      val (pt,c) = cappend_atomic pt p l f (Rewrite thm') (f',asm) Complete
    2.35        val pt = update_branch pt p TransitiveB (*040312*)
    2.36      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm);9.6.03??*)
    2.37    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
    2.38 @@ -297,7 +301,8 @@
    2.39  (* val (thy, Rewrite_Set_Inst' (_,_,subs',rls',f,(f',asm)), l, (p,p_), pt) = 
    2.40         (assoc_thy "Isac.thy", tac_, is, pos, pt);
    2.41     *)
    2.42 -  let val (pt,c) = cappend_atomic pt p l f 
    2.43 +  let val _= writeln("###generate1 Rewrite_Set_Inst': pos= "^pos'2str (p,p_))
    2.44 +      val (pt,c) = cappend_atomic pt p l f 
    2.45        (Rewrite_Set_Inst (subst2subs subs',id_rls rls')) (f',asm) Complete
    2.46        val pt = update_branch pt p TransitiveB (*040312*)
    2.47      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
    2.48 @@ -314,7 +319,8 @@
    2.49    in (*implicit Take*) generate1 thy tac_ is pos' pt end
    2.50  
    2.51    | generate1 thy (Rewrite_Set' (_,_,rls',f,(f',asm))) l (p,p_) pt =
    2.52 -  let val (pt,c) = cappend_atomic pt p l f 
    2.53 +  let val _= writeln("###generate1 Rewrite_Set': pos= "^pos'2str (p,p_))
    2.54 +      val (pt,c) = cappend_atomic pt p l f 
    2.55        (Rewrite_Set (id_rls rls')) (f',asm) Complete
    2.56        val pt = update_branch pt p TransitiveB (*040312*)
    2.57      (*val pt = union_asm pt (par_pblobj pt p) (map (rpair p) asm');9.6.03??*)
    2.58 @@ -331,7 +337,8 @@
    2.59    in (*implicit Take*) generate1 thy tac_ is pos' pt end
    2.60  
    2.61    | generate1 thy (Check_Postcond' (pI,(scval,asm))) l (p,p_) pt =
    2.62 -    let (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
    2.63 +    let val _= writeln("###generate1 Check_Postcond': pos= "^pos'2str (p,p_))
    2.64 +       (*val (l',_) = get_obj g_loc pt p..don't overwrite with l from subpbl*)
    2.65  	val (pt,c) = append_result pt p l (scval,map str2term asm) Complete
    2.66      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), 
    2.67  				   Nundef, term2str scval)), pt) end
    2.68 @@ -342,7 +349,8 @@
    2.69        pt)end
    2.70  
    2.71    | generate1 thy (Check_elementwise' (consts,pred,(f',asm))) l (p,p_) pt =
    2.72 -    let val (pt,c) = cappend_atomic pt p l consts 
    2.73 +    let val _=writeln("###generate1 Check_elementwise': pos= "^pos'2str (p,p_))
    2.74 +	val (pt,c) = cappend_atomic pt p l consts 
    2.75  	(Check_elementwise pred) (f',asm) Complete;
    2.76    in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, term2str f')),
    2.77        pt)end
    2.78 @@ -360,7 +368,8 @@
    2.79  
    2.80    | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f)) 
    2.81  	      l (p,p_) pt =
    2.82 -    let val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
    2.83 +    let val _=writeln("###generate1 Subproblem': pos= "^pos'2str (p,p_))
    2.84 +	val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
    2.85  				     (oris, (domID, pblID, metID), hdl);
    2.86  	(*val pbl = init_pbl ((#ppc o get_pbt) pblID);
    2.87  	val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)

     3.1 --- a/src/sml/ROOT.ML	Sat Feb 19 23:34:39 2005 +0100
     3.2 +++ b/src/sml/ROOT.ML	Sun Feb 20 13:55:25 2005 +0100
     3.3 @@ -159,7 +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 + (**       use"ctree.sml"; 
     3.9 +     **)
    3.10         	use"calculate.sml"; 
    3.11          use"details.sml"; (*can notyet ackn. 'Rewrite_Set "cancel"' *);
    3.12         	use"root-equ.sml"; 

     4.1 --- a/src/sml/systest/ctree.sml	Sat Feb 19 23:34:39 2005 +0100
     4.2 +++ b/src/sml/systest/ctree.sml	Sun Feb 20 13:55:25 2005 +0100
     4.3 @@ -85,9 +85,10 @@
     4.4  
     4.5  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_form: pos =[3,1]*);
     4.6  val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,1]*);
     4.7 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
     4.8 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
     4.9 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    4.10 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[3,2]*);
    4.11 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[3]*);
    4.12 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*cappend_atomic: pos =[4]*);
    4.13 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt(*.append_result: pos =[]*);
    4.14  val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
    4.15  if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
    4.16  else raise error "new behaviour in test: miniscript with mini-subpbl";
    4.17 @@ -161,8 +162,11 @@
    4.18  "-------------- cut_level (from ptree above)----------------------";
    4.19  "-------------- cut_level (from ptree above)----------------------";
    4.20  "-------------- cut_level (from ptree above)----------------------";
    4.21 -val (pt',cuts) = cut_level [] [] pt ([2],Frm);
    4.22 -if cuts = [([2], Res),
    4.23 +show_pt pt;
    4.24 +show_pt pt';
    4.25 +print_depth 99; cuts; print_depth 3;
    4.26 +
    4.27 +(*if cuts = [([2], Res),
    4.28  	   ([3], Frm),
    4.29  	   ([3, 1], Frm),
    4.30  	   ([3, 1], Res),
    4.31 @@ -172,7 +176,9 @@
    4.32  then () else raise error "ctree.sml: diff:behav. in cut_level 1a";
    4.33  val (res,asm) = get_obj g_result pt' [2];
    4.34  if res = e_term andalso asm = [] then () else
    4.35 -raise error "ctree.sml: diff:behav. in cut_level 1aa" (*WN050219*);
    4.36 +raise error "ctree.sml: diff:behav. in cut_level 1aa" WN050219*);
    4.37 +if not (existpt [2] pt') then () else
    4.38 +raise error "ctree.sml: diff:behav. in cut_level 1aa2" (*WN050220*);
    4.39  
    4.40  val (res,asm) = get_obj g_result pt' [];
    4.41  if term2str res = "[x = 1]" (*WN050219 e_term in cut_tree!!!*) then () else
    4.42 @@ -471,6 +477,12 @@
    4.43  if not (existpt ((lev_on o fst) p) pt) then () else
    4.44  raise error "ctree.sml, diff.behav. cappend minisubpbl ([3,1],Res) nxt";
    4.45  
    4.46 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_form: pos =[3,1]*);
    4.47 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,1]*);
    4.48 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[3,2]*);
    4.49 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[3]*);
    4.50 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**)cappend_atomic: pos =[4]*);
    4.51 +(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt(**).append_result: pos =[]*);
    4.52  
    4.53  
    4.54  "=====new ptree 3 ================================================";