# HG changeset patch # User nipkow # Date 1356130330 -3600 # Node ID eefab127e9f16db3c4327f4af5a577694f726a81 # Parent 99af6b652b3afce67adecbde6a4c617907ae24f0# Parent 168befd6cfa660aef847c7d42e65fa4be37972ed merged diff -r 168befd6cfa6 -r eefab127e9f1 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri Dec 21 16:31:37 2012 +0100 +++ b/src/HOL/TPTP/mash_export.ML Fri Dec 21 23:52:10 2012 +0100 @@ -36,12 +36,6 @@ fun in_range (from, to) j = j >= from andalso (to = NONE orelse j <= the to) -fun thy_map_from_facts ths = - ths |> rev - |> map (snd #> `(theory_of_thm #> Context.theory_name)) - |> AList.coalesce (op =) - |> map (apsnd (map nickname_of)) - fun has_thm_thy th thy = Context.theory_name thy = Context.theory_name (theory_of_thm th) @@ -53,18 +47,6 @@ |> sort (thm_ord o pairself snd) end -fun add_thy_parent_facts thy_map thy = - 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.get_theory thy o thy_name_of_fact - fun generate_accessibility ctxt thys include_thys file_name = let val path = file_name |> Path.explode @@ -74,16 +56,11 @@ val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" val _ = File.append path s in [fact] end - val thy_map = + val facts = all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd) - |> thy_map_from_facts - fun do_thy facts = - let - val thy = thy_of_fact (Proof_Context.theory_of ctxt) (hd facts) - val parents = add_thy_parent_facts thy_map thy [] - in fold_rev do_fact facts parents; () end - in fold_rev (fn (_, facts) => fn () => do_thy facts) thy_map () end + |> map (snd #> nickname_of) + in fold do_fact facts []; () end fun generate_features ctxt prover thys include_thys file_name = let @@ -172,8 +149,7 @@ in query ^ update end else "" - val thy_map = old_facts |> thy_map_from_facts - val parents = fold (add_thy_parent_facts thy_map) thys [] + val parents = map (nickname_of o snd) (the_list (try List.last old_facts)) val new_facts = new_facts |> map (`(nickname_of o snd)) val prevss = fst (split_last (parents :: map (single o fst) new_facts)) val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss)) diff -r 168befd6cfa6 -r eefab127e9f1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 21 16:31:37 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 21 23:52:10 2012 +0100 @@ -260,7 +260,7 @@ | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop (* FIXME: Here a "Graph.update_node" function would be useful *) -fun update_fact_graph_node (name, kind) = +fun update_access_graph_node (name, kind) = Graph.default_node (name, Isar_Proof) #> kind <> Isar_Proof ? Graph.map_node name (K kind) @@ -290,9 +290,9 @@ string_of_int (length (Graph.minimals G)) ^ " minimal, " ^ string_of_int (length (Graph.maximals G)) ^ " maximal" -type mash_state = {fact_G : unit Graph.T, dirty : string list option} +type mash_state = {access_G : unit Graph.T, dirty : string list option} -val empty_state = {fact_G = Graph.empty, dirty = SOME []} +val empty_state = {access_G = Graph.empty, dirty = SOME []} local @@ -324,9 +324,9 @@ case extract_node line of NONE => I (* shouldn't happen *) | SOME (name, parents, kind) => - update_fact_graph_node (name, kind) + update_access_graph_node (name, kind) #> fold (add_edge_to name) parents - val fact_G = + val access_G = case string_ord (version', version) of EQUAL => try_graph ctxt "loading state" Graph.empty (fn () => @@ -335,14 +335,14 @@ | GREATER => raise Too_New () in trace_msg ctxt (fn () => - "Loaded fact graph (" ^ graph_info fact_G ^ ")"); - {fact_G = fact_G, dirty = SOME []} + "Loaded fact graph (" ^ graph_info access_G ^ ")"); + {access_G = access_G, dirty = SOME []} end | _ => empty_state) end fun save _ (state as {dirty = SOME [], ...}) = state - | save ctxt {fact_G, dirty} = + | save ctxt {access_G, dirty} = let fun str_of_entry (name, parents, kind) = str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^ @@ -352,17 +352,17 @@ val (banner, entries) = case dirty of SOME names => - (NONE, fold (append_entry o Graph.get_entry fact_G) names []) - | NONE => (SOME (version ^ "\n"), Graph.fold append_entry fact_G []) + (NONE, fold (append_entry o Graph.get_entry access_G) names []) + | NONE => (SOME (version ^ "\n"), Graph.fold append_entry access_G []) in write_file banner (entries, str_of_entry) (mash_state_file ()); trace_msg ctxt (fn () => - "Saved fact graph (" ^ graph_info fact_G ^ + "Saved fact graph (" ^ graph_info access_G ^ (case dirty of SOME dirty => "; " ^ string_of_int (length dirty) ^ " dirty fact(s)" | _ => "") ^ ")"); - {fact_G = fact_G, dirty = SOME []} + {access_G = access_G, dirty = SOME []} end val global_state = @@ -694,7 +694,7 @@ fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0 -fun maximal_in_graph fact_G facts = +fun maximal_in_graph access_G facts = let val facts = [] |> fold (cons o nickname_of o snd) facts val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts @@ -703,11 +703,11 @@ fun find_maxes _ (maxs, []) = map snd maxs | find_maxes seen (maxs, new :: news) = find_maxes - (seen |> num_keys (Graph.imm_succs fact_G new) > 1 + (seen |> num_keys (Graph.imm_succs access_G new) > 1 ? Symtab.default (new, ())) (if Symtab.defined tab new then let - val newp = Graph.all_preds fact_G [new] + val newp = Graph.all_preds access_G [new] fun is_ancestor x yp = member (op =) yp x val maxs = maxs |> filter (fn (_, max) => not (is_ancestor max newp)) @@ -721,11 +721,11 @@ end else (maxs, Graph.Keys.fold (insert_new seen) - (Graph.imm_preds fact_G new) news)) - in find_maxes Symtab.empty ([], Graph.maximals fact_G) end + (Graph.imm_preds access_G new) news)) + in find_maxes Symtab.empty ([], Graph.maximals access_G) end -fun is_fact_in_graph fact_G (_, th) = - can (Graph.get_node fact_G) (nickname_of th) +fun is_fact_in_graph access_G (_, th) = + can (Graph.get_node access_G) (nickname_of th) val weight_raw_mash_facts = weight_mepo_facts val weight_mash_facts = weight_raw_mash_facts @@ -762,23 +762,23 @@ concl_t facts = let val thy = Proof_Context.theory_of ctxt - val (fact_G, suggs) = - peek_state ctxt (fn {fact_G, ...} => - if Graph.is_empty fact_G then - (fact_G, []) + val (access_G, suggs) = + peek_state ctxt (fn {access_G, ...} => + if Graph.is_empty access_G then + (access_G, []) else let - val parents = maximal_in_graph fact_G facts + val parents = maximal_in_graph access_G facts val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) in - (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats)) + (access_G, mash_QUERY ctxt overlord max_facts (parents, feats)) end) val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) - val unknown = facts |> filter_out (is_fact_in_graph fact_G) + val unknown = facts |> filter_out (is_fact_in_graph access_G) in find_mash_suggestions max_facts suggs facts chained unknown end -fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) = +fun add_wrt_access_graph ctxt (name, parents, feats, deps) (adds, graph) = let fun maybe_add_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => @@ -788,17 +788,17 @@ val (deps, _) = ([], graph) |> fold maybe_add_from deps in ((name, parents, feats, deps) :: adds, graph) end -fun reprove_wrt_fact_graph ctxt (name, deps) (reps, graph) = +fun reprove_wrt_access_graph ctxt (name, deps) (reps, graph) = let fun maybe_rep_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) graph)) - val graph = graph |> update_fact_graph_node (name, Automatic_Proof) + val graph = graph |> update_access_graph_node (name, Automatic_Proof) val (deps, _) = ([], graph) |> fold maybe_rep_from deps in ((name, deps) :: reps, graph) end -fun flop_wrt_fact_graph name = - update_fact_graph_node (name, Isar_Proof_wegen_Prover_Flop) +fun flop_wrt_access_graph name = + update_access_graph_node (name, Isar_Proof_wegen_Prover_Flop) val learn_timeout_slack = 2.0 @@ -826,8 +826,8 @@ val feats = features_of ctxt prover thy (Local, General) [t] val deps = used_ths |> map nickname_of in - peek_state ctxt (fn {fact_G, ...} => - let val parents = maximal_in_graph fact_G facts in + peek_state ctxt (fn {access_G, ...} => + let val parents = maximal_in_graph access_G facts in mash_ADD ctxt overlord [(name, parents, feats, deps)] end); (true, "") @@ -844,10 +844,10 @@ val timer = Timer.startRealTimer () fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout) - val {fact_G, ...} = peek_state ctxt I + val {access_G, ...} = peek_state ctxt I val facts = facts |> sort (thm_ord o pairself snd) val (old_facts, new_facts) = - facts |> List.partition (is_fact_in_graph fact_G) + facts |> List.partition (is_fact_in_graph access_G) in if null new_facts andalso (not run_prover orelse null old_facts) then if auto_level < 2 then @@ -873,14 +873,14 @@ else isar_dependencies_of all_names th fun do_commit [] [] [] state = state - | do_commit adds reps flops {fact_G, dirty} = + | do_commit adds reps flops {access_G, dirty} = let - val was_empty = Graph.is_empty fact_G - val (adds, fact_G) = - ([], fact_G) |> fold (add_wrt_fact_graph ctxt) adds - val (reps, fact_G) = - ([], fact_G) |> fold (reprove_wrt_fact_graph ctxt) reps - val fact_G = fact_G |> fold flop_wrt_fact_graph flops + val was_empty = Graph.is_empty access_G + val (adds, access_G) = + ([], access_G) |> fold (add_wrt_access_graph ctxt) adds + val (reps, access_G) = + ([], access_G) |> fold (reprove_wrt_access_graph ctxt) reps + val access_G = access_G |> fold flop_wrt_access_graph flops val dirty = case (was_empty, dirty, reps) of (false, SOME names, []) => SOME (map #1 adds @ names) @@ -888,7 +888,7 @@ in mash_ADD ctxt overlord (rev adds); mash_REPROVE ctxt overlord reps; - {fact_G = fact_G, dirty = dirty} + {access_G = access_G, dirty = dirty} end fun commit last adds reps flops = (if debug andalso auto_level = 0 then @@ -936,7 +936,7 @@ val ancestors = old_facts |> filter (fn (_, th) => thm_ord (th, last_th) <> GREATER) - val parents = maximal_in_graph fact_G ancestors + val parents = maximal_in_graph access_G ancestors val (adds, (_, n, _, _)) = ([], (parents, 0, next_commit_time (), false)) |> fold learn_new_fact new_facts @@ -967,7 +967,7 @@ let val max_isar = 1000 * max_dependencies fun kind_of_proof th = - try (Graph.get_node fact_G) (nickname_of th) + try (Graph.get_node access_G) (nickname_of th) |> the_default Isar_Proof fun priority_of (_, th) = random_range 0 max_isar @@ -1034,7 +1034,7 @@ fun is_mash_enabled () = (getenv "MASH" = "yes") fun mash_can_suggest_facts ctxt = - not (Graph.is_empty (#fact_G (peek_state ctxt I))) + not (Graph.is_empty (#access_G (peek_state ctxt I))) (* Generate more suggestions than requested, because some might be thrown out later for various reasons. *)