--- a/src/HOL/TPTP/MaSh_Export.thy Thu Dec 06 23:01:49 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Thu Dec 06 23:07:10 2012 +0100
@@ -11,8 +11,8 @@
ML_file "mash_export.ML"
sledgehammer_params
- [provers = spass, max_relevant = 40, strict, dont_slice, type_enc = mono_native,
- lam_trans = combs_and_lifting, timeout = 1, dont_preplay, minimize]
+ [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
+ lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
ML {*
open MaSh_Export
@@ -57,7 +57,7 @@
ML {*
if do_it then
- generate_commands @{context} params thys (prefix ^ "mash_commands")
+ generate_isar_commands @{context} prover thys (prefix ^ "mash_commands")
else
()
*}
@@ -76,4 +76,11 @@
()
*}
+ML {*
+if do_it then
+ generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands")
+else
+ ()
+*}
+
end
--- a/src/HOL/TPTP/mash_eval.ML Thu Dec 06 23:01:49 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Dec 06 23:07:10 2012 +0100
@@ -23,8 +23,6 @@
val MeshN = "Mesh"
val IsarN = "Isar"
-val max_facts_slack = 2
-
val all_names = map (rpair () o nickname_of) #> Symtab.make
fun evaluate_mash_suggestions ctxt params file_name =
@@ -32,7 +30,7 @@
val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
Sledgehammer_Isar.default_params ctxt []
val prover = hd provers
- val slack_max_facts = max_facts_slack * the max_facts
+ val slack_max_facts = generous_max_facts (the max_facts)
val path = file_name |> Path.explode
val lines = path |> File.read_lines
val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -78,10 +76,12 @@
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 = suggested_facts suggs facts
+ val mash_facts =
+ find_mash_suggestions slack_max_facts suggs facts [] []
+ |> weight_mash_facts
val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, []))]
val mesh_facts = mesh_facts slack_max_facts mess
- val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
+ val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
fun prove ok heading get facts =
let
val facts =
--- a/src/HOL/TPTP/mash_export.ML Thu Dec 06 23:01:49 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Thu Dec 06 23:07:10 2012 +0100
@@ -17,7 +17,9 @@
Proof.context -> theory list -> bool -> string -> unit
val generate_atp_dependencies :
Proof.context -> params -> theory list -> bool -> string -> unit
- val generate_commands :
+ val generate_isar_commands :
+ Proof.context -> string -> theory list -> string -> unit
+ val generate_atp_commands :
Proof.context -> params -> theory list -> string -> unit
val generate_mepo_suggestions :
Proof.context -> params -> theory list -> int -> string -> unit
@@ -97,29 +99,18 @@
in File.append path s end
in List.app do_fact facts end
-fun generate_isar_dependencies ctxt thys include_thys file_name =
+fun isar_or_atp_dependencies_of ctxt params_opt facts all_names th =
+ (case params_opt of
+ SOME (params as {provers = prover :: _, ...}) =>
+ atp_dependencies_of ctxt params prover 0 facts all_names th |> snd
+ | NONE => isar_dependencies_of all_names th)
+ |> these
+
+fun generate_isar_or_atp_dependencies ctxt params_opt thys include_thys
+ file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val ths =
- all_facts ctxt
- |> not include_thys ? filter_out (has_thys thys o snd)
- |> map snd
- val all_names = all_names ths
- fun do_thm th =
- let
- val name = nickname_of th
- val deps = isar_dependencies_of all_names th |> these
- val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
- in File.append path s end
- in List.app do_thm ths end
-
-fun generate_atp_dependencies ctxt (params as {provers, ...}) thys include_thys
- file_name =
- let
- val path = file_name |> Path.explode
- val _ = File.write path ""
- val prover = hd provers
val facts =
all_facts ctxt
|> not include_thys ? filter_out (has_thys thys o snd)
@@ -129,17 +120,21 @@
let
val name = nickname_of th
val deps =
- atp_dependencies_of ctxt params prover 0 facts all_names th
- |> snd |> these
+ isar_or_atp_dependencies_of ctxt params_opt facts all_names th
val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
in File.append path s end
in List.app do_thm ths end
-fun generate_commands ctxt (params as {provers, ...}) thys file_name =
+fun generate_isar_dependencies ctxt =
+ generate_isar_or_atp_dependencies ctxt NONE
+
+fun generate_atp_dependencies ctxt params =
+ generate_isar_or_atp_dependencies ctxt (SOME params)
+
+fun generate_isar_or_atp_commands ctxt prover params_opt thys file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val prover = hd provers
val facts = all_facts ctxt
val (new_facts, old_facts) =
facts |> List.partition (has_thys thys o snd)
@@ -151,8 +146,7 @@
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val deps =
- atp_dependencies_of ctxt params prover 0 facts all_names th
- |> snd |> these
+ isar_or_atp_dependencies_of ctxt params_opt facts all_names th
val kind = Thm.legacy_get_kind th
val core =
escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
@@ -166,6 +160,12 @@
val parents = fold (add_thy_parent_facts thy_map) thys []
in fold do_fact new_facts parents; () end
+fun generate_isar_commands ctxt prover =
+ generate_isar_or_atp_commands ctxt prover NONE
+
+fun generate_atp_commands ctxt (params as {provers = prover :: _, ...}) =
+ generate_isar_or_atp_commands ctxt prover (SOME params)
+
fun generate_mepo_suggestions ctxt (params as {provers, ...}) thys max_relevant
file_name =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 06 23:01:49 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 06 23:07:10 2012 +0100
@@ -41,7 +41,7 @@
-> (string * real) list
val mash_unlearn : Proof.context -> unit
val nickname_of : thm -> string
- val suggested_facts :
+ val find_suggested_facts :
(string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
val mesh_facts :
int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
@@ -59,6 +59,9 @@
Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
-> thm -> bool * string list option
val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
+ val find_mash_suggestions :
+ int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
+ -> ('b * thm) list -> ('b * thm) list
val mash_suggested_facts :
Proof.context -> params -> string -> int -> term list -> term -> fact list
-> fact list
@@ -69,6 +72,7 @@
Proof.context -> params -> fact_override -> thm list -> bool -> unit
val is_mash_enabled : unit -> bool
val mash_can_suggest_facts : Proof.context -> bool
+ val generous_max_facts : int -> int
val relevant_facts :
Proof.context -> params -> string -> int -> fact_override -> term list
-> term -> fact list -> fact list
@@ -410,7 +414,7 @@
else
backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
-fun suggested_facts suggs facts =
+fun find_suggested_facts suggs facts =
let
fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
val tab = Symtab.empty |> fold add_fact facts
@@ -732,6 +736,20 @@
fun weight_proximity_facts facts =
facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
+fun find_mash_suggestions max_facts suggs facts chained unknown =
+ let
+ val raw_mash =
+ facts |> find_suggested_facts suggs
+ (* The weights currently returned by "mash.py" are too spaced out to
+ make any sense. *)
+ |> map fst
+ val proximity = facts |> sort (thm_ord o pairself snd o swap)
+ val mess =
+ [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])),
+ (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
+ (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))]
+ in mesh_facts max_facts mess end
+
fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
concl_t facts =
let
@@ -749,18 +767,8 @@
(fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
end)
val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
- val raw_mash =
- facts |> suggested_facts suggs
- (* The weights currently returned by "mash.py" are too spaced out to
- make any sense. *)
- |> map fst
- val proximity = facts |> sort (thm_ord o pairself snd o swap)
val unknown = facts |> filter_out (is_fact_in_graph fact_G)
- val mess =
- [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])),
- (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
- (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))]
- in mesh_facts max_facts mess end
+ in find_mash_suggestions max_facts suggs facts chained unknown end
fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
let