# HG changeset patch
# User blanchet
# Date 1409237907 -7200
# Node ID df0d6ce8fb66ad5f629ba0a863a60f051b102603
# Parent  d44c9dc4bf3095dc503f4352a956306d2b50e8ad
made trace more informative when minimization is enabled

diff -r d44c9dc4bf30 -r df0d6ce8fb66 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -37,12 +37,12 @@
 val slack = seconds 0.025
 
 fun minimized_isar_step ctxt time
-    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meth :: _, comment)) =
+    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
   let
     val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
 
     fun mk_step_lfs_gfs lfs gfs =
-      Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), [meth], comment)
+      Prove (qs, xs, l, t, subproofs, sort_facts (lfs, gfs), meths, comment)
 
     fun minimize_half _ min_facts [] time = (min_facts, time)
       | minimize_half mk_step min_facts (fact :: facts) time =
@@ -58,11 +58,17 @@
   end
 
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (_, _, l, _, _, _, meth :: _, _)) =
+      (step as Prove (_, _, l, _, _, _, meth :: meths, _)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
-      let val (time', step') = minimized_isar_step ctxt time step in
-        set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' [(meth, Played time')];
+      let
+        fun old_data_for_method meth' =
+          (meth', peek_at_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth'))
+
+        val (time', step') = minimized_isar_step ctxt time step
+      in
+        set_preplay_outcomes_of_isar_step ctxt time' preplay_data step'
+          ((meth, Played time') :: (if step' = step then map old_data_for_method meths else []));
         step'
       end
     | _ => step (* don't touch steps that time out or fail *))
diff -r d44c9dc4bf30 -r df0d6ce8fb66 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -17,6 +17,7 @@
 
   type isar_preplay_data
 
+  val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome
   val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
   val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
     play_outcome
@@ -41,6 +42,9 @@
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
 
+fun peek_at_outcome outcome =
+  if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
+
 fun par_list_map_filter_with_timeout _ _ _ _ [] = []
   | par_list_map_filter_with_timeout get_time min_timeout timeout0 f xs =
     let
@@ -200,9 +204,6 @@
     end
   | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
 
-fun peek_at_outcome outcome =
-  if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
-
 fun get_best_method_outcome force =
   tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *)
   #> map (apsnd force)