--- a/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 15 21:26:10 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Sat Dec 15 21:34:32 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:26:10 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy Sat Dec 15 21:34:32 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:26:10 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 15 21:34:32 2012 +0100
@@ -10,7 +10,8 @@
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 =
@@ -28,7 +29,10 @@
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
@@ -70,63 +74,68 @@
|> 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 =
- 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) =
+ 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
- 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
+ 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))
--- a/src/HOL/TPTP/mash_export.ML Sat Dec 15 21:26:10 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Sat Dec 15 21:34:32 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)