merged
authorwenzelm
Thu, 17 Jan 2013 14:12:35 +0100
changeset 50933 e424e17ee420
parent 50929 7f0bc95af61c (diff)
parent 50932 ca071373b695 (current diff)
child 50934 a076e01b803f
merged
--- a/Admin/components/components.sha1	Thu Jan 17 14:11:26 2013 +0100
+++ b/Admin/components/components.sha1	Thu Jan 17 14:12:35 2013 +0100
@@ -6,6 +6,8 @@
 cb3b0706d208f104b800267697204f6d82f7b48a  cygwin-20130114.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 b98a98025d1f7e560ca6864a53296137dae736b4  e-1.6.tar.gz
+2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
+e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
 6d34b18ca0aa1e10bab6413045d079188c0e2dfb  exec_process-1.0.1.tar.gz
 8b9bffd10e396d965e815418295f2ee2849bea75  exec_process-1.0.2.tar.gz
 e6aada354da11e533af2dee3dcdd96c06479b053  exec_process-1.0.3.tar.gz
--- a/Admin/components/main	Thu Jan 17 14:11:26 2013 +0100
+++ b/Admin/components/main	Thu Jan 17 14:12:35 2013 +0100
@@ -1,6 +1,6 @@
 #main components for everyday use, without big impact on overall build time
 cvc3-2.4.1
-e-1.6
+e-1.6-2
 exec_process-1.0.3
 Haskabelle-2013
 jdk-7u11
--- a/src/Doc/Sledgehammer/document/root.tex	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jan 17 14:12:35 2013 +0100
@@ -12,7 +12,7 @@
 %\usepackage[scaled=.85]{beramono}
 \usepackage{isabelle,iman,pdfsetup}
 
