1.1 --- a/src/sml/FE-interface/interface.sml	Wed Aug 23 09:15:43 2006 +0200
     1.2 +++ b/src/sml/FE-interface/interface.sml	Wed Aug 23 19:19:42 2006 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4     val (cI, ip) = (1, ([], Res));
     1.5     val (cI, ip) = (1, ([2], Res));
     1.6     val (cI, ip) = (1, ([3,1], Res));
     1.7 -   val (cI, ip) = (1, ([1], Res));
     1.8 +   val (cI, ip) = (1, ([1,2,1], Res));
     1.9     *)
    1.10  fun interSteps cI ip =
    1.11      (let val ((pt,p), tacis) = get_calc cI

     2.1 --- a/src/sml/ME/ctree.sml	Wed Aug 23 09:15:43 2006 +0200
     2.2 +++ b/src/sml/ME/ctree.sml	Wed Aug 23 19:19:42 2006 +0200
     2.3 @@ -498,6 +498,10 @@
     2.4    | End_Proof'              => "End_Proof'"
     2.5    | _                       => "tac2str not impl. for ?!";
     2.6  
     2.7 +fun rls_of (Rewrite_Set_Inst (_, rls)) = rls
     2.8 +  | rls_of (Rewrite_Set rls) = rls
     2.9 +  | rls_of tac = raise error ("rls_of: called with tac '"^tac2IDstr tac^"'");
    2.10 +
    2.11  fun thm_of_rew (Rewrite_Inst (subs,(thmID,_))) = 
    2.12      (thmID, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst))
    2.13    | thm_of_rew (Rewrite  (thmID,_)) = (thmID, None)
    2.14 @@ -510,6 +514,10 @@
    2.15    | rls_of_rewset (Detail_Set_Inst (subs, rls)) = 
    2.16      (rls, Some ((subs2subst (assoc_thy "Isac.thy") subs):subst));
    2.17  
    2.18 +fun Thm2Rewrite (Thm (thmID,_)) = Rewrite_Set thmID
    2.19 +  | Thm2Rewrite rule = 
    2.20 +    raise error ("Thm2Rewrite: called with '" ^ rule2str rule ^ "'");
    2.21 +
    2.22  
    2.23  
    2.24  type fmz_ = cterm' list;
    2.25 @@ -1076,7 +1084,7 @@
    2.26    | ins_chn ns (Nd (b, bs)) (p::ps) =
    2.27       Nd (b, repl_app bs p (ins_chn ns (nth p bs) ps));
    2.28  
    2.29 -print_depth 11;ins_chn;print_depth 3 (*###insert#########################*);
    2.30 +(* print_depth 11;ins_chn;print_depth 3; ###insert#########################*);
    2.31  
    2.32  
    2.33  (** apply f to obj at pos, f: ppobj -> ppobj **)
    2.34 @@ -1934,7 +1942,6 @@
    2.35  	val _= writeln("####cut_bottom cuts#="^string_of_int (length cuts)^
    2.36  		       ", cuts="^pos's2str cuts)*)
    2.37      in ((pt'', cuts:pos' list), cutlevup b) end;
    2.38 -print_depth 3;
    2.39  
    2.40  
    2.41  (*.go all levels from the bottom of 'pos' up to the root, 
    2.42 @@ -1949,7 +1956,6 @@
    2.43  returns		     :
    2.44     ptree * pos' list : the updated parent-Nd and the pos's of the Nds cut
    2.45  .*)
    2.46 -print_depth 99;
    2.47  fun cut_levup (cuts:pos' list) clevup pt pt' (P:pos, p:posel) (Nd (b, bs)) =
    2.48      let (*divide level into 3 parts...*)
    2.49  	val keep = take (p - 1, bs)
    2.50 @@ -1995,8 +2001,6 @@
    2.51  		 in cut_levup cuts clevup pt pt' (P, p) (get_nd pt P)
    2.52  		 end
    2.53  	 end;
    2.54 -print_depth 3;
    2.55 -(*########\ inserted from ctreeNEW.sml /#################################**)
    2.56  
    2.57  fun append_atomic p l f r f' s pt = 
    2.58    let (**val _= writeln("#@append_atomic: pos ="^pos2str p)**)
    2.59 @@ -2004,7 +2008,6 @@
    2.60  		     then (*after Take*)
    2.61  			 ((fst (get_obj g_loc pt p), Some l), 
    2.62  			  get_obj g_form pt p) 
    2.63 -(*040223	     else ((Some l, None), f)*)
    2.64  		     else ((None, Some l), f)
    2.65    in insert (PrfObj {cell = None,
    2.66  		     form  = f,
    2.67 @@ -2014,6 +2017,7 @@
    2.68  		     result= f',
    2.69  		     ostate= s}) pt p end;
    2.70  
    2.71 +
    2.72  (*20.8.02: cappend_* FIXXXXME cut branches below cannot be decided here:
    2.73    detail - generate - cappend: inserted, not appended !!!
    2.74  

     3.1 --- a/src/sml/ME/solve.sml	Wed Aug 23 09:15:43 2006 +0200
     3.2 +++ b/src/sml/ME/solve.sml	Wed Aug 23 19:19:42 2006 +0200
     3.3 @@ -496,6 +496,14 @@
     3.4  				e_istate ptp;
     3.5      in complete_solve auto (c@c') ptp end;
     3.6  
     3.7 +(*.aux.fun for detailrls with Rrls, reverse rewriting.*)
     3.8 +(* val (nds, t, ((rule, (t', asm)) :: rts)) = ([], t, rul_terms);
     3.9 +   *)
    3.10 +fun rul_terms_2nds nds t [] = nds
    3.11 +  | rul_terms_2nds nds t ((rule, res as (t', _)) :: rts) =
    3.12 +    (append_atomic [] e_istate t (Thm2Rewrite rule) res Complete EmptyPtree) ::
    3.13 +    (rul_terms_2nds nds t' rts);
    3.14 +
    3.15  
    3.16  (*. detail steps done internally by Rewrite_Set* 
    3.17      into ctree by use of a script .*)
    3.18 @@ -503,19 +511,32 @@
    3.19     *)
    3.20  fun detailrls pt ((p,p_):pos') = 
    3.21      let val t = get_obj g_form pt p
    3.22 -	val is = init_istate (get_obj g_tac pt p) t
    3.23 +	val tac = get_obj g_tac pt p
    3.24 +	val rls = (assoc_rls o rls_of) tac
    3.25 +    in case rls of
    3.26 +(* val Rrls {scr = Rfuns {init_state,...},...} = rls;
    3.27 +   *)
    3.28 +	   Rrls {scr = Rfuns {init_state,...},...} => 
    3.29 +	   let val (_,_,_,rul_terms) = init_state t
    3.30 +	       val newnds = rul_terms_2nds [] t rul_terms
    3.31 +	       val pt''' = ins_chn newnds pt p 
    3.32 +	   in ("detailrls", pt''', (p @ [length newnds], Res):pos') end
    3.33 +	 | _ =>
    3.34 +	   let val is = init_istate tac t
    3.35  	(*TODO.WN060602 ScrState (["(t_, Problem (Isac,[equation,univar]))"]
    3.36  				      is wrong for simpl, but working ?!? *)
    3.37 -	val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), 
    3.38 -				  Some t, is)
    3.39 -	val pos' = ((lev_on o lev_dn) p, Frm)
    3.40 -	val thy = assoc_thy "Isac.thy"
    3.41 -	val (_,_,_,pt') = (*implicit Take*) generate1 thy tac_ is pos' pt;
    3.42 -	val (_, _, (pt'',_)) = complete_solve CompleteSubpbl [] (pt', pos');
    3.43 -        val newnds =children (get_nd pt'' p)
    3.44 -	val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
    3.45 -in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p) cn*),
    3.46 -    (p @ [length newnds], Res):pos') end;
    3.47 +	       val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), 
    3.48 +					 Some t, is)
    3.49 +	       val pos' = ((lev_on o lev_dn) p, Frm)
    3.50 +	       val thy = assoc_thy "Isac.thy"
    3.51 +	       val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
    3.52 +	       val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
    3.53 +	       val newnds = children (get_nd pt'' p)
    3.54 +	       val pt''' = ins_chn newnds pt p 
    3.55 +	   (*complete_solve cuts branches after*)
    3.56 +	   in ("detailrls", pt'''(*, get_formress [] ((lev_on o lev_dn) p)cn*),
    3.57 +	       (p @ [length newnds], Res):pos') end
    3.58 +    end;
    3.59  
    3.60  
    3.61  

     4.1 --- a/src/smltest/IsacKnowledge/rational.sml	Wed Aug 23 09:15:43 2006 +0200
     4.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Wed Aug 23 19:19:42 2006 +0200
     4.3 @@ -32,6 +32,7 @@
     4.4  "-------- double fractions ---------------------------------------";
     4.5  "-------- me Schalk I No.186 -------------------------------------";
     4.6  "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
     4.7 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
     4.8  "-----------------------------------------------------------------";
     4.9  "-----------------------------------------------------------------";
    4.10  "-----------------------------------------------------------------";
    4.11 @@ -893,7 +894,6 @@
    4.12  "-------- 'reverse-ruleset' cancel_p -----------------------------";
    4.13  "-------- 'reverse-ruleset' cancel_p -----------------------------";
    4.14  "-------- 'reverse-ruleset' cancel_p -----------------------------";
    4.15 -
    4.16  (*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
    4.17  
    4.18    (*the term for which reverse rewriting is demonstrated*)
    4.19 @@ -901,10 +901,14 @@
    4.20  	      "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
    4.21    val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
    4.22    		       next_rule=nex,normal_form=nor,...},...} = cancel_p;
    4.23 +
    4.24    (*normal_form produces the result in ONE step*)
    4.25 -  val Some (t',_) = nor t;
    4.26 -  term2str t';
    4.27 +  val Some (t',_) = nor t; term2str t';
    4.28 +
    4.29    (*initialize the interpreter state used by the 'me'*)
    4.30 +val Some (t', asm) = cancel_p_ thy t; term2str t'; terms2str asm;
    4.31 +
    4.32 +
    4.33  (* WN.14.3.03: rewrite__ Thm | Calc | missing: Rls_  FIXXXXME --------
    4.34    val (t,_,revsets,_) = ini t;
    4.35  ---------------------------------------------------------------------*)
    4.36 @@ -915,7 +919,12 @@
    4.37  		      "sym_real_mult_0",
    4.38  		      "sym_real_mult_1"]) rs;
    4.39  
    4.40 - 10.10.02: dieser Fall terminiert nicht (make_poly enth"alt zu viele rules)
    4.41 + 10.10.02: dieser Fall terminiert nicht 
    4.42 +           (make_polynomial enth"alt zu viele rules)
    4.43 +WN060823 'init_state' requires rewriting on specified location in the term
    4.44 +print_depth 99; Rfuns; print_depth 3;
    4.45 +
    4.46 +
    4.47    val Some r = nex revsets t;
    4.48    val (r,(t,asm))::_ = loc revsets t r;
    4.49    term2str t;
    4.50 @@ -2007,3 +2016,28 @@
    4.51  
    4.52  interSteps 1 ([1],Res);
    4.53  val ((pt,p),_) = get_calc 1; show_pt pt;
    4.54 +
    4.55 +
    4.56 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
    4.57 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
    4.58 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
    4.59 +states:=[];
    4.60 +CalcTree
    4.61 +[(["term ((14 * x * y) / ( x * y ))", "normalform N"], 
    4.62 +  ("Rational.thy",["rational","simplification"],
    4.63 +  ["simplification","of_rationals"]))];
    4.64 +Iterator 1;
    4.65 +moveActiveRoot 1;
    4.66 +autoCalculate 1 CompleteCalc;
    4.67 +val ((pt,p),_) = get_calc 1; show_pt pt;
    4.68 +
    4.69 +interSteps 1 ([1],Res);
    4.70 +val ((pt,p),_) = get_calc 1; show_pt pt;
    4.71 +
    4.72 +interSteps 1 ([1,2],Res);
    4.73 +val ((pt,p),_) = get_calc 1; show_pt pt;
    4.74 +
    4.75 +(*WN060823 cancel_p_ init_state does not terminate, see Rational.ML
    4.76 +interSteps 1 ([1,2,1],Res);
    4.77 +val ((pt,p),_) = get_calc 1; show_pt pt;
    4.78 +*)
    4.79 \ No newline at end of file