merged
authornipkow
Fri, 21 Dec 2012 23:52:10 +0100
changeset 50614 eefab127e9f1
parent 50611 99af6b652b3a (diff)
parent 50613 168befd6cfa6 (current diff)
child 50615 965d4c108584
merged
--- 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))
--- 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. *)