# HG changeset patch # User blanchet # Date 1357332980 -3600 # Node ID 6b232d76cbc991623ee2e3bf836a9ff195b60d17 # Parent 73612ad116e6408f564187a09aa75fc48fe874e1 refined class handling, to prevent cycles in fact graph diff -r 73612ad116e6 -r 6b232d76cbc9 src/HOL/TPTP/atp_theory_export.ML --- 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) diff -r 73612ad116e6 -r 6b232d76cbc9 src/HOL/TPTP/mash_eval.ML --- 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 diff -r 73612ad116e6 -r 6b232d76cbc9 src/HOL/TPTP/mash_export.ML --- 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 "" diff -r 73612ad116e6 -r 6b232d76cbc9 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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) diff -r 73612ad116e6 -r 6b232d76cbc9 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 = diff -r 73612ad116e6 -r 6b232d76cbc9 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 =