# HG changeset patch
# User blanchet
# Date 1344946073 -7200
# Node ID 5c9356f8c968fa7db95db16307155fed63a29a38
# Parent  9152e66f98da8f786ee1ad0259feaa44133fd27a
warn users about unused "using" facts

diff -r 9152e66f98da -r 5c9356f8c968 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 14 13:20:59 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Aug 14 14:07:53 2012 +0200
@@ -52,7 +52,7 @@
     Proof.context -> (string * stature) list vector -> 'a proof
     -> string list option
   val unalias_type_enc : string -> string list
-  val one_line_proof_text : one_line_params -> string
+  val one_line_proof_text : int -> one_line_params -> string
   val make_tvar : string -> typ
   val make_tfree : Proof.context -> string -> typ
   val term_from_atp :
@@ -64,7 +64,7 @@
   val isar_proof_text :
     Proof.context -> bool -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool -> isar_params -> one_line_params -> string
+    Proof.context -> bool -> isar_params -> int -> one_line_params -> string
 end;
 
 structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -250,21 +250,33 @@
 fun show_time NONE = ""
   | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
 
+fun unusing_chained_facts _ 0 = ""
+  | unusing_chained_facts used_chaineds num_chained =
+    if length used_chaineds = num_chained then ""
+    else if null used_chaineds then "(* using no facts *) "
+    else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+
 fun apply_on_subgoal _ 1 = "by "
   | apply_on_subgoal 1 _ = "apply "
   | apply_on_subgoal i n =
     "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
 fun command_call name [] =
     name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
 fun try_command_line banner time command =
   banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ show_time time ^ "."
+
 fun using_labels [] = ""
   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun reconstructor_command reconstr i n (ls, ss) =
+
+fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
+  unusing_chained_facts used_chaineds num_chained ^
   using_labels ls ^ apply_on_subgoal i n ^
   command_call (string_for_reconstructor reconstr) ss
+
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of
@@ -276,8 +288,9 @@
   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
         |> pairself (sort_distinct (string_ord o pairself fst))
 
-fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
-                         subgoal, subgoal_count) =
+fun one_line_proof_text num_chained
+        (preplay, banner, used_facts, minimize_command, subgoal,
+         subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
     val (failed, reconstr, ext_time) =
@@ -292,7 +305,8 @@
       | Failed_to_Play reconstr => (true, reconstr, NONE)
     val try_line =
       ([], map fst extra)
-      |> reconstructor_command reconstr subgoal subgoal_count
+      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained)
+                               num_chained
       |> (if failed then
             enclose "One-line proof reconstruction failed: "
                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
@@ -845,7 +859,7 @@
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
     val reconstr = Metis (type_enc, lam_trans)
     fun do_facts (ls, ss) =
-      reconstructor_command reconstr 1 1
+      reconstructor_command reconstr 1 1 [] 0
           (ls |> sort_distinct (prod_ord string_ord int_ord),
            ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =
@@ -887,7 +901,7 @@
       (if isar_proof_requested then 1 else 2) * isar_shrink_factor
     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
-    val one_line_proof = one_line_proof_text one_line_params
+    val one_line_proof = one_line_proof_text 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
@@ -982,11 +996,11 @@
                   ""
   in one_line_proof ^ isar_proof end
 
-fun proof_text ctxt isar_proof isar_params
+fun proof_text ctxt isar_proof isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
      isar_proof_text ctxt isar_proof isar_params
    else
-     one_line_proof_text) one_line_params
+     one_line_proof_text num_chained) one_line_params
 
 end;
diff -r 9152e66f98da -r 5c9356f8c968 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 14 13:20:59 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Aug 14 14:07:53 2012 +0200
@@ -132,7 +132,7 @@
               (filter_used_facts true used_facts xs)
               (filter_used_facts false used_facts seen, result)
         | _ => min timeout xs (x :: seen, result)
-  in min timeout (rev xs) ([], result) end
+  in min timeout xs ([], result) end
 
 fun binary_minimize test timeout result xs =
   let
@@ -193,9 +193,8 @@
       get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
     fun test timeout = test_facts params silent prover timeout i n state
     val (chained, non_chained) = List.partition is_fact_chained facts
-    (* Pull chained facts to the front, so that they are less likely to be
-       kicked out by the minimization algorithms (cf. "rev" in
-       "linear_minimize"). *)
+    (* Push chained facts to the back, so that they are less likely to be
+       kicked out by the linear minimization algorithm. *)
     val facts = non_chained @ chained
   in
     (print silent (fn () => "Sledgehammer minimizer: " ^
diff -r 9152e66f98da -r 5c9356f8c968 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 13:20:59 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 14:07:53 2012 +0200
@@ -884,7 +884,11 @@
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command params minimize_command name preplay,
                    subgoal, subgoal_count)
-              in proof_text ctxt isar_proof isar_params one_line_params end,
+                val num_chained = length (#facts (Proof.goal state))
+              in
+                proof_text ctxt isar_proof isar_params num_chained
+                           one_line_params
+              end,
            (if verbose then
               "\nATP real CPU time: " ^ string_from_time run_time ^ "."
             else
@@ -1062,7 +1066,8 @@
                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command params minimize_command name preplay,
                  subgoal, subgoal_count)
-            in one_line_proof_text one_line_params end,
+              val num_chained = length (#facts (Proof.goal state))
+            in one_line_proof_text num_chained one_line_params end,
          if verbose then
            "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
          else
@@ -1104,7 +1109,8 @@
                 (play, proof_banner mode name, used_facts,
                  minimize_command override_params name, subgoal,
                  subgoal_count)
-            in one_line_proof_text one_line_params end,
+              val num_chained = length (#facts (Proof.goal state))
+            in one_line_proof_text num_chained one_line_params end,
        message_tail = ""}
     | play =>
       let