# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID 192444b53e868a9939acd9b7761fafdb0336b40c
# Parent  5781c4620245757e16e4f2187bd8daedfbfffb09
speed up MaSh queries

diff -r 5781c4620245 -r 192444b53e86 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
@@ -92,6 +92,7 @@
   |> tap (Isabelle_System.mkdir o Path.explode)
 fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
 
+
 (*** Isabelle helpers ***)
 
 fun meta_char c =
@@ -121,9 +122,11 @@
     [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
   | _ => ("", [])
 
-fun find_suggested facts sugg =
-  find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
-fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
+fun suggested_facts suggs facts =
+  let
+    fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
+    val tab = Symtab.empty |> fold add_fact facts
+  in map_filter (Symtab.lookup tab) suggs end
 
 (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
 fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
@@ -454,16 +457,26 @@
 
 fun parents_wrt_facts ctxt facts fact_graph =
   let
-    val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
-    val facts =
-      try_graph ctxt "when computing ancestor facts" [] (fn () =>
-          [] |> fold (cons o Thm.get_name_hint o snd) facts
-             |> filter (Symtab.defined graph_facts)
-             |> Graph.all_preds fact_graph)
-    val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
+    val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
+    val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
+    val maxs = Graph.maximals fact_graph
   in
-    try_graph ctxt "when computing parent facts" [] (fn () =>
-        fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals)
+    if forall (Symtab.defined tab) maxs then
+      maxs
+    else
+      let
+        val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
+        val ancestors =
+          try_graph ctxt "when computing ancestor facts" [] (fn () =>
+              facts |> filter (Symtab.defined graph_facts)
+                    |> Graph.all_preds fact_graph)
+        val ancestors =
+          Symtab.empty |> fold (fn name => Symtab.update (name, ())) ancestors
+      in
+        try_graph ctxt "when computing parent facts" [] (fn () =>
+            fact_graph |> Graph.restrict (Symtab.defined ancestors)
+                       |> Graph.maximals)
+      end
   end
 
 (* Generate more suggestions than requested, because some might be thrown out
@@ -477,15 +490,23 @@
 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                        concl_t facts =
   let
+val timer = Timer.startRealTimer ()
     val thy = Proof_Context.theory_of ctxt
+val _ = tracing ("A1: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val fact_graph = #fact_graph (mash_get ctxt)
+val _ = tracing ("A2: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val parents = parents_wrt_facts ctxt facts fact_graph
+val _ = tracing ("A3: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
+val _ = tracing ("A4: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val suggs =
       if Graph.is_empty fact_graph then []
       else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
+val _ = tracing ("A5: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val selected = facts |> suggested_facts suggs
+val _ = tracing ("A6: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
     val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
+val _ = tracing ("END: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
   in (selected, unknown) end
 
 fun add_thys_for thy =