# HG changeset patch
# User blanchet
# Date 1272383073 -7200
# Node ID af99c98121d6e00d9e2c2ad248777d91c2f4ef10
# Parent  1e01a7162435b6dc383f42f439d08c1801c80eb5
make Sledgehammer more friendly if no subgoal is left

diff -r 1e01a7162435 -r af99c98121d6 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Apr 27 17:05:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Apr 27 17:44:33 2010 +0200
@@ -11,7 +11,7 @@
   type prover_result = ATP_Manager.prover_result
 
   val minimize_theorems :
-    params -> int -> Proof.state -> (string * thm list) list
+    params -> int -> int -> Proof.state -> (string * thm list) list
     -> (string * thm list) list option * string
 end;
 
@@ -69,14 +69,13 @@
 
 fun minimize_theorems (params as {debug, atps, minimize_timeout, isar_proof,
                                   shrink_factor, sorts, ...})
-                      i state name_thms_pairs =
+                      i n state name_thms_pairs =
   let
     val thy = Proof.theory_of state
     val prover = case atps of
                    [atp_name] => get_prover thy atp_name
                  | _ => error "Expected a single ATP."
     val msecs = Time.toMilliseconds minimize_timeout
-    val n = length name_thms_pairs
     val _ =
       priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
                 " with a time limit of " ^ string_of_int msecs ^ " ms.")
@@ -88,7 +87,6 @@
       | _ => NONE
 
     val {context = ctxt, facts, goal} = Proof.goal state;
-    val n = Logic.count_prems (prop_of goal)
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of
@@ -105,9 +103,9 @@
           val (min_thms, {proof, internal_thm_names, ...}) =
             linear_minimize (test_thms (SOME filtered_clauses)) to_use
                             ([], result)
-          val n = length min_thms
+          val m = length min_thms
           val _ = priority (cat_lines
-            ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^ ".")
+            ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
         in
           (SOME min_thms,
            proof_text isar_proof
diff -r 1e01a7162435 -r af99c98121d6 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 27 17:05:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 27 17:44:33 2010 +0200
@@ -487,8 +487,8 @@
           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
        |> fold count_constants_clause extra_clauses
        |> fold count_constants_clause helper_clauses
-     val _ = List.app (display_arity explicit_apply const_needs_hBOOL)
-                      (Symtab.dest (const_min_arity))
+     val _ = app (display_arity explicit_apply const_needs_hBOOL)
+                 (Symtab.dest (const_min_arity))
      in (const_min_arity, const_needs_hBOOL) end
   else (Symtab.empty, Symtab.empty);
 
diff -r 1e01a7162435 -r af99c98121d6 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 27 17:05:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 27 17:44:33 2010 +0200
@@ -217,20 +217,25 @@
 fun get_params thy = extract_params thy (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)
 
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
 (* Sledgehammer the given subgoal *)
 
 fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
   | run (params as {atps, timeout, ...}) i relevance_override minimize_command
-        proof_state =
-    let
-      val birth_time = Time.now ()
-      val death_time = Time.+ (birth_time, timeout)
-      val _ = kill_atps ()  (* race w.r.t. other invocations of Sledgehammer *)
-      val _ = priority "Sledgehammering..."
-      val _ = List.app (start_prover_thread params birth_time death_time i
-                                            relevance_override minimize_command
-                                            proof_state) atps
-    in () end
+        state =
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n =>
+      let
+        val birth_time = Time.now ()
+        val death_time = Time.+ (birth_time, timeout)
+        val _ = kill_atps ()  (* race w.r.t. other Sledgehammer invocations *)
+        val _ = priority "Sledgehammering..."
+        val _ = app (start_prover_thread params birth_time death_time i n
+                                         relevance_override minimize_command
+                                         state) atps
+      in () end
 
 fun minimize override_params i fact_refs state =
   let
@@ -240,8 +245,10 @@
       map o pairf Facts.string_of_ref o ProofContext.get_fact
     val name_thms_pairs = theorems_from_refs ctxt fact_refs
   in
-    priority (#2 (minimize_theorems (get_params thy override_params) i state
-                                    name_thms_pairs))
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
+                                           state name_thms_pairs))
   end
 
 val sledgehammerN = "sledgehammer"
@@ -262,9 +269,7 @@
 val is_raw_param_relevant_for_minimize =
   member (op =) params_for_minimize o fst o unalias_raw_param
 fun string_for_raw_param (key, values) =
-  key ^ (case space_implode " " values of
-           "" => ""
-         | value => " = " ^ value)
+  key ^ (case space_implode " " values of "" => "" | value => " = " ^ value)
 
 fun minimize_command override_params i atp_name facts =
   sledgehammerN ^ " " ^ minimizeN ^ " [atp = " ^ atp_name ^
@@ -276,7 +281,7 @@
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let
     val thy = Proof.theory_of state
-    val _ = List.app check_raw_param override_params
+    val _ = app check_raw_param override_params
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in