-\newcommand\download{\url{http://www21.in.tum.de/~blanchet/\#software}}
+\newcommand\download{\url{http://isabelle.in.tum.de/components/}}
 
 \def\qty#1{\ensuremath{\left<\mathit{#1\/}\right>}}
 \def\qtybf#1{$\mathbf{\left<\textbf{\textit{#1\/}}\right>}$}
@@ -865,6 +865,12 @@
 that contains the \texttt{emales.py} script. Sledgehammer has been tested with
 version 1.1.
 
+\item[\labelitemi] \textbf{\textit{e\_par}:} E-Par is a metaprover developed
+by Josef Urban that implements strategy scheduling on top of E. To use
+E-Par, set the environment variable \texttt{E\_HOME} to the directory
+that contains the \texttt{runepar.pl} script and the \texttt{eprover} and
+\texttt{epclextract} executables, or use the prebuilt E package from \download.
+
 \item[\labelitemi] \textbf{\textit{iprover}:} iProver is a pure
 instantiation-based prover developed by Konstantin Korovin \cite{korovin-2009}.
 To use iProver, set the environment variable \texttt{IPROVER\_HOME} to the
--- a/src/HOL/Sledgehammer.thy	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Sledgehammer.thy	Thu Jan 17 14:12:35 2013 +0100
@@ -16,6 +16,7 @@
 ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" 
 ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
--- a/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 14:12:35 2013 +0100
@@ -12,9 +12,9 @@
 
 sledgehammer_params
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
-   lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
+   lam_trans = lifting, timeout = 15, dont_preplay, minimize]
 
-declare [[sledgehammer_instantiate_inducts]]
+declare [[sledgehammer_instantiate_inducts = false]]
 
 ML {*
 !Multithreading.max_threads
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 14:12:35 2013 +0100
@@ -12,9 +12,9 @@
 
 sledgehammer_params
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
-   lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
+   lam_trans = lifting, timeout = 2, dont_preplay, minimize]
 
-declare [[sledgehammer_instantiate_inducts]]
+declare [[sledgehammer_instantiate_inducts = false]]
 
 ML {*
 !Multithreading.max_threads
@@ -29,7 +29,7 @@
 val thys = [@{theory List}]
 val params as {provers, ...} = Sledgehammer_Isar.default_params @{context} []
 val prover = hd provers
-val max_suggestions = 1024
+val max_suggestions = 1536
 val dir = "List"
 val prefix = "/tmp/" ^ dir ^ "/"
 *}
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -68,9 +68,9 @@
                     |> File.write_list prob_file
     val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
     val command =
-      File.shell_path (Path.explode path) ^
-      " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^
-      File.shell_path prob_file
+      File.shell_path (Path.explode path) ^ " " ^
+      arguments ctxt false "" (seconds 1.0) (File.shell_path prob_file)
+                (ord, K [], K [])
   in
     TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command
     |> fst
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -16,7 +16,7 @@
   type atp_config =
     {exec : string list * string list,
      arguments :
-       Proof.context -> bool -> string -> Time.time
+       Proof.context -> bool -> string -> Time.time -> string
        -> term_order * (unit -> (string * int) list)
           * (unit -> (string * real) list) -> string,
      proof_delims : (string * string) list,
@@ -45,6 +45,7 @@
   val dummy_thfN : string
   val eN : string
   val e_malesN : string
+  val e_parN : string
   val e_sineN : string
   val e_tofofN : string
   val iproverN : string
@@ -88,7 +89,7 @@
 type atp_config =
   {exec : string list * string list,
    arguments :
-     Proof.context -> bool -> string -> Time.time
+     Proof.context -> bool -> string -> Time.time -> string
      -> term_order * (unit -> (string * int) list)
         * (unit -> (string * real) list) -> string,
    proof_delims : (string * string) list,
@@ -140,6 +141,7 @@
 val dummy_thfN = "dummy_thf" (* for experiments *)
 val eN = "e"
 val e_malesN = "e_males"
+val e_parN = "e_par"
 val e_sineN = "e_sine"
 val e_tofofN = "e_tofof"
 val iproverN = "iprover"
@@ -189,9 +191,9 @@
 
 val alt_ergo_config : atp_config =
   {exec = (["WHY3_HOME"], ["why3"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--format tff1 --prover alt-ergo --timelimit " ^
-       string_of_int (to_secs 1 timeout),
+       string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims = [],
    known_failures =
      [(ProofMissing, ": Valid"),
@@ -301,13 +303,14 @@
 val e_config : atp_config =
   {exec = (["E_HOME"], ["eproof_ram", "eproof"]),
    arguments = fn ctxt => fn full_proof => fn heuristic => fn timeout =>
+       fn file_name =>
        fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
        "--tstp-in --tstp-out --output-level=5 --silent " ^
        e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
        "--term-ordering=" ^ (if is_lpo then "LPO4" else e_kbo ()) ^ " " ^
        "--cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^
-       e_shell_level_argument full_proof,
+       e_shell_level_argument full_proof ^ " " ^ file_name,
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
@@ -334,27 +337,45 @@
 
 val e_males_config : atp_config =
   {exec = (["E_MALES_HOME"], ["emales.py"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-       "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p",
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+       "-t " ^ string_of_int (to_secs 1 timeout) ^ " -p " ^ file_name,
    proof_delims = tstp_proof_delims,
    known_failures = #known_failures e_config,
    prem_role = Conjecture,
    best_slices =
      (* FUDGE *)
-     K [(1.0, ((1000, FOF, "mono_tags??", combsN, false), ""))],
+     K [(0.5, ((1000, FOF, "mono_tags??", combsN, false), "")),
+        (0.5, ((1000, FOF, "mono_guards??", combsN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val e_males = (e_malesN, fn () => e_males_config)
 
 
+(* E-Par *)
+
+val e_par_config : atp_config =
+  {exec = (["E_HOME"], ["runepar.pl"]),
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+       string_of_int (to_secs 1 timeout) ^ " 1 " (* SInE *) ^ file_name ^
+       " 2" (* proofs *),
+   proof_delims = tstp_proof_delims,
+   known_failures = #known_failures e_config,
+   prem_role = Conjecture,
+   best_slices = #best_slices e_males_config,
+   best_max_mono_iters = default_max_mono_iters,
+   best_max_new_mono_instances = default_max_new_mono_instances}
+
+val e_par = (e_parN, fn () => e_par_config)
+
+
 (* iProver *)
 
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iprover"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--clausifier \"$IPROVER_HOME\"/vclausify_rel --time_out_real " ^
-       string_of_real (Time.toReal timeout),
+       string_of_real (Time.toReal timeout) ^ " " ^ file_name,
    proof_delims = tstp_proof_delims,
    known_failures =
      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
@@ -393,10 +414,11 @@
 
 val leo2_config : atp_config =
   {exec = (["LEO2_HOME"], ["leo"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--foatp e --atp e=\"$E_HOME\"/eprover \
        \--atp epclextract=\"$E_HOME\"/epclextract \
-       \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
+       \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+       file_name,
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
@@ -419,8 +441,8 @@
 
 val satallax_config : atp_config =
   {exec = (["SATALLAX_HOME"], ["satallax"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
-       "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+       "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims =
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    known_failures = known_szs_status_failures,
@@ -446,9 +468,11 @@
 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
 val spass_config : atp_config =
   {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
-   arguments = fn _ => fn _ => fn extra_options => fn timeout => fn _ =>
-       ("-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
-       |> extra_options <> "" ? prefix (extra_options ^ " "),
+   arguments =
+     fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
+         "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^
+         file_name
+         |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      [(OldSPASS, "Unrecognized option Isabelle"),
@@ -489,14 +513,14 @@
 
 val vampire_config : atp_config =
   {exec = (["VAMPIRE_HOME"], ["vampire"]),
-   arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn sos => fn timeout => fn file_name => fn _ =>
        "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
        " --proof tptp --output_axiom_names on" ^
        (if is_vampire_at_least_1_8 () then
           " --forced_options propositional_to_bdd=off"
         else
           "") ^
-       " --thanks \"Andrei and Krystof\" --input_file"
+       " --thanks \"Andrei and Krystof\" --input_file " ^ file_name
        |> sos = sosN ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",
@@ -535,9 +559,9 @@
 
 val z3_tptp_config : atp_config =
   {exec = (["Z3_HOME"], ["z3"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
+   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "MBQI=true DISPLAY_UNSAT_CORE=true -tptp -t:" ^
-       string_of_int (to_secs 1 timeout),
+       string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims = [("\ncore(", ").")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -557,7 +581,7 @@
 
 fun dummy_config format type_enc : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
-   arguments = K (K (K (K (K "")))),
+   arguments = K (K (K (K (K (K ""))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
@@ -623,10 +647,12 @@
 fun remote_config system_name system_versions proof_delims known_failures
                   prem_role best_slice : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
-   arguments = fn _ => fn _ => fn command => fn timeout => fn _ =>
-       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
-       "-s " ^ the_remote_system system_name system_versions ^ " " ^
-       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)),
+   arguments =
+     fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
+         (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+         "-s " ^ the_remote_system system_name system_versions ^ " " ^
+         "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+         " " ^ file_name,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    prem_role = prem_role,
@@ -726,10 +752,10 @@
   end
 
 val atps=
-  [alt_ergo, e, e_males, iprover, iprover_eq, leo2, satallax, spass, spass_poly,
-   vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine, remote_e_tofof,
-   remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax,
-   remote_vampire, remote_snark, remote_waldmeister]
+  [alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass,
+   spass_poly, vampire, z3_tptp, dummy_thf, remote_e, remote_e_sine,
+   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2,
+   remote_satallax, remote_vampire, remote_snark, remote_waldmeister]
 
 val setup = fold add_atp atps
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -0,0 +1,112 @@
+(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Steffen Juilf Smolka, TU Muenchen
+
+Preplaying of isar proofs.
+*)
+
+signature SLEDGEHAMMER_PREPLAY =
+sig
+  type isar_step = Sledgehammer_Proof.isar_step
+  eqtype preplay_time
+  val zero_preplay_time : preplay_time
+  val some_preplay_time : preplay_time
+  val add_preplay_time : preplay_time -> preplay_time -> preplay_time
+  val string_of_preplay_time : preplay_time -> string
+  val try_metis : bool -> string -> string -> Proof.context ->
+    Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
+  val try_metis_quietly : bool -> string -> string -> Proof.context ->
+    Time.time -> (isar_step option * isar_step) -> unit -> preplay_time
+end
+
+structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Proof
+
+(* The boolean flag encodes whether the time is exact (false) or an lower bound
+     (true) *)
+type preplay_time = bool * Time.time
+
+val zero_preplay_time = (false, Time.zeroTime)
+val some_preplay_time = (true, Time.zeroTime)
+
+fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
+
+val string_of_preplay_time = ATP_Util.string_from_ext_time
+
+(* timing *)
+fun take_time timeout tac arg =
+  let
+    val timing = Timing.start ()
+  in
+    (TimeLimit.timeLimit timeout tac arg;
+      Timing.result timing |> #cpu |> pair false)
+    handle TimeLimit.TimeOut => (true, timeout)
+  end
+
+(* lookup facts in context *)
+fun resolve_fact_names ctxt names =
+  names
+    |>> map string_for_label
+    |> op @
+    |> maps (thms_of_name ctxt)
+
+exception ZEROTIME
+fun try_metis debug type_enc lam_trans ctxt timeout (succedent, step) =
+  let
+    val (t, byline, obtain) =
+      (case step of
+        Prove (_, _, t, byline) => (t, byline, false)
+      | Obtain (_, xs, _, t, byline) =>
+        (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+           (see ~~/src/Pure/Isar/obtain.ML) *)
+        let
+          val thesis = Term.Free ("thesis", HOLogic.boolT)
+          val thesis_prop = thesis |> HOLogic.mk_Trueprop
+          val frees = map Term.Free xs
+
+          (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+          val inner_prop =
+            fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
+
+          (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+          val prop =
+            Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
+        in
+          (prop, byline, true)
+        end
+      | _ => raise ZEROTIME)
+    val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
+    val facts =
+      (case byline of
+        By_Metis fact_names => resolve_fact_names ctxt fact_names
+      | Case_Split (cases, fact_names) =>
+        resolve_fact_names ctxt fact_names
+          @ (case the succedent of
+              Assume (_, t) => make_thm t
+            | Obtain (_, _, _, t, _) => make_thm t
+            | Prove (_, _, t, _) => make_thm t
+            | _ => error "preplay error: unexpected succedent of case split")
+          :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
+                          | _ => error "preplay error: malformed case split")
+                     #> make_thm)
+               cases)
+    val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
+                    |> obtain ? Config.put Metis_Tactic.new_skolem true
+    val goal =
+      Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
+    fun tac {context = ctxt, prems = _} =
+      Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+  in
+    take_time timeout
+      (fn () => goal tac handle ERROR msg => error ("preplay error: " ^ msg))
+  end
+  handle ZEROTIME => K zero_preplay_time
+
+(* this version treats exceptions like timeouts *)
+fun try_metis_quietly debug type_enc lam_trans ctxt timeout =
+   the_default (true, timeout) oo try o try_metis debug type_enc lam_trans ctxt timeout
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -786,12 +786,12 @@
             fun ord_info () = atp_problem_term_order_info atp_problem
             val ord = effective_term_order ctxt name
             val full_proof = debug orelse isar_proofs
-            val args = arguments ctxt full_proof extra
-                                 (slice_timeout |> the_default one_day)
-                                 (ord, ord_info, sel_weights)
+            val args =
+              arguments ctxt full_proof extra
+                        (slice_timeout |> the_default one_day)
+                        (File.shell_path prob_path) (ord, ord_info, sel_weights)
             val command =
-              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
-              File.shell_path prob_path ^ ")"
+              "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
               |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
             val _ =
               atp_problem
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -741,7 +741,7 @@
         and do_case outer (c, infs) =
           Assume (label_of_clause c, prop_of_clause c) ::
           map (isar_step_of_direct_inf outer) infs
-        val (isar_proof, (preplay_fail, ext_time)) =
+        val (isar_proof, (preplay_fail, preplay_time)) =
           ref_graph
           |> redirect_graph axioms tainted
           |> map (isar_step_of_direct_inf true)
@@ -771,8 +771,8 @@
           let
             val msg =
               (if preplay then
-                [if preplay_fail then "may fail"
-                 else string_from_ext_time ext_time]
+                [(if preplay_fail then "may fail, " else "") ^
+                   Sledgehammer_Preplay.string_of_preplay_time preplay_time]
                else
                  []) @
               (if verbose then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 17 14:11:26 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Thu Jan 17 14:12:35 2013 +0100
@@ -2,15 +2,16 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
-Shrinking and preplaying of reconstructed isar proofs.
+Shrinking of reconstructed isar proofs.
 *)
 
 signature SLEDGEHAMMER_SHRINK =
 sig
   type isar_step = Sledgehammer_Proof.isar_step
+  type preplay_time = Sledgehammer_Preplay.preplay_time
   val shrink_proof :
     bool -> Proof.context -> string -> string -> bool -> Time.time option
-    -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
+    -> real -> isar_step list -> isar_step list * (bool * preplay_time)
 end
 
 structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
@@ -18,6 +19,7 @@
 
 open Sledgehammer_Util
 open Sledgehammer_Proof
+open Sledgehammer_Preplay
 
 (* Parameters *)
 val merge_timeout_slack = 1.2
@@ -44,17 +46,6 @@
 fun pop_max tab = pop tab (the (Inttab.max_key tab))
 fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
 
-(* Timing *)
-fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val no_time = (false, Time.zeroTime)
-fun take_time timeout tac arg =
-  let val timing = Timing.start () in
-    (TimeLimit.timeLimit timeout tac arg;
-     Timing.result timing |> #cpu |> SOME)
-    handle TimeLimit.TimeOut => NONE
-  end
-
-
 (* Main function for shrinking proofs *)
 fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
                  isar_shrink proof =
@@ -70,9 +61,11 @@
       fun handle_metis_fail try_metis () =
         try_metis () handle exn =>
           (if Exn.is_interrupt exn orelse debug then reraise exn
-           else metis_fail := true; SOME Time.zeroTime)
+           else metis_fail := true; some_preplay_time)
       fun get_time lazy_time =
-        if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
+        if !metis_fail andalso not (Lazy.is_finished lazy_time)
+          then some_preplay_time
+          else Lazy.force lazy_time
       val metis_fail = fn () => !metis_fail
     end
 
@@ -118,116 +111,60 @@
         v_fold_index (add_if_cand proof_vect) refed_by_vect []
         |> Inttab.make_list
 
-      (* Metis Preplaying *)
-      fun resolve_fact_names names =
-        names
-          |>> map string_for_label
-          |> op @
-          |> maps (thms_of_name ctxt)
-
-      (* TODO: add "Obtain" case *)
-      exception ZEROTIME
-      fun try_metis timeout (succedent, step) =
-        (if not preplay then K (SOME Time.zeroTime) else
-          let
-            val (t, byline, obtain) =
-              (case step of
-                Prove (_, _, t, byline) => (t, byline, false)
-              | Obtain (_, xs, _, t, byline) =>
-                (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
-                   (see ~~/src/Pure/Isar/obtain.ML) *)
-                let
-                  val thesis = Term.Free ("thesis", HOLogic.boolT)
-                  val thesis_prop = thesis |> HOLogic.mk_Trueprop
-                  val frees = map Term.Free xs
-
-                  (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
-                  val inner_prop =
-                    fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
-
-                  (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
-                  val prop =
-                    Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
-                in
-                  (prop, byline, true)
-                end
-              | _ => raise ZEROTIME)
-            val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
-            val facts =
-              (case byline of
-                By_Metis fact_names => resolve_fact_names fact_names
-              | Case_Split (cases, fact_names) =>
-                resolve_fact_names fact_names
-                  @ (case the succedent of
-                      Assume (_, t) => make_thm t
-                    | Obtain (_, _, _, t, _) => make_thm t
-                    | Prove (_, _, t, _) => make_thm t
-                    | _ => error "Internal error: unexpected succedent of case split")
-                  :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t)
-                                  | _ => error "Internal error: malformed case split")
-                             #> make_thm)
-                       cases)
-            val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
-                            |> obtain ? Config.put Metis_Tactic.new_skolem true
-            val goal =
-              Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t
-            fun tac {context = ctxt, prems = _} =
-              Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
-          in
-            take_time timeout (fn () => goal tac)
-          end)
-          handle ZEROTIME => K (SOME Time.zeroTime)
-
-      val try_metis_quietly = the_default NONE oo try oo try_metis
-
       (* cache metis preplay times in lazy time vector *)
       val metis_time =
         v_map_index
-          (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout
-            o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the)
+          (if not preplay then K (zero_preplay_time) #> Lazy.value
+           else
+             apsnd the (* step *)
+             #> apfst (fn i => try (get (i-1) #> the) proof_vect) (* succedent *)
+             #> try_metis debug type_enc lam_trans ctxt preplay_timeout
+             #> handle_metis_fail
+             #> Lazy.lazy)
           proof_vect
+
       fun sum_up_time lazy_time_vector =
         Vector.foldl
-          ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts))
-             | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout)))
-            o apfst get_time)
-          no_time lazy_time_vector
+          (apfst get_time #> uncurry add_preplay_time)
+          zero_preplay_time lazy_time_vector
 
       (* Merging *)
-      (* TODO: consider adding "Obtain" cases *)
       fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) step2 =
           let
             val (step_constructor, lfs2, gfs2) =
               (case step2 of
                 (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) =>
                   (fn by => Prove (qs2, label2, t, by), lfs2, gfs2)
-              | (Obtain(qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
+              | (Obtain (qs2, xs, label2, t, By_Metis (lfs2, gfs2))) =>
                   (fn by => Obtain (qs2, xs, label2, t, by), lfs2, gfs2)
-              | _ => error "Internal error: unmergeable Isar steps" )
+              | _ => error "sledgehammer_shrink: unmergeable Isar steps" )
             val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1
             val gfs = union (op =) gfs1 gfs2
           in step_constructor (By_Metis (lfs, gfs)) end
-        | merge _ _ = error "Internal error: unmergeable Isar steps"
+        | merge _ _ = error "sledgehammer_shrink: unmergeable Isar steps"
 
       fun try_merge metis_time (s1, i) (s2, j) =
-        (case get i metis_time |> Lazy.force of
-          NONE => (NONE, metis_time)
-        | SOME t1 =>
-          (case get j metis_time |> Lazy.force of
-            NONE => (NONE, metis_time)
-          | SOME t2 =>
-            let
-              val s12 = merge s1 s2
-              val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
-            in
-              case try_metis_quietly timeout (NONE, s12) () of
-                NONE => (NONE, metis_time)
-              | some_t12 =>
-                (SOME s12, metis_time
-                           |> replace (Time.zeroTime |> SOME |> Lazy.value) i
-                           |> replace (Lazy.value some_t12) j)
+        if not preplay then (merge s1 s2 |> SOME, metis_time)
+        else
+          (case get i metis_time |> Lazy.force of
+            (true, _) => (NONE, metis_time)
+          | (_, t1) =>
+            (case get j metis_time |> Lazy.force of
+              (true, _) => (NONE, metis_time)
+            | (_, t2) =>
+              let
+                val s12 = merge s1 s2
+                val timeout = time_mult merge_timeout_slack (Time.+(t1, t2))
+              in
+                case try_metis_quietly debug type_enc lam_trans ctxt timeout
+                (NONE, s12) () of
+                  (true, _) => (NONE, metis_time)
+                | exact_time =>
+                  (SOME s12, metis_time
+                             |> replace (zero_preplay_time |> Lazy.value) i
+                             |> replace (Lazy.value exact_time) j)
 
-            end))
+              end))
 
       fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' =
         if Inttab.is_empty cand_tab
@@ -286,20 +223,20 @@
           proof |> do_case_splits rich_ctxt
                 |>> shrink_top_level on_top_level rich_ctxt
       in
-        (proof, ext_time_add lower_level_time top_level_time)
+        (proof, add_preplay_time lower_level_time top_level_time)
       end
 
     and do_case_splits ctxt proof =
       let
         fun shrink_each_and_collect_time shrink candidates =
-          let fun f_m cand time = shrink cand ||> ext_time_add time
-          in fold_map f_m candidates no_time end
+          let fun f_m cand time = shrink cand ||> add_preplay_time time
+          in fold_map f_m candidates zero_preplay_time end
         val shrink_case_split =
           shrink_each_and_collect_time (do_proof false ctxt)
         fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) =
             let val (cases, time) = shrink_case_split cases
             in (Prove (qs, l, t, Case_Split (cases, facts)), time) end
-          | shrink step = (step, no_time)
+          | shrink step = (step, zero_preplay_time)
       in
         shrink_each_and_collect_time shrink proof
       end