merged
authorwenzelm
Sat, 15 Dec 2012 22:19:14 +0100
changeset 50560 e4dc37ec1427
parent 50559 89c0d2f13cca (diff)
parent 50554 0493efcc97e9 (current diff)
child 50561 9a733bd6c0ba
merged
--- a/src/HOL/TPTP/MaSh_Eval.thy	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Sat Dec 15 22:19:14 2012 +0100
@@ -41,7 +41,7 @@
 
 ML {*
 if do_it then
-  evaluate_mash_suggestions @{context} params (SOME prob_dir)
+  evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir)
       (prefix ^ "mash_suggestions") (prefix ^ "mash_eval")
 else
   ()
--- a/src/HOL/TPTP/MaSh_Export.thy	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Sat Dec 15 22:19:14 2012 +0100
@@ -79,7 +79,7 @@
 
 ML {*
 if do_it then
-  generate_prover_dependencies @{context} params thys false
+  generate_prover_dependencies @{context} params (1, NONE) thys false
       (prefix ^ "mash_prover_dependencies")
 else
   ()
@@ -87,7 +87,7 @@
 
 ML {*
 if do_it then
-  generate_prover_commands @{context} params thys
+  generate_prover_commands @{context} params (1, NONE) thys
       (prefix ^ "mash_prover_commands")
 else
   ()
--- a/src/HOL/TPTP/mash_eval.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -10,33 +10,41 @@
   type params = Sledgehammer_Provers.params
 
   val evaluate_mash_suggestions :
-    Proof.context -> params -> string option -> string -> string -> unit
+    Proof.context -> params -> int * int option -> string option -> string
+    -> string -> unit
 end;
 
 structure MaSh_Eval : MASH_EVAL =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Fact
+open Sledgehammer_MePo
 open Sledgehammer_MaSh
+open Sledgehammer_Provers
+open Sledgehammer_Isar
 
 val MePoN = "MePo"
 val MaShN = "MaSh"
 val MeShN = "MeSh"
 val IsarN = "Isar"
 
-fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name
+fun in_range (from, to) j =
+  j >= from andalso (to = NONE orelse j <= the to)
+
+fun evaluate_mash_suggestions ctxt params range prob_dir_name sugg_file_name
                               report_file_name =
   let
     val report_path = report_file_name |> Path.explode
     val _ = File.write report_path ""
     fun print s = (tracing s; File.append report_path (s ^ "\n"))
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
-      Sledgehammer_Isar.default_params ctxt []
+      default_params ctxt []
     val prover = hd provers
     val slack_max_facts = generous_max_facts (the max_facts)
     val sugg_path = sugg_file_name |> Path.explode
     val lines = sugg_path |> File.read_lines
-    val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
+    val css = clasimpset_rule_table_of ctxt
     val facts = all_facts ctxt true false Symtab.empty [] [] css
     val all_names = build_all_names nickname_of facts
     val mepo_ok = Unsynchronized.ref 0
@@ -46,7 +54,7 @@
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
     fun str_of_res label facts ({outcome, run_time, used_facts, ...}
-                                : Sledgehammer_Provers.prover_result) =
+                                : prover_result) =
       let val facts = facts |> map (fn ((name, _), _) => name ()) in
         "  " ^ label ^ ": " ^
         (if is_none outcome then
@@ -66,69 +74,78 @@
                   |> space_implode " "))
       end
     fun solve_goal (j, line) =
