1.1 --- a/test/Tools/isac/Interpret/script.sml	Sun Jun 30 17:27:34 2013 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Thu Jul 11 16:58:31 2013 +0200
     1.3 @@ -195,59 +195,42 @@
     1.4  autoCalculate 1 (Step 1);
     1.5  val ((pt, p), _) = get_calc 1; show_pt pt;
     1.6  val appltacs = sel_appl_atomic_tacs pt p;
     1.7 -
     1.8 -(*========== inhibit exn AK110721 ================================================
     1.9 -(*(*These SHOULD be the same*)
    1.10 - print_depth(999);
    1.11 - appltacs;
    1.12 - [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
    1.13 -    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
    1.14 -    Calculate "TIMES"];*)
    1.15 -
    1.16  if appltacs = 
    1.17 -   [Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),
    1.18 -    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"),
    1.19 -    Calculate "TIMES"] then ()
    1.20 -else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
    1.21 -========== inhibit exn AK110721 ================================================*)
    1.22 +(* WN130613
    1.23 +   [Rewrite ("radd_commute", "Test.radd_commute") (*"?m + ?n = ?n + ?m"*),
    1.24 +    Rewrite ("radd_assoc", "?m + ?n + ?k = ?m + (?n + ?k)"), Calculate "TIMES"] *)
    1.25 +   [Rewrite ("radd_commute", "Test.radd_commute"), 
    1.26 +    Rewrite ("add_assoc", "Groups.semigroup_add_class.add_assoc"), Calculate "TIMES"]
    1.27 +then () else error "script.sml fun sel_appl_atomic_tacs diff.behav.";
    1.28  
    1.29  trace_script := true;
    1.30  trace_script := false;
    1.31  applyTactic 1 p (hd appltacs);
    1.32  val ((pt, p), _) = get_calc 1; show_pt pt;
    1.33  val appltacs = sel_appl_atomic_tacs pt p;
    1.34 +(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
    1.35  
    1.36 -(*(* AK110722 Debugging start*)
    1.37 -(*applyTactic 1 p (hd appltacs); WAS assy: call by ([3], Pbl)*)
    1.38  "~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
    1.39  val ((pt, _), _) = get_calc cI;
    1.40  val p = get_pos cI 1;
    1.41 -
    1.42  locatetac;
    1.43  locatetac tac;
    1.44 -locatetac tac;
    1.45  
    1.46  (*locatetac tac (pt, ip); (*WAS assy: call by ([3], Pbl)*)*)
    1.47  "~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
    1.48  val (mI,m) = mk_tac'_ tac;
    1.49 -
    1.50  applicable_in p pt m ; (*Appl*)
    1.51 -
    1.52  member op = specsteps mI; (*false*)
    1.53 -
    1.54  (*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
    1.55  loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
    1.56  (*val it = fn: string * tac_ -> ptree * (pos * pos_) -> lOc_*)
    1.57  (mI,m); (*string * tac*)
    1.58  ptp (*ptree * pos'*);
    1.59 -
    1.60  "~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = ((mI,m), ptp);
    1.61  (*val (msg, cs') = solve m (pt, pos);
    1.62  (*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
    1.63 -
    1.64  m;
    1.65  (pt, pos);
    1.66 -
    1.67  "~~~~~ fun solve, args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
    1.68  (*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
    1.69  
    1.70 @@ -259,15 +242,6 @@
    1.71  (assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
    1.72  assoc_thy;
    1.73  
    1.74 -(*not finished - error continues in fun generate1*)
    1.75 -(* AK110722 Debugging end*)*)
    1.76 -(*========== inhibit exn AK110721 ================================================
    1.77 -"----- WN080102 these vvv do not work, because locatetac starts the search" ^
    1.78 - "1 stac too low";
    1.79 -(* AK110722 ERROR: assy: call by ([3], Pbl) *)
    1.80 -applyTactic 1 p (hd appltacs);
    1.81 -============ inhibit exn AK110721 ==============================================*)
    1.82 -
    1.83  autoCalculate 1 CompleteCalc;
    1.84  
    1.85  "----------- fun init_form, fun get_stac -------------------------";