--- a/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/ATP_Theory_Export.thy Tue Jul 10 23:36:03 2012 +0200
@@ -5,7 +5,7 @@
header {* ATP Theory Exporter *}
theory ATP_Theory_Export
-imports "~~/src/HOL/Sledgehammer2d" (*###*) Complex_Main
+imports Complex_Main
uses "atp_theory_export.ML"
begin
@@ -16,7 +16,7 @@
ML {*
val do_it = false; (* switch to "true" to generate the files *)
-val thy = @{theory Complex_Main};
+val thy = @{theory};
val ctxt = @{context}
*}
--- a/src/HOL/TPTP/MaSh_Export.thy Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Tue Jul 10 23:36:03 2012 +0200
@@ -9,16 +9,23 @@
uses "mash_export.ML"
begin
+sledgehammer_params [provers = e, max_relevant = 500]
+
ML {*
open MaSh_Export
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *)
+val do_it = false (* switch to "true" to generate the files *);
val thy = @{theory List}
*}
ML {*
+if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
+else ()
+*}
+
+ML {*
if do_it then generate_mash_commands thy "/tmp/mash_commands"
else ()
*}
@@ -38,8 +45,4 @@
else ()
*}
-ML {*
-find_index (curry (op =) 22) [0, 0, 9, 1, 2, 3]
-*}
-
end
--- a/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy Tue Jul 10 23:36:03 2012 +0200
@@ -9,6 +9,10 @@
uses "mash_import.ML"
begin
+sledgehammer_params
+ [max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+ lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
+
declare [[sledgehammer_instantiate_inducts]]
ML {*
@@ -16,12 +20,12 @@
*}
ML {*
-val do_it = true (* switch to "true" to generate the files *);
-val thy = @{theory List}
+val do_it = false (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
*}
ML {*
-if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions2"
+if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions"
else ()
*}
--- a/src/HOL/TPTP/mash_export.ML Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Tue Jul 10 23:36:03 2012 +0200
@@ -14,10 +14,16 @@
val theory_ord : theory * theory -> order
val thm_ord : thm * thm -> order
val dependencies_of : string list -> thm -> string list
+ val meng_paulson_facts :
+ Proof.context -> string -> int -> real * real -> thm -> int
+ -> (((unit -> string) * stature) * thm) list
+ -> ((string * stature) * thm) list
val generate_mash_accessibility : theory -> bool -> string -> unit
val generate_mash_features : theory -> bool -> string -> unit
val generate_mash_dependencies : theory -> bool -> string -> unit
val generate_mash_commands : theory -> string -> unit
+ val generate_meng_paulson_suggestions :
+ Proof.context -> theory -> string -> unit
end;
structure MaSh_Export : MASH_EXPORT =
@@ -192,6 +198,32 @@
val dependencies_of =
map fact_name_of oo theorems_mentioned_in_proof_term o SOME
+val freezeT = Type.legacy_freeze_type
+
+fun freeze (t $ u) = freeze t $ freeze u
+ | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
+ | freeze (Var ((s, _), T)) = Free (s, freezeT T)
+ | freeze (Const (s, T)) = Const (s, freezeT T)
+ | freeze (Free (s, T)) = Free (s, freezeT T)
+ | freeze t = t
+
+val goal_of_thm = prop_of #> freeze #> cterm_of thy #> Goal.init
+
+fun meng_paulson_facts ctxt prover_name max_relevant relevance_thresholds
+ goal i =
+ let
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val is_built_in_const =
+ Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
+ val relevance_fudge =
+ Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
+ val relevance_override = {add = [], del = [], only = false}
+ in
+ Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
+ max_relevant is_built_in_const relevance_fudge relevance_override []
+ hyp_ts concl_t
+ end
+
fun generate_mash_accessibility thy include_thy file_name =
let
val path = file_name |> Path.explode
@@ -210,10 +242,8 @@
val thy = theory_of_thm (hd ths)
val parents = parent_thms thy_ths thy
val ths = ths |> map (fact_name_of o Thm.get_name_hint)
- val _ = fold do_thm ths parents
- in () end
- val _ = List.app (do_thy o snd) thy_ths
- in () end
+ in fold do_thm ths parents; () end
+ in List.app (do_thy o snd) thy_ths end
fun generate_mash_features thy include_thy file_name =
let
@@ -228,8 +258,7 @@
val feats = features_of thy (status, th)
val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
in File.append path s end
- val _ = List.app do_fact facts
- in () end
+ in List.app do_fact facts end
fun generate_mash_dependencies thy include_thy file_name =
let
@@ -246,8 +275,7 @@
val deps = dependencies_of all_names th
val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
in File.append path s end
- val _ = List.app do_thm ths
- in () end
+ in List.app do_thm ths end
fun generate_mash_commands thy file_name =
let
@@ -274,7 +302,38 @@
in [name] end
val thy_ths = old_facts |> thms_by_thy
val parents = parent_thms thy_ths thy
- val _ = fold do_fact new_facts parents
- in () end
+ in fold do_fact new_facts parents; () end
+
+fun generate_meng_paulson_suggestions ctxt thy file_name =
+ let
+ val {provers, max_relevant, relevance_thresholds, ...} =
+ Sledgehammer_Isar.default_params ctxt []
+ val prover_name = hd provers
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val facts = non_tautological_facts_of thy
+ val (new_facts, old_facts) =
+ facts |> List.partition (has_thy thy o snd)
+ |>> sort (thm_ord o pairself snd)
+ val i = 1
+ fun do_fact (fact as (_, th)) old_facts =
+ let
+ val name = Thm.get_name_hint th
+ val goal = goal_of_thm th
+ val kind = Thm.legacy_get_kind th
+ val _ =
+ if kind <> "" then
+ let
+ val suggs =
+ old_facts
+ |> meng_paulson_facts ctxt prover_name (the max_relevant)
+ relevance_thresholds goal i
+ |> map (fact_name_of o Thm.get_name_hint o snd)
+ val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
+ in File.append path s end
+ else
+ ()
+ in fact :: old_facts end
+ in fold do_fact new_facts old_facts; () end
end;
--- a/src/HOL/TPTP/mash_import.ML Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML Tue Jul 10 23:36:03 2012 +0200
@@ -28,63 +28,23 @@
val of_fact_name = unescape_meta
-val freezeT = Type.legacy_freeze_type;
-
-fun freeze (t $ u) = freeze t $ freeze u
- | freeze (Abs (s, T, t)) = Abs (s, freezeT T, freeze t)
- | freeze (Var ((s, _), T)) = Free (s, freezeT T)
- | freeze (Const (s, T)) = Const (s, freezeT T)
- | freeze (Free (s, T)) = Free (s, freezeT T)
- | freeze t = t
-
-val prover_name = ATP_Systems.spassN
-val max_relevant = 40
-val slack_max_relevant = 2 * max_relevant
-val timeout = 5
+val max_relevant_slack = 2
fun import_and_evaluate_mash_suggestions ctxt thy file_name =
let
- val params as {relevance_thresholds, ...} =
- Sledgehammer_Isar.default_params ctxt
- [("strict", "true"),
- ("slice", "false"),
- ("type_enc", "poly_guards??"),
- ("timeout", string_of_int timeout),
- ("preplay_timeout", "0"),
- ("minimize", "true")]
- val is_built_in_const =
- Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
- val relevance_fudge =
- Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
- val relevance_override = {add = [], del = [], only = false}
+ val params as {provers, max_relevant, relevance_thresholds, ...} =
+ Sledgehammer_Isar.default_params ctxt []
+ val prover_name = hd provers
val path = file_name |> Path.explode
val lines = path |> File.read_lines
val facts = non_tautological_facts_of thy
val all_names = facts |> map (Thm.get_name_hint o snd)
val i = 1
- fun run_sh facts goal =
- let
- val facts =
- facts |> take max_relevant
- |> map Sledgehammer_Provers.Untranslated_Fact
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
- facts = facts}
- val prover =
- Sledgehammer_Run.get_minimizing_prover ctxt
- Sledgehammer_Provers.Normal prover_name
- in prover params (K (K (K ""))) problem end
- fun meng_facts goal =
- let val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i in
- Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- slack_max_relevant is_built_in_const relevance_fudge
- relevance_override [] hyp_ts concl_t
- end
fun find_sugg facts sugg =
find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
fun sugg_facts hyp_ts concl_t facts =
map_filter (find_sugg facts o of_fact_name)
- #> take slack_max_relevant
+ #> take (max_relevant_slack * the max_relevant)
#> Sledgehammer_Filter.maybe_instantiate_inducts ctxt hyp_ts concl_t
#> map (apfst (apfst (fn name => name ())))
fun hybrid_facts fs1 fs2 =
@@ -98,12 +58,12 @@
in
union fact_eq fs1 fs2
|> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
- |> take max_relevant
+ |> take (the max_relevant)
end
fun with_index facts s =
(find_index (fn ((s', _), _) => s = s') facts + 1, s)
fun index_string (j, s) = s ^ "@" ^ string_of_int j
- fun print_res label facts {outcome, run_time, used_facts, ...} =
+ fun print_result label facts {outcome, run_time, used_facts, ...} =
tracing (" " ^ label ^ ": " ^
(if is_none outcome then
"Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
@@ -113,6 +73,18 @@
|> map index_string)
else
"Failure: " ^ space_implode " " (map (fst o fst) facts) ))
+ fun run_sh heading facts goal =
+ let
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
+ facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+ val prover =
+ Sledgehammer_Run.get_minimizing_prover ctxt
+ Sledgehammer_Provers.Normal prover_name
+ in
+ prover params (K (K (K ""))) problem
+ |> tap (print_result heading facts)
+ end
fun solve_goal name suggs =
let
val name = of_fact_name name
@@ -122,22 +94,22 @@
SOME (_, th) => th
| NONE => error ("No fact called \"" ^ name ^ "\"")
val deps = dependencies_of all_names th
- val goal = th |> prop_of |> freeze |> cterm_of thy |> Goal.init
+ val goal = goal_of_thm th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
val deps_facts = sugg_facts hyp_ts concl_t facts deps
- val meng_facts = meng_facts goal facts
+ val meng_facts =
+ meng_paulson_facts ctxt prover_name
+ (max_relevant_slack * the max_relevant) relevance_thresholds goal
+ i facts
val mash_facts = sugg_facts hyp_ts concl_t facts suggs
val hybrid_facts = hybrid_facts meng_facts mash_facts
- val deps_res = run_sh deps_facts goal
- val meng_res = run_sh meng_facts goal
- val mash_res = run_sh mash_facts goal
- val hybrid_res = run_sh hybrid_facts goal
in
- print_res "Dependencies" deps_facts deps_res;
- print_res "Meng & Paulson" meng_facts meng_res;
- print_res "MaSh" mash_facts mash_res;
- print_res "Hybrid" hybrid_facts hybrid_res
+ run_sh "Dependencies" deps_facts goal;
+ run_sh "Meng & Paulson" meng_facts goal;
+ run_sh "MaSh" mash_facts goal;
+ run_sh "Hybrid" hybrid_facts goal;
+ ()
end
val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
fun do_line line =