# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID 252f45c04042fed8c63c1c2e010f1614cdf454be # Parent 82d6e46c673f79071bd7124c5bca77edb27fb178 drastic overhaul of MaSh data structures + fixed a few performance issues diff -r 82d6e46c673f -r 252f45c04042 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -134,7 +134,7 @@ atp_problem |> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) val ths = facts |> map snd - val all_names = ths |> map Thm.get_name_hint + val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make val infers = facts |> map (fn (_, th) => (fact_name_of (Thm.get_name_hint th), diff -r 82d6e46c673f -r 252f45c04042 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 @@ -26,6 +26,10 @@ val max_facts_slack = 2 +val all_names = + filter_out (is_likely_tautology orf is_too_meta) + #> map (rpair () o Thm.get_name_hint) #> Symtab.make + fun evaluate_mash_suggestions ctxt params thy file_name = let val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = @@ -36,10 +40,7 @@ val lines = path |> File.read_lines val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = all_facts_of thy css_table - val all_names = - facts |> map snd - |> filter_out (is_likely_tautology orf is_too_meta) - |> map Thm.get_name_hint + val all_names = all_names (facts |> map snd) val iter_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 val mesh_ok = Unsynchronized.ref 0 diff -r 82d6e46c673f -r 252f45c04042 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -26,8 +26,31 @@ open Sledgehammer_Filter_Iter open Sledgehammer_Filter_MaSh +fun thy_map_from_facts ths = + ths |> sort (thm_ord o swap o pairself snd) + |> map (snd #> `(theory_of_thm #> Context.theory_name)) + |> AList.coalesce (op =) + |> map (apsnd (map Thm.get_name_hint)) + +fun has_thy thy th = + Context.theory_name thy = Context.theory_name (theory_of_thm th) + +fun parent_facts thy thy_map = + let + fun add_last thy = + case AList.lookup (op =) thy_map (Context.theory_name thy) of + SOME (last_fact :: _) => insert (op =) last_fact + | _ => add_parent thy + and add_parent thy = fold add_last (Theory.parents_of thy) + in add_parent thy [] end + +val thy_name_of_fact = hd o Long_Name.explode fun thy_of_fact thy = Context.this_theory thy o thy_name_of_fact +val all_names = + filter_out (is_likely_tautology orf is_too_meta) + #> map (rpair () o Thm.get_name_hint) #> Symtab.make + fun generate_accessibility thy include_thy file_name = let val path = file_name |> Path.explode @@ -72,9 +95,7 @@ all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> map snd - val all_names = - ths |> filter_out (is_likely_tautology orf is_too_meta) - |> map Thm.get_name_hint + val all_names = all_names ths fun do_thm th = let val name = Thm.get_name_hint th @@ -92,9 +113,7 @@ all_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd - val all_names = - ths |> filter_out (is_likely_tautology orf is_too_meta) - |> map Thm.get_name_hint + val all_names = all_names ths fun is_dep dep (_, th) = Thm.get_name_hint th = dep fun add_isa_dep facts dep accum = if exists (is_dep dep) accum then @@ -142,9 +161,7 @@ facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) val ths = facts |> map snd - val all_names = - ths |> filter_out (is_likely_tautology orf is_too_meta) - |> map Thm.get_name_hint + val all_names = all_names ths fun do_fact ((_, (_, status)), th) prevs = let val name = Thm.get_name_hint th diff -r 82d6e46c673f -r 252f45c04042 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Jul 18 08:44:04 2012 +0200 @@ -91,12 +91,6 @@ InternalError | UnknownError of string -fun elide_string threshold s = - if size s > threshold then - String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ - String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) - else - s fun short_output verbose output = if verbose then if output = "" then "No details available" else elide_string 1000 output diff -r 82d6e46c673f -r 252f45c04042 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 18 08:44:04 2012 +0200 @@ -12,6 +12,7 @@ val stringN_of_int : int -> int -> string val strip_spaces : bool -> (char -> bool) -> string -> string val strip_spaces_except_between_idents : string -> string + val elide_string : int -> string -> string val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string @@ -106,6 +107,13 @@ fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" val strip_spaces_except_between_idents = strip_spaces true is_ident_char +fun elide_string threshold s = + if size s > threshold then + String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ + String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) + else + s + val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) fun nat_subscript n = n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript diff -r 82d6e46c673f -r 252f45c04042 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -30,27 +30,27 @@ val is_too_meta : thm -> bool val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order - val thy_map_from_facts : fact list -> (string * string list) list - val has_thy : theory -> thm -> bool - val parent_facts : theory -> (string * string list) list -> string list val features_of : theory -> status -> term list -> string list - val isabelle_dependencies_of : string list -> thm -> string list + val isabelle_dependencies_of : unit Symtab.table -> thm -> string list val goal_of_thm : theory -> thm -> thm val run_prover : Proof.context -> params -> fact list -> thm -> prover_result - val thy_name_of_fact : string -> string val mash_RESET : Proof.context -> unit + val mash_INIT : + Proof.context -> bool + -> (string * string list * string list * string list) list -> unit val mash_ADD : - Proof.context -> (string * string list * string list * string list) list - -> unit - val mash_DEL : Proof.context -> string list -> string list -> unit - val mash_QUERY : Proof.context -> string list * string list -> string list + Proof.context -> bool + -> (string * string list * string list * string list) list -> unit + val mash_QUERY : + Proof.context -> bool -> string list * string list -> string list val mash_reset : Proof.context -> unit val mash_can_suggest_facts : Proof.context -> bool val mash_suggest_facts : Proof.context -> params -> string -> term list -> term -> fact list -> fact list - val mash_learn_thy : Proof.context -> theory -> real -> unit - val mash_learn_proof : Proof.context -> theory -> term -> thm list -> unit + val mash_learn_thy : Proof.context -> params -> theory -> real -> unit + val mash_learn_proof : + Proof.context -> params -> term -> thm list -> fact list -> unit val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list -> term -> fact list -> fact list @@ -79,7 +79,7 @@ fun mash_home () = getenv "MASH_HOME" fun mash_state_dir () = getenv "ISABELLE_HOME_USER" ^ "/mash" - |> tap (fn dir => Isabelle_System.mkdir (Path.explode dir)) + |> tap (Isabelle_System.mkdir o Path.explode) fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode (*** Isabelle helpers ***) @@ -161,10 +161,11 @@ exists_Const (fn (c, T) => not (is_conn c) andalso exists has_bool (binder_types T)) -fun higher_inst_const thy (c, T) = +fun higher_inst_const thy (s, T) = case binder_types T of [] => false - | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts + | Ts => length (binder_types (Sign.the_const_type thy s)) <> length Ts + handle TYPE _ => false val binders = [@{const_name All}, @{const_name Ex}] @@ -246,24 +247,6 @@ val thm_ord = theory_ord o pairself theory_of_thm -fun thy_map_from_facts ths = - ths |> sort (thm_ord o swap o pairself snd) - |> map (snd #> `(theory_of_thm #> Context.theory_name)) - |> AList.coalesce (op =) - |> map (apsnd (map Thm.get_name_hint)) - -fun has_thy thy th = - Context.theory_name thy = Context.theory_name (theory_of_thm th) - -fun parent_facts thy thy_map = - let - fun add_last thy = - case AList.lookup (op =) thy_map (Context.theory_name thy) of - SOME (last_fact :: _) => insert (op =) last_fact - | _ => add_parent thy - and add_parent thy = fold add_last (Theory.parents_of thy) - in add_parent thy [] end - fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) val term_max_depth = 1 @@ -310,41 +293,67 @@ Sledgehammer_Provers.Normal (hd provers) in prover params (K (K (K ""))) problem end -fun accessibility_of thy thy_map = - case AList.lookup (op =) thy_map (Context.theory_name thy) of - SOME (fact :: _) => [fact] - | _ => parent_facts thy thy_map - -val thy_name_of_fact = hd o Long_Name.explode - (*** Low-level communication with MaSh ***) -fun run_mash ctxt save write_cmds read_preds = +val max_preds = 500 + +fun mash_info overlord = + if overlord then (getenv "ISABELLE_HOME_USER", "") + else (getenv "ISABELLE_TMP", serial_string ()) + +fun run_mash ctxt (temp_dir, serial) core = let - val temp_dir = getenv "ISABELLE_TMP" - val serial = serial_string () - val cmd_file = temp_dir ^ "/mash_commands." ^ serial - val cmd_path = Path.explode cmd_file - val pred_file = temp_dir ^ "/mash_preds." ^ serial - val log_file = temp_dir ^ "/mash_log." ^ serial + val log_file = temp_dir ^ "/mash_log" ^ serial + val err_file = temp_dir ^ "/mash_err" ^ serial val command = - mash_home () ^ "/mash.py --quiet --inputFile " ^ cmd_file ^ - " --outputDir " ^ mash_state_dir () ^ " --predictions " ^ pred_file ^ - " --log " ^ log_file ^ " --numberOfPredictions 1000" ^ - (if save then " --saveModel" else "") - val _ = File.write cmd_path "" - val _ = write_cmds (File.append cmd_path) - val _ = trace_msg ctxt (fn () => " running " ^ command) - val _ = Isabelle_System.bash command - in read_preds (fn () => File.read_lines (Path.explode pred_file)) end + mash_home () ^ "/mash.py --quiet --outputDir " ^ mash_state_dir () ^ + " --log " ^ log_file ^ " " ^ core ^ " 2>&1 > " ^ err_file + in + trace_msg ctxt (fn () => "Running " ^ command); + Isabelle_System.bash command; () + end + +fun write_file write file = + let val path = Path.explode file in + File.write path ""; write (File.append path) + end -fun str_of_update (fact, access, feats, deps) = - "! " ^ escape_meta fact ^ ": " ^ escape_metas access ^ "; " ^ +fun run_mash_init ctxt overlord write_access write_feats write_deps = + let + val info as (temp_dir, serial) = mash_info overlord + val in_dir = temp_dir ^ "/mash_init" ^ serial + |> tap (Isabelle_System.mkdir o Path.explode) + in + write_file write_access (in_dir ^ "/mash_accessibility"); + write_file write_feats (in_dir ^ "/mash_features"); + write_file write_deps (in_dir ^ "/mash_dependencies"); + run_mash ctxt info ("--init --inputDir " ^ in_dir) + end + +fun run_mash_commands ctxt overlord save write_cmds read_preds = + let + val info as (temp_dir, serial) = mash_info overlord + val cmd_file = temp_dir ^ "/mash_commands" ^ serial + val pred_file = temp_dir ^ "/mash_preds" ^ serial + in + write_file write_cmds cmd_file; + run_mash ctxt info + ("--inputFile " ^ cmd_file ^ " --predictions " ^ pred_file ^ + " --numberOfPredictions " ^ string_of_int max_preds ^ + (if save then " --saveModel" else "")); + read_preds (fn () => File.read_lines (Path.explode pred_file)) + end + +fun str_of_update (name, parents, feats, deps) = + "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^ escape_metas feats ^ "; " ^ escape_metas deps ^ "\n" -fun str_of_query (access, feats) = - "? " ^ escape_metas access ^ "; " ^ escape_metas feats +fun str_of_query (parents, feats) = + "? " ^ escape_metas parents ^ "; " ^ escape_metas feats + +fun init_str_of_update get (upd as (name, _, _, _)) = + escape_meta name ^ ": " ^ escape_metas (get upd) ^ "\n" fun mash_RESET ctxt = let val path = mash_state_dir () |> Path.explode in @@ -354,30 +363,37 @@ path () end -fun mash_ADD _ [] = () - | mash_ADD ctxt upds = - (trace_msg ctxt (fn () => "MaSh ADD " ^ space_implode " " (map #1 upds)); - run_mash ctxt true (fn append => List.app (append o str_of_update) upds) - (K ())) +fun mash_INIT ctxt _ [] = mash_RESET ctxt + | mash_INIT ctxt overlord upds = + (trace_msg ctxt (fn () => "MaSh INIT " ^ + elide_string 1000 (space_implode " " (map #1 upds))); + run_mash_init ctxt overlord + (fn append => List.app (append o init_str_of_update #2) upds) + (fn append => List.app (append o init_str_of_update #3) upds) + (fn append => List.app (append o init_str_of_update #4) upds)) -fun mash_DEL ctxt facts feats = - trace_msg ctxt (fn () => - "MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) +fun mash_ADD _ _ [] = () + | mash_ADD ctxt overlord upds = + (trace_msg ctxt (fn () => "MaSh ADD " ^ + elide_string 1000 (space_implode " " (map #1 upds))); + run_mash_commands ctxt overlord true + (fn append => List.app (append o str_of_update) upds) (K ())) -fun mash_QUERY ctxt (query as (_, feats)) = +fun mash_QUERY ctxt overlord (query as (_, feats)) = (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); - run_mash ctxt false (fn append => append (str_of_query query)) - (fn preds => snd (extract_query (List.last (preds ())))) + run_mash_commands ctxt overlord false + (fn append => append (str_of_query query)) + (fn preds => snd (extract_query (List.last (preds ())))) handle List.Empty => []) (*** High-level communication with MaSh ***) type mash_state = - {dirty_thys : string list, - thy_map : (string * string list) list} + {thys : bool Symtab.table, + fact_graph : unit Graph.T} -val empty_state = {dirty_thys = [], thy_map = []} +val empty_state = {thys = Symtab.empty, fact_graph = Graph.empty} local @@ -386,27 +402,35 @@ let val path = mash_state_path () in (true, case try File.read_lines path of - SOME (dirty_line :: facts_lines) => + SOME (comp_thys :: incomp_thys :: fact_lines) => let - fun add_facts_line line = - case unescape_metas line of - thy :: facts => cons (thy, facts) - | _ => I (* shouldn't happen *) - in - {dirty_thys = unescape_metas dirty_line, - thy_map = fold_rev add_facts_line facts_lines []} - end + fun add_thy comp thy = Symtab.update (thy, comp) + fun add_fact_line line = + case extract_query line of + ("", _) => I (* shouldn't happen *) + | (name, parents) => + Graph.default_node (name, ()) + #> fold (fn par => Graph.add_edge (par, name)) parents + val thys = + Symtab.empty |> fold (add_thy true) (unescape_metas comp_thys) + |> fold (add_thy false) (unescape_metas incomp_thys) + val fact_graph = Graph.empty |> fold add_fact_line fact_lines + in {thys = thys, fact_graph = fact_graph} end | _ => empty_state) end -fun mash_save ({dirty_thys, thy_map} : mash_state) = +fun mash_save ({thys, fact_graph, ...} : mash_state) = let val path = mash_state_path () - val dirty_line = escape_metas dirty_thys ^ "\n" - fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n" + val thys = Symtab.dest thys + fun line_for_thys comp = AList.find (op =) thys comp |> escape_metas + fun fact_line_for name parents = name :: parents |> escape_metas + val append_fact = File.append path o suffix "\n" oo fact_line_for in - File.write path dirty_line; - List.app (File.append path o fact_line_for) thy_map + File.write path (line_for_thys true ^ "\n" ^ line_for_thys false ^ "\n"); + Graph.fold (fn (name, ((), (parents, _))) => fn () => + append_fact name (Graph.Keys.dest parents)) + fact_graph () end val global_state = @@ -427,52 +451,51 @@ end fun mash_can_suggest_facts (_ : Proof.context) = - mash_home () <> "" andalso not (null (#thy_map (mash_get ()))) + mash_home () <> "" andalso not (Graph.is_empty (#fact_graph (mash_get ()))) -fun mash_suggest_facts ctxt params prover hyp_ts concl_t facts = +fun parents_wrt facts fact_graph = + let + val facts = + Symtab.empty + |> fold (fn (_, th) => Symtab.update (Thm.get_name_hint th, ())) facts + in fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals end + +fun mash_suggest_facts ctxt ({overlord, ...} : params) prover hyp_ts concl_t + facts = let val thy = Proof_Context.theory_of ctxt - val thy_map = #thy_map (mash_get ()) - val access = accessibility_of thy thy_map + val fact_graph = #fact_graph (mash_get ()) + val parents = parents_wrt facts fact_graph val feats = features_of thy General (concl_t :: hyp_ts) - val suggs = mash_QUERY ctxt (access, feats) + val suggs = mash_QUERY ctxt overlord (parents, feats) in suggested_facts suggs facts end -fun is_fact_in_thy_map thy_map fact = - case AList.lookup (op =) thy_map (thy_name_of_fact fact) of - SOME facts => member (op =) facts fact - | NONE => false +fun add_thys_for thy = + let fun add comp thy = Symtab.update (Context.theory_name thy, comp) in + add false thy #> fold (add true) (Theory.ancestors_of thy) + end -fun zip_facts news [] = news - | zip_facts [] olds = olds - | zip_facts (new :: news) (old :: olds) = - if new = old then - new :: zip_facts news olds - else if member (op =) news old then - old :: zip_facts (filter_out (curry (op =) old) news) olds - else if member (op =) olds new then - new :: zip_facts news (filter_out (curry (op =) new) olds) - else - new :: old :: zip_facts news olds +fun update_fact_graph ctxt (name, parents, feats, deps) (upds, graph) = + let + fun maybe_add_from from (accum as (parents, graph)) = + (from :: parents, Graph.add_edge_acyclic (from, name) graph) + handle Graph.CYCLES _ => + (trace_msg ctxt (fn () => + "Cycle between " ^ quote from ^ " and " ^ quote name); accum) + | Graph.UNDEF _ => + (trace_msg ctxt (fn () => "Unknown node " ^ quote from); accum) + val graph = graph |> Graph.new_node (name, ()) + val (parents, graph) = ([], graph) |> fold maybe_add_from parents + val (deps, graph) = ([], graph) |> fold maybe_add_from deps + in ((name, parents, feats, deps) :: upds, graph) end -fun add_thy_map_from_thys [] old = old - | add_thy_map_from_thys new old = - let - fun add_thy (thy, new_facts) = - case AList.lookup (op =) old thy of - SOME old_facts => - AList.update (op =) (thy, zip_facts old_facts new_facts) - | NONE => cons (thy, new_facts) - in old |> fold add_thy new end - -fun mash_learn_thy ctxt thy timeout = +fun mash_learn_thy ctxt ({overlord, ...} : params) thy timeout = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val facts = all_facts_of thy css_table - val {thy_map, ...} = mash_get () - fun is_old (_, th) = is_fact_in_thy_map thy_map (Thm.get_name_hint th) - val (old_facts, new_facts) = - facts |> List.partition is_old ||> sort (thm_ord o pairself snd) + val {fact_graph, ...} = mash_get () + fun is_old (_, th) = can (Graph.get_node fact_graph) (Thm.get_name_hint th) + val new_facts = facts |> filter_out is_old |> sort (thm_ord o pairself snd) in if null new_facts then () @@ -481,39 +504,49 @@ val ths = facts |> map snd val all_names = ths |> filter_out (is_likely_tautology orf is_too_meta) - |> map Thm.get_name_hint - fun do_fact ((_, (_, status)), th) (prevs, upds) = + |> map (rpair () o Thm.get_name_hint) + |> Symtab.make + fun do_fact ((_, (_, status)), th) (parents, upds) = let val name = Thm.get_name_hint th val feats = features_of thy status [prop_of th] val deps = isabelle_dependencies_of all_names th - val upd = (name, prevs, feats, deps) + val upd = (name, parents, feats, deps) in ([name], upd :: upds) end - val parents = parent_facts thy thy_map - val (_, upds) = (parents, []) |> fold do_fact new_facts - val new_thy_map = new_facts |> thy_map_from_facts - fun trans {dirty_thys, thy_map} = - (mash_ADD ctxt (rev upds); - {dirty_thys = dirty_thys, - thy_map = thy_map |> add_thy_map_from_thys new_thy_map}) + val parents = parents_wrt facts fact_graph + val (_, upds) = (parents, []) |> fold do_fact new_facts ||> rev + fun trans {thys, fact_graph} = + let + val mash_INIT_or_ADD = + if Graph.is_empty fact_graph then mash_INIT else mash_ADD + val (upds, fact_graph) = + ([], fact_graph) |> fold (update_fact_graph ctxt) upds + in + (mash_INIT_or_ADD ctxt overlord (rev upds); + {thys = thys |> add_thys_for thy, + fact_graph = fact_graph}) + end in mash_map trans end end -fun mash_learn_proof ctxt thy t ths = - mash_map (fn state as {dirty_thys, thy_map} => - let val deps = ths |> map Thm.get_name_hint in - if forall (is_fact_in_thy_map thy_map) deps then +fun mash_learn_proof ctxt ({overlord, ...} : params) t used_ths facts = + let + val thy = Proof_Context.theory_of ctxt + val name = ATP_Util.timestamp () (* should be fairly fresh *) + val feats = features_of thy General [t] + val deps = used_ths |> map Thm.get_name_hint + in + mash_map (fn {thys, fact_graph} => let - val fact = ATP_Util.timestamp () (* should be fairly fresh *) - val access = accessibility_of thy thy_map - val feats = features_of thy General [t] + val parents = parents_wrt facts fact_graph + val upds = [(name, parents, feats, deps)] + val (upds, fact_graph) = + ([], fact_graph) |> fold (update_fact_graph ctxt) upds in - mash_ADD ctxt [(fact, access, feats, deps)]; - {dirty_thys = dirty_thys, thy_map = thy_map} - end - else - state - end) + mash_ADD ctxt overlord upds; + {thys = thys, fact_graph = fact_graph} + end) + end fun relevant_facts ctxt (params as {fact_filter, ...}) prover max_facts ({add, only, ...} : fact_override) hyp_ts concl_t facts = diff -r 82d6e46c673f -r 252f45c04042 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 18 08:44:04 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Jul 18 08:44:04 2012 +0200 @@ -13,7 +13,7 @@ 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 list option -> thm -> string list + val thms_in_proof : unit Symtab.table option -> thm -> string list end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = @@ -63,28 +63,24 @@ 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) + thms |> fold (fn (_, (name, _, body)) => fn accum => + let + (* The second disjunct caters for the uncommon case where the proved + theorem occurs in its own proof (e.g., + "Transitive_Closure.trancl_into_trancl"). *) + val no_name = (name = "" orelse (n = 1 andalso name = thm_name)) + val accum = + accum |> (if n = 1 andalso not no_name then f 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 fun thms_in_proof all_names th = let - val is_name_ok = + val collect = 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 + SOME names => (fn s => Symtab.defined names s ? insert (op =) s) + | NONE => insert (op =) val names = [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th] in names end