tuning
authorblanchet
Fri Jan 31 16:10:39 2014 +0100 (2014-01-31)
changeset 552125832470d956e
parent 55211 5d027af93a08
child 55213 dcb36a2540bc
tuning
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 16:07:20 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 16:10:39 2014 +0100
     1.3 @@ -418,8 +418,8 @@
     1.4      val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     1.5      val i = 1
     1.6      fun set_file_name (SOME dir) =
     1.7 -        Config.put Sledgehammer_Prover.dest_dir dir
     1.8 -        #> Config.put Sledgehammer_Prover.problem_prefix
     1.9 +        Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
    1.10 +        #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
    1.11            ("prob_" ^ str0 (Position.line_of pos) ^ "__")
    1.12          #> Config.put SMT_Config.debug_files
    1.13            (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
    1.14 @@ -467,7 +467,7 @@
    1.15           : Sledgehammer_Prover.prover_result,
    1.16           time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
    1.17        let
    1.18 -        val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover_name
    1.19 +        val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover_name
    1.20          val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
    1.21          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.22          val facts =
     2.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 16:07:20 2014 +0100
     2.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Fri Jan 31 16:10:39 2014 +0100
     2.3 @@ -109,7 +109,7 @@
     2.4             extract_relevance_fudge args Sledgehammer_MePo.default_relevance_fudge
     2.5           val subgoal = 1
     2.6           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal subgoal ctxt
     2.7 -         val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
     2.8 +         val ho_atp = Sledgehammer_Prover_ATP.is_ho_atp ctxt prover
     2.9           val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
    2.10           val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.11           val facts =
     3.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 16:07:20 2014 +0100
     3.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 16:10:39 2014 +0100
     3.3 @@ -56,7 +56,7 @@
     3.4  
     3.5  ML {*
     3.6  if do_it then
     3.7 -  generate_features @{context} prover thys (prefix ^ "mash_features")
     3.8 +  generate_features @{context} thys (prefix ^ "mash_features")
     3.9  else
    3.10    ()
    3.11  *}
     4.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 16:07:20 2014 +0100
     4.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 16:10:39 2014 +0100
     4.3 @@ -182,7 +182,7 @@
     4.4  fun atp_tac ctxt completeness override_params timeout prover =
     4.5    let
     4.6      val ctxt =
     4.7 -      ctxt |> Config.put Sledgehammer_Prover.completish (completeness > 0)
     4.8 +      ctxt |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
     4.9      fun ref_of th = (Facts.named (Thm.derivation_name th), [])
    4.10    in
    4.11      Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
     5.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 16:07:20 2014 +0100
     5.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 31 16:10:39 2014 +0100
     5.3 @@ -29,6 +29,7 @@
     5.4  open Sledgehammer_MePo
     5.5  open Sledgehammer_MaSh
     5.6  open Sledgehammer_Prover
     5.7 +open Sledgehammer_Prover_ATP
     5.8  open Sledgehammer_Commands
     5.9  
    5.10  val prefix = Library.prefix
    5.11 @@ -125,8 +126,8 @@
    5.12                    "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
    5.13                    method
    5.14                in
    5.15 -                Config.put dest_dir dir
    5.16 -                #> Config.put problem_prefix (prob_prefix ^ "__")
    5.17 +                Config.put atp_dest_dir dir
    5.18 +                #> Config.put atp_problem_prefix (prob_prefix ^ "__")
    5.19                  #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
    5.20                end
    5.21              | set_file_name _ NONE = I
     6.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jan 31 16:07:20 2014 +0100
     6.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jan 31 16:10:39 2014 +0100
     6.3 @@ -9,24 +9,18 @@
     6.4  sig
     6.5    type params = Sledgehammer_Prover.params
     6.6  
     6.7 -  val generate_accessibility :
     6.8 -    Proof.context -> theory list -> bool -> string -> unit
     6.9 -  val generate_features :
    6.10 -    Proof.context -> string -> theory list -> string -> unit
    6.11 -  val generate_isar_dependencies :
    6.12 -    Proof.context -> int * int option -> theory list -> bool -> string -> unit
    6.13 -  val generate_prover_dependencies :
    6.14 -    Proof.context -> params -> int * int option -> theory list -> bool -> string
    6.15 -    -> unit
    6.16 -  val generate_isar_commands :
    6.17 -    Proof.context -> string -> (int * int option) * int -> theory list -> bool
    6.18 -    -> int -> string -> unit
    6.19 -  val generate_prover_commands :
    6.20 -    Proof.context -> params -> (int * int option) * int -> theory list -> bool
    6.21 -    -> int -> string -> unit
    6.22 -  val generate_mepo_suggestions :
    6.23 -    Proof.context -> params -> (int * int option) * int -> theory list -> bool
    6.24 -    -> int -> string -> unit
    6.25 +  val generate_accessibility : Proof.context -> theory list -> bool -> string -> unit
    6.26 +  val generate_features : Proof.context -> theory list -> string -> unit
    6.27 +  val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> bool ->
    6.28 +    string -> unit
    6.29 +  val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list ->
    6.30 +    bool -> string -> unit
    6.31 +  val generate_isar_commands : Proof.context -> string -> (int * int option) * int -> theory list ->
    6.32 +    bool -> int -> string -> unit
    6.33 +  val generate_prover_commands : Proof.context -> params -> (int * int option) * int ->
    6.34 +    theory list -> bool -> int -> string -> unit
    6.35 +  val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int ->
    6.36 +    theory list -> bool -> int -> string -> unit
    6.37    val generate_mesh_suggestions : int -> string -> string -> string -> unit
    6.38  end;
    6.39  
    6.40 @@ -34,6 +28,7 @@
    6.41  struct
    6.42  
    6.43  open Sledgehammer_Fact
    6.44 +open Sledgehammer_Prover_ATP
    6.45  open Sledgehammer_MePo
    6.46  open Sledgehammer_MaSh
    6.47  
    6.48 @@ -70,7 +65,7 @@
    6.49        |> map (apsnd (nickname_of_thm o snd))
    6.50    in fold do_fact facts []; () end
    6.51  
    6.52 -fun generate_features ctxt prover thys file_name =
    6.53 +fun generate_features ctxt thys file_name =
    6.54    let
    6.55      val path = file_name |> Path.explode
    6.56      val _ = File.write path ""
    6.57 @@ -80,8 +75,7 @@
    6.58          val name = nickname_of_thm th
    6.59          val feats =
    6.60            features_of ctxt (theory_of_thm th) 0 Symtab.empty stature false [prop_of th] |> map fst
    6.61 -        val s =
    6.62 -          encode_str name ^ ": " ^ encode_plain_features (sort_wrt hd feats) ^ "\n"
    6.63 +        val s = encode_str name ^ ": " ^ encode_plain_features (sort_wrt hd feats) ^ "\n"
    6.64        in File.append path s end
    6.65    in List.app do_fact facts end
    6.66  
    6.67 @@ -148,7 +142,7 @@
    6.68  fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
    6.69                                       linearize max_suggs file_name =
    6.70    let
    6.71 -    val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
    6.72 +    val ho_atp = is_ho_atp ctxt prover
    6.73      val path = file_name |> Path.explode
    6.74      val facts = all_facts ctxt
    6.75      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    6.76 @@ -229,7 +223,7 @@
    6.77  fun generate_mepo_suggestions ctxt (params as {provers = prover :: _, ...})
    6.78                                (range, step) thys linearize max_suggs file_name =
    6.79    let
    6.80 -    val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover
    6.81 +    val ho_atp = is_ho_atp ctxt prover
    6.82      val path = file_name |> Path.explode
    6.83      val facts = all_facts ctxt
    6.84      val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
     7.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 16:07:20 2014 +0100
     7.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Fri Jan 31 16:10:39 2014 +0100
     7.3 @@ -21,6 +21,7 @@
     7.4  open Sledgehammer_Util
     7.5  open Sledgehammer_Fact
     7.6  open Sledgehammer_Prover
     7.7 +open Sledgehammer_Prover_ATP
     7.8  open Sledgehammer_Prover_Minimize
     7.9  open Sledgehammer_MaSh
    7.10  open Sledgehammer_Commands
     8.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 31 16:07:20 2014 +0100
     8.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 31 16:10:39 2014 +0100
     8.3 @@ -18,9 +18,8 @@
     8.4    datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
     8.5  
     8.6    datatype scope = Global | Local | Assum | Chained
     8.7 -  datatype status =
     8.8 -    General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def |
     8.9 -    Rec_Def
    8.10 +  datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
    8.11 +
    8.12    type stature = scope * status
    8.13  
    8.14    datatype strictness = Strict | Non_Strict
    8.15 @@ -130,8 +129,8 @@
    8.16  datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
    8.17  
    8.18  datatype scope = Global | Local | Assum | Chained
    8.19 -datatype status =
    8.20 -  General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
    8.21 +datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
    8.22 +
    8.23  type stature = scope * status
    8.24  
    8.25  datatype order =
    8.26 @@ -906,7 +905,7 @@
    8.27                 else
    8.28                   `make_fixed_type_const s, []), map term Ts)
    8.29      | term (TFree (s, _)) = AType ((`make_tfree s, []), [])
    8.30 -    | term (TVar (z as (_, S))) = AType ((tvar_name z, []), [])
    8.31 +    | term (TVar z) = AType ((tvar_name z, []), [])
    8.32    in term end
    8.33  
    8.34  fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys)
    8.35 @@ -1266,8 +1265,8 @@
    8.36    end
    8.37    handle TERM _ => @{const True}
    8.38  
    8.39 -(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "="
    8.40 -   for technical reasons. *)
    8.41 +(* Satallax prefers "=" to "<=>" (for definitions) and Metis (CNF) requires "=" for technical
    8.42 +   reasons. *)
    8.43  fun should_use_iff_for_eq CNF _ = false
    8.44    | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format)
    8.45    | should_use_iff_for_eq _ _ = true
    8.46 @@ -1305,14 +1304,8 @@
    8.47  fun make_conjecture ctxt format type_enc =
    8.48    map (fn ((name, stature), (role, t)) =>
    8.49            let
    8.50 -            (* FIXME: The commented-out code is a hack to get decent performance
    8.51 -               out of LEO-II on the TPTP THF benchmarks. *)
    8.52              val role =
    8.53 -              if (* is_format_with_defs format andalso *)
    8.54 -                 role <> Conjecture andalso is_legitimate_tptp_def t then
    8.55 -                Definition
    8.56 -              else
    8.57 -                role
    8.58 +              if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
    8.59            in
    8.60              t |> role = Conjecture ? s_not
    8.61                |> make_formula ctxt format type_enc true name stature role
    8.62 @@ -2526,6 +2519,7 @@
    8.63              else pair_append (do_alias (ary - 1)))
    8.64        end
    8.65    in do_alias end
    8.66 +
    8.67  fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
    8.68          (s, {min_ary, types, in_conj, ...} : sym_info) =
    8.69    (case unprefix_and_unascii const_prefix s of
    8.70 @@ -2538,6 +2532,7 @@
    8.71      else
    8.72        ([], [])
    8.73    | NONE => ([], []))
    8.74 +
    8.75  fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab =
    8.76    ([], [])
    8.77    |> uncurried_aliases
    8.78 @@ -2619,9 +2614,8 @@
    8.79  
    8.80  val app_op_and_predicator_threshold = 45
    8.81  
    8.82 -fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans
    8.83 -                        uncurried_aliases readable_names presimp hyp_ts concl_t
    8.84 -                        facts =
    8.85 +fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
    8.86 +    readable_names presimp hyp_ts concl_t facts =
    8.87    let
    8.88      val thy = Proof_Context.theory_of ctxt
    8.89      val type_enc = type_enc |> adjust_type_enc format
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 31 16:07:20 2014 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Jan 31 16:10:39 2014 +0100
     9.3 @@ -18,6 +18,7 @@
     9.4    val noneN : string
     9.5    val timeoutN : string
     9.6    val unknownN : string
     9.7 +
     9.8    val string_of_factss : (string * fact list) list -> string
     9.9    val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
    9.10      ((string * string list) list -> string -> minimize_command) -> Proof.state ->
    9.11 @@ -28,12 +29,12 @@
    9.12  struct
    9.13  
    9.14  open ATP_Util
    9.15 +open ATP_Proof
    9.16  open ATP_Problem_Generate
    9.17 -open ATP_Proof
    9.18 -open ATP_Proof_Reconstruct
    9.19  open Sledgehammer_Util
    9.20  open Sledgehammer_Fact
    9.21  open Sledgehammer_Prover
    9.22 +open Sledgehammer_Prover_ATP
    9.23  open Sledgehammer_Prover_Minimize
    9.24  open Sledgehammer_MaSh
    9.25  
    9.26 @@ -196,9 +197,7 @@
    9.27        in (outcome_code, state) end
    9.28      else
    9.29        (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
    9.30 -                            ((fn (outcome_code, message) =>
    9.31 -                                 (verbose orelse outcome_code = someN,
    9.32 -                                  message ())) o go);
    9.33 +         ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
    9.34         (unknownN, state))
    9.35    end
    9.36  
    9.37 @@ -289,9 +288,6 @@
    9.38              |> (if blocking then Par_List.map else map) (launch problem #> fst)
    9.39              |> max_outcome_code |> rpair state
    9.40          end
    9.41 -
    9.42 -      fun maybe f (accum as (outcome_code, _)) =
    9.43 -        accum |> (mode = Normal orelse outcome_code <> someN) ? f
    9.44      in
    9.45        (if blocking then launch_provers state
    9.46         else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 31 16:07:20 2014 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Jan 31 16:10:39 2014 +0100
    10.3 @@ -20,25 +20,22 @@
    10.4  
    10.5    val instantiate_inducts : bool Config.T
    10.6    val no_fact_override : fact_override
    10.7 -  val fact_of_ref :
    10.8 -    Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
    10.9 -    -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   10.10 +
   10.11 +  val fact_of_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table ->
   10.12 +    Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   10.13    val backquote_thm : Proof.context -> thm -> string
   10.14    val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
   10.15    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   10.16 -  val build_name_tables :
   10.17 -    (thm -> string) -> ('a * thm) list
   10.18 -    -> string Symtab.table * string Symtab.table
   10.19 -  val maybe_instantiate_inducts :
   10.20 -    Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
   10.21 -    -> (((unit -> string) * 'a) * thm) list
   10.22 +  val build_name_tables : (thm -> string) -> ('a * thm) list ->
   10.23 +    string Symtab.table * string Symtab.table
   10.24 +  val maybe_instantiate_inducts : Proof.context -> term list -> term ->
   10.25 +    (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
   10.26    val fact_of_raw_fact : raw_fact -> fact
   10.27 -  val all_facts :
   10.28 -    Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
   10.29 -    -> status Termtab.table -> raw_fact list
   10.30 -  val nearly_all_facts :
   10.31 -    Proof.context -> bool -> fact_override -> unit Symtab.table
   10.32 -    -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
   10.33 +
   10.34 +  val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
   10.35 +    status Termtab.table -> raw_fact list
   10.36 +  val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table ->
   10.37 +    status Termtab.table -> thm list -> term list -> term -> raw_fact list
   10.38    val drop_duplicate_facts : raw_fact list -> raw_fact list
   10.39  end;
   10.40  
   10.41 @@ -47,7 +44,6 @@
   10.42  
   10.43  open ATP_Util
   10.44  open ATP_Problem_Generate
   10.45 -open Metis_Tactic
   10.46  open Sledgehammer_Util
   10.47  
   10.48  type raw_fact = ((unit -> string) * stature) * thm
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:07:20 2014 +0100
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 16:10:39 2014 +0100
    11.3 @@ -26,12 +26,10 @@
    11.4  open ATP_Util
    11.5  open ATP_Problem
    11.6  open ATP_Proof
    11.7 -open ATP_Problem_Generate
    11.8  open ATP_Proof_Reconstruct
    11.9  open Sledgehammer_Util
   11.10  open Sledgehammer_Reconstructor
   11.11  open Sledgehammer_Isar_Proof
   11.12 -open Sledgehammer_Isar_Annotate
   11.13  open Sledgehammer_Isar_Preplay
   11.14  open Sledgehammer_Isar_Compress
   11.15  open Sledgehammer_Isar_Try0
   11.16 @@ -344,7 +342,7 @@
   11.17          and isar_proof outer fix assms lems infs =
   11.18            Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
   11.19  
   11.20 -        val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) =
   11.21 +        val (preplay_data as {overall_preplay_outcome, ...}, isar_proof) =
   11.22            refute_graph
   11.23  (*
   11.24            |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
   11.25 @@ -356,15 +354,14 @@
   11.26            |> isar_proof true params assms lems
   11.27            |> postprocess_remove_unreferenced_steps I
   11.28            |> relabel_proof_canonically
   11.29 -          |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
   11.30 +          |> `(proof_preplay_data debug ctxt metis_type_enc metis_lam_trans do_preplay
   11.31                 preplay_timeout)
   11.32  
   11.33          val (play_outcome, isar_proof) =
   11.34            isar_proof
   11.35 -          |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
   11.36 -               preplay_interface
   11.37 -          |> try0_isar ? try0 preplay_timeout preplay_interface
   11.38 -          |> postprocess_remove_unreferenced_steps (try0_isar ? min_deps_of_step preplay_interface)
   11.39 +          |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0) preplay_data
   11.40 +          |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
   11.41 +          |> postprocess_remove_unreferenced_steps (try0_isar ? minimal_deps_of_step preplay_data)
   11.42            |> `overall_preplay_outcome
   11.43            ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
   11.44  
   11.45 @@ -381,7 +378,7 @@
   11.46            let
   11.47              val msg =
   11.48                (if verbose then
   11.49 -                let val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in
   11.50 +                let val num_steps = add_isar_steps (steps_of_proof isar_proof) 0 in
   11.51                    [string_of_int num_steps ^ " step" ^ plural_s num_steps]
   11.52                  end
   11.53                 else
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:07:20 2014 +0100
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML	Fri Jan 31 16:10:39 2014 +0100
    12.3 @@ -1,17 +1,15 @@
    12.4  (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
    12.5 +    Author:     Steffen Juilf Smolka, TU Muenchen
    12.6      Author:     Jasmin Blanchette, TU Muenchen
    12.7 -    Author:     Steffen Juilf Smolka, TU Muenchen
    12.8  
    12.9 -Supplements term with a locally minmal, complete set of type constraints.
   12.10 -Complete: The constraints suffice to infer the term's types.
   12.11 -Minimal: Reducing the set of constraints further will make it incomplete.
   12.12 +Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints
   12.13 +suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it
   12.14 +incomplete.
   12.15  
   12.16 -When configuring the pretty printer appropriately, the constraints will show up
   12.17 -as type annotations when printing the term. This allows the term to be printed
   12.18 -and reparsed without a change of types.
   12.19 +When configuring the pretty printer appropriately, the constraints will show up as type annotations
   12.20 +when printing the term. This allows the term to be printed and reparsed without a change of types.
   12.21  
   12.22 -NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
   12.23 -syntax.
   12.24 +NOTE: Terms should be unchecked before calling annotate_types to avoid awkward syntax.
   12.25  *)
   12.26  
   12.27  signature SLEDGEHAMMER_ISAR_ANNOTATE =
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 16:07:20 2014 +0100
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 16:10:39 2014 +0100
    13.3 @@ -9,9 +9,9 @@
    13.4  signature SLEDGEHAMMER_ISAR_COMPRESS =
    13.5  sig
    13.6    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    13.7 -  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
    13.8 +  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
    13.9  
   13.10 -  val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
   13.11 +  val compress_proof : real -> preplay_data -> isar_proof -> isar_proof
   13.12  end;
   13.13  
   13.14  structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
   13.15 @@ -22,6 +22,8 @@
   13.16  open Sledgehammer_Isar_Proof
   13.17  open Sledgehammer_Isar_Preplay
   13.18  
   13.19 +val dummy_isar_step = Let (Term.dummy, Term.dummy)
   13.20 +
   13.21  (* traverses steps in post-order and collects the steps with the given labels *)
   13.22  fun collect_successors steps lbls =
   13.23    let
   13.24 @@ -94,14 +96,14 @@
   13.25  (* Precondition: The proof must be labeled canonically
   13.26     (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
   13.27  fun compress_proof compress_isar
   13.28 -    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
   13.29 +    ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data) proof =
   13.30    if compress_isar <= 1.0 then
   13.31      proof
   13.32    else
   13.33      let
   13.34        val (compress_further, decrement_step_count) =
   13.35          let
   13.36 -          val number_of_steps = add_proof_steps (steps_of_proof proof) 0
   13.37 +          val number_of_steps = add_isar_steps (steps_of_proof proof) 0
   13.38            val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
   13.39            val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
   13.40          in
   13.41 @@ -112,17 +114,17 @@
   13.42          let
   13.43            fun add_refs (Let _) = I
   13.44              | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
   13.45 -              fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
   13.46 +              fold (fn key => Canonical_Label_Tab.cons_list (key, v)) lfs
   13.47  
   13.48            val tab =
   13.49 -            Canonical_Lbl_Tab.empty
   13.50 +            Canonical_Label_Tab.empty
   13.51              |> fold_isar_steps add_refs (steps_of_proof proof)
   13.52              (* "rev" should have the same effect as "sort canonical_label_ord" *)
   13.53 -            |> Canonical_Lbl_Tab.map (K rev)
   13.54 +            |> Canonical_Label_Tab.map (K rev)
   13.55              |> Unsynchronized.ref
   13.56  
   13.57 -          fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
   13.58 -          fun set_successors l refs = tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
   13.59 +          fun get_successors l = Canonical_Label_Tab.lookup_list (!tab) l
   13.60 +          fun set_successors l refs = tab := Canonical_Label_Tab.update (l, refs) (!tab)
   13.61            fun replace_successor old new dest =
   13.62              get_successors dest
   13.63              |> Ord_List.remove canonical_label_ord old
   13.64 @@ -179,8 +181,7 @@
   13.65                Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
   13.66              | _ => step)
   13.67  
   13.68 -      (** top_level compression: eliminate steps by merging them into their
   13.69 -          successors **)
   13.70 +      (** top_level compression: eliminate steps by merging them into their successors **)
   13.71  
   13.72        fun compress_top_level steps =
   13.73          let
   13.74 @@ -193,10 +194,12 @@
   13.75  
   13.76            val cand_ord = pairself cand_key #> compression_ord
   13.77  
   13.78 -          fun pop_next_cand candidates =
   13.79 -            (case max_list cand_ord candidates of
   13.80 -              NONE => (NONE, [])
   13.81 -            | cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates))
   13.82 +          fun pop_next_cand [] = (NONE, [])
   13.83 +            | pop_next_cand (cands as (cand :: cands')) =
   13.84 +              let
   13.85 +                val best as (i, _, _) =
   13.86 +                  fold (fn x => fn y => if cand_ord (x, y) = GREATER then x else y) cands' cand
   13.87 +              in (SOME best, filter_out (fn (j, _, _) => j = i) cands) end
   13.88  
   13.89            val candidates =
   13.90              let
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 16:07:20 2014 +0100
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 16:10:39 2014 +0100
    14.3 @@ -7,26 +7,25 @@
    14.4  
    14.5  signature SLEDGEHAMMER_ISAR_MINIMIZE =
    14.6  sig
    14.7 -  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
    14.8 +  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
    14.9    type isar_step = Sledgehammer_Isar_Proof.isar_step
   14.10    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   14.11  
   14.12 -  val min_deps_of_step : preplay_interface -> isar_step -> isar_step
   14.13 +  val minimal_deps_of_step : preplay_data -> isar_step -> isar_step
   14.14    val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
   14.15  end;
   14.16  
   14.17  structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
   14.18  struct
   14.19  
   14.20 -open Sledgehammer_Util
   14.21  open Sledgehammer_Reconstructor
   14.22  open Sledgehammer_Isar_Proof
   14.23  open Sledgehammer_Isar_Preplay
   14.24  
   14.25  val slack = seconds 0.1
   14.26  
   14.27 -fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
   14.28 -  | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
   14.29 +fun minimal_deps_of_step (_ : preplay_data) (step as Let _) = step
   14.30 +  | minimal_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
   14.31        (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
   14.32      (case get_preplay_outcome l of
   14.33        Played time =>
   14.34 @@ -57,12 +56,8 @@
   14.35        end
   14.36      and do_steps [] = ([], [])
   14.37        | do_steps steps =
   14.38 -        let
   14.39 -          (* the last step is always implicitly referenced *)
   14.40 -          val (steps, (refed, concl)) =
   14.41 -            split_last steps
   14.42 -            ||> do_refed_step
   14.43 -        in
   14.44 +        (* the last step is always implicitly referenced *)
   14.45 +        let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in
   14.46            fold_rev do_step steps (refed, [concl])
   14.47          end
   14.48      and do_step step (refed, accu) =
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 16:07:20 2014 +0100
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 16:10:39 2014 +0100
    15.3 @@ -8,26 +8,25 @@
    15.4  signature SLEDGEHAMMER_ISAR_PREPLAY =
    15.5  sig
    15.6    type play_outcome = Sledgehammer_Reconstructor.play_outcome
    15.7 +  type isar_step = Sledgehammer_Isar_Proof.isar_step
    15.8    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    15.9 -  type isar_step = Sledgehammer_Isar_Proof.isar_step
   15.10    type label = Sledgehammer_Isar_Proof.label
   15.11  
   15.12 -  val trace: bool Config.T
   15.13 +  val trace : bool Config.T
   15.14  
   15.15 -  type preplay_interface =
   15.16 +  type preplay_data =
   15.17      {get_preplay_outcome: label -> play_outcome,
   15.18       set_preplay_outcome: label -> play_outcome -> unit,
   15.19       preplay_quietly: Time.time -> isar_step -> play_outcome,
   15.20       overall_preplay_outcome: isar_proof -> play_outcome}
   15.21  
   15.22 -  val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
   15.23 -    isar_proof -> preplay_interface
   15.24 +  val proof_preplay_data : bool -> Proof.context -> string -> string -> bool -> Time.time ->
   15.25 +    isar_proof -> preplay_data
   15.26  end;
   15.27  
   15.28  structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
   15.29  struct
   15.30  
   15.31 -open ATP_Util
   15.32  open Sledgehammer_Util
   15.33  open Sledgehammer_Reconstructor
   15.34  open Sledgehammer_Isar_Proof
   15.35 @@ -148,7 +147,7 @@
   15.36  
   15.37  (*** proof preplay interface ***)
   15.38  
   15.39 -type preplay_interface =
   15.40 +type preplay_data =
   15.41    {get_preplay_outcome: label -> play_outcome,
   15.42     set_preplay_outcome: label -> play_outcome -> unit,
   15.43     preplay_quietly: Time.time -> isar_step -> play_outcome,
   15.44 @@ -186,13 +185,13 @@
   15.45  
   15.46     Precondition: The proof must be labeled canonically; cf.
   15.47     "Slegehammer_Proof.relabel_proof_canonically". *)
   15.48 -fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   15.49 +fun proof_preplay_data debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
   15.50    if not do_preplay then
   15.51      (* the "dont_preplay" option pretends that everything works just fine *)
   15.52      {get_preplay_outcome = K (Played Time.zeroTime),
   15.53       set_preplay_outcome = K (K ()),
   15.54       preplay_quietly = K (K (Played Time.zeroTime)),
   15.55 -     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_interface
   15.56 +     overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_data
   15.57    else
   15.58      let
   15.59        val ctxt = enrich_context_with_local_facts proof ctxt
   15.60 @@ -200,15 +199,14 @@
   15.61        fun preplay quietly timeout step =
   15.62          preplay_raw debug type_enc lam_trans ctxt timeout step
   15.63          handle exn =>
   15.64 -               if Exn.is_interrupt exn then
   15.65 -                 reraise exn
   15.66 -               else
   15.67 -                (if not quietly andalso debug then
   15.68 -                   warning ("Preplay failure:\n  " ^ @{make_string} step ^ "\n  " ^
   15.69 -                     @{make_string} exn)
   15.70 -                 else
   15.71 -                   ();
   15.72 -                 Play_Failed)
   15.73 +          if Exn.is_interrupt exn then
   15.74 +            reraise exn
   15.75 +          else
   15.76 +            (if not quietly andalso debug then
   15.77 +               warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
   15.78 +             else
   15.79 +               ();
   15.80 +             Play_Failed)
   15.81  
   15.82        (* preplay steps treating exceptions like timeouts *)
   15.83        fun preplay_quietly timeout = preplay true timeout
   15.84 @@ -219,22 +217,22 @@
   15.85              (case label_of_step step of
   15.86                NONE => tab
   15.87              | SOME l =>
   15.88 -              Canonical_Lbl_Tab.update_new
   15.89 +              Canonical_Label_Tab.update_new
   15.90                  (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
   15.91 -            handle Canonical_Lbl_Tab.DUP _ =>
   15.92 +            handle Canonical_Label_Tab.DUP _ =>
   15.93                raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
   15.94          in
   15.95 -          Canonical_Lbl_Tab.empty
   15.96 +          Canonical_Label_Tab.empty
   15.97            |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
   15.98            |> Unsynchronized.ref
   15.99          end
  15.100  
  15.101        fun get_preplay_outcome l =
  15.102 -        Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
  15.103 +        Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
  15.104          handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
  15.105  
  15.106        fun set_preplay_outcome l result =
  15.107 -        preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
  15.108 +        preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
  15.109  
  15.110        val result_of_step =
  15.111          try (label_of_step #> the #> get_preplay_outcome)
    16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:07:20 2014 +0100
    16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 16:10:39 2014 +0100
    16.3 @@ -27,32 +27,23 @@
    16.4    val no_facts : facts
    16.5  
    16.6    val label_ord : label * label -> order
    16.7 -
    16.8 -  val dummy_isar_step : isar_step
    16.9 -
   16.10    val string_of_label : label -> string
   16.11  
   16.12 -  val fix_of_proof : isar_proof -> (string * typ) list
   16.13 -  val assms_of_proof : isar_proof -> (label * term) list
   16.14    val steps_of_proof : isar_proof -> isar_step list
   16.15  
   16.16    val label_of_step : isar_step -> label option
   16.17 -  val subproofs_of_step : isar_step -> isar_proof list option
   16.18    val byline_of_step : isar_step -> (facts * proof_method list list) option
   16.19  
   16.20 -  val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
   16.21    val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
   16.22 +  val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
   16.23 +  val add_isar_steps : isar_step list -> int -> int
   16.24  
   16.25 -  val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
   16.26 -
   16.27 -  val add_proof_steps : isar_step list -> int -> int
   16.28 +  structure Canonical_Label_Tab : TABLE
   16.29  
   16.30    (** canonical proof labels: 1, 2, 3, ... in postorder **)
   16.31    val canonical_label_ord : (label * label) -> order
   16.32    val relabel_proof_canonically : isar_proof -> isar_proof
   16.33  
   16.34 -  structure Canonical_Lbl_Tab : TABLE
   16.35 -
   16.36    val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
   16.37  end;
   16.38  
   16.39 @@ -87,12 +78,8 @@
   16.40  
   16.41  val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
   16.42  
   16.43 -val dummy_isar_step = Let (Term.dummy, Term.dummy)
   16.44 -
   16.45  fun string_of_label (s, num) = s ^ string_of_int num
   16.46  
   16.47 -fun fix_of_proof (Proof (fix, _, _)) = fix
   16.48 -fun assms_of_proof (Proof (_, assms, _)) = assms
   16.49  fun steps_of_proof (Proof (_, _, steps)) = steps
   16.50  
   16.51  fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
   16.52 @@ -104,26 +91,24 @@
   16.53  fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
   16.54    | byline_of_step _ = NONE
   16.55  
   16.56 -fun fold_isar_steps f = fold (fold_isar_step f)
   16.57 -and fold_isar_step f step =
   16.58 +fun fold_isar_step f step =
   16.59    fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
   16.60 +and fold_isar_steps f = fold (fold_isar_step f)
   16.61  
   16.62  fun map_isar_steps f =
   16.63    let
   16.64 -    fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps)
   16.65 -    and do_step (step as Let _) = f step
   16.66 -      | do_step (Prove (qs, xs, l, t, subproofs, by)) =
   16.67 -        f (Prove (qs, xs, l, t, map do_proof subproofs, by))
   16.68 -  in
   16.69 -    do_proof
   16.70 -  end
   16.71 +    fun map_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map map_step steps)
   16.72 +    and map_step (step as Let _) = f step
   16.73 +      | map_step (Prove (qs, xs, l, t, subproofs, by)) =
   16.74 +        f (Prove (qs, xs, l, t, map map_proof subproofs, by))
   16.75 +  in map_proof end
   16.76  
   16.77 -val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
   16.78 +val add_isar_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
   16.79  
   16.80  (* canonical proof labels: 1, 2, 3, ... in post traversal order *)
   16.81  fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
   16.82  
   16.83 -structure Canonical_Lbl_Tab = Table(
   16.84 +structure Canonical_Label_Tab = Table(
   16.85    type key = label
   16.86    val ord = canonical_label_ord)
   16.87  
   16.88 @@ -220,15 +205,15 @@
   16.89        | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
   16.90  
   16.91      val using_facts = with_facts "" (enclose "using " " ")
   16.92 +    fun by_facts meth ls ss = "by " ^ with_facts meth (enclose ("by (" ^ meth) ")") ls ss
   16.93  
   16.94      (* Local facts are always passed via "using", which affects "meson" and "metis". This is
   16.95         arguably stylistically superior, because it emphasises the structure of the proof. It is also
   16.96         more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
   16.97         and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
   16.98      fun of_method ls ss Metis_Method =
   16.99 -        using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ss
  16.100 -      | of_method ls ss Meson_Method =
  16.101 -        using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
  16.102 +        using_facts ls [] ^ by_facts (metis_call type_enc lam_trans) [] ss
  16.103 +      | of_method ls ss Meson_Method = using_facts ls [] ^ by_facts "meson" [] ss
  16.104        | of_method ls ss meth = using_facts ls ss ^ by_method meth
  16.105  
  16.106      fun of_byline ind (ls, ss) meth =
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 16:07:20 2014 +0100
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 16:10:39 2014 +0100
    17.3 @@ -9,9 +9,9 @@
    17.4  signature SLEDGEHAMMER_ISAR_TRY0 =
    17.5  sig
    17.6    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    17.7 -  type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
    17.8 +  type preplay_data = Sledgehammer_Isar_Preplay.preplay_data
    17.9  
   17.10 -  val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
   17.11 +  val try0_isar_proof : Time.time -> preplay_data -> isar_proof -> isar_proof
   17.12  end;
   17.13  
   17.14  structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
   17.15 @@ -30,7 +30,7 @@
   17.16  
   17.17  fun try0_step _ _ (step as Let _) = step
   17.18    | try0_step preplay_timeout
   17.19 -      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface)
   17.20 +      ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_data)
   17.21        (step as Prove (_, _, l, _, _, _)) =
   17.22      let
   17.23        val timeout =
   17.24 @@ -48,6 +48,6 @@
   17.25        | NONE => step)
   17.26      end
   17.27  
   17.28 -val try0 = map_isar_steps oo try0_step
   17.29 +val try0_isar_proof = map_isar_steps oo try0_step
   17.30  
   17.31  end;
    18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:07:20 2014 +0100
    18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 16:10:39 2014 +0100
    18.3 @@ -65,10 +65,6 @@
    18.4      params -> ((string * string list) list -> string -> minimize_command)
    18.5      -> prover_problem -> prover_result
    18.6  
    18.7 -  val dest_dir : string Config.T
    18.8 -  val problem_prefix : string Config.T
    18.9 -  val completish : bool Config.T
   18.10 -  val atp_full_names : bool Config.T
   18.11    val SledgehammerN : string
   18.12    val plain_metis : reconstructor
   18.13    val overlord_file_location_of_prover : string -> string * string
   18.14 @@ -76,13 +72,8 @@
   18.15    val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
   18.16    val is_reconstructor : string -> bool
   18.17    val is_atp : theory -> string -> bool
   18.18 -  val is_ho_atp: Proof.context -> string -> bool
   18.19 -  val supported_provers : Proof.context -> unit
   18.20 -  val kill_provers : unit -> unit
   18.21 -  val running_provers : unit -> unit
   18.22 -  val messages : int option -> unit
   18.23 +  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
   18.24    val is_fact_chained : (('a * stature) * 'b) -> bool
   18.25 -  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
   18.26    val filter_used_facts :
   18.27      bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
   18.28      ((''a * stature) * 'b) list
   18.29 @@ -94,7 +85,11 @@
   18.30      string -> reconstructor * play_outcome -> 'a
   18.31    val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
   18.32      Proof.context
   18.33 -  val run_reconstructor : mode -> string -> prover
   18.34 +
   18.35 +  val supported_provers : Proof.context -> unit
   18.36 +  val kill_provers : unit -> unit
   18.37 +  val running_provers : unit -> unit
   18.38 +  val messages : int option -> unit
   18.39  end;
   18.40  
   18.41  structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
   18.42 @@ -102,25 +97,12 @@
   18.43  
   18.44  open ATP_Util
   18.45  open ATP_Problem
   18.46 -open ATP_Proof
   18.47  open ATP_Systems
   18.48  open ATP_Problem_Generate
   18.49  open ATP_Proof_Reconstruct
   18.50  open Metis_Tactic
   18.51 -open Sledgehammer_Util
   18.52  open Sledgehammer_Fact
   18.53  open Sledgehammer_Reconstructor
   18.54 -open Sledgehammer_Isar
   18.55 -
   18.56 -(* Empty string means create files in Isabelle's temporary files directory. *)
   18.57 -val dest_dir = Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
   18.58 -val problem_prefix = Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
   18.59 -val completish = Attrib.setup_config_bool @{binding sledgehammer_completish} (K false)
   18.60 -
   18.61 -(* In addition to being easier to read, readable names are often much shorter,
   18.62 -   especially if types are mangled in names. This makes a difference for some
   18.63 -   provers (e.g., E). For these reason, short names are enabled by default. *)
   18.64 -val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
   18.65  
   18.66  datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
   18.67  
   18.68 @@ -134,16 +116,6 @@
   18.69  
   18.70  val is_atp = member (op =) o supported_atps
   18.71  
   18.72 -fun is_atp_of_format is_format ctxt name =
   18.73 -  let val thy = Proof_Context.theory_of ctxt in
   18.74 -    (case try (get_atp thy) name of
   18.75 -      SOME config =>
   18.76 -      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
   18.77 -    | NONE => false)
   18.78 -  end
   18.79 -
   18.80 -val is_ho_atp = is_atp_of_format is_format_higher_order
   18.81 -
   18.82  fun remotify_atp_if_supported_and_not_already_remote thy name =
   18.83    if String.isPrefix remote_prefix name then
   18.84      SOME name
   18.85 @@ -156,23 +128,6 @@
   18.86    if is_atp thy name andalso is_atp_installed thy name then SOME name
   18.87    else remotify_atp_if_supported_and_not_already_remote thy name
   18.88  
   18.89 -fun supported_provers ctxt =
   18.90 -  let
   18.91 -    val thy = Proof_Context.theory_of ctxt
   18.92 -    val (remote_provers, local_provers) =
   18.93 -      reconstructor_names @
   18.94 -      sort_strings (supported_atps thy) @
   18.95 -      sort_strings (SMT_Solver.available_solvers_of ctxt)
   18.96 -      |> List.partition (String.isPrefix remote_prefix)
   18.97 -  in
   18.98 -    Output.urgent_message ("Supported provers: " ^
   18.99 -                           commas (local_provers @ remote_provers) ^ ".")
  18.100 -  end
  18.101 -
  18.102 -fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
  18.103 -fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
  18.104 -val messages = Async_Manager.thread_messages SledgehammerN "prover"
  18.105 -
  18.106  type params =
  18.107    {debug : bool,
  18.108     verbose : bool,
  18.109 @@ -334,45 +289,21 @@
  18.110         (max_new_instances |> the_default best_max_new_instances)
  18.111    #> Config.put Monomorph.max_thm_instances max_fact_instances
  18.112  
  18.113 -fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
  18.114 -    minimize_command
  18.115 -    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
  18.116 +fun supported_provers ctxt =
  18.117    let
  18.118 -    val reconstr =
  18.119 -      if name = metisN then
  18.120 -        Metis (type_enc |> the_default (hd partial_type_encs),
  18.121 -               lam_trans |> the_default default_metis_lam_trans)
  18.122 -      else if name = smtN then
  18.123 -        SMT
  18.124 -      else
  18.125 -        raise Fail ("unknown reconstructor: " ^ quote name)
  18.126 -    val used_facts = facts |> map fst
  18.127 +    val thy = Proof_Context.theory_of ctxt
  18.128 +    val (remote_provers, local_provers) =
  18.129 +      reconstructor_names @
  18.130 +      sort_strings (supported_atps thy) @
  18.131 +      sort_strings (SMT_Solver.available_solvers_of ctxt)
  18.132 +      |> List.partition (String.isPrefix remote_prefix)
  18.133    in
  18.134 -    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
  18.135 -       state subgoal reconstr [reconstr] of
  18.136 -      play as (_, Played time) =>
  18.137 -      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
  18.138 -       preplay = Lazy.value play,
  18.139 -       message =
  18.140 -         fn play =>
  18.141 -            let
  18.142 -              val (_, override_params) = extract_reconstructor params reconstr
  18.143 -              val one_line_params =
  18.144 -                (play, proof_banner mode name, used_facts, minimize_command override_params name,
  18.145 -                 subgoal, subgoal_count)
  18.146 -              val num_chained = length (#facts (Proof.goal state))
  18.147 -            in
  18.148 -              one_line_proof_text num_chained one_line_params
  18.149 -            end,
  18.150 -       message_tail = ""}
  18.151 -    | play =>
  18.152 -      let
  18.153 -        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
  18.154 -      in
  18.155 -        {outcome = SOME failure, used_facts = [], used_from = [],
  18.156 -         run_time = Time.zeroTime, preplay = Lazy.value play,
  18.157 -         message = fn _ => string_of_atp_failure failure, message_tail = ""}
  18.158 -      end)
  18.159 +    Output.urgent_message ("Supported provers: " ^
  18.160 +                           commas (local_provers @ remote_provers) ^ ".")
  18.161    end
  18.162  
  18.163 +fun kill_provers () = Async_Manager.kill_threads SledgehammerN "prover"
  18.164 +fun running_provers () = Async_Manager.running_threads SledgehammerN "prover"
  18.165 +val messages = Async_Manager.thread_messages SledgehammerN "prover"
  18.166 +
  18.167  end;
    19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 16:07:20 2014 +0100
    19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 16:10:39 2014 +0100
    19.3 @@ -11,6 +11,13 @@
    19.4    type mode = Sledgehammer_Prover.mode
    19.5    type prover = Sledgehammer_Prover.prover
    19.6  
    19.7 +  val atp_dest_dir : string Config.T
    19.8 +  val atp_problem_prefix : string Config.T
    19.9 +  val atp_completish : bool Config.T
   19.10 +  val atp_full_names : bool Config.T
   19.11 +
   19.12 +  val is_ho_atp : Proof.context -> string -> bool
   19.13 +
   19.14    val run_atp : mode -> string -> prover
   19.15  end;
   19.16  
   19.17 @@ -28,6 +35,26 @@
   19.18  open Sledgehammer_Isar
   19.19  open Sledgehammer_Prover
   19.20  
   19.21 +(* Empty string means create files in Isabelle's temporary files directory. *)
   19.22 +val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "")
   19.23 +val atp_problem_prefix =
   19.24 +  Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob")
   19.25 +val atp_completish = Attrib.setup_config_bool @{binding sledgehammer_atp_completish} (K false)
   19.26 +(* In addition to being easier to read, readable names are often much shorter, especially if types
   19.27 +   are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short
   19.28 +   names are enabled by default. *)
   19.29 +val atp_full_names = Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)
   19.30 +
   19.31 +fun is_atp_of_format is_format ctxt name =
   19.32 +  let val thy = Proof_Context.theory_of ctxt in
   19.33 +    (case try (get_atp thy) name of
   19.34 +      SOME config =>
   19.35 +      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
   19.36 +    | NONE => false)
   19.37 +  end
   19.38 +
   19.39 +val is_ho_atp = is_atp_of_format is_format_higher_order
   19.40 +
   19.41  fun choose_type_enc strictness best_type_enc format =
   19.42    the_default best_type_enc
   19.43    #> type_enc_of_string strictness
   19.44 @@ -115,11 +142,11 @@
   19.45      val {exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
   19.46        best_max_new_mono_instances, ...} = get_atp thy name ()
   19.47  
   19.48 -    val atp_mode = if Config.get ctxt completish then Sledgehammer_Completish else Sledgehammer
   19.49 +    val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer
   19.50      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
   19.51      val (dest_dir, problem_prefix) =
   19.52        if overlord then overlord_file_location_of_prover name
   19.53 -      else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
   19.54 +      else (Config.get ctxt atp_dest_dir, Config.get ctxt atp_problem_prefix)
   19.55      val problem_file_name =
   19.56        Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
   19.57                    suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
   19.58 @@ -171,6 +198,7 @@
   19.59                NONE => max_facts_of_slices I all_slices
   19.60              | SOME max => max)
   19.61            / Real.fromInt (max_facts_of_slices snd actual_slices)
   19.62 +
   19.63          fun monomorphize_facts facts =
   19.64            let
   19.65              val ctxt =
    20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jan 31 16:07:20 2014 +0100
    20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jan 31 16:10:39 2014 +0100
    20.3 @@ -40,6 +40,7 @@
    20.4  open ATP_Util
    20.5  open ATP_Proof
    20.6  open ATP_Problem_Generate
    20.7 +open ATP_Proof_Reconstruct
    20.8  open ATP_Systems
    20.9  open Sledgehammer_Util
   20.10  open Sledgehammer_Fact
   20.11 @@ -49,6 +50,47 @@
   20.12  open Sledgehammer_Prover_ATP
   20.13  open Sledgehammer_Prover_SMT
   20.14  
   20.15 +fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
   20.16 +    minimize_command
   20.17 +    ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
   20.18 +  let
   20.19 +    val reconstr =
   20.20 +      if name = metisN then
   20.21 +        Metis (type_enc |> the_default (hd partial_type_encs),
   20.22 +               lam_trans |> the_default default_metis_lam_trans)
   20.23 +      else if name = smtN then
   20.24 +        SMT
   20.25 +      else
   20.26 +        raise Fail ("unknown reconstructor: " ^ quote name)
   20.27 +    val used_facts = facts |> map fst
   20.28 +  in
   20.29 +    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
   20.30 +       state subgoal reconstr [reconstr] of
   20.31 +      play as (_, Played time) =>
   20.32 +      {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
   20.33 +       preplay = Lazy.value play,
   20.34 +       message =
   20.35 +         fn play =>
   20.36 +            let
   20.37 +              val (_, override_params) = extract_reconstructor params reconstr
   20.38 +              val one_line_params =
   20.39 +                (play, proof_banner mode name, used_facts, minimize_command override_params name,
   20.40 +                 subgoal, subgoal_count)
   20.41 +              val num_chained = length (#facts (Proof.goal state))
   20.42 +            in
   20.43 +              one_line_proof_text num_chained one_line_params
   20.44 +            end,
   20.45 +       message_tail = ""}
   20.46 +    | play =>
   20.47 +      let
   20.48 +        val failure = (case play of (_, Play_Failed) => GaveUp | _ => TimedOut)
   20.49 +      in
   20.50 +        {outcome = SOME failure, used_facts = [], used_from = [],
   20.51 +         run_time = Time.zeroTime, preplay = Lazy.value play,
   20.52 +         message = fn _ => string_of_atp_failure failure, message_tail = ""}
   20.53 +      end)
   20.54 +  end
   20.55 +
   20.56  fun is_prover_supported ctxt =
   20.57    let val thy = Proof_Context.theory_of ctxt in
   20.58      is_reconstructor orf is_atp thy orf is_smt_prover ctxt
    21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:07:20 2014 +0100
    21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Fri Jan 31 16:10:39 2014 +0100
    21.3 @@ -25,18 +25,15 @@
    21.4    val smt_slice_time_frac : real Config.T
    21.5    val smt_slice_min_secs : int Config.T
    21.6  
    21.7 -  val select_smt_solver : string -> Proof.context -> Proof.context
    21.8    val is_smt_prover : Proof.context -> string -> bool
    21.9 -  val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int
   21.10 -    -> (string * stature) * (int option * thm)
   21.11    val run_smt_solver : mode -> string -> prover
   21.12  end;
   21.13  
   21.14  structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT =
   21.15  struct
   21.16  
   21.17 +open ATP_Util
   21.18  open ATP_Proof
   21.19 -open ATP_Util
   21.20  open ATP_Systems
   21.21  open ATP_Problem_Generate
   21.22  open ATP_Proof_Reconstruct
   21.23 @@ -50,30 +47,24 @@
   21.24  val smt_weight_min_facts =
   21.25    Attrib.setup_config_int @{binding sledgehammer_smt_weight_min_facts} (K 20)
   21.26  
   21.27 -val select_smt_solver = Context.proof_map o SMT_Config.select_solver
   21.28 -
   21.29  fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
   21.30  
   21.31  (* FUDGE *)
   21.32 -val smt_min_weight =
   21.33 -  Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
   21.34 -val smt_max_weight =
   21.35 -  Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
   21.36 +val smt_min_weight = Attrib.setup_config_int @{binding sledgehammer_smt_min_weight} (K 0)
   21.37 +val smt_max_weight = Attrib.setup_config_int @{binding sledgehammer_smt_max_weight} (K 10)
   21.38  val smt_max_weight_index =
   21.39    Attrib.setup_config_int @{binding sledgehammer_smt_max_weight_index} (K 200)
   21.40  val smt_weight_curve = Unsynchronized.ref (fn x : int => x * x)
   21.41  
   21.42  fun smt_fact_weight ctxt j num_facts =
   21.43 -  if Config.get ctxt smt_weights andalso
   21.44 -     num_facts >= Config.get ctxt smt_weight_min_facts then
   21.45 +  if Config.get ctxt smt_weights andalso num_facts >= Config.get ctxt smt_weight_min_facts then
   21.46      let
   21.47        val min = Config.get ctxt smt_min_weight
   21.48        val max = Config.get ctxt smt_max_weight
   21.49        val max_index = Config.get ctxt smt_max_weight_index
   21.50        val curve = !smt_weight_curve
   21.51      in
   21.52 -      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1))
   21.53 -            div curve max_index)
   21.54 +      SOME (max - (max - min + 1) * curve (Int.max (0, max_index - j - 1)) div curve max_index)
   21.55      end
   21.56    else
   21.57      NONE
   21.58 @@ -120,7 +111,7 @@
   21.59        ...} : params) state goal i =
   21.60    let
   21.61      fun repair_context ctxt =
   21.62 -      ctxt |> select_smt_solver name
   21.63 +      ctxt |> Context.proof_map (SMT_Config.select_solver name)
   21.64             |> Config.put SMT_Config.verbose debug
   21.65             |> (if overlord then
   21.66                   Config.put SMT_Config.debug_files
   21.67 @@ -139,7 +130,7 @@
   21.68      val max_slices = if slice then Config.get ctxt smt_max_slices else 1
   21.69  
   21.70      fun do_slice timeout slice outcome0 time_so_far
   21.71 -                 (weighted_factss as (fact_filter, weighted_facts) :: _) =
   21.72 +        (weighted_factss as (fact_filter, weighted_facts) :: _) =
   21.73        let
   21.74          val timer = Timer.startRealTimer ()
   21.75          val slice_timeout =
   21.76 @@ -259,9 +250,8 @@
   21.77        | SOME failure =>
   21.78          (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
   21.79    in
   21.80 -    {outcome = outcome, used_facts = used_facts, used_from = used_from,
   21.81 -     run_time = run_time, preplay = preplay, message = message,
   21.82 -     message_tail = message_tail}
   21.83 +    {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
   21.84 +     preplay = preplay, message = message, message_tail = message_tail}
   21.85    end
   21.86  
   21.87  end;
    22.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Fri Jan 31 16:07:20 2014 +0100
    22.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Fri Jan 31 16:10:39 2014 +0100
    22.3 @@ -24,10 +24,9 @@
    22.4      (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
    22.5  
    22.6    val smtN : string
    22.7 +
    22.8    val string_of_reconstructor : reconstructor -> string
    22.9    val string_of_play_outcome : play_outcome -> string
   22.10 -  val reconstructor_command : reconstructor -> int -> int -> string list -> int -> string list ->
   22.11 -    string
   22.12    val one_line_proof_text : int -> one_line_params -> string
   22.13  
   22.14    val silence_reconstructors : bool -> Proof.context -> Proof.context
    23.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 16:07:20 2014 +0100
    23.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 16:10:39 2014 +0100
    23.3 @@ -14,7 +14,6 @@
    23.4    val serial_commas : string -> string list -> string list
    23.5    val simplify_spaces : string -> string
    23.6    val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
    23.7 -  val infinite_timeout : Time.time
    23.8    val time_mult : real -> Time.time -> Time.time
    23.9    val parse_bool_option : bool -> string -> string -> bool option
   23.10    val parse_time : string -> string -> Time.time
   23.11 @@ -27,11 +26,6 @@
   23.12    val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
   23.13    val hackish_string_of_term : Proof.context -> term -> string
   23.14    val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
   23.15 -
   23.16 -  (** extrema **)
   23.17 -  val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
   23.18 -  val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
   23.19 -  val max_list : ('a * 'a -> order) -> 'a list -> 'a option
   23.20  end;
   23.21  
   23.22  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
   23.23 @@ -42,7 +36,6 @@
   23.24  val sledgehammerN = "sledgehammer"
   23.25  
   23.26  val log10_2 = Math.log10 2.0
   23.27 -
   23.28  fun log2 n = Math.log10 n / log10_2
   23.29  
   23.30  fun app_hd f (x :: xs) = f x :: xs
   23.31 @@ -63,10 +56,7 @@
   23.32    |> tap (fn _ => clean_up x)
   23.33    |> Exn.release
   23.34  
   23.35 -val infinite_timeout = seconds 31536000.0 (* one year *)
   23.36 -
   23.37 -fun time_mult k t =
   23.38 -  Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
   23.39 +fun time_mult k t = Time.fromMilliseconds (Real.ceil (k * Real.fromInt (Time.toMilliseconds t)))
   23.40  
   23.41  fun parse_bool_option option name s =
   23.42    (case s of
   23.43 @@ -161,12 +151,4 @@
   23.44          (spying_version ^ " " ^ timestamp () ^ ": " ^ hash ^ ": " ^ tool ^ ": " ^ message ^ "\n")
   23.45      end
   23.46  
   23.47 -(** extrema **)
   23.48 -
   23.49 -fun max ord x y = case ord(x,y) of LESS => y | _ => x
   23.50 -
   23.51 -fun max_option ord = max (option_ord ord)
   23.52 -
   23.53 -fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
   23.54 -
   23.55  end;