--- a/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Sun Jun 29 18:28:27 2014 +0200
@@ -47,7 +47,9 @@
val zeros = [0, 0, 0, 0, 0, 0]
val report_path = report_file_name |> Path.explode
val _ = File.write report_path ""
+
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 max_suggs = generous_max_suggestions (the max_facts)
@@ -59,18 +61,21 @@
mesh_isar_lines, mesh_prover_lines] =
map lines_of file_names
val num_lines = fold (Integer.max o length) lines 0
+
fun pad lines = lines @ replicate (num_lines - length lines) ""
+
val lines =
pad mepo_lines ~~ pad mash_isar_lines ~~ pad mash_prover_lines ~~
pad mesh_isar_lines ~~ pad mesh_prover_lines
val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
val name_tabs = build_name_tables nickname_of_thm facts
+
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
fun index_str (j, s) = s ^ "@" ^ string_of_int j
val str_of_method = enclose " " ": "
- fun str_of_result method facts ({outcome, run_time, used_facts, ...}
- : prover_result) =
+
+ fun str_of_result method facts ({outcome, run_time, used_facts, ...} : prover_result) =
let val facts = facts |> map (fst o fst) in
str_of_method method ^
(if is_none outcome then
@@ -89,8 +94,9 @@
|> map index_str
|> space_implode " "))
end
- fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line),
- mesh_isar_line), mesh_prover_line)) =
+
+ fun solve_goal (j, ((((mepo_line, mash_isar_line), mash_prover_line), mesh_isar_line),
+ mesh_prover_line)) =
if in_range range j then
let
val get_suggs = extract_suggestions ##> (take max_suggs #> map fst)
@@ -111,18 +117,18 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
val isar_deps = these (isar_dependencies_of name_tabs th)
val facts = facts |> filter (fn (_, th') => thm_less (th', th))
+
(* adapted from "mirabelle_sledgehammer.ML" *)
fun set_file_name method (SOME dir) =
let
- val prob_prefix =
- "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
- method
+ val prob_prefix = "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^ method
in
Config.put atp_dest_dir dir
#> Config.put atp_problem_prefix (prob_prefix ^ "__")
#> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
end
| set_file_name _ NONE = I
+
fun prove method suggs =
if not (member (op =) methods method) orelse
(null facts andalso method <> IsarN) then
@@ -131,6 +137,7 @@
let
fun nickify ((_, stature), th) =
((K (encode_str (nickname_of_thm th)), stature), th)
+
val facts =
suggs
|> find_suggested_facts ctxt facts
@@ -142,7 +149,10 @@
val res as {outcome, ...} =
run_prover_for_mash ctxt params prover name facts goal
val ok = if is_none outcome then 1 else 0
- in (str_of_result method facts res, ok) end
+ in
+ (str_of_result method facts res, ok)
+ end
+
val ress =
[fn () => prove MePoN mepo_suggs,
fn () => prove MaSh_IsarN mash_isar_suggs,
@@ -158,10 +168,12 @@
end
else
zeros
+
fun total_of method ok n =
str_of_method method ^ string_of_int ok ^ " (" ^
Real.fmt (StringCvt.FIX (SOME 1))
(100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
+
val inst_inducts = Config.get ctxt instantiate_inducts
val options =
["prover = " ^ prover,
@@ -175,8 +187,7 @@
val _ = print ("Options: " ^ commas options);
val oks = Par_List.map solve_goal (tag_list 1 lines)
val n = length oks
- val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
- isar_ok] =
+ val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok, isar_ok] =
if n = 0 then zeros else map Integer.sum (map_transpose I oks)
in
["Successes (of " ^ string_of_int n ^ " goals)",
--- a/src/HOL/TPTP/mash_export.ML Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Sun Jun 29 18:28:27 2014 +0200
@@ -40,6 +40,11 @@
fun in_range (from, to) j =
j >= from andalso (to = NONE orelse j <= the to)
+fun encode_feature (names, weight) =
+ encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
+
+val encode_features = map encode_feature #> space_implode " "
+
(* The suggested weights do not make much sense. *)
fun extract_suggestion sugg =
(case space_explode "=" sugg of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 29 18:28:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jun 29 18:28:27 2014 +0200
@@ -32,7 +32,6 @@
val encode_strs : string list -> string
val decode_str : string -> string
val decode_strs : string -> string list
- val encode_features : (string * real) list -> string
datatype mash_engine =
MaSh_kNN
@@ -62,8 +61,8 @@
val extra_feature_factor : real
val weight_facts_smoothly : 'a list -> ('a * real) list
val weight_facts_steeply : 'a list -> ('a * real) list
- val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list ->
- ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
+ val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list ->
+ ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term ->
raw_fact list -> fact list * fact list
@@ -72,8 +71,8 @@
val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time ->
raw_fact list -> string
val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
+ val mash_can_suggest_facts : Proof.context -> bool
- val mash_can_suggest_facts : Proof.context -> bool
val generous_max_suggestions : int -> int
val mepo_weight : real
val mash_weight : real
@@ -160,36 +159,6 @@
val the_mash_engine = the_default MaSh_NB o mash_engine
-(*** Maintenance of the persistent, string-based state ***)
-
-fun meta_char c =
- if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
- c = #"," then
- String.str c
- else
- (* fixed width, in case more digits follow *)
- "%" ^ stringN_of_int 3 (Char.ord c)
-
-fun unmeta_chars accum [] = String.implode (rev accum)
- | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
- (case Int.fromString (String.implode [d1, d2, d3]) of
- SOME n => unmeta_chars (Char.chr n :: accum) cs
- | NONE => "" (* error *))
- | unmeta_chars _ (#"%" :: _) = "" (* error *)
- | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
-
-val encode_str = String.translate meta_char
-val decode_str = String.explode #> unmeta_chars []
-
-val encode_strs = map encode_str #> space_implode " "
-val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
-
-fun encode_feature (names, weight) =
- encode_str names ^ (if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
-
-val encode_features = map encode_feature #> space_implode " "
-
-
(*** Isabelle-agnostic machine learning ***)
structure MaSh =
@@ -464,14 +433,14 @@
val naive_bayes_ext = external_tool "predict/nbayes"
fun query_external ctxt engine max_suggs learns goal_feats =
- (trace_msg ctxt (fn () => "MaSh query external " ^ encode_features goal_feats);
+ (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
(case engine of
MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats
| MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats))
fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
(freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
- (trace_msg ctxt (fn () => "MaSh query internal " ^ encode_features goal_feats ^ " from {" ^
+ (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
(case engine of
MaSh_kNN =>
@@ -490,7 +459,29 @@
end;
-(*** Middle-level communication with MaSh ***)
+(*** Persistent, stringly-typed state ***)
+
+fun meta_char c =
+ if Char.isAlphaNum c orelse c = #"_" orelse c = #"." orelse c = #"(" orelse c = #")" orelse
+ c = #"," then
+ String.str c
+ else
+ (* fixed width, in case more digits follow *)
+ "%" ^ stringN_of_int 3 (Char.ord c)
+
+fun unmeta_chars accum [] = String.implode (rev accum)
+ | unmeta_chars accum (#"%" :: d1 :: d2 :: d3 :: cs) =
+ (case Int.fromString (String.implode [d1, d2, d3]) of
+ SOME n => unmeta_chars (Char.chr n :: accum) cs
+ | NONE => "" (* error *))
+ | unmeta_chars _ (#"%" :: _) = "" (* error *)
+ | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
+
+val encode_str = String.translate meta_char
+val decode_str = String.explode #> unmeta_chars []
+
+val encode_strs = map encode_str #> space_implode " "
+val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str
datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop