--- a/src/HOL/TPTP/atp_theory_export.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jan 04 21:56:20 2013 +0100
@@ -137,12 +137,12 @@
val atp_problem =
atp_problem
|> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
- val all_names = Sledgehammer_Fact.build_all_names Thm.get_name_hint facts
+ val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
val infers =
facts
|> map (fn (_, th) =>
(fact_name_of (Thm.get_name_hint th),
- th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
+ th |> Sledgehammer_Util.thms_in_proof (SOME name_tabs)
|> map fact_name_of))
val all_atp_problem_names =
atp_problem |> maps (map ident_of_problem_line o snd)
--- a/src/HOL/TPTP/mash_eval.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jan 04 21:56:20 2013 +0100
@@ -46,7 +46,7 @@
val lines = sugg_path |> File.read_lines
val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
- val all_names = build_all_names nickname_of_thm facts
+ 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_string (j, s) = s ^ "@" ^ string_of_int j
fun str_of_res label facts ({outcome, run_time, used_facts, ...}
@@ -79,7 +79,7 @@
| 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 isar_deps = isar_dependencies_of name_tabs 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
--- a/src/HOL/TPTP/mash_export.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Fri Jan 04 21:56:20 2013 +0100
@@ -79,15 +79,15 @@
in File.append path s end
in List.app do_fact facts end
-fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+fun isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
isar_deps_opt =
(case params_opt of
SOME (params as {provers = prover :: _, ...}) =>
- prover_dependencies_of ctxt params prover 0 facts all_names th |> snd
+ prover_dependencies_of ctxt params prover 0 facts name_tabs th |> snd
| NONE =>
case isar_deps_opt of
SOME deps => deps
- | NONE => isar_dependencies_of all_names th)
+ | NONE => isar_dependencies_of name_tabs th)
|> these
fun generate_isar_or_prover_dependencies ctxt params_opt range thys include_thys
@@ -96,14 +96,14 @@
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_thm facts
+ val name_tabs = build_name_tables nickname_of_thm facts
fun do_fact (j, (_, th)) =
if in_range range j then
let
val name = nickname_of_thm th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val deps =
- isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+ isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
NONE
in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
else
@@ -128,16 +128,16 @@
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_thm facts
+ val name_tabs = build_name_tables nickname_of_thm facts
fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
if in_range range j then
let
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
- val isar_deps = isar_dependencies_of all_names th
+ val isar_deps = isar_dependencies_of name_tabs th
val deps =
- isar_or_prover_dependencies_of ctxt params_opt facts all_names th
+ isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
(SOME isar_deps)
val core =
escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
@@ -169,13 +169,13 @@
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_thm facts
+ val name_tabs = build_name_tables nickname_of_thm facts
fun do_fact ((_, th), old_facts) =
let
val name = nickname_of_thm th
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
+ val isar_deps = isar_dependencies_of name_tabs th
in
if is_bad_query ctxt ho_atp th (these isar_deps) then
""
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jan 04 21:56:20 2013 +0100
@@ -26,8 +26,9 @@
val backquote_thm : Proof.context -> thm -> string
val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
- val build_all_names :
- (thm -> string) -> ('a * thm) list -> string Symtab.table
+ val build_name_tables :
+ (thm -> string) -> ('a * thm) list
+ -> string Symtab.table * string Symtab.table
val maybe_instantiate_inducts :
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
@@ -338,16 +339,19 @@
SOME (pref, suf) => [s, pref ^ suf]
| NONE => [s]
-fun build_all_names name_of facts =
+fun build_name_tables name_of facts =
let
fun cons_thm (_, th) = Termtab.cons_list (normalize_eq_etc (prop_of th), th)
- fun add_alias canon alias =
- fold (fn s => Symtab.update (s, name_of (if_thm_before canon alias)))
- (un_class_ify (Thm.get_name_hint canon))
- fun add_aliases (_, aliases as canon :: _) =
- fold (add_alias canon) aliases
- val tab = fold_rev cons_thm facts Termtab.empty
- in Termtab.fold add_aliases tab Symtab.empty end
+ fun add_plain canon alias =
+ Symtab.update (Thm.get_name_hint canon,
+ name_of (if_thm_before canon alias))
+ fun add_plains (_, aliases as canon :: _) = fold (add_plain canon) aliases
+ fun add_inclass (name, target) =
+ fold (fn s => Symtab.update (s, target)) (un_class_ify name)
+ val prop_tab = fold_rev cons_thm facts Termtab.empty
+ val plain_name_tab = Termtab.fold add_plains prop_tab Symtab.empty
+ val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
+ in (plain_name_tab, inclass_name_tab) end
fun uniquify facts =
Termtab.fold (cons o snd)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 04 21:56:20 2013 +0100
@@ -59,10 +59,12 @@
val features_of :
Proof.context -> string -> theory -> stature -> term list
-> (string * real) list
- val isar_dependencies_of : string Symtab.table -> thm -> string list option
+ val isar_dependencies_of :
+ string Symtab.table * string Symtab.table -> thm -> string list option
val prover_dependencies_of :
- Proof.context -> params -> string -> int -> fact list -> string Symtab.table
- -> thm -> bool * string list option
+ Proof.context -> params -> string -> int -> fact list
+ -> string Symtab.table * string Symtab.table -> thm
+ -> bool * string list option
val weight_mash_facts : 'a list -> ('a * real) list
val find_mash_suggestions :
int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
@@ -643,12 +645,12 @@
else
deps)
-fun isar_dependencies_of all_names th =
- th |> thms_in_proof (SOME all_names) |> trim_dependencies th
+fun isar_dependencies_of name_tabs th =
+ th |> thms_in_proof (SOME name_tabs) |> trim_dependencies th
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover
- auto_level facts all_names th =
- case isar_dependencies_of all_names th of
+ auto_level facts name_tabs th =
+ case isar_dependencies_of name_tabs th of
SOME [] => (false, SOME [])
| isar_deps =>
let
@@ -871,16 +873,16 @@
""
else
let
- val all_names = build_all_names nickname_of_thm facts
+ val name_tabs = build_name_tables nickname_of_thm facts
fun deps_of status th =
if status = Non_Rec_Def orelse status = Rec_Def then
SOME []
else if run_prover then
- prover_dependencies_of ctxt params prover auto_level facts all_names
+ prover_dependencies_of ctxt params prover auto_level facts name_tabs
th
|> (fn (false, _) => NONE | (true, deps) => deps)
else
- isar_dependencies_of all_names th
+ isar_dependencies_of name_tabs th
fun do_commit [] [] [] state = state
| do_commit learns relearns flops {access_G, dirty} =
let
@@ -985,7 +987,7 @@
Isar_Proof => 0
| Automatic_Proof => 2 * max_isar
| Isar_Proof_wegen_Prover_Flop => max_isar)
- - 500 * (th |> isar_dependencies_of all_names
+ - 500 * (th |> isar_dependencies_of name_tabs
|> Option.map length
|> the_default max_dependencies)
val old_facts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 04 21:56:19 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jan 04 21:56:20 2013 +0100
@@ -18,7 +18,8 @@
val parse_time_option : string -> string -> Time.time option
val subgoal_count : Proof.state -> int
val reserved_isar_keyword_table : unit -> unit Symtab.table
- val thms_in_proof : string Symtab.table option -> thm -> string list
+ val thms_in_proof :
+ (string Symtab.table * string Symtab.table) option -> thm -> string list
val thms_of_name : Proof.context -> string -> thm list
val one_day : Time.time
val one_year : Time.time
@@ -86,36 +87,43 @@
(* 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 name_map =
+fun fold_body_thms outer_name (map_plain_name, map_inclass_name) =
let
- val thm_name' = name_map thm_name
- fun app n (PBody {thms, ...}) =
+ fun app map_name n (PBody {thms, ...}) =
thms |> fold (fn (_, (name, _, body)) => fn accum =>
let
- val name' = name_map name
- val collect = union (op =) o the_list
- (* The "name = thm_name" case caters for the uncommon case where the
- proved theorem occurs in its own proof (e.g.,
- "Transitive_Closure.trancl_into_trancl"). The "name' = thm_name'"
- case is to unfold low-level class facts ("Xxx.yyy.zzz") in the
- proof of high-level class facts ("XXX.yyy_class.zzz"). *)
- val no_name =
- (name = "" orelse
- (n = 1 andalso (name = thm_name orelse name' = thm_name')))
+ val collect = union (op =) o the_list o map_name
+ (* The "name = outer_name" case caters for the uncommon case where
+ the proved theorem occurs in its own proof (e.g.,
+ "Transitive_Closure.trancl_into_trancl"). *)
+ val (anonymous, enter_class) =
+ if name = "" orelse (n = 1 andalso name = outer_name) then
+ (true, false)
+ else if n = 1 andalso map_inclass_name name = SOME outer_name then
+ (true, true)
+ else
+ (false, false)
val accum =
- accum |> (if n = 1 andalso not no_name then collect name' else I)
- val n = n + (if no_name then 0 else 1)
- in accum |> (if n <= 1 then app n (Future.join body) else I) end)
- in fold (app 0) end
+ accum |> (if n = 1 andalso not anonymous then collect name else I)
+ val n = n + (if anonymous then 0 else 1)
+ in
+ accum
+ |> (if n <= 1 then
+ app (if enter_class then map_inclass_name else map_name) n
+ (Future.join body)
+ else
+ I)
+ end)
+ in fold (app map_plain_name 0) end
-fun thms_in_proof all_names th =
+fun thms_in_proof name_tabs th =
let
- val name_map =
- case all_names of
- SOME names => Symtab.lookup names
- | NONE => SOME
+ val map_names =
+ case name_tabs of
+ SOME p => pairself Symtab.lookup p
+ | NONE => `I SOME
val names =
- [] |> fold_body_thms (Thm.get_name_hint th) name_map [Thm.proof_body_of th]
+ fold_body_thms (Thm.get_name_hint th) map_names [Thm.proof_body_of th] []
in names end
fun thms_of_name ctxt name =