# HG changeset patch
# User blanchet
# Date 1342035799 -7200
# Node ID 854a4767733544b7f8111ebd929c2a43c7f3492f
# Parent b88c3e0b752e9f89c9b3e71c6ddb5c62358aed74
generate ATP dependencies
diff -r b88c3e0b752e -r 854a47677335 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
@@ -9,40 +9,66 @@
uses "mash_export.ML"
begin
-sledgehammer_params [provers = e, max_relevant = 500]
+sledgehammer_params
+ [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
+ lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
ML {*
open MaSh_Export
*}
ML {*
-val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory List}
+if do_it then
+ generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+else
+ ()
+*}
+
+ML {*
+val do_it = true (* switch to "true" to generate the files *);
+val thy = @{theory Nat}
*}
ML {*
-if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
-else ()
+if do_it then
+ generate_features thy false "/tmp/mash_features"
+else
+ ()
*}
ML {*
-if do_it then generate_mash_commands thy "/tmp/mash_commands"
-else ()
+if do_it then
+ generate_accessibility thy false "/tmp/mash_accessibility"
+else
+ ()
*}
ML {*
-if do_it then generate_mash_features thy false "/tmp/mash_features"
-else ()
+if do_it then
+ generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
+else
+ ()
+*}
+
+ML {*
+if do_it then
+ generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+else
+ ()
*}
ML {*
-if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility"
-else ()
+if do_it then
+ generate_commands thy "/tmp/mash_commands"
+else
+ ()
*}
ML {*
-if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies"
-else ()
+if do_it then
+ generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
+else
+ ()
*}
end
diff -r b88c3e0b752e -r 854a47677335 src/HOL/TPTP/MaSh_Import.thy
--- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
@@ -21,11 +21,11 @@
ML {*
val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory Nat}
+val thy = @{theory List}
*}
ML {*
-if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions"
+if do_it then import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
else ()
*}
diff -r b88c3e0b752e -r 854a47677335 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
@@ -8,6 +8,7 @@
signature MASH_EXPORT =
sig
type stature = ATP_Problem_Generate.stature
+ type prover_result = Sledgehammer_Provers.prover_result
val non_tautological_facts_of :
theory -> (((unit -> string) * stature) * thm) list
@@ -16,15 +17,18 @@
val dependencies_of : string list -> thm -> string list
val goal_of_thm : thm -> thm
val meng_paulson_facts :
- Proof.context -> string -> int -> real * real -> thm -> int
- -> (((unit -> string) * stature) * thm) list
+ Proof.context -> int -> thm -> (((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 run_sledgehammer :
+ Proof.context -> ((string * stature) * thm) list -> thm -> prover_result
+ val generate_accessibility : theory -> bool -> string -> unit
+ val generate_features : theory -> bool -> string -> unit
+ val generate_isa_dependencies : theory -> bool -> string -> unit
+ val generate_atp_dependencies :
+ Proof.context -> theory -> bool -> string -> unit
+ val generate_commands : theory -> string -> unit
val generate_meng_paulson_suggestions :
- Proof.context -> theory -> string -> unit
+ Proof.context -> theory -> int -> string -> unit
end;
structure MaSh_Export : MASH_EXPORT =
@@ -33,6 +37,8 @@
open ATP_Problem_Generate
open ATP_Util
+type prover_result = Sledgehammer_Provers.prover_result
+
fun stringN_of_int 0 _ = ""
| stringN_of_int k n =
stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
@@ -105,13 +111,11 @@
let
val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
val bad_consts = atp_widely_irrelevant_consts
- val add_classes =
- subtract (op =) @{sort type} #> map class_name_of #> union (op =)
fun do_add_type (Type (s, Ts)) =
(not (member (op =) bad_types s) ? insert (op =) (type_name_of s))
#> fold do_add_type Ts
- | do_add_type (TFree (_, S)) = add_classes S
- | do_add_type (TVar (_, S)) = add_classes S
+ | do_add_type (TFree (_, S)) = union (op =) (map class_name_of S)
+ | do_add_type (TVar (_, S)) = union (op =) (map class_name_of S)
fun add_type T = type_max_depth >= 0 ? do_add_type T
fun mk_app s args =
if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
@@ -211,10 +215,12 @@
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 =
+fun meng_paulson_facts ctxt max_relevant goal =
let
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val {provers, relevance_thresholds, ...} =
+ Sledgehammer_Isar.default_params ctxt []
+ val prover_name = hd provers
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
val relevance_fudge =
@@ -226,7 +232,18 @@
hyp_ts concl_t
end
-fun generate_mash_accessibility thy include_thy file_name =
+fun run_sledgehammer ctxt facts goal =
+ let
+ val params as {provers, ...} = Sledgehammer_Isar.default_params ctxt []
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
+ facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+ val prover =
+ Sledgehammer_Run.get_minimizing_prover ctxt
+ Sledgehammer_Provers.Normal (hd provers)
+ in prover params (K (K (K ""))) problem end
+
+fun generate_accessibility thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -247,7 +264,7 @@
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 =
+fun generate_features thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -262,7 +279,7 @@
in File.append path s end
in List.app do_fact facts end
-fun generate_mash_dependencies thy include_thy file_name =
+fun generate_isa_dependencies thy include_thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -279,7 +296,35 @@
in File.append path s end
in List.app do_thm ths end
-fun generate_mash_commands thy file_name =
+fun generate_atp_dependencies ctxt thy include_thy file_name =
+ let
+ val {max_relevant, ...} = Sledgehammer_Isar.default_params ctxt []
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val facts =
+ non_tautological_facts_of thy
+ |> not include_thy ? filter_out (has_thy thy o snd)
+ val ths = facts |> map snd
+ val all_names = ths |> map Thm.get_name_hint
+ fun do_thm th =
+ let
+ val name = Thm.get_name_hint th
+ val goal = goal_of_thm th
+ val facts =
+ facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+ |> meng_paulson_facts ctxt (the max_relevant) goal
+ |> map (fn ((_, stature), th) =>
+ ((th |> Thm.get_name_hint |> fact_name_of, stature),
+ th))
+ val deps =
+ case run_sledgehammer ctxt facts goal of
+ {outcome = NONE, used_facts, ...} => used_facts |> map fst
+ | _ => dependencies_of all_names th
+ val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
+ in File.append path s end
+ in List.app do_thm ths end
+
+fun generate_commands thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
@@ -306,18 +351,14 @@
val parents = parent_thms thy_ths thy
in fold do_fact new_facts parents; () end
-fun generate_meng_paulson_suggestions ctxt thy file_name =
+fun generate_meng_paulson_suggestions ctxt thy max_relevant 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
@@ -327,10 +368,8 @@
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)
+ old_facts |> meng_paulson_facts ctxt max_relevant goal
+ |> map (fact_name_of o fst o fst)
val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
in File.append path s end
else
diff -r b88c3e0b752e -r 854a47677335 src/HOL/TPTP/mash_import.ML
--- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 13:59:39 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
@@ -39,15 +39,13 @@
fun import_and_evaluate_mash_suggestions ctxt thy file_name =
let
- val params as {provers, max_relevant, relevance_thresholds,
- slice, type_enc, lam_trans, timeout, ...} =
+ val {provers, max_relevant, slice, type_enc, lam_trans, timeout, ...} =
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
val meng_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
val meng_mash_ok = Unsynchronized.ref 0
@@ -90,19 +88,14 @@
else
"Failure: " ^
(facts |> map (fst o fst)
+ |> take (the max_relevant)
|> tag_list 1
|> map index_string
|> space_implode " "))
fun run_sh ok heading facts goal =
let
- val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = 1,
- facts = facts |> take (the max_relevant)
- |> map Sledgehammer_Provers.Untranslated_Fact}
- val prover =
- Sledgehammer_Run.get_minimizing_prover ctxt
- Sledgehammer_Provers.Normal prover_name
- val res as {outcome, ...} = prover params (K (K (K ""))) problem
+ val facts = facts |> take (the max_relevant)
+ val res as {outcome, ...} = run_sledgehammer ctxt facts goal
val _ = if is_none outcome then ok := !ok + 1 else ()
in str_of_res heading facts res end
fun solve_goal j name suggs =
@@ -114,13 +107,12 @@
| NONE => error ("No fact called \"" ^ name ^ "\"")
val deps = dependencies_of all_names th
val goal = goal_of_thm th
- val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
+ val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
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_paulson_facts ctxt prover_name
- (max_relevant_slack * the max_relevant) relevance_thresholds goal
- i facts
+ meng_paulson_facts ctxt (max_relevant_slack * the max_relevant) goal
+ facts
val mash_facts = sugg_facts hyp_ts concl_t facts suggs
val meng_mash_facts = meng_mash_facts meng_facts mash_facts
val meng_s = run_sh meng_ok mengN meng_facts goal
@@ -142,7 +134,7 @@
Real.fmt (StringCvt.FIX (SOME 1))
(100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
val inst_inducts = Config.get ctxt Sledgehammer_Filter.instantiate_inducts
- val params =
+ val options =
[prover_name, string_of_int (the max_relevant) ^ " facts",
"slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
the_default "smart" lam_trans, ATP_Util.string_from_time timeout,
@@ -150,7 +142,7 @@
val n = length lines
in
tracing " * * *";
- tracing ("Options: " ^ commas params);
+ tracing ("Options: " ^ commas options);
List.app do_line (tag_list 1 lines);
["Successes (of " ^ string_of_int n ^ " goals)",
total_of mengN meng_ok n,