1.1 --- a/src/sml/FE-interface/interface.sml	Mon Dec 31 17:56:24 2007 +0100
     1.2 +++ b/src/sml/FE-interface/interface.sml	Wed Jan 02 09:56:26 2008 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4      val checkContext : calcID -> pos' -> guh -> unit
     1.5      val fetchApplicableTactics : calcID -> int -> pos' -> unit
     1.6      val fetchProposedTactic : calcID -> unit
     1.7 +    val applyTactic : calcID -> pos' -> tac -> unit
     1.8      val getAccumulatedAsms : calcID -> pos' -> unit
     1.9      val getActiveFormula : calcID -> unit
    1.10      val getAssumptions : calcID -> pos' -> unit
    1.11 @@ -129,6 +130,9 @@
    1.12      in if existpt' p pt then (upd_ipos cI 1 p; iteratorOK2xml cI p)
    1.13         else sysERROR2xml cI "frontend sends a non-existing pos" end;
    1.14  
    1.15 +(*. set the next tactic to be applied: dont't change the calc-tree,
    1.16 +    but remember the envisaged changes for fun autoCalculate;
    1.17 +    compare force NextTactic .*)
    1.18  (* val (cI, tac) = (1, Add_Given "equality (x ^^^ 2 + 4 * x + 3 = 0)");
    1.19     val (cI, tac) = (1, Specify_Theory "PolyEq.thy");
    1.20     val (cI, tac) = (1, Specify_Problem ["normalize","polynomial",
    1.21 @@ -156,6 +160,32 @@
    1.22  	 | ("failure",_) => sysERROR2xml cI "failure"
    1.23      end;
    1.24  
    1.25 +(*. apply a tactic at a position and update the calc-tree if applicable .*)
    1.26 +fun applyTactic (cI:calcID) ip tac =
    1.27 +    let val ((pt, _), _) = get_calc cI
    1.28 +	val p = get_pos cI 1
    1.29 +    in case locatetac tac (pt, ip) of
    1.30 +(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
    1.31 +   *)
    1.32 +	   ("ok", (_, c, ptp as (_,p'))) =>
    1.33 +	     (upd_calc cI (ptp, []); upd_ipos cI 1 p';
    1.34 +	      autocalculateOK2xml cI p (if null c then p'
    1.35 +					   else last_elem c) p')
    1.36 +	 | ("unsafe-ok", (_, c, ptp as (_,p'))) =>
    1.37 +	     (upd_calc cI (ptp, []); upd_ipos cI 1 p';
    1.38 +	      autocalculateOK2xml cI p (if null c then p'
    1.39 +					   else last_elem c) p')
    1.40 +	 | ("end-of-calculation", (_, c, ptp as (_,p'))) =>
    1.41 +	     (upd_calc cI (ptp, []); upd_ipos cI 1 p';
    1.42 +	      autocalculateOK2xml cI p (if null c then p'
    1.43 +					   else last_elem c) p')
    1.44 +
    1.45 +
    1.46 +	 | (str,_) => autocalculateERROR2xml cI "failure"
    1.47 +    end;
    1.48 +
    1.49 +
    1.50 +
    1.51  (* val cI = 1;
    1.52     *)
    1.53  fun fetchProposedTactic (cI:calcID) =

     2.1 --- a/src/sml/ME/mathengine.sml	Mon Dec 31 17:56:24 2007 +0100
     2.2 +++ b/src/sml/ME/mathengine.sml	Wed Jan 02 09:56:26 2008 +0100
     2.3 @@ -271,6 +271,9 @@
     2.4  
     2.5     *)
     2.6  
     2.7 +
     2.8 +
     2.9 +
    2.10  (*.does several steps within one calculation as given by "type auto";
    2.11     the steps may arbitrarily go into and leave different phases, 
    2.12     i.e. specify-phase and solve-phase.*)

     3.1 --- a/src/sml/ME/rewtools.sml	Mon Dec 31 17:56:24 2007 +0100
     3.2 +++ b/src/sml/ME/rewtools.sml	Wed Jan 02 09:56:26 2008 +0100
     3.3 @@ -612,22 +612,39 @@
     3.4  > thms_of_rls rls;
     3.5     *)
     3.6  
     3.7 +(*@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@#@#@#@#
     3.8 +(*. check if an _atomic_ (Thm, Calc) rule is contained in a rule set 
     3.9 +   (recursivley down in Rls_) .*)
    3.10 +fun contains_rule rule (Rls {rules,...}) = 
    3.11 +
    3.12 +    if eq_rule thm rule then true 
    3.13 +    else
    3.14 +  | contains_rule (cal as Calc _) rule = eq_rule thm rule
    3.15 +    case 
    3.16 +
    3.17 +fun thm_of_rule Erule = []
    3.18 +  | thm_of_rule (thm as Thm _) = [thm]
    3.19 +  | thm_of_rule (Calc _) = []
    3.20 +  | thm_of_rule (Rls_ rls) = thms_of_rls rls
    3.21 +and thms_of_rls Erls = []
    3.22 +  | thms_of_rls (Rls {rules,...}) = (flat o (map  thm_of_rule)) rules
    3.23 +  | thms_of_rls (Seq {rules,...}) = (flat o (map  thm_of_rule)) rules
    3.24 +  | thms_of_rls (Rrls _) = [];
    3.25 +@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@#@#@#@#*)
    3.26 +
    3.27  (*. try if a rewrite-rule is applicable to a given formula; 
    3.28 -    in case of rule-sets (recursivley) collect all _atomic_ rewrites .*)
    3.29 +    in case of rule-sets (recursivley) collect all _atomic_ rewrites .*) 
    3.30  fun try_rew thy ((_, ro):rew_ord) erls (subst:subst) f (thm' as Thm(id, thm)) =
    3.31      if contains_bdv thm
    3.32      then case rewrite_inst_ thy ro erls false subst thm f of
    3.33 -	      Some (f',_) => (writeln("@@@ try_rew: "^id^" -> "^term2str f');
    3.34 -			      [rule2tac subst thm'])
    3.35 +	      Some (f',_) =>[rule2tac subst thm']
    3.36  	    | None => []
    3.37      else (case rewrite_ thy ro erls false thm f of
    3.38 -	Some (f',_) => (writeln("@@@ try_rew: "^id^" -> "^term2str f');
    3.39 -			      [rule2tac [] thm'])
    3.40 +	Some (f',_) => [rule2tac [] thm']
    3.41  	    | None => [])
    3.42    | try_rew thy _ _ _ f (cal as Calc c) = 
    3.43      (case get_calculation_ thy c f of
    3.44 -	Some (str, _) => (writeln("@@@ try_rew: Calc -> "^str);
    3.45 -			      [rule2tac [] cal])
    3.46 +	Some (str, _) => [rule2tac [] cal]
    3.47        | None => [])
    3.48    | try_rew thy _ _ subst f (Rls_ rls) = filter_appl_rews thy subst f rls
    3.49  and filter_appl_rews thy subst f (Rls {rew_ord = ro, erls, rules,...}) = 

     4.1 --- a/src/sml/ME/script.sml	Mon Dec 31 17:56:24 2007 +0100
     4.2 +++ b/src/sml/ME/script.sml	Wed Jan 02 09:56:26 2008 +0100
     4.3 @@ -641,6 +641,14 @@
     4.4  	  AssWeak (m,f'))
     4.5    else ((*writeln"3### assod ..NotAss";*)NotAss))
     4.6  
     4.7 +(*#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#
     4.8 +  | assod pt d (m as Rewrite' (thy,rod,rls,put,(thmID,thm),f,(f',asm))) 
     4.9 +  (Const ("Script.Rewrite'_Set",_) $ Free (rls_,_) $ _ $ f_) =
    4.10 +  if contains_rule (Thm (thmID, refl(*dummy*))) (assoc_rls rls) then 
    4.11 +    if f = f_ then Ass (m,f') else AssWeak (m,f')
    4.12 +  else NotAss
    4.13 +#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#@#*)
    4.14 +
    4.15  (*val f = (term_of o the o (parse thy))"#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
    4.16  > val f'= (term_of o the o (parse thy))"#0+(sqrt(sqrt a))^^^#2=#0";
    4.17  > val m =   Rewrite'("Script.thy","tless_true","eval_rls",false,

     5.1 --- a/src/sml/calcelems.sml	Mon Dec 31 17:56:24 2007 +0100
     5.2 +++ b/src/sml/calcelems.sml	Wed Jan 02 09:56:26 2008 +0100
     5.3 @@ -457,6 +457,7 @@
     5.4    | append_rls id (Rrls _) _ = 
     5.5      raise error ("append_rls: not for reverse-rewrite-rule-set "^id);
     5.6  
     5.7 +(*. are _atomic_ rules equal ?.*)
     5.8  fun eq_rule (Thm (thm1,_), Thm (thm2,_)) = thm1 = thm2
     5.9    | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2
    5.10    | eq_rule _ = false;

     6.1 --- a/src/smltest/ME/script.sml	Mon Dec 31 17:56:24 2007 +0100
     6.2 +++ b/src/smltest/ME/script.sml	Wed Jan 02 09:56:26 2008 +0100
     6.3 @@ -229,9 +229,9 @@
     6.4  autoCalculate 1 CompleteCalcHead;
     6.5  autoCalculate 1 (Step 1);
     6.6  autoCalculate 1 (Step 1);
     6.7 -val ((pt, (p, p_)), _) = get_calc 1; show_pt pt;
     6.8 +val ((pt, p), _) = get_calc 1; show_pt pt;
     6.9  show_pt pt;
    6.10 -if sel_appl_atomic_tacs pt (p,p_) = 
    6.11 +if sel_appl_atomic_tacs pt p = 
    6.12     [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
    6.13      Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
    6.14      Calculate "op *"] then ()