# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID b6af899a78ac92e57ee1b0bbc9899e2ff32704aa
# Parent  25d1495e6641bff0459b154b09d617965e1ac4bf
tuning

diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -61,15 +61,16 @@
 fun play_one_line_proof mode timeout used_facts state i (preferred, methss as (meth :: _) :: _) =
   let
     fun dont_know () =
-      (if exists (fn meths => member (op =) meths preferred) methss then preferred else meth,
-       Play_Timed_Out Time.zeroTime)
+      (used_facts,
+       (if exists (fn meths => member (op =) meths preferred) methss then preferred else meth,
+        Play_Timed_Out Time.zeroTime))
   in
     if timeout = Time.zeroTime then
       dont_know ()
     else
       let
         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
-        val facts = used_facts |> map (fst o fst) |> sort string_ord
+        val fact_names = used_facts |> map fst |> sort string_ord
 
         val {context = ctxt, facts = chained, goal} = Proof.goal state
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
@@ -77,9 +78,9 @@
 
         fun try_methss [] = dont_know ()
           | try_methss (meths :: methss) =
-            let val step = Prove ([], [], ("", 0), goal_t, [], ([], facts), meths, "") in
+            let val step = Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") in
               (case preplay_isar_step ctxt timeout [] step of
-                (res as (_, Played _)) :: _ => res
+                (res as (_, Played _)) :: _ => (used_facts, res)
               | _ => try_methss methss)
             end
       in
@@ -157,12 +158,11 @@
           print_used_facts used_facts used_from
         | _ => ())
       |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
-      |> (fn {outcome, used_facts, used_from, preferred_methss, message, ...} =>
+      |> (fn {outcome, used_facts, preferred_methss, message, ...} =>
         (if outcome = SOME ATP_Proof.TimedOut then timeoutN
          else if is_some outcome then noneN
          else someN,
-         fn () => message (play_one_line_proof mode preplay_timeout
-           (filter_used_facts false used_facts used_from) state subgoal
+         fn () => message (play_one_line_proof mode preplay_timeout used_facts state subgoal
            preferred_methss)))
 
     fun go () =
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -127,7 +127,7 @@
 val skolem_methods = basic_systematic_methods
 
 fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
-    (one_line_params as ((_, one_line_play), banner, used_facts, subgoal, subgoal_count)) =
+    (one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) =
   let
     val _ = if debug then Output.urgent_message "Constructing Isar proof..." else ()
 
@@ -351,7 +351,7 @@
                (case isar_proof of
                  Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) =>
                  let val used_facts' = filter (member (op =) gfs o fst) used_facts in
-                   ((meth, play_outcome), banner, used_facts', subgoal, subgoal_count)
+                   ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
                  end)
              else
                one_line_params) ^
@@ -387,7 +387,7 @@
   | Play_Failed => true)
 
 fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
-    (one_line_params as (preplay, _, _, _, _)) =
+    (one_line_params as ((_, preplay), _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
      isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -43,15 +43,15 @@
 
     fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
 
-    fun minimize_facts _ min_facts [] time = (min_facts, time)
-      | minimize_facts mk_step min_facts (fact :: facts) time =
+    fun minimize_half _ min_facts [] time = (min_facts, time)
+      | minimize_half mk_step min_facts (fact :: facts) time =
         (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
             (mk_step (min_facts @ facts)) of
-          Played time' => minimize_facts mk_step min_facts facts time'
-        | _ => minimize_facts mk_step (fact :: min_facts) facts time)
+          Played time' => minimize_half mk_step min_facts facts time'
+        | _ => minimize_half mk_step (fact :: min_facts) facts time)
 
-    val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
-    val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time'
+    val (min_lfs, time') = minimize_half (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
+    val (min_gfs, time'') = minimize_half (mk_step_lfs_gfs min_lfs) [] gfs0 time'
   in
     (time'', mk_step_lfs_gfs min_lfs min_gfs)
   end
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -30,7 +30,7 @@
     Play_Failed
 
   type one_line_params =
-    (proof_method * play_outcome) * string * (string * stature) list * int * int
+    ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
   val is_proof_method_direct : proof_method -> bool
   val string_of_proof_method : Proof.context -> string list -> proof_method -> string
@@ -68,7 +68,8 @@
   Play_Timed_Out of Time.time |
   Play_Failed
 
-type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * int * int
+type one_line_params =
+  ((string * stature) list * (proof_method * play_outcome)) * string * int * int
 
 fun is_proof_method_direct (Metis_Method _) = true
   | is_proof_method_direct Meson_Method = true
@@ -182,7 +183,7 @@
   |> pairself (sort_distinct (string_ord o pairself fst))
 
 fun one_line_proof_text ctxt num_chained
-    ((meth, play), banner, used_facts, subgoal, subgoal_count) =
+    ((used_facts, (meth, play)), banner, subgoal, subgoal_count) =
   let val (chained, extra) = split_used_facts used_facts in
     map fst extra
     |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -58,7 +58,7 @@
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      run_time : Time.time,
-     message : proof_method * play_outcome -> string}
+     message : (string * stature) list * (proof_method * play_outcome) -> string}
 
   type prover = params -> prover_problem -> prover_result
 
@@ -149,7 +149,7 @@
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    run_time : Time.time,
-   message : proof_method * play_outcome -> string}
+   message : (string * stature) list * (proof_method * play_outcome) -> string}
 
 type prover = params -> prover_problem -> prover_result
 
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -385,8 +385,7 @@
                      minimize, atp_proof, goal)
                   end
 
-                val one_line_params =
-                  (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
+                val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -22,7 +22,8 @@
   val binary_min_facts : int Config.T
   val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
     Proof.state -> thm -> ((string * stature) * thm list) list ->
-    ((string * stature) * thm list) list option * ((proof_method * play_outcome) -> string)
+    ((string * stature) * thm list) list option
+    * (((string * stature) list * (proof_method * play_outcome)) -> string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
 end;
 
diff -r 25d1495e6641 -r b6af899a78ac src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -208,8 +208,7 @@
                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
                   goal)
 
-               val one_line_params =
-                 (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
+               val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained