1.1 --- a/src/sml/ME/rewtools.sml	Fri Aug 25 16:46:20 2006 +0200
     1.2 +++ b/src/sml/ME/rewtools.sml	Tue Aug 29 10:07:24 2006 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (* tools for rewriting, reverse rewriting, context to thy concerning rewriting
     1.5 -   authors: Walther Neuper 2000, 2006
     1.6 +   authors: Walther Neuper 2002, 2006
     1.7    (c) due to copyright terms
     1.8  
     1.9  use"ME/rewtools.sml";
    1.10 @@ -10,11 +10,13 @@
    1.11  
    1.12  (***.reverse rewriting.***)
    1.13  
    1.14 -(*WN.12.8.02*)
    1.15 +(*.derivation for insertin one level of nodes into the calctree.*)
    1.16 +type deriv  = (term * rule * (term *term list)) list;
    1.17  
    1.18  fun trta2str (t,r,(t',a)) = "\n("^(term2str t)^", "^(rule2str r)^", ("^
    1.19  			    (term2str t')^", "^(terms2str a)^"))";
    1.20  fun trtas2str trtas = (strs2str o (map trta2str)) trtas;
    1.21 +val deriv2str = trtas2str;
    1.22  fun rta2str (r,(t,a)) = "\n("^(rule2str r)^", ("^
    1.23  			    (term2str t)^", "^(terms2str a)^"))";
    1.24  fun rtas2str rtas = (strs2str o (map rta2str)) rtas;
    1.25 @@ -131,6 +133,60 @@
    1.26  		     rew_once (rts @ [(t,r,(t',a'))]) t' Appl rrs');
    1.27  
    1.28      in rew_once [] tt Noap rs end;
    1.29 +fun make_deriv thy erls (rs:rule list) ro(*rew_ord*) goal tt = 
    1.30 +    let datatype switch = Appl | Noap
    1.31 +	fun rew_once lim rts t Noap [] = 
    1.32 +	    (case goal of 
    1.33 +		 None => rts
    1.34 +	       | Some g => 
    1.35 +		 raise error ("make_deriv: no derivation for "^(term2str t)))
    1.36 +	  | rew_once lim rts t Appl [] = 
    1.37 +	    (*(case rs of Rls _ =>*) rew_once lim rts t Noap rs
    1.38 +	  (*| Seq _ => rts) FIXXXXXME 14.3.03*)
    1.39 +	  | rew_once lim rts t apno rs' =
    1.40 +	    (case goal of 
    1.41 +		 None => rew_or_calc lim rts t apno rs'
    1.42 +	       | Some g =>
    1.43 +		 if g = t then rts
    1.44 +		 else rew_or_calc lim rts t apno rs')
    1.45 +	and rew_or_calc lim rts t apno (rrs' as (r::rs')) =
    1.46 +	    if lim < 0 
    1.47 +	    then (writeln ("make_deriv exceeds " ^ int2str (!lim_deriv) ^
    1.48 +			   "with deriv =\n"); writeln (deriv2str rts); rts)
    1.49 +	    else
    1.50 +	    case r of
    1.51 +		Thm (thmid, tm) =>
    1.52 +		(if not (!trace_rewrite) then () else
    1.53 +		 writeln ("### trying thm '" ^ thmid ^ "'");
    1.54 +		 case rewrite_ thy ro erls true tm t of
    1.55 +		     None => rew_once lim rts t apno rs'
    1.56 +		   | Some (t',a') =>
    1.57 +		     (if ! trace_rewrite 
    1.58 +		      then writeln ("### rewrites to: "^(term2str t')) else();
    1.59 +		      rew_once (lim-1) (rts@[(t,r,(t',a'))]) t' Appl rrs'))
    1.60 +	      | Calc (c as (op_,_)) => 
    1.61 +		let val _ = if not (!trace_rewrite) then () else
    1.62 +			    writeln ("### trying calc. '" ^ op_ ^ "'")
    1.63 +		    val t = app_num_tr'2 t
    1.64 +		in case get_calculation_ thy c t of
    1.65 +		       None => rew_once lim rts t apno rs'
    1.66 +		     | Some (thmid, tm) => 
    1.67 +		       (let val Some (t',a') = rewrite_ thy ro erls true tm t
    1.68 +			    val _ = if not (!trace_rewrite) then () else
    1.69 +				    writeln("### calc. to: " ^ (term2str t'))
    1.70 +			    val r' = Thm (thmid, tm)
    1.71 +			in rew_once (lim-1) (rts@[(t,r',(t',a'))]) t' Appl rrs'
    1.72 +			end) 
    1.73 +		       handle _ => raise error "derive_norm, Calc: no rewrite"
    1.74 +		end
    1.75 +	      | Rls_ rls => 
    1.76 +		(case rewrite_set_ thy true rls t of
    1.77 +		     None => rew_once lim rts t apno rs'
    1.78 +		   | Some (t',a') =>
    1.79 +		     rew_once (lim-1) (rts @ [(t,r,(t',a'))]) t' Appl rrs');
    1.80 +
    1.81 +    in rew_once (!lim_deriv) [] tt Noap rs end;
    1.82 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
    1.83  
    1.84  (*.toggles the marker for 'fun sym_thm'.*)
    1.85  fun sym_thmID (thmID : thmID) =

     2.1 --- a/src/sml/calcelems.sml	Fri Aug 25 16:46:20 2006 +0200
     2.2 +++ b/src/sml/calcelems.sml	Tue Aug 29 10:07:24 2006 +0200
     2.3 @@ -581,15 +581,19 @@
     2.4  
     2.5  (*.trace internal steps of isac's rewriter*)
     2.6  val trace_rewrite = ref false;
     2.7 -
     2.8  (*.depth of recursion in traces of the rewriter, if trace_rewrite:=true.*)
     2.9  val depth = ref 99999;
    2.10 -
    2.11 -(*.check guhs unique before storing a pbl or met;
    2.12 +(*.no of rewrites exceeding this int -> NO rewrite.*)
    2.13 +(*WN060829 still unused...*)
    2.14 +val lim_rewrite = ref 99999;
    2.15 +(*.no of derivation-elements exceeding this int -> SOME derivation-elements.*)
    2.16 +val lim_deriv = ref 100;
    2.17 +(*.switch for checking guhs unique before storing a pbl or met;
    2.18     set true at startup (done at begin of ROOT.ML)
    2.19     set false for editing IsacKnowledge (done at end of ROOT.ML).*)
    2.20  val check_guhs_unique = ref false;
    2.21  
    2.22 +
    2.23  datatype lrd = (*elements of a path (=loc_) into an Isabelle term*)
    2.24  	 L     (*go left at $*) 
    2.25         | R     (*go right at $*)