merged

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 21 08:34:56 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 21 08:45:31 2009 +0200
@@ -38,9 +38,9 @@
   }
 
 datatype min_data = MinData of {
-  calls: int,
-  ratios: int,
-  lemmas: int
+  succs: int,
+  ab_ratios: int,
+  it_ratios: int
   }
 
 (* The first me_data component is only used if "minimize" is on.
@@ -52,8 +52,8 @@
   ShData{calls=calls, success=success, lemmas=lemmas, time_isa=time_isa,
     time_atp=time_atp, time_atp_fail=time_atp_fail}
 
-fun make_min_data (calls, ratios, lemmas) =
-  MinData{calls=calls, ratios=ratios, lemmas=lemmas}
+fun make_min_data (succs, ab_ratios, it_ratios) =
+  MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
 
 fun make_me_data (calls, success, time, timeout, lemmas, posns) =
   MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
@@ -61,7 +61,7 @@
 val empty_data =
   Data(make_sh_data (0, 0, 0, 0, 0, 0),
        make_me_data(0, 0, 0, 0, 0, []),
-       MinData{calls=0, ratios=0, lemmas=0},
+       MinData{succs=0, ab_ratios=0, it_ratios=0},
        make_me_data(0, 0, 0, 0, 0, []))
 
 fun map_sh_data f
@@ -70,8 +70,8 @@
         meda0, minda, meda)
 
 fun map_min_data f
-  (Data(shda, meda0, MinData{calls,ratios,lemmas}, meda)) =
-  Data(shda, meda0, make_min_data(f(calls,ratios,lemmas)), meda)
+  (Data(shda, meda0, MinData{succs,ab_ratios,it_ratios}, meda)) =
+  Data(shda, meda0, make_min_data(f(succs,ab_ratios,it_ratios)), meda)
 
 fun map_me_data0 f (Data (shda, MeData{calls,success,time,timeout,lemmas,posns}, minda, meda)) =
   Data(shda, make_me_data(f (calls,success,time,timeout,lemmas,posns)), minda, meda)
@@ -103,11 +103,14 @@
   map_sh_data (fn (calls, success, lemmas, time_isa, time_atp, time_atp_fail)
     => (calls, success, lemmas, time_isa, time_atp, time_atp_fail + t))
 
