# HG changeset patch
# User blanchet
# Date 1407145399 -7200
# Node ID d2ad1320c77011361ee85299bd27df86f2bc2040
# Parent  2719eb9d40fe40377060adc64f8947218379f456
honor 'dont_minimize' option when preplaying one-liner proof

diff -r 2719eb9d40fe -r d2ad1320c770 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Jun 22 06:16:57 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 04 11:43:19 2014 +0200
@@ -20,7 +20,7 @@
   val timeoutN : string
   val unknownN : string
 
-  val play_one_line_proof : Time.time -> (string * 'a) list -> Proof.state -> int ->
+  val play_one_line_proof : bool -> Time.time -> (string * 'a) list -> Proof.state -> int ->
     proof_method * proof_method list list -> (string * 'a) list * (proof_method * play_outcome)
   val string_of_factss : (string * fact list) list -> string
   val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
@@ -63,7 +63,11 @@
   (quote name,
    if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
 
-fun play_one_line_proof timeout used_facts state i (preferred, methss as (meth :: _) :: _) =
+fun is_metis_method (Metis_Method _) = true
+  | is_metis_method _ = false
+
+fun play_one_line_proof minimize timeout used_facts state i
+    (preferred, methss as (meth :: _) :: _) =
   let
     fun dont_know () =
       (used_facts,
@@ -87,17 +91,19 @@
                 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
             in
               (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of
-                (res as (Metis_Method _, Played _)) :: _ =>
-                (used_facts, res) (* if a fact is needed by an ATP, it will be needed by "metis" *)
-              | (meth, Played time) :: _ =>
-                let
-                  val (time', used_names') =
-                    minimized_isar_step ctxt time (mk_step fact_names [meth])
-                    ||> (facts_of_isar_step #> snd)
-                  val used_facts' = filter (member (op =) used_names' o fst) used_facts
-                in
-                  (used_facts', (meth, Played time'))
-                end
+                (res as (meth, Played time)) :: _ =>
+                (* if a fact is needed by an ATP, it will be needed by "metis" *)
+                if not minimize orelse is_metis_method meth then
+                  (used_facts, res)
+                else
+                  let
+                    val (time', used_names') =
+                      minimized_isar_step ctxt time (mk_step fact_names [meth])
+                      ||> (facts_of_isar_step #> snd)
+                    val used_facts' = filter (member (op =) used_names' o fst) used_facts
+                  in
+                    (used_facts', (meth, Played time'))
+                  end
               | _ => try_methss methss)
             end
       in
@@ -105,8 +111,8 @@
       end
   end
 
-fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, preplay_timeout,
-      expect, ...}) mode output_result only learn
+fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout,
+      preplay_timeout, expect, ...}) mode output_result only learn
     {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
   let
     val ctxt = Proof.context_of state
@@ -179,8 +185,8 @@
         (if outcome = SOME ATP_Proof.TimedOut then timeoutN
          else if is_some outcome then noneN
          else someN,
-         fn () => message (fn () => play_one_line_proof preplay_timeout used_facts state subgoal
-           preferred_methss)))
+         fn () => message (fn () => play_one_line_proof minimize preplay_timeout used_facts state
+           subgoal preferred_methss)))
 
     fun go () =
       let