1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -92,6 +92,7 @@
     1.4    |> tap (Isabelle_System.mkdir o Path.explode)
     1.5  fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
     1.6  
     1.7 +
     1.8  (*** Isabelle helpers ***)
     1.9  
    1.10  fun meta_char c =
    1.11 @@ -121,9 +122,11 @@
    1.12      [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
    1.13    | _ => ("", [])
    1.14  
    1.15 -fun find_suggested facts sugg =
    1.16 -  find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
    1.17 -fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
    1.18 +fun suggested_facts suggs facts =
    1.19 +  let
    1.20 +    fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
    1.21 +    val tab = Symtab.empty |> fold add_fact facts
    1.22 +  in map_filter (Symtab.lookup tab) suggs end
    1.23  
    1.24  (* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
    1.25  fun score x = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt x) + 15.0
    1.26 @@ -454,16 +457,26 @@
    1.27  
    1.28  fun parents_wrt_facts ctxt facts fact_graph =
    1.29    let
    1.30 -    val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
    1.31 -    val facts =
    1.32 -      try_graph ctxt "when computing ancestor facts" [] (fn () =>
    1.33 -          [] |> fold (cons o Thm.get_name_hint o snd) facts
    1.34 -             |> filter (Symtab.defined graph_facts)
    1.35 -             |> Graph.all_preds fact_graph)
    1.36 -    val facts = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
    1.37 +    val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
    1.38 +    val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
    1.39 +    val maxs = Graph.maximals fact_graph
    1.40    in
    1.41 -    try_graph ctxt "when computing parent facts" [] (fn () =>
    1.42 -        fact_graph |> Graph.restrict (Symtab.defined facts) |> Graph.maximals)
    1.43 +    if forall (Symtab.defined tab) maxs then
    1.44 +      maxs
    1.45 +    else
    1.46 +      let
    1.47 +        val graph_facts = Symtab.make (map (rpair ()) (Graph.keys fact_graph))
    1.48 +        val ancestors =
    1.49 +          try_graph ctxt "when computing ancestor facts" [] (fn () =>
    1.50 +              facts |> filter (Symtab.defined graph_facts)
    1.51 +                    |> Graph.all_preds fact_graph)
    1.52 +        val ancestors =
    1.53 +          Symtab.empty |> fold (fn name => Symtab.update (name, ())) ancestors
    1.54 +      in
    1.55 +        try_graph ctxt "when computing parent facts" [] (fn () =>
    1.56 +            fact_graph |> Graph.restrict (Symtab.defined ancestors)
    1.57 +                       |> Graph.maximals)
    1.58 +      end
    1.59    end
    1.60  
    1.61  (* Generate more suggestions than requested, because some might be thrown out
    1.62 @@ -477,15 +490,23 @@
    1.63  fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
    1.64                         concl_t facts =
    1.65    let
    1.66 +val timer = Timer.startRealTimer ()
    1.67      val thy = Proof_Context.theory_of ctxt
    1.68 +val _ = tracing ("A1: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.69      val fact_graph = #fact_graph (mash_get ctxt)
    1.70 +val _ = tracing ("A2: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.71      val parents = parents_wrt_facts ctxt facts fact_graph
    1.72 +val _ = tracing ("A3: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.73      val feats = features_of ctxt prover thy General (concl_t :: hyp_ts)
    1.74 +val _ = tracing ("A4: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.75      val suggs =
    1.76        if Graph.is_empty fact_graph then []
    1.77        else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
    1.78 +val _ = tracing ("A5: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.79      val selected = facts |> suggested_facts suggs
    1.80 +val _ = tracing ("A6: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.81      val unknown = facts |> filter_out (is_fact_in_graph fact_graph)
    1.82 +val _ = tracing ("END: " ^ PolyML.makestring (Timer.checkRealTimer timer)) (*###*)
    1.83    in (selected, unknown) end
    1.84  
    1.85  fun add_thys_for thy =