-val inc_min_calls =
-  map_min_data (fn (calls, ratios, lemmas) => (calls + 1, ratios, lemmas))
+val inc_min_succs =
+  map_min_data (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
 
-fun inc_min_ratios n =
-  map_min_data (fn (calls, ratios, lemmas) => (calls, ratios + n, lemmas))
+fun inc_min_ab_ratios r =
+  map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
+
+fun inc_min_it_ratios r =
+  map_min_data (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
 
 val inc_metis_calls = map_me_data
  (fn (calls, success, time, timeout, lemmas,posns)
@@ -202,9 +205,10 @@
   else ()
  )
 
-fun log_min_data log calls ratios =
-  (log ("Number of minimizations: " ^ string_of_int calls);
-   log ("Minimization ratios: " ^ string_of_int ratios)
+fun log_min_data log succs ab_ratios it_ratios =
+  (log ("Number of successful minimizations: " ^ string_of_int succs);
+   log ("After/before ratios: " ^ string_of_int ab_ratios);
+   log ("Iterations ratios: " ^ string_of_int it_ratios)
   )
 
 in
@@ -215,7 +219,7 @@
     MeData{calls=metis_calls0,
       success=metis_success0, time=metis_time0, timeout=metis_timeout0,
       lemmas=metis_lemmas0,posns=metis_posns0},
-    MinData{calls=min_calls, ratios=min_ratios, lemmas=min_lemmas},
+    MinData{succs=min_succs, ab_ratios=ab_ratios, it_ratios=it_ratios},
     MeData{calls=metis_calls,
       success=metis_success, time=metis_time, timeout=metis_timeout,
       lemmas=metis_lemmas,posns=metis_posns})) =
@@ -228,7 +232,7 @@
       metis_success metis_time metis_timeout metis_lemmas  metis_posns else ();
     log "";
     if metis_calls0 > 0
-      then (log_min_data log min_calls min_ratios; log "";
+      then (log_min_data log min_succs ab_ratios it_ratios; log "";
             log_metis_data log "unminimized " sh_calls sh_success metis_calls0
               metis_success0 metis_time0 metis_timeout0 metis_lemmas0 metis_posns0)
       else ()
@@ -360,8 +364,9 @@
   in
     case minimize timeout st (these (!named_thms)) of
       (SOME (named_thms',its), msg) =>
-        (change_data id inc_min_calls;
-         change_data id (inc_min_ratios ((100*its) div n0));
+        (change_data id inc_min_succs;
+         change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
+         change_data id (inc_min_it_ratios ((100*its) div n0));
          if length named_thms' = n0
          then log (minimize_tag id ^ "already minimal")
          else (named_thms := SOME named_thms';
@@ -405,20 +410,20 @@
     val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
         inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
     val named_thms = ref (NONE : (string * thm list) list option)
-
-    fun if_enabled k f =
-      if AList.defined (op =) args k andalso is_some (!named_thms)
-      then f id st else ()
-
-    val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
-    val _ = if_enabled minimizeK
-      (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))))
-    val _ = if_enabled minimizeK
-      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
-    val _ = if is_some (!named_thms)
-      then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st
-      else ()
-  in () end
+    val minimize = AList.defined (op =) args minimizeK
+  in 
+    Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
+    if is_some (!named_thms)
+      then
+       (if minimize
+          then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st
+          else ();
+       if minimize andalso not(null(these(!named_thms)))
+         then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
+         else ();
+       Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st)
+    else ()
+  end
 
 fun invoke args =
   let

--- a/src/HOL/Tools/inductive.ML	Mon Sep 21 08:34:56 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Sep 21 08:45:31 2009 +0200
@@ -103,6 +103,7 @@
       "(P & True) = P" "(True & P) = P"
     by (fact simp_thms)+};
 
+val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
 
 
 (** context data **)
@@ -559,7 +560,7 @@
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
          REPEAT (resolve_tac [le_funI, le_boolI] 1),
-         rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'),
+         rewrite_goals_tac simp_thms'',
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
@@ -568,7 +569,7 @@
          REPEAT (FIRSTGOAL
            (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
-             (inductive_conj_def :: rec_preds_defs @ simp_thms') prem,
+             (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
            conjI, refl] 1)) prems)]);
 
     val lemma = SkipProof.prove ctxt'' [] []

--- a/src/HOL/ex/ROOT.ML	Mon Sep 21 08:34:56 2009 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Sep 21 08:45:31 2009 +0200
@@ -68,8 +68,7 @@
   "Landau"
 ];
 
-Future.shutdown ();
-(setmp_noncritical proofs 2 (setmp_noncritical Multithreading.max_threads 1 use_thy))
+(setmp_noncritical proofs 2 (setmp_noncritical Goal.parallel_proofs 0 use_thy))
   "Hilbert_Classical";
 
 use_thy "SVC_Oracle";

--- a/src/Pure/Concurrent/future.ML	Mon Sep 21 08:34:56 2009 +0200
+++ b/src/Pure/Concurrent/future.ML	Mon Sep 21 08:45:31 2009 +0200
@@ -237,7 +237,7 @@
               val total = length (! workers);
               val active = count_active ();
             in
-              "SCHEDULE " ^ string_of_int (Time.toMilliseconds now) ^ ": " ^
+              "SCHEDULE " ^ Time.toString now ^ ": " ^
                 string_of_int ready ^ " ready, " ^
                 string_of_int pending ^ " pending, " ^
                 string_of_int running ^ " running; " ^
@@ -257,7 +257,7 @@
               "SCHEDULE: disposed " ^ string_of_int (length dead) ^ " dead worker threads")));
 
     val m = if ! do_shutdown then 0 else Multithreading.max_threads_value ();
-    val mm = (m * 3) div 2;
+    val mm = if m = 9999 then 1 else (m * 3) div 2;
     val l = length (! workers);
     val _ = excessive := l - mm;
     val _ =

--- a/src/Pure/Concurrent/par_list.ML	Mon Sep 21 08:34:56 2009 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Mon Sep 21 08:45:31 2009 +0200
@@ -27,8 +27,10 @@
 struct
 
 fun raw_map f xs =
-  let val group = Task_Queue.new_group (Future.worker_group ())
-  in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end;
+  if Multithreading.enabled () then
+    let val group = Task_Queue.new_group (Future.worker_group ())
+    in Future.join_results (map (fn x => Future.fork_group group (fn () => f x)) xs) end
+  else map (Exn.capture f) xs;
 
 fun map f xs = Exn.release_first (raw_map f xs);