# HG changeset patch
# User blanchet
# Date 1387441700 -3600
# Node ID c8b04da1bd01c155e42ceeeb6aa32741993d932d
# Parent  a368cd086e46d7a1a85d02d55a437cc32f3753ba
tuning

diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -464,7 +464,7 @@
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], used_from = [],
         run_time = Time.zeroTime,
-        preplay = Lazy.value (Sledgehammer_Reconstructor.Failed_to_Play
+        preplay = Lazy.value (Sledgehammer_Reconstructor.Play_Failed
           Sledgehammer_Provers.plain_metis),
         message = K "", message_tail = ""}, ~1)
     val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_compress.ML
+    Author:     Steffen Juilf Smolka, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Steffen Juilf Smolka, TU Muenchen
 
 Compression of isar proofs by merging steps.
 Only proof steps using the same proof method are merged.
@@ -170,13 +170,13 @@
           | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'")
 
       fun elim_subproofs (step as Let _) = step
-        | elim_subproofs
-          (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
-            if subproofs = [] then step else
-              case get_preplay_time l of
-                (true, _) => step (* timeout or fail *)
-              | (false, time) =>
-                  elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+          if subproofs = [] then
+            step
+          else
+            (case get_preplay_time l of
+              (true, _) => step (* timeout or fail *)
+            | (false, time) => elim_subproofs' time qs fix l t lfs gfs meth subproofs [])
 
       (** top_level compression: eliminate steps by merging them into their
           successors **)
@@ -229,8 +229,7 @@
               val succs = collect_successors steps' succ_lbls
               val succs' = map (try_merge cand #> the) succs
 
-              (* TODO: should be lazy: stop preplaying as soon as one step
-                 fails/times out *)
+              (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
               val preplay_times = map2 preplay_quietly timeouts succs'
 
               (* ensure none of the modified successors timed out *)
@@ -243,8 +242,7 @@
               decrement_step_count (); (* candidate successfully eliminated *)
               map2 set_preplay_time succ_lbls preplay_times;
               map (replace_successor l succ_lbls) lfs;
-              (* removing the step would mess up the indices
-                 -> replace with dummy step instead *)
+              (* removing the step would mess up the indices -> replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2
             end
             handle Bind => steps
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -239,8 +239,7 @@
      | {preplay, message, ...} =>
        (NONE, (preplay, prefix "Prover error: " o message, "")))
     handle ERROR msg =>
-           (NONE, (Lazy.value (Failed_to_Play plain_metis),
-            fn _ => "Error: " ^ msg, ""))
+           (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, ""))
   end
 
 fun adjust_reconstructor_params override_params
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -28,8 +28,7 @@
   | min_deps_of_step {get_preplay_time, set_preplay_time, preplay_quietly, ...}
       (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
     (case get_preplay_time l of
-      (* don't touch steps that time out or fail; minimizing won't help (not true -- FIXME) *)
-      (true, _) => step
+      (true, _) => step (* don't touch steps that time out or fail *)
     | (false, time) =>
       let
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
@@ -69,12 +68,12 @@
       (case label_of_step step of
         NONE => (refed, step :: accu)
       | SOME l =>
-          if Ord_List.member label_ord refed l then
-            do_refed_step step
-            |>> Ord_List.union label_ord refed
-            ||> (fn x => x :: accu)
-          else
-            (refed, accu))
+        if Ord_List.member label_ord refed l then
+          do_refed_step step
+          |>> Ord_List.union label_ord refed
+          ||> (fn x => x :: accu)
+        else
+          (refed, accu))
     and do_refed_step step = step |> postproc_step |> do_refed_step'
     and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
       | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -132,9 +132,10 @@
           (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
              (cf. "~~/src/Pure/Isar/obtain.ML") *)
           let
-            val thesis = Term.Free ("thesis", HOLogic.boolT)
+            (* FIXME: generate fresh name *)
+            val thesis = Free ("thesis", HOLogic.boolT)
             val thesis_prop = thesis |> HOLogic.mk_Trueprop
-            val frees = map Term.Free xs
+            val frees = map Free xs
 
             (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
             val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -88,12 +88,12 @@
     val (failed, reconstr, ext_time) =
       case preplay of
         Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
-      | Trust_Playable (reconstr, time) =>
+      | Play_Timed_Out (reconstr, time) =>
         (false, reconstr,
          (case time of
            NONE => NONE
          | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)))
-      | Failed_to_Play reconstr => (true, reconstr, NONE)
+      | Play_Failed reconstr => (true, reconstr, NONE)
     val try_line =
       ([], map fst extra)
       |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -403,16 +403,15 @@
       else List.last reconstrs
   in
     if timeout = SOME Time.zeroTime then
-      Trust_Playable (get_preferred reconstrs, NONE)
+      Play_Timed_Out (get_preferred reconstrs, NONE)
     else
       let
         val _ =
           if mode = Minimize then Output.urgent_message "Preplaying proof..."
           else ()
         val ths = pairs |> sort_wrt (fst o fst) |> map snd
-        fun play [] [] = Failed_to_Play (get_preferred reconstrs)
-          | play timed_outs [] =
-            Trust_Playable (get_preferred timed_outs, timeout)
+        fun play [] [] = Play_Failed (get_preferred reconstrs)
+          | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout)
           | play timed_out (reconstr :: reconstrs) =
             let
               val _ =
@@ -861,8 +860,7 @@
               ""))
         end
       | SOME failure =>
-        ([], Lazy.value (Failed_to_Play plain_metis),
-         fn _ => string_of_atp_failure failure, "")
+        ([], Lazy.value (Play_Failed plain_metis), fn _ => string_of_atp_failure failure, "")
   in
     {outcome = outcome, used_facts = used_facts, used_from = used_from,
      run_time = run_time, preplay = preplay, message = message,
@@ -1063,7 +1061,7 @@
          else
            "")
       | SOME failure =>
-        (Lazy.value (Failed_to_Play plain_metis),
+        (Lazy.value (Play_Failed plain_metis),
          fn _ => string_of_atp_failure failure, "")
   in
     {outcome = outcome, used_facts = used_facts, used_from = used_from,
@@ -1108,7 +1106,7 @@
        message_tail = ""}
     | play =>
       let
-        val failure = case play of Failed_to_Play _ => GaveUp | _ => TimedOut
+        val failure = case play of Play_Failed _ => GaveUp | _ => TimedOut
       in
         {outcome = SOME failure, used_facts = [], used_from = [],
          run_time = Time.zeroTime, preplay = Lazy.value play,
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -410,8 +410,8 @@
 fun isar_proof_would_be_a_good_idea preplay =
   (case preplay of
     Played (reconstr, _) => reconstr = SMT
-  | Trust_Playable _ => false
-  | Failed_to_Play _ => true)
+  | Play_Timed_Out _ => false
+  | Play_Failed _ => true)
 
 fun proof_text ctxt isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
diff -r a368cd086e46 -r c8b04da1bd01 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Wed Dec 18 22:55:43 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 09:28:20 2013 +0100
@@ -15,8 +15,8 @@
 
   datatype play =
     Played of reconstructor * Time.time |
-    Trust_Playable of reconstructor * Time.time option |
-    Failed_to_Play of reconstructor
+    Play_Timed_Out of reconstructor * Time.time option |
+    Play_Failed of reconstructor
 
   type minimize_command = string list -> string
   type one_line_params = play * string * (string * stature) list * minimize_command * int * int
@@ -35,8 +35,8 @@
 
 datatype play =
   Played of reconstructor * Time.time |
-  Trust_Playable of reconstructor * Time.time option |
-  Failed_to_Play of reconstructor
+  Play_Timed_Out of reconstructor * Time.time option |
+  Play_Failed of reconstructor
 
 type minimize_command = string list -> string
 type one_line_params = play * string * (string * stature) list * minimize_command * int * int