# HG changeset patch
# User blanchet
# Date 1360916240 -3600
# Node ID d03ded5dcf65c3994a8f369c0af4b7fbb0043d62
# Parent  fb16c4276620bc6ff3190a602068d2011fd89a9e
more MaSh tracing

diff -r fb16c4276620 -r d03ded5dcf65 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -111,7 +111,8 @@
           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
           val isar_deps = isar_dependencies_of name_tabs th
           val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
-          val find_suggs = find_suggested_facts facts #> map fact_of_raw_fact
+          val find_suggs =
+            find_suggested_facts ctxt facts #> map fact_of_raw_fact
           fun get_facts [] compute = compute facts
             | get_facts suggs _ = find_suggs suggs
           val mepo_facts =
@@ -121,7 +122,7 @@
             |> weight_mepo_facts
           fun mash_of suggs =
             get_facts suggs (fn _ =>
-                find_mash_suggestions slack_max_facts suggs facts [] []
+                find_mash_suggestions ctxt slack_max_facts suggs facts [] []
                 |> fst |> map fact_of_raw_fact)
             |> weight_mash_facts
           val mash_isar_facts = mash_of mash_isar_suggs
diff -r fb16c4276620 -r d03ded5dcf65 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -50,7 +50,8 @@
 
   val mash_unlearn : Proof.context -> unit
   val nickname_of_thm : thm -> string
-  val find_suggested_facts : ('b * thm) list -> string list -> ('b * thm) list
+  val find_suggested_facts :
+    Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
   val mesh_facts :
     ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list
     -> 'a list
@@ -72,8 +73,8 @@
   val weight_mepo_facts : 'a list -> ('a * real) list
   val weight_mash_facts : 'a list -> ('a * real) list
   val find_mash_suggestions :
-    int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
-    -> ('b * thm) list * ('b * thm) list
+    Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list
+    -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term
     -> raw_fact list -> fact list * fact list
@@ -450,11 +451,15 @@
   else
     elided_backquote_thm 200 th
 
-fun find_suggested_facts facts =
+fun find_suggested_facts ctxt facts =
   let
-    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
-    val tab = fold add_fact facts Symtab.empty
-  in map_filter (Symtab.lookup tab) end
+    fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
+    val tab = fold add facts Symtab.empty
+    fun lookup nick =
+      Symtab.lookup tab nick
+      |> tap (fn NONE => trace_msg ctxt (fn () => "Cannot find " ^ quote nick)
+               | _ => ())
+  in map_filter lookup end
 
 fun scaled_avg [] = 0
   | scaled_avg xs =
@@ -789,10 +794,10 @@
 
 val max_proximity_facts = 100
 
-fun find_mash_suggestions _ [] _ _ raw_unknown = ([], raw_unknown)
-  | find_mash_suggestions max_facts suggs facts chained raw_unknown =
+fun find_mash_suggestions _ _ [] _ _ raw_unknown = ([], raw_unknown)
+  | find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
     let
-      val raw_mash = find_suggested_facts facts suggs
+      val raw_mash = find_suggested_facts ctxt facts suggs
       val unknown_chained =
         inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
       val proximity =
@@ -831,7 +836,7 @@
             end)
     val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
   in
-    find_mash_suggestions max_facts suggs facts chained unknown
+    find_mash_suggestions ctxt max_facts suggs facts chained unknown
     |> pairself (map fact_of_raw_fact)
   end