--- a/src/HOL/TPTP/mash_eval.ML Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed May 28 17:42:36 2014 +0200
@@ -54,7 +54,7 @@
fun print s = File.append report_path (s ^ "\n")
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
val prover = hd provers
- val slack_max_facts = generous_max_facts (the max_facts)
+ val max_suggs = generous_max_suggestions (the max_facts)
val lines_of = Path.explode #> try File.read_lines #> these
val file_names =
[mepo_file_name, mash_isar_file_name, mash_prover_file_name,
@@ -97,7 +97,7 @@
mesh_isar_line), mesh_prover_line)) =
if in_range range j then
let
- val get_suggs = extract_suggestions ##> take slack_max_facts
+ val get_suggs = extract_suggestions ##> take max_suggs
val (name1, mepo_suggs) = get_suggs mepo_line
val (name2, mash_isar_suggs) = get_suggs mash_isar_line
val (name3, mash_prover_suggs) = get_suggs mash_prover_line
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed May 28 17:42:36 2014 +0200
@@ -377,7 +377,9 @@
val prop_tab = fold cons_thm facts Termtab.empty
val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
- in (plain_name_tab, inclass_name_tab) end
+ in
+ (plain_name_tab, inclass_name_tab)
+ end
fun fact_distinct eq facts =
fold (fn fact as (_, th) =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed May 28 17:42:36 2014 +0200
@@ -85,7 +85,7 @@
val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
val mash_can_suggest_facts : Proof.context -> bool -> bool
- val generous_max_facts : int -> int
+ val generous_max_suggestions : int -> int
val mepo_weight : real
val mash_weight : real
val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
@@ -1574,7 +1574,7 @@
(* Generate more suggestions than requested, because some might be thrown out
later for various reasons. *)
-fun generous_max_facts max_facts = max_facts + Int.min (50, max_facts)
+fun generous_max_suggestions max_facts = max_facts (*### 11 * max_facts div 10 + 20 *)
val mepo_weight = 0.5
val mash_weight = 0.5
@@ -1655,7 +1655,7 @@
|> weight_facts_steeply, [])
fun mash () =
- mash_suggested_facts ctxt params (generous_max_facts max_facts) hyp_ts concl_t facts
+ mash_suggested_facts ctxt params (generous_max_suggestions max_facts) hyp_ts concl_t facts
|>> weight_facts_steeply
val mess =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed May 28 17:42:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed May 28 17:42:36 2014 +0200
@@ -84,9 +84,8 @@
fun reserved_isar_keyword_table () =
Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
-(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
- fixes that seem to be missing over there; or maybe the two code portions are
- not doing the same? *)
+(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few fixes that seem to
+ be missing over there; or maybe the two code portions are not doing the same? *)
fun fold_body_thm outer_name (map_plain_name, map_inclass_name) =
let
fun app_thm map_name (_, (name, _, body)) accum =
@@ -104,7 +103,9 @@
accum |> union (op =) (the_list (map_name name))
end
and app_body map_name (PBody {thms, ...}) = fold (app_thm map_name) thms
- in app_body map_plain_name end
+ in
+ app_body map_plain_name
+ end
fun thms_in_proof name_tabs th =
let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in