--- a/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Sledgehammer.thy Wed Jul 11 21:43:19 2012 +0200
@@ -14,9 +14,9 @@
"Tools/Sledgehammer/sledgehammer_fact.ML"
"Tools/Sledgehammer/sledgehammer_filter_iter.ML"
"Tools/Sledgehammer/sledgehammer_provers.ML"
+ "Tools/Sledgehammer/sledgehammer_minimize.ML"
"Tools/Sledgehammer/sledgehammer_filter_mash.ML"
"Tools/Sledgehammer/sledgehammer_filter.ML"
- "Tools/Sledgehammer/sledgehammer_minimize.ML"
"Tools/Sledgehammer/sledgehammer_run.ML"
"Tools/Sledgehammer/sledgehammer_isar.ML"
begin
--- a/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Wed Jul 11 21:43:19 2012 +0200
@@ -14,17 +14,19 @@
lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
ML {*
+open Sledgehammer_Filter_MaSh
open MaSh_Export
*}
ML {*
val do_it = false (* switch to "true" to generate the files *);
-val thy = @{theory Nat}
+val thy = @{theory Nat};
+val params = Sledgehammer_Isar.default_params @{context} []
*}
ML {*
if do_it then
- generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+ generate_accessibility thy false "/tmp/mash_accessibility"
else
()
*}
@@ -38,13 +40,6 @@
ML {*
if do_it then
- generate_accessibility thy false "/tmp/mash_accessibility"
-else
- ()
-*}
-
-ML {*
-if do_it then
generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
else
()
@@ -52,7 +47,7 @@
ML {*
if do_it then
- generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
+ generate_atp_dependencies @{context} params thy false "/tmp/mash_atp_dependencies"
else
()
*}
@@ -66,7 +61,7 @@
ML {*
if do_it then
- generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
+ generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
else
()
*}
--- a/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Import.thy Wed Jul 11 21:43:19 2012 +0200
@@ -16,13 +16,14 @@
*}
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 List};
+val params = Sledgehammer_Isar.default_params @{context} []
*}
ML {*
if do_it then
- import_and_evaluate_mash_suggestions @{context} thy "/tmp/mash_suggestions_list"
+ import_and_evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions_list"
else
()
*}
--- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 11 21:43:19 2012 +0200
@@ -8,11 +8,7 @@
signature ATP_THEORY_EXPORT =
sig
type atp_format = ATP_Problem.atp_format
- type stature = Sledgehammer_Filter.stature
- val theorems_mentioned_in_proof_term :
- string list option -> thm -> string list
- val all_facts_of_theory : theory -> (((unit -> string) * stature) * thm) list
val generate_atp_inference_file_for_theory :
Proof.context -> theory -> atp_format -> string -> string -> unit
end;
@@ -27,45 +23,6 @@
val fact_name_of = prefix fact_prefix o ascii_of
-(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
- fixes that seem to be missing over there; or maybe the two code portions are
- not doing the same? *)
-fun fold_body_thms thm_name f =
- let
- fun app n (PBody {thms, ...}) =
- thms |> fold (fn (_, (name, prop, body)) => fn x =>
- let
- val body' = Future.join body
- val n' =
- n + (if name = "" orelse
- (* uncommon case where the proved theorem occurs twice
- (e.g., "Transitive_Closure.trancl_into_trancl") *)
- (n = 1 andalso name = thm_name) then
- 0
- else
- 1)
- val x' = x |> n' <= 1 ? app n' body'
- in (x' |> n = 1 ? f (name, prop, body')) end)
- in fold (app 0) end
-
-fun theorems_mentioned_in_proof_term all_names th =
- let
- val is_name_ok =
- case all_names of
- SOME names => member (op =) names
- | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
- fun collect (s, _, _) = is_name_ok s ? insert (op =) s
- val names =
- [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
- in names end
-
-fun all_facts_of_theory thy =
- let val ctxt = Proof_Context.init_global thy in
- Sledgehammer_Fact.all_facts ctxt false Symtab.empty true [] []
- (Sledgehammer_Fact.clasimpset_rule_table_of ctxt)
- |> rev (* try to restore the original order of facts, for MaSh *)
- end
-
fun inference_term [] = NONE
| inference_term ss =
ATerm (("inference", []),
@@ -153,7 +110,7 @@
val mono = not (is_type_enc_polymorphic type_enc)
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts = all_facts_of_theory thy
+ val facts = Sledgehammer_Fact.all_facts_of thy
val atp_problem =
facts
|> map (fn ((_, loc), th) =>
@@ -170,7 +127,7 @@
val infers =
facts |> map (fn (_, th) =>
(fact_name_of (Thm.get_name_hint th),
- th |> theorems_mentioned_in_proof_term (SOME all_names)
+ th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
|> map fact_name_of))
val all_atp_problem_names =
atp_problem |> maps (map ident_of_problem_line o snd)
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 11 21:43:19 2012 +0200
@@ -7,348 +7,23 @@
signature MASH_EXPORT =
sig
- type stature = ATP_Problem_Generate.stature
- type prover_result = Sledgehammer_Provers.prover_result
+ type params = Sledgehammer_Provers.params
- val non_tautological_facts_of :
- theory -> (((unit -> string) * stature) * thm) list
- val theory_ord : theory * theory -> order
- val thm_ord : thm * thm -> order
- val dependencies_of : string list -> thm -> string list
- val goal_of_thm : theory -> thm -> thm
- val meng_paulson_facts :
- Proof.context -> int -> thm -> (((unit -> string) * stature) * thm) list
- -> ((string * stature) * thm) list
- 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 -> int -> string -> unit
+ val generate_iter_suggestions :
+ Proof.context -> params -> theory -> int -> string -> unit
end;
structure MaSh_Export : MASH_EXPORT =
struct
-open ATP_Util
-open ATP_Problem_Generate
-open ATP_Theory_Export
-
-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)
-
-fun escape_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)
-
-val escape_meta = String.translate escape_meta_char
-
-val thy_prefix = "y_"
-
-val fact_name_of = escape_meta
-val thy_name_of = prefix thy_prefix o escape_meta
-val const_name_of = prefix const_prefix o escape_meta
-val type_name_of = prefix type_const_prefix o escape_meta
-val class_name_of = prefix class_prefix o escape_meta
-
-val thy_name_of_thm = theory_of_thm #> Context.theory_name
-
-local
-
-fun has_bool @{typ bool} = true
- | has_bool (Type (_, Ts)) = exists has_bool Ts
- | has_bool _ = false
-
-fun has_fun (Type (@{type_name fun}, _)) = true
- | has_fun (Type (_, Ts)) = exists has_fun Ts
- | has_fun _ = false
-
-val is_conn = member (op =)
- [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
- @{const_name HOL.implies}, @{const_name Not},
- @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
- @{const_name HOL.eq}]
-
-val has_bool_arg_const =
- exists_Const (fn (c, T) =>
- not (is_conn c) andalso exists has_bool (binder_types T))
-
-fun higher_inst_const thy (c, T) =
- case binder_types T of
- [] => false
- | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
-
-val binders = [@{const_name All}, @{const_name Ex}]
-
-in
-
-fun is_fo_term thy t =
- let
- val t =
- t |> Envir.beta_eta_contract
- |> transform_elim_prop
- |> Object_Logic.atomize_term thy
- in
- Term.is_first_order binders t andalso
- not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
- | _ => false) t orelse
- has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
- end
-
-end
-
-fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
- let
- val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
- val bad_consts = atp_widely_irrelevant_consts
- 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)) = 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 ^ ")"
- else s
- fun patternify ~1 _ = ""
- | patternify depth t =
- case strip_comb t of
- (Const (s, _), args) =>
- mk_app (const_name_of s) (map (patternify (depth - 1)) args)
- | _ => ""
- fun add_term_patterns ~1 _ = I
- | add_term_patterns depth t =
- insert (op =) (patternify depth t)
- #> add_term_patterns (depth - 1) t
- val add_term = add_term_patterns term_max_depth
- fun add_patterns t =
- let val (head, args) = strip_comb t in
- (case head of
- Const (s, T) =>
- not (member (op =) bad_consts s) ? (add_term t #> add_type T)
- | Free (_, T) => add_type T
- | Var (_, T) => add_type T
- | Abs (_, T, body) => add_type T #> add_patterns body
- | _ => I)
- #> fold add_patterns args
- end
- in [] |> add_patterns t |> sort string_ord end
-
-fun is_likely_tautology th =
- null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
- not (Thm.eq_thm_prop (@{thm ext}, th))
-
-fun is_too_meta thy th =
- fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
-
-fun non_tautological_facts_of thy =
- all_facts_of_theory thy
- |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
-
-fun theory_ord p =
- if Theory.eq_thy p then EQUAL
- else if Theory.subthy p then LESS
- else if Theory.subthy (swap p) then GREATER
- else EQUAL
-
-val thm_ord = theory_ord o pairself theory_of_thm
-
-fun thms_by_thy ths =
- ths |> map (snd #> `thy_name_of_thm)
- |> AList.group (op =)
- |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
- o hd o snd))
- |> map (apsnd (sort thm_ord))
-
-fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
-
-fun parent_thms thy_ths thy =
- Theory.parents_of thy
- |> map Context.theory_name
- |> map_filter (AList.lookup (op =) thy_ths)
- |> map List.last
- |> map (fact_name_of o Thm.get_name_hint)
-
-fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
-
-val max_depth = 1
-
-(* TODO: Generate type classes for types? *)
-fun features_of thy (status, th) =
- let val t = Thm.prop_of th in
- thy_name_of (thy_name_of_thm th) ::
- interesting_terms_types_and_classes max_depth max_depth t
- |> not (has_no_lambdas t) ? cons "lambdas"
- |> exists_Const is_exists t ? cons "skolems"
- |> not (is_fo_term thy t) ? cons "ho"
- |> (case status of
- General => I
- | Induction => cons "induction"
- | Intro => cons "intro"
- | Inductive => cons "inductive"
- | Elim => cons "elim"
- | Simp => cons "simp"
- | Def => cons "def")
- end
-
-fun dependencies_of all_facts =
- theorems_mentioned_in_proof_term (SOME all_facts)
- #> map fact_name_of
- #> sort string_ord
-
-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
-
-fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
-
-fun meng_paulson_facts ctxt max_relevant goal =
- let
- 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 =
- 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 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_Minimize.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 ""
- fun do_thm th prevs =
- let
- val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
- val _ = File.append path s
- in [th] end
- val thy_ths =
- non_tautological_facts_of thy
- |> not include_thy ? filter_out (has_thy thy o snd)
- |> thms_by_thy
- fun do_thy ths =
- let
- 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)
- in fold do_thm ths parents; () end
- in List.app (do_thy o snd) thy_ths end
-
-fun generate_features thy include_thy file_name =
- let
- 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)
- fun do_fact ((_, (_, status)), th) =
- let
- val name = Thm.get_name_hint th
- val feats = features_of thy (status, th)
- val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
- in File.append path s end
- in List.app do_fact facts end
-
-fun generate_isa_dependencies thy include_thy file_name =
- let
- val path = file_name |> Path.explode
- val _ = File.write path ""
- val ths =
- non_tautological_facts_of thy
- |> not include_thy ? filter_out (has_thy thy o snd)
- |> map snd
- val all_names = ths |> map Thm.get_name_hint
- fun do_thm th =
- let
- val name = Thm.get_name_hint th
- val deps = 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_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 is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
- fun add_isa_dep facts dep accum =
- if exists (is_dep dep) accum then
- accum
- else case find_first (is_dep dep) facts of
- SOME ((name, status), th) => accum @ [((name (), status), th)]
- | NONE => accum (* shouldn't happen *)
- fun fix_name ((_, stature), th) =
- ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
- fun do_thm th =
- let
- val name = Thm.get_name_hint th
- val goal = goal_of_thm thy th
- val deps =
- case dependencies_of all_names th of
- [] => []
- | isa_dep as [_] => isa_dep (* can hardly beat that *)
- | isa_deps =>
- let
- val facts =
- facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val facts =
- facts |> meng_paulson_facts ctxt (the max_relevant) goal
- |> fold (add_isa_dep facts) isa_deps
- |> map fix_name
- in
- case run_sledgehammer ctxt facts goal of
- {outcome = NONE, used_facts, ...} =>
- used_facts |> map fst |> sort string_ord
- | _ => isa_deps
- end
- val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
- in File.append path s end
- in List.app do_thm ths end
+open Sledgehammer_Filter_MaSh
fun generate_commands thy file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts = non_tautological_facts_of thy
+ val facts = all_non_tautological_facts_of thy
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
@@ -358,7 +33,7 @@
let
val name = Thm.get_name_hint th
val feats = features_of thy (status, th)
- val deps = dependencies_of all_names th
+ val deps = isabelle_dependencies_of all_names th
val kind = Thm.legacy_get_kind th
val name = fact_name_of name
val core =
@@ -371,11 +46,11 @@
val parents = parent_thms thy_ths thy
in fold do_fact new_facts parents; () end
-fun generate_meng_paulson_suggestions ctxt thy max_relevant file_name =
+fun generate_iter_suggestions ctxt params thy max_relevant file_name =
let
val path = file_name |> Path.explode
val _ = File.write path ""
- val facts = non_tautological_facts_of thy
+ val facts = all_non_tautological_facts_of thy
val (new_facts, old_facts) =
facts |> List.partition (has_thy thy o snd)
|>> sort (thm_ord o pairself snd)
@@ -388,7 +63,7 @@
if kind <> "" then
let
val suggs =
- old_facts |> meng_paulson_facts ctxt max_relevant goal
+ old_facts |> iter_facts ctxt params max_relevant goal
|> map (fact_name_of o fst o fst)
|> sort string_ord
val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
--- a/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/TPTP/mash_import.ML Wed Jul 11 21:43:19 2012 +0200
@@ -8,13 +8,16 @@
signature MASH_IMPORT =
sig
+ type params = Sledgehammer_Provers.params
+
val import_and_evaluate_mash_suggestions :
- Proof.context -> theory -> string -> unit
+ Proof.context -> params -> theory -> string -> unit
end;
structure MaSh_Import : MASH_IMPORT =
struct
+open Sledgehammer_Filter_MaSh
open MaSh_Export
val unescape_meta =
@@ -30,26 +33,26 @@
val of_fact_name = unescape_meta
-val depN = "Dependencies"
-val mengN = "Meng & Paulson"
+val isaN = "Isabelle"
+val iterN = "Iterative"
val mashN = "MaSh"
-val meng_mashN = "M&P+MaSh"
+val iter_mashN = "Iter+MaSh"
val max_relevant_slack = 2
-fun import_and_evaluate_mash_suggestions ctxt thy file_name =
+fun import_and_evaluate_mash_suggestions ctxt params thy file_name =
let
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 facts = all_non_tautological_facts_of thy
val all_names = facts |> map (Thm.get_name_hint o snd)
- val meng_ok = Unsynchronized.ref 0
+ val iter_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
- val meng_mash_ok = Unsynchronized.ref 0
- val dep_ok = Unsynchronized.ref 0
+ val iter_mash_ok = Unsynchronized.ref 0
+ val isa_ok = Unsynchronized.ref 0
fun find_sugg facts sugg =
find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
fun sugg_facts hyp_ts concl_t facts =
@@ -57,7 +60,7 @@
#> take (max_relevant_slack * the max_relevant)
#> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
#> map (apfst (apfst (fn name => name ())))
- fun meng_mash_facts fs1 fs2 =
+ fun iter_mash_facts fs1 fs2 =
let
val fact_eq = (op =) o pairself fst
fun score_in f fs =
@@ -92,10 +95,10 @@
|> tag_list 1
|> map index_string
|> space_implode " "))
- fun run_sh ok heading facts goal =
+ fun prove ok heading facts goal =
let
val facts = facts |> take (the max_relevant)
- val res as {outcome, ...} = run_sledgehammer ctxt facts goal
+ val res as {outcome, ...} = run_prover ctxt params 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 =
@@ -105,23 +108,23 @@
case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
SOME (_, th) => th
| NONE => error ("No fact called \"" ^ name ^ "\"")
- val deps = dependencies_of all_names th
+ val isa_deps = isabelle_dependencies_of all_names th
val goal = goal_of_thm thy th
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 (max_relevant_slack * the max_relevant) goal
- facts
+ val isa_facts = sugg_facts hyp_ts concl_t facts isa_deps
+ val iter_facts =
+ iter_facts ctxt params (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
- val mash_s = run_sh mash_ok mashN mash_facts goal
- val meng_mash_s = run_sh meng_mash_ok meng_mashN meng_mash_facts goal
- val dep_s = run_sh dep_ok depN deps_facts goal
+ val iter_mash_facts = iter_mash_facts iter_facts mash_facts
+ val iter_s = prove iter_ok iterN iter_facts goal
+ val mash_s = prove mash_ok mashN mash_facts goal
+ val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal
+ val isa_s = prove isa_ok isaN isa_facts goal
in
- ["Goal " ^ string_of_int j ^ ": " ^ name, meng_s, mash_s, meng_mash_s,
- dep_s]
+ ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, iter_mash_s,
+ isa_s]
|> cat_lines |> tracing
end
val explode_suggs = space_explode " " #> filter_out (curry (op =) "")
@@ -145,10 +148,10 @@
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,
+ total_of iterN iter_ok n,
total_of mashN mash_ok n,
- total_of meng_mashN meng_mash_ok n,
- total_of depN dep_ok n]
+ total_of iter_mashN iter_mash_ok n,
+ total_of isaN isa_ok n]
|> cat_lines |> tracing
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200
@@ -252,10 +252,6 @@
Other characters go to _nnn where nnn is the decimal ASCII code.*)
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
-fun stringN_of_int 0 _ = ""
- | stringN_of_int k n =
- stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
-
fun ascii_of_char c =
if Char.isAlphaNum c then
String.str c
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200
@@ -9,6 +9,7 @@
val timestamp : unit -> string
val hash_string : string -> int
val hash_term : term -> int
+ val stringN_of_int : int -> int -> string
val strip_spaces : bool -> (char -> bool) -> string -> string
val strip_spaces_except_between_idents : string -> string
val nat_subscript : int -> string
@@ -65,6 +66,10 @@
fun hash_string s = Word.toInt (hashw_string (s, 0w0))
val hash_term = Word.toInt o hashw_term
+fun stringN_of_int 0 _ = ""
+ | stringN_of_int k n =
+ stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
+
fun strip_spaces skip_comments is_evil =
let
fun strip_c_style_comment [] accum = accum
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 11 21:43:19 2012 +0200
@@ -21,15 +21,16 @@
val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
- val all_facts :
- Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
- -> thm list -> status Termtab.table
- -> (((unit -> string) * stature) * thm) list
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val maybe_instantiate_inducts :
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
+ val all_facts :
+ Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
+ -> thm list -> status Termtab.table
+ -> (((unit -> string) * stature) * thm) list
+ val all_facts_of : theory -> (((unit -> string) * stature) * thm) list
val nearly_all_facts :
Proof.context -> bool -> relevance_override -> thm list -> term list -> term
-> (((unit -> string) * stature) * thm) list
@@ -240,77 +241,6 @@
(Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
-fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
- let
- val thy = Proof_Context.theory_of ctxt
- val global_facts = Global_Theory.facts_of thy
- val local_facts = Proof_Context.facts_of ctxt
- val named_locals = local_facts |> Facts.dest_static []
- val assms = Assumption.all_assms_of ctxt
- fun is_good_unnamed_local th =
- not (Thm.has_name_hint th) andalso
- forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
- val unnamed_locals =
- union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
- |> filter is_good_unnamed_local |> map (pair "" o single)
- val full_space =
- Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
- fun add_facts global foldx facts =
- foldx (fn (name0, ths) =>
- if not exporter andalso name0 <> "" andalso
- forall (not o member Thm.eq_thm_prop add_ths) ths andalso
- (Facts.is_concealed facts name0 orelse
- (not (Config.get ctxt ignore_no_atp) andalso
- is_package_def name0) orelse
- exists (fn s => String.isSuffix s name0)
- (multi_base_blacklist ctxt ho_atp)) then
- I
- else
- let
- val multi = length ths > 1
- val backquote_thm =
- backquote o hackish_string_for_term ctxt o close_form o prop_of
- fun check_thms a =
- case try (Proof_Context.get_thms ctxt) a of
- NONE => false
- | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
- in
- pair 1
- #> fold (fn th => fn (j, (multis, unis)) =>
- (j + 1,
- if not (member Thm.eq_thm_prop add_ths th) andalso
- is_theorem_bad_for_atps ho_atp exporter th then
- (multis, unis)
- else
- let
- val new =
- (((fn () =>
- if name0 = "" then
- th |> backquote_thm
- else
- [Facts.extern ctxt facts name0,
- Name_Space.extern ctxt full_space name0,
- name0]
- |> find_first check_thms
- |> (fn SOME name =>
- make_name reserved multi j name
- | NONE => "")),
- stature_of_thm global assms chained_ths
- css_table name0 th), th)
- in
- if multi then (new :: multis, unis)
- else (multis, new :: unis)
- end)) ths
- #> snd
- end)
- in
- (* The single-name theorems go after the multiple-name ones, so that single
- names are preferred when both are available. *)
- ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
- |> add_facts true Facts.fold_static global_facts global_facts
- |> op @
- end
-
fun clasimpset_rule_table_of ctxt =
let
val thy = Proof_Context.theory_of ctxt
@@ -416,6 +346,84 @@
fun maybe_filter_no_atps ctxt =
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
+fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val global_facts = Global_Theory.facts_of thy
+ val local_facts = Proof_Context.facts_of ctxt
+ val named_locals = local_facts |> Facts.dest_static []
+ val assms = Assumption.all_assms_of ctxt
+ fun is_good_unnamed_local th =
+ not (Thm.has_name_hint th) andalso
+ forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
+ val unnamed_locals =
+ union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
+ |> filter is_good_unnamed_local |> map (pair "" o single)
+ val full_space =
+ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
+ fun add_facts global foldx facts =
+ foldx (fn (name0, ths) =>
+ if not exporter andalso name0 <> "" andalso
+ forall (not o member Thm.eq_thm_prop add_ths) ths andalso
+ (Facts.is_concealed facts name0 orelse
+ (not (Config.get ctxt ignore_no_atp) andalso
+ is_package_def name0) orelse
+ exists (fn s => String.isSuffix s name0)
+ (multi_base_blacklist ctxt ho_atp)) then
+ I
+ else
+ let
+ val multi = length ths > 1
+ val backquote_thm =
+ backquote o hackish_string_for_term ctxt o close_form o prop_of
+ fun check_thms a =
+ case try (Proof_Context.get_thms ctxt) a of
+ NONE => false
+ | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
+ in
+ pair 1
+ #> fold (fn th => fn (j, (multis, unis)) =>
+ (j + 1,
+ if not (member Thm.eq_thm_prop add_ths th) andalso
+ is_theorem_bad_for_atps ho_atp exporter th then
+ (multis, unis)
+ else
+ let
+ val new =
+ (((fn () =>
+ if name0 = "" then
+ th |> backquote_thm
+ else
+ [Facts.extern ctxt facts name0,
+ Name_Space.extern ctxt full_space name0,
+ name0]
+ |> find_first check_thms
+ |> (fn SOME name =>
+ make_name reserved multi j name
+ | NONE => "")),
+ stature_of_thm global assms chained_ths
+ css_table name0 th), th)
+ in
+ if multi then (new :: multis, unis)
+ else (multis, new :: unis)
+ end)) ths
+ #> snd
+ end)
+ in
+ (* The single-name theorems go after the multiple-name ones, so that single
+ names are preferred when both are available. *)
+ ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+ |> add_facts true Facts.fold_static global_facts global_facts
+ |> op @
+ end
+
+fun all_facts_of thy =
+ let val ctxt = Proof_Context.init_global thy in
+ all_facts ctxt false Symtab.empty true [] []
+ (clasimpset_rule_table_of ctxt)
+ |> rev (* try to restore the original order of facts, for MaSh *)
+ end
+
fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override)
chained_ths hyp_ts concl_t =
if only andalso null add then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200
@@ -6,6 +6,35 @@
signature SLEDGEHAMMER_FILTER_MASH =
sig
+ type status = ATP_Problem_Generate.status
+ type stature = ATP_Problem_Generate.stature
+ type params = Sledgehammer_Provers.params
+ type prover_result = Sledgehammer_Provers.prover_result
+
+ val fact_name_of : string -> string
+ val all_non_tautological_facts_of :
+ theory -> (((unit -> string) * stature) * thm) list
+ val theory_ord : theory * theory -> order
+ val thm_ord : thm * thm -> order
+ val thms_by_thy : ('a * thm) list -> (string * thm list) list
+ val has_thy : theory -> thm -> bool
+ val parent_thms : (string * thm list) list -> theory -> string list
+ val features_of : theory -> status * thm -> string list
+ val isabelle_dependencies_of : string list -> thm -> string list
+ val goal_of_thm : theory -> thm -> thm
+ val iter_facts :
+ Proof.context -> params -> int -> thm
+ -> (((unit -> string) * stature) * thm) list
+ -> ((string * stature) * thm) list
+ val run_prover :
+ Proof.context -> params -> ((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 -> params -> theory -> bool -> string -> unit
+
val reset : unit -> unit
val can_suggest : unit -> bool
val can_learn_thy : theory -> bool
@@ -16,6 +45,16 @@
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
struct
+open ATP_Util
+open ATP_Problem_Generate
+open Sledgehammer_Util
+open Sledgehammer_Fact
+open Sledgehammer_Filter_Iter
+open Sledgehammer_Provers
+
+
+(*** Low-level communication with MaSh ***)
+
fun mash_reset () =
tracing "MaSh RESET"
@@ -30,6 +69,311 @@
tracing ("MaSh SUGGEST " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^
space_implode " " feats)
+
+(*** Isabelle helpers ***)
+
+val fact_name_of = prefix fact_prefix o ascii_of
+
+fun escape_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)
+
+val escape_meta = String.translate escape_meta_char
+
+val thy_prefix = "y_"
+
+val fact_name_of = escape_meta
+val thy_name_of = prefix thy_prefix o escape_meta
+val const_name_of = prefix const_prefix o escape_meta
+val type_name_of = prefix type_const_prefix o escape_meta
+val class_name_of = prefix class_prefix o escape_meta
+
+val thy_name_of_thm = theory_of_thm #> Context.theory_name
+
+local
+
+fun has_bool @{typ bool} = true
+ | has_bool (Type (_, Ts)) = exists has_bool Ts
+ | has_bool _ = false
+
+fun has_fun (Type (@{type_name fun}, _)) = true
+ | has_fun (Type (_, Ts)) = exists has_fun Ts
+ | has_fun _ = false
+
+val is_conn = member (op =)
+ [@{const_name Trueprop}, @{const_name HOL.conj}, @{const_name HOL.disj},
+ @{const_name HOL.implies}, @{const_name Not},
+ @{const_name All}, @{const_name Ex}, @{const_name Ball}, @{const_name Bex},
+ @{const_name HOL.eq}]
+
+val has_bool_arg_const =
+ exists_Const (fn (c, T) =>
+ not (is_conn c) andalso exists has_bool (binder_types T))
+
+fun higher_inst_const thy (c, T) =
+ case binder_types T of
+ [] => false
+ | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts
+
+val binders = [@{const_name All}, @{const_name Ex}]
+
+in
+
+fun is_fo_term thy t =
+ let
+ val t =
+ t |> Envir.beta_eta_contract
+ |> transform_elim_prop
+ |> Object_Logic.atomize_term thy
+ in
+ Term.is_first_order binders t andalso
+ not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
+ | _ => false) t orelse
+ has_bool_arg_const t orelse exists_Const (higher_inst_const thy) t)
+ end
+
+end
+
+fun interesting_terms_types_and_classes term_max_depth type_max_depth t =
+ let
+ val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}]
+ val bad_consts = atp_widely_irrelevant_consts
+ 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)) = 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 ^ ")"
+ else s
+ fun patternify ~1 _ = ""
+ | patternify depth t =
+ case strip_comb t of
+ (Const (s, _), args) =>
+ mk_app (const_name_of s) (map (patternify (depth - 1)) args)
+ | _ => ""
+ fun add_term_patterns ~1 _ = I
+ | add_term_patterns depth t =
+ insert (op =) (patternify depth t)
+ #> add_term_patterns (depth - 1) t
+ val add_term = add_term_patterns term_max_depth
+ fun add_patterns t =
+ let val (head, args) = strip_comb t in
+ (case head of
+ Const (s, T) =>
+ not (member (op =) bad_consts s) ? (add_term t #> add_type T)
+ | Free (_, T) => add_type T
+ | Var (_, T) => add_type T
+ | Abs (_, T, body) => add_type T #> add_patterns body
+ | _ => I)
+ #> fold add_patterns args
+ end
+ in [] |> add_patterns t |> sort string_ord end
+
+fun is_likely_tautology th =
+ null (interesting_terms_types_and_classes 0 ~1 (prop_of th)) andalso
+ not (Thm.eq_thm_prop (@{thm ext}, th))
+
+fun is_too_meta thy th =
+ fastype_of (Object_Logic.atomize_term thy (prop_of th)) <> @{typ bool}
+
+fun all_non_tautological_facts_of thy =
+ all_facts_of thy
+ |> filter_out ((is_likely_tautology orf is_too_meta thy) o snd)
+
+fun theory_ord p =
+ if Theory.eq_thy p then EQUAL
+ else if Theory.subthy p then LESS
+ else if Theory.subthy (swap p) then GREATER
+ else EQUAL
+
+val thm_ord = theory_ord o pairself theory_of_thm
+
+fun thms_by_thy ths =
+ ths |> map (snd #> `thy_name_of_thm)
+ |> AList.group (op =)
+ |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm
+ o hd o snd))
+ |> map (apsnd (sort thm_ord))
+
+fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th)
+
+fun parent_thms thy_ths thy =
+ Theory.parents_of thy
+ |> map Context.theory_name
+ |> map_filter (AList.lookup (op =) thy_ths)
+ |> map List.last
+ |> map (fact_name_of o Thm.get_name_hint)
+
+fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1})
+
+val max_depth = 1
+
+(* TODO: Generate type classes for types? *)
+fun features_of thy (status, th) =
+ let val t = Thm.prop_of th in
+ thy_name_of (thy_name_of_thm th) ::
+ interesting_terms_types_and_classes max_depth max_depth t
+ |> not (has_no_lambdas t) ? cons "lambdas"
+ |> exists_Const is_exists t ? cons "skolems"
+ |> not (is_fo_term thy t) ? cons "ho"
+ |> (case status of
+ General => I
+ | Induction => cons "induction"
+ | Intro => cons "intro"
+ | Inductive => cons "inductive"
+ | Elim => cons "elim"
+ | Simp => cons "simp"
+ | Def => cons "def")
+ end
+
+fun isabelle_dependencies_of all_facts =
+ thms_in_proof (SOME all_facts)
+ #> map fact_name_of #> sort string_ord
+
+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
+
+fun goal_of_thm thy = prop_of #> freeze #> cterm_of thy #> Goal.init
+
+fun iter_facts ctxt ({provers, relevance_thresholds, ...} : params) max_relevant
+ goal =
+ let
+ 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 =
+ Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
+ val relevance_override = {add = [], del = [], only = false}
+ in
+ iterative_relevant_facts ctxt relevance_thresholds max_relevant
+ is_built_in_const relevance_fudge
+ relevance_override [] hyp_ts concl_t
+ end
+
+fun run_prover ctxt (params as {provers, ...}) facts goal =
+ let
+ val problem =
+ {state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
+ facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+ val prover =
+ Sledgehammer_Minimize.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 ""
+ fun do_thm th prevs =
+ let
+ val s = th ^ ": " ^ space_implode " " prevs ^ "\n"
+ val _ = File.append path s
+ in [th] end
+ val thy_ths =
+ all_non_tautological_facts_of thy
+ |> not include_thy ? filter_out (has_thy thy o snd)
+ |> thms_by_thy
+ fun do_thy ths =
+ let
+ 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)
+ in fold do_thm ths parents; () end
+ in List.app (do_thy o snd) thy_ths end
+
+fun generate_features thy include_thy file_name =
+ let
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val facts =
+ all_non_tautological_facts_of thy
+ |> not include_thy ? filter_out (has_thy thy o snd)
+ fun do_fact ((_, (_, status)), th) =
+ let
+ val name = Thm.get_name_hint th
+ val feats = features_of thy (status, th)
+ val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n"
+ in File.append path s end
+ in List.app do_fact facts end
+
+fun generate_isa_dependencies thy include_thy file_name =
+ let
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val ths =
+ all_non_tautological_facts_of thy
+ |> not include_thy ? filter_out (has_thy thy o snd)
+ |> map snd
+ val all_names = ths |> map Thm.get_name_hint
+ fun do_thm th =
+ let
+ val name = Thm.get_name_hint th
+ val deps = isabelle_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_atp_dependencies ctxt (params as {max_relevant, ...}) thy
+ include_thy file_name =
+ let
+ val path = file_name |> Path.explode
+ val _ = File.write path ""
+ val facts =
+ all_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 is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep
+ fun add_isa_dep facts dep accum =
+ if exists (is_dep dep) accum then
+ accum
+ else case find_first (is_dep dep) facts of
+ SOME ((name, status), th) => accum @ [((name (), status), th)]
+ | NONE => accum (* shouldn't happen *)
+ fun fix_name ((_, stature), th) =
+ ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
+ fun do_thm th =
+ let
+ val name = Thm.get_name_hint th
+ val goal = goal_of_thm thy th
+ val deps =
+ case isabelle_dependencies_of all_names th of
+ [] => []
+ | isa_dep as [_] => isa_dep (* can hardly beat that *)
+ | isa_deps =>
+ let
+ val facts =
+ facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
+ val facts =
+ facts |> iter_facts ctxt params (the max_relevant) goal
+ |> fold (add_isa_dep facts) isa_deps
+ |> map fix_name
+ in
+ case run_prover ctxt params facts goal of
+ {outcome = NONE, used_facts, ...} =>
+ used_facts |> map fst |> sort string_ord
+ | _ => isa_deps
+ end
+ val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n"
+ in File.append path s end
+ in List.app do_thm ths end
+
+
+(*** High-level communication with MaSh ***)
+
fun reset () =
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 11 21:43:19 2012 +0200
@@ -14,6 +14,7 @@
val subgoal_count : Proof.state -> int
val normalize_chained_theorems : thm list -> thm list
val reserved_isar_keyword_table : unit -> unit Symtab.table
+ val thms_in_proof : string list option -> thm -> string list
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -60,4 +61,36 @@
Keyword.dest () |-> union (op =)
|> map (rpair ()) |> Symtab.make
+(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
+ fixes that seem to be missing over there; or maybe the two code portions are
+ not doing the same? *)
+fun fold_body_thms thm_name f =
+ let
+ fun app n (PBody {thms, ...}) =
+ thms |> fold (fn (_, (name, prop, body)) => fn x =>
+ let
+ val body' = Future.join body
+ val n' =
+ n + (if name = "" orelse
+ (* uncommon case where the proved theorem occurs twice
+ (e.g., "Transitive_Closure.trancl_into_trancl") *)
+ (n = 1 andalso name = thm_name) then
+ 0
+ else
+ 1)
+ val x' = x |> n' <= 1 ? app n' body'
+ in (x' |> n = 1 ? f (name, prop, body')) end)
+ in fold (app 0) end
+
+fun thms_in_proof all_names th =
+ let
+ val is_name_ok =
+ case all_names of
+ SOME names => member (op =) names
+ | NONE => (fn s => s <> "" andalso not (String.isPrefix "Pure." s))
+ fun collect (s, _, _) = is_name_ok s ? insert (op =) s
+ val names =
+ [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
+ in names end
+
end;