-      let
-        val (name, suggs) = extract_query line
-        val th =
-          case find_first (fn (_, th) => nickname_of th = name) facts of
-            SOME (_, th) => th
-          | NONE => error ("No fact called \"" ^ name ^ "\".")
-        val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
-        val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
-        val isar_deps = isar_dependencies_of all_names th |> these
-        val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
-        val mepo_facts =
-          Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
-              slack_max_facts NONE hyp_ts concl_t facts
-          |> Sledgehammer_MePo.weight_mepo_facts
-        val (mash_facts, mash_unks) =
-          find_mash_suggestions slack_max_facts suggs facts [] []
-          |>> weight_mash_facts
-        val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
-        val mesh_facts = mesh_facts slack_max_facts mess
-        val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
-        (* adapted from "mirabelle_sledgehammer.ML" *)
-        fun set_file_name heading (SOME dir) =
-            let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in
-              Config.put Sledgehammer_Provers.dest_dir dir
-              #> Config.put Sledgehammer_Provers.problem_prefix
-                            (prob_prefix ^ "__")
-              #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
-            end
-          | set_file_name _ NONE = I
-        fun prove ok heading get facts =
-          let
-            fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th)
-            val facts =
-              facts
-              |> map get
-              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
-              |> take (the max_facts)
-              |> map nickify
-            val ctxt = ctxt |> set_file_name heading prob_dir_name
-            val res as {outcome, ...} =
-              run_prover_for_mash ctxt params prover facts goal
-            val _ = if is_none outcome then ok := !ok + 1 else ()
-          in str_of_res heading facts res end
-        val [mepo_s, mash_s, mesh_s, isar_s] =
-          [fn () => prove mepo_ok MePoN fst mepo_facts,
-           fn () => prove mash_ok MaShN fst mash_facts,
-           fn () => prove mesh_ok MeShN I mesh_facts,
-           fn () => prove isar_ok IsarN fst isar_facts]
-          |> (* Par_List. *) map (fn f => f ())
-      in
-        ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
-         isar_s]
-        |> cat_lines |> print
-      end
+      if in_range range j then
+        let
+          val (name, suggs) = extract_query line
+          val th =
+            case find_first (fn (_, th) => nickname_of th = name) facts of
+              SOME (_, th) => th
+            | NONE => error ("No fact called \"" ^ name ^ "\".")
+          val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
+          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
+          val isar_deps = isar_dependencies_of all_names th |> these
+          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+          val mepo_facts =
+            mepo_suggested_facts ctxt params prover slack_max_facts NONE hyp_ts
+                concl_t facts
+            |> weight_mepo_facts
+          val (mash_facts, mash_unks) =
+            find_mash_suggestions slack_max_facts suggs facts [] []
+            |>> weight_mash_facts
+          val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
+          val mesh_facts = mesh_facts slack_max_facts mess
+          val isar_facts =
+            find_suggested_facts (map (rpair 1.0) isar_deps) facts
+          (* adapted from "mirabelle_sledgehammer.ML" *)
+          fun set_file_name heading (SOME dir) =
+              let
+                val prob_prefix =
+                  "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
+                  heading
+              in
+                Config.put dest_dir dir
+                #> Config.put problem_prefix (prob_prefix ^ "__")
+                #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
+              end
+            | set_file_name _ NONE = I
+          fun prove ok heading get facts =
+            let
+              fun nickify ((_, stature), th) =
+                ((K (nickname_of th), stature), th)
+              val facts =
+                facts
+                |> map get
+                |> maybe_instantiate_inducts ctxt hyp_ts concl_t
+                |> take (the max_facts)
+                |> map nickify
+              val ctxt = ctxt |> set_file_name heading prob_dir_name
+              val res as {outcome, ...} =
+                run_prover_for_mash ctxt params prover facts goal
+              val _ = if is_none outcome then ok := !ok + 1 else ()
+            in str_of_res heading facts res end
+          val [mepo_s, mash_s, mesh_s, isar_s] =
+            [fn () => prove mepo_ok MePoN fst mepo_facts,
+             fn () => prove mash_ok MaShN fst mash_facts,
+             fn () => prove mesh_ok MeShN I mesh_facts,
+             fn () => prove isar_ok IsarN fst isar_facts]
+            |> (* Par_List. *) map (fn f => f ())
+        in
+          ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
+           isar_s]
+          |> cat_lines |> print
+        end
+      else
+        ()
     fun total_of heading ok n =
       "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
       Real.fmt (StringCvt.FIX (SOME 1))
                (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
-    val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
+    val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
       [prover, string_of_int (the max_facts) ^ " facts",
        "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
-       the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
+       the_default "smart" lam_trans,
+       ATP_Util.string_from_time (timeout |> the_default one_year),
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val n = length lines
   in
--- a/src/HOL/TPTP/mash_export.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -16,11 +16,12 @@
   val generate_isar_dependencies :
     Proof.context -> theory list -> bool -> string -> unit
   val generate_prover_dependencies :
-    Proof.context -> params -> theory list -> bool -> string -> unit
+    Proof.context -> params -> int * int option -> theory list -> bool -> string
+    -> unit
   val generate_isar_commands :
     Proof.context -> string -> theory list -> string -> unit
   val generate_prover_commands :
-    Proof.context -> params -> theory list -> string -> unit
+    Proof.context -> params -> int * int option -> theory list -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> theory list -> int -> string -> unit
 end;
@@ -32,6 +33,9 @@
 open Sledgehammer_MePo
 open Sledgehammer_MaSh
 
+fun in_range (from, to) j =
+  j >= from andalso (to = NONE orelse j <= the to)
+
 fun thy_map_from_facts ths =
   ths |> rev
       |> map (snd #> `(theory_of_thm #> Context.theory_name))
@@ -108,24 +112,28 @@
      | NONE => isar_dependencies_of all_names th)
   |> these
 
-fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys
+fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
                                          file_name =
   let
     val path = file_name |> Path.explode
     val facts =
       all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
     val all_names = build_all_names nickname_of facts
-    fun do_fact (_, th) =
-      let
-        val name = nickname_of th
-        val deps =
-          isar_or_prover_dependencies_of ctxt params_opt facts all_names th NONE
-      in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
-    val lines = Par_List.map do_fact facts
+    fun do_fact (j, (_, th)) =
+      if in_range range j then
+        let
+          val name = nickname_of th
+          val deps =
+            isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+                                           NONE
+        in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
+      else
+        ""
+    val lines = Par_List.map do_fact (tag_list 1 facts)
   in File.write_list path lines end
 
 fun generate_isar_dependencies ctxt =
-  generate_isar_or_prover_dependencies ctxt NONE
+  generate_isar_or_prover_dependencies ctxt NONE (1, NONE)
 
 fun generate_prover_dependencies ctxt params =
   generate_isar_or_prover_dependencies ctxt (SOME params)
@@ -134,38 +142,42 @@
   Thm.legacy_get_kind th = "" orelse null isar_deps orelse
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
-fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
+fun generate_isar_or_prover_commands ctxt prover params_opt range thys
+                                     file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
     val facts = all_facts ctxt
     val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     val all_names = build_all_names nickname_of facts
-    fun do_fact ((name, ((_, stature), th)), prevs) =
-      let
-        val feats =
-          features_of ctxt prover (theory_of_thm th) stature [prop_of th]
-        val isar_deps = isar_dependencies_of all_names th
-        val deps =
-          isar_or_prover_dependencies_of ctxt params_opt facts all_names th
-                                         (SOME isar_deps)
-        val core =
-          escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
-          encode_features feats
-        val query =
-          if is_bad_query ctxt ho_atp th (these isar_deps) then ""
-          else "? " ^ core ^ "\n"
-        val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
-      in query ^ update end
+    fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
+      if in_range range j then
+        let
+          val feats =
+            features_of ctxt prover (theory_of_thm th) stature [prop_of th]
+          val isar_deps = isar_dependencies_of all_names th
+          val deps =
+            isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+                                           (SOME isar_deps)
+          val core =
+            escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
+            encode_features feats
+          val query =
+            if is_bad_query ctxt ho_atp th (these isar_deps) then ""
+            else "? " ^ core ^ "\n"
+          val update = "! " ^ core ^ "; " ^ escape_metas deps ^ "\n"
+        in query ^ update end
+      else
+        ""
     val thy_map = old_facts |> thy_map_from_facts
     val parents = fold (add_thy_parent_facts thy_map) thys []
     val new_facts = new_facts |> map (`(nickname_of o snd))
     val prevss = fst (split_last (parents :: map (single o fst) new_facts))
-    val lines = Par_List.map do_fact (new_facts ~~ prevss)
+    val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
   in File.write_list path lines end
 
 fun generate_isar_commands ctxt prover =
-  generate_isar_or_prover_commands ctxt prover NONE
+  generate_isar_or_prover_commands ctxt prover NONE (1, NONE)
 
 fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) =
   generate_isar_or_prover_commands ctxt prover (SOME params)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -283,9 +283,7 @@
 val monomorphic_term = ATP_Util.monomorphic_term
 val specialize_type = ATP_Util.specialize_type
 val eta_expand = ATP_Util.eta_expand
-
-fun time_limit NONE = I
-  | time_limit (SOME delay) = TimeLimit.timeLimit delay
+val time_limit = Sledgehammer_Util.time_limit
 
 fun DETERM_TIMEOUT delay tac st =
   Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ()))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -249,8 +249,6 @@
                          end)]
   end
 
-val the_timeout = the_default infinite_timeout
-
 fun extract_params mode default_params override_params =
   let
     val raw_params = rev override_params @ rev default_params
@@ -320,11 +318,10 @@
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize =
       if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
-    val timeout =
-      (if mode = Auto_Try then NONE else lookup_time "timeout") |> the_timeout
+    val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
     val preplay_timeout =
-      if mode = Auto_Try then Time.zeroTime
-      else lookup_time "preplay_timeout" |> the_timeout
+      if mode = Auto_Try then SOME Time.zeroTime
+      else lookup_time "preplay_timeout"
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -818,7 +818,7 @@
   if is_smt_prover ctxt prover then
     ()
   else
-    launch_thread timeout (fn () =>
+    launch_thread (timeout |> the_default one_day) (fn () =>
         let
           val thy = Proof_Context.theory_of ctxt
           val name = freshish_name ()
@@ -920,7 +920,10 @@
                   (commit false adds [] []; ([], next_commit_time ()))
                 else
                   (adds, next_commit)
-              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+              val timed_out =
+                case learn_timeout of
+                  SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
+                | NONE => false
             in (adds, ([name], n, next_commit, timed_out)) end
         val n =
           if null new_facts then
@@ -951,7 +954,10 @@
                   (commit false [] reps flops; ([], [], next_commit_time ()))
                 else
                   (reps, flops, next_commit)
-              val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout)
+              val timed_out =
+                case learn_timeout of
+                  SOME timeout => Time.> (Timer.checkRealTimer timer, timeout)
+                | NONE => false
             in ((reps, flops), (n, next_commit, timed_out)) end
         val n =
           if not run_prover orelse null old_facts then
@@ -1003,15 +1009,15 @@
     val num_facts = length facts
     val prover = hd provers
     fun learn auto_level run_prover =
-      mash_learn_facts ctxt params prover auto_level run_prover infinite_timeout
-                       facts
+      mash_learn_facts ctxt params prover auto_level run_prover NONE facts
       |> Output.urgent_message
   in
     if run_prover then
       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
        plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
-       " timeout: " ^ string_from_time timeout ^
-       ").\n\nCollecting Isar proofs first..."
+       (case timeout of
+          SOME timeout => " timeout: " ^ string_from_time timeout
+        | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
        |> Output.urgent_message;
        learn 1 false;
        "Now collecting automatic proofs. This may take several hours. You can \
@@ -1048,9 +1054,12 @@
     let
       fun maybe_learn () =
         if learn andalso not (Async_Manager.has_running_threads MaShN) andalso
-           Time.toSeconds timeout >= min_secs_for_learning then
-          let val timeout = time_mult learn_timeout_slack timeout in
-            launch_thread timeout
+           (timeout = NONE orelse
+            Time.toSeconds (the timeout) >= min_secs_for_learning) then
+          let
+            val timeout = Option.map (time_mult learn_timeout_slack) timeout
+          in
+            launch_thread (timeout |> the_default one_day)
                 (fn () => (true, mash_learn_facts ctxt params prover 2 false
                                                   timeout facts))
           end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -61,8 +61,12 @@
     val _ =
       print silent (fn () =>
           "Testing " ^ n_facts (map fst facts) ^
-          (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
-           else "") ^ "...")
+          (if verbose then
+             case timeout of
+               SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+             | _ => ""
+           else
+             "") ^ "...")
     val {goal, ...} = Proof.goal state
     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
@@ -101,10 +105,11 @@
    part of the timeout. *)
 val slack_msecs = 200
 
-fun new_timeout timeout run_time =
-  Int.min (Time.toMilliseconds timeout,
-           Time.toMilliseconds run_time + slack_msecs)
-  |> Time.fromMilliseconds
+fun new_timeout NONE _ = NONE
+  | new_timeout (SOME timeout) run_time =
+    Int.min (Time.toMilliseconds timeout,
+             Time.toMilliseconds run_time + slack_msecs)
+    |> Time.fromMilliseconds |> SOME
 
 (* The linear algorithm usually outperforms the binary algorithm when over 60%
    of the facts are actually needed. The binary algorithm is much more
@@ -222,11 +227,12 @@
      | {outcome = SOME TimedOut, preplay, ...} =>
        (NONE,
         (preplay,
-         fn _ => "Timeout: You can increase the time limit using the \
-                 \\"timeout\" option (e.g., \"timeout = " ^
-                 string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
-                 "\").",
-         ""))
+         fn _ =>
+            "Timeout: You can increase the time limit using the \"timeout\" \
+            \option (e.g., \"timeout = " ^
+            string_of_int (10 + Time.toMilliseconds
+                (timeout |> the_default (seconds 60.0)) div 1000) ^
+            "\").", ""))
      | {preplay, message, ...} =>
        (NONE, (preplay, prefix "Prover error: " o message, "")))
     handle ERROR msg =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -37,8 +37,8 @@
      isar_shrink : real,
      slice : bool,
      minimize : bool option,
-     timeout : Time.time,
-     preplay_timeout : Time.time,
+     timeout : Time.time option,
+     preplay_timeout : Time.time option,
      expect : string}
 
   type relevance_fudge =
@@ -330,8 +330,8 @@
    isar_shrink : real,
    slice : bool,
    minimize : bool option,
-   timeout : Time.time,
-   preplay_timeout : Time.time,
+   timeout : Time.time option,
+   preplay_timeout : Time.time option,
    expect : string}
 
 type relevance_fudge =
@@ -479,7 +479,7 @@
   let
     val {context = ctxt, facts, goal} = Proof.goal state
     val full_tac = Method.insert_tac facts i THEN tac ctxt i
-  in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
+  in time_limit timeout (try (Seq.pull o full_tac)) goal end
 
 fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
     metis_tac [type_enc] lam_trans
@@ -500,39 +500,40 @@
 fun play_one_line_proof mode debug verbose timeout pairs state i preferred
                         reconstrs =
   let
-    val _ =
-      if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then
-        Output.urgent_message "Preplaying proof..."
-      else
-        ()
-    val ths = pairs |> sort_wrt (fst o fst) |> map snd
     fun get_preferred reconstrs =
       if member (op =) reconstrs preferred then preferred
       else List.last reconstrs
-    fun play [] [] = Failed_to_Play (get_preferred reconstrs)
-      | play timed_outs [] =
-        Trust_Playable (get_preferred timed_outs, SOME timeout)
-      | play timed_out (reconstr :: reconstrs) =
-        let
-          val _ =
-            if verbose then
-              "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^
-              string_from_time timeout ^ "..."
-              |> Output.urgent_message
-            else
-              ()
-          val timer = Timer.startRealTimer ()
-        in
-          case timed_reconstructor reconstr debug timeout ths state i of
-            SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
-          | _ => play timed_out reconstrs
-        end
-        handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
   in
-    if timeout = Time.zeroTime then
+    if timeout = SOME Time.zeroTime then
       Trust_Playable (get_preferred reconstrs, NONE)
     else
-      play [] reconstrs
+      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)
+          | play timed_out (reconstr :: reconstrs) =
+            let
+              val _ =
+                if verbose then
+                  "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^
+                  (case timeout of
+                     SOME timeout => " for " ^ string_from_time timeout
+                   | NONE => "") ^ "..."
+                  |> Output.urgent_message
+                else
+                  ()
+              val timer = Timer.startRealTimer ()
+            in
+              case timed_reconstructor reconstr debug timeout ths state i of
+                SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer)
+              | _ => play timed_out reconstrs
+            end
+            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+      in play [] reconstrs end
   end
 
 
@@ -734,20 +735,27 @@
             val sound = is_type_enc_sound type_enc
             val real_ms = Real.fromInt o Time.toMilliseconds
             val slice_timeout =
-              ((real_ms time_left
-                |> (if slice < num_actual_slices - 1 then
-                      curry Real.min (time_frac * real_ms timeout)
-                    else
-                      I))
-               * 0.001) |> seconds
+              case time_left of
+                SOME time_left =>
+                ((real_ms time_left
+                  |> (if slice < num_actual_slices - 1 then
+                        curry Real.min (time_frac * real_ms (the timeout))
+                      else
+                        I))
+                 * 0.001)
+                |> seconds |> SOME
+              | NONE => NONE
             val generous_slice_timeout =
-              Time.+ (slice_timeout, atp_timeout_slack)
+              if mode = MaSh then NONE
+              else Option.map (curry Time.+ atp_timeout_slack) slice_timeout
             val _ =
               if debug then
                 quote name ^ " slice #" ^ string_of_int (slice + 1) ^
                 " with " ^ string_of_int num_facts ^ " fact" ^
-                plural_s num_facts ^ " for " ^
-                string_from_time slice_timeout ^ "..."
+                plural_s num_facts ^
+                (case slice_timeout of
+                   SOME timeout => " for " ^ string_from_time timeout
+                 | NONE => "") ^ "..."
                 |> Output.urgent_message
               else
                 ()
@@ -778,7 +786,8 @@
             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
+            val args = arguments ctxt full_proof extra
+                                 (slice_timeout |> the_default one_day)
                                  (ord, ord_info, sel_weights)
             val command =
               "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
@@ -790,8 +799,8 @@
               |> cons ("% " ^ command ^ "\n")
               |> File.write_list prob_path
             val ((output, run_time), (atp_proof, outcome)) =
-              TimeLimit.timeLimit generous_slice_timeout
-                                  Isabelle_System.bash_output command
+              time_limit generous_slice_timeout Isabelle_System.bash_output
+                         command
               |>> (if overlord then
                      prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
                    else
@@ -805,7 +814,7 @@
                       handle UNRECOGNIZED_ATP_PROOF () =>
                              ([], SOME ProofIncomplete)))
               handle TimeLimit.TimeOut =>
-                     (("", slice_timeout), ([], SOME TimedOut))
+                     (("", the slice_timeout), ([], SOME TimedOut))
             val outcome =
               case outcome of
                 NONE =>
@@ -826,9 +835,13 @@
         fun maybe_run_slice slice
                 (result as (cache, (_, run_time0, _, SOME _))) =
             let
-              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
+              val time_left =
+                Option.map
+                    (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+                    timeout
             in
-              if Time.<= (time_left, Time.zeroTime) then
+              if time_left <> NONE andalso
+                 Time.<= (the time_left, Time.zeroTime) then
                 result
               else
                 run_slice time_left cache slice
@@ -979,22 +992,25 @@
                        (repair_monomorph_context max_mono_iters
                             default_max_mono_iters max_new_mono_instances
                             default_max_new_mono_instances)
-        val ms = timeout |> Time.toMilliseconds
         val slice_timeout =
-          if slice < max_slices then
-            Int.min (ms,
-                Int.max (1000 * Config.get ctxt smt_slice_min_secs,
-                    Real.ceil (Config.get ctxt smt_slice_time_frac
-                               * Real.fromInt ms)))
-            |> Time.fromMilliseconds
+          if slice < max_slices andalso timeout <> NONE then
+            let val ms = timeout |> the |> Time.toMilliseconds in
+              Int.min (ms,
+                  Int.max (1000 * Config.get ctxt smt_slice_min_secs,
+                      Real.ceil (Config.get ctxt smt_slice_time_frac
+                                 * Real.fromInt ms)))
+              |> Time.fromMilliseconds |> SOME
+            end
           else
             timeout
         val num_facts = length facts
         val _ =
           if debug then
             quote name ^ " slice " ^ string_of_int slice ^ " with " ^
-            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^ " for " ^
-            string_from_time slice_timeout ^ "..."
+            string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+            (case slice_timeout of
+               SOME timeout => " for " ^ string_from_time timeout
+             | NONE => "") ^ "..."
             |> Output.urgent_message
           else
             ()
@@ -1004,7 +1020,7 @@
         val state_facts = these (try (#facts o Proof.goal) state)
         val (outcome, used_facts) =
           SMT_Solver.smt_filter_preprocess ctxt state_facts goal facts i
-          |> SMT_Solver.smt_filter_apply slice_timeout
+          |> SMT_Solver.smt_filter_apply (slice_timeout |> the_default one_day)
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn => if Exn.is_interrupt exn then
                           reraise exn
@@ -1022,10 +1038,14 @@
           | SOME (SMT_Failure.Abnormal_Termination _) => true (* kind of *)
           | SOME SMT_Failure.Out_Of_Memory => true
           | SOME (SMT_Failure.Other_Failure _) => true
-        val timeout = Time.- (timeout, Timer.checkRealTimer timer)
+        val timeout =
+          Option.map
+              (fn timeout => Time.- (timeout, Timer.checkRealTimer timer))
+              timeout
       in
         if too_many_facts_perhaps andalso slice < max_slices andalso
-           num_facts > 0 andalso Time.> (timeout, Time.zeroTime) then
+           num_facts > 0 andalso
+           (timeout = NONE orelse Time.> (the timeout, Time.zeroTime)) then
           let
             val new_num_facts =
               Real.ceil (Config.get ctxt smt_slice_fact_frac
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -23,7 +23,7 @@
   type one_line_params =
     play * string * (string * stature) list * minimize_command * int * int
   type isar_params =
-    bool * bool * Time.time * real * string Symtab.table
+    bool * bool * Time.time option * real * string Symtab.table
     * (string * stature) list vector * int Symtab.table * string proof * thm
 
   val smtN : string
@@ -592,7 +592,7 @@
   in chain_proof NONE end
 
 type isar_params =
-  bool * bool * Time.time * real * string Symtab.table
+  bool * bool * Time.time option * real * string Symtab.table
   * (string * stature) list vector * int Symtab.table * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
@@ -607,7 +607,7 @@
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
     val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
-    val preplay = preplay_timeout <> seconds 0.0
+    val preplay = preplay_timeout <> SOME Time.zeroTime
 
     fun isar_proof_of () =
       let
@@ -693,10 +693,12 @@
           |> redirect_graph axioms tainted
           |> map (do_inf true)
           |> append assms
-          |> (if not preplay andalso isar_shrink <= 1.0
-              then pair (false, (true, seconds 0.0)) #> swap
-              else shrink_proof debug ctxt type_enc lam_trans preplay
-                preplay_timeout (if isar_proofs then isar_shrink else 1000.0))
+          |> (if not preplay andalso isar_shrink <= 1.0 then
+                pair (false, (true, seconds 0.0)) #> swap
+              else
+                shrink_proof debug ctxt type_enc lam_trans preplay
+                    preplay_timeout
+                    (if isar_proofs then isar_shrink else 1000.0))
        (* |>> reorder_proof_to_minimize_jumps (* ? *) *)
           |>> chain_direct_proof
           |>> kill_useless_labels_in_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -68,7 +68,7 @@
                   {state, goal, subgoal, subgoal_count, facts} name =
   let
     val ctxt = Proof.context_of state
-    val hard_timeout = Time.+ (timeout, timeout)
+    val hard_timeout = time_mult 2.0 (timeout |> the_default one_day)
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, hard_timeout)
     val max_facts =
@@ -131,7 +131,7 @@
       in (outcome_code, message) end
   in
     if mode = Auto_Try then
-      let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+      let val (outcome_code, message) = time_limit timeout go () in
         (outcome_code,
          state
          |> outcome_code = someN
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -9,8 +9,8 @@
 sig
   type isar_step = Sledgehammer_Proof.isar_step
 	val shrink_proof : 
-    bool -> Proof.context -> string -> string -> bool -> Time.time -> real
-    -> isar_step list -> isar_step list * (bool * (bool * Time.time))
+    bool -> Proof.context -> string -> string -> bool -> Time.time option
+    -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time))
 end
 
 structure Sledgehammer_Shrink : SLEDGEHAMMER_SHRINK =
@@ -46,7 +46,7 @@
 
 (* Timing *)
 fun ext_time_add (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val no_time = (false, seconds 0.0)
+val no_time = (false, Time.zeroTime)
 fun take_time timeout tac arg =
   let val timing = Timing.start () in
     (TimeLimit.timeLimit timeout tac arg;
@@ -59,15 +59,18 @@
 fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout
                  isar_shrink proof =
 let
+  (* 60 seconds seems like a good interpreation of "no timeout" *)
+  val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
+
   (* handle metis preplay fail *)
   local
     open Unsynchronized
     val metis_fail = ref false
   in
     fun handle_metis_fail try_metis () =
-      try_metis () handle _ => (metis_fail := true ; SOME (seconds 0.0))
+      try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime)
     fun get_time lazy_time = 
-      if !metis_fail then SOME (seconds 0.0) else Lazy.force lazy_time
+      if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time
     val metis_fail = fn () => !metis_fail
   end
   
@@ -120,7 +123,7 @@
         |> maps (thms_of_name ctxt)
 
     fun try_metis timeout (succedent, Prove (_, _, t, byline)) =
-      if not preplay then (fn () => SOME (seconds 0.0)) else
+      if not preplay then (fn () => SOME Time.zeroTime) else
       (case byline of
         By_Metis fact_names =>
           let
@@ -154,7 +157,7 @@
           in
             take_time timeout (fn () => goal tac)
           end)
-      | try_metis _ _  = (fn () => SOME (seconds 0.0) )
+      | try_metis _ _  = (fn () => SOME Time.zeroTime)
 
     val try_metis_quietly = the_default NONE oo try oo try_metis
 
@@ -195,7 +198,7 @@
               NONE => (NONE, metis_time)
             | some_t12 =>
               (SOME s12, metis_time
-                         |> replace (seconds 0.0 |> SOME |> Lazy.value) i
+                         |> replace (Time.zeroTime |> SOME |> Lazy.value) i
                          |> replace (Lazy.value some_t12) j)
 
           end))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Dec 15 21:07:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Dec 15 22:19:14 2012 +0100
@@ -19,6 +19,9 @@
   val reserved_isar_keyword_table : unit -> unit Symtab.table
   val thms_in_proof : string Symtab.table option -> thm -> string list
   val thms_of_name : Proof.context -> string -> thm list
+  val one_day : Time.time
+  val one_year : Time.time
+  val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
 end;
 
@@ -119,6 +122,12 @@
     |> Source.exhaust
   end
 
+val one_day = seconds (24.0 * 60.0 * 60.0)
+val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
+
+fun time_limit NONE = I
+  | time_limit (SOME delay) = TimeLimit.timeLimit delay
+
 fun with_vanilla_print_mode f x =
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                            (print_mode_value ())) f x