# HG changeset patch
# User blanchet
# Date 1342815585 -7200
# Node ID 9e96486d53ad9883f6532b495e4ec360cc1f5996
# Parent  4a11914fd53084fbb21c2e7cf951e101ad34f9f5
handle local facts smoothly in MaSh

diff -r 4a11914fd530 -r 9e96486d53ad src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -28,7 +28,7 @@
 
 val all_names =
   filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o Thm.get_name_hint) #> Symtab.make
+  #> map (rpair () o nickname_of) #> Symtab.make
 
 fun evaluate_mash_suggestions ctxt params thy file_name =
   let
@@ -70,7 +70,7 @@
       let
         val (name, suggs) = extract_query line
         val th =
-          case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
+          case find_first (fn (_, th) => nickname_of th = name) facts of
             SOME (_, th) => th
           | NONE => error ("No fact called \"" ^ name ^ "\"")
         val goal = goal_of_thm thy th
diff -r 4a11914fd530 -r 9e96486d53ad src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -32,7 +32,7 @@
   ths |> sort (thm_ord o swap o pairself snd)
       |> map (snd #> `(theory_of_thm #> Context.theory_name))
       |> AList.coalesce (op =)
-      |> map (apsnd (map Thm.get_name_hint))
+      |> map (apsnd (map nickname_of))
 
 fun has_thy thy th =
   Context.theory_name thy = Context.theory_name (theory_of_thm th)
@@ -51,7 +51,7 @@
 
 val all_names =
   filter_out is_likely_tautology_or_too_meta
-  #> map (rpair () o Thm.get_name_hint) #> Symtab.make
+  #> map (rpair () o nickname_of) #> Symtab.make
 
 fun generate_accessibility thy include_thy file_name =
   let
@@ -83,7 +83,7 @@
       |> not include_thy ? filter_out (has_thy thy o snd)
     fun do_fact ((_, (_, status)), th) =
       let
-        val name = Thm.get_name_hint th
+        val name = nickname_of th
         val feats =
           features_of ctxt prover (theory_of_thm th) status [prop_of th]
         val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n"
@@ -101,7 +101,7 @@
     val all_names = all_names ths
     fun do_thm th =
       let
-        val name = Thm.get_name_hint th
+        val name = nickname_of th
         val deps = isabelle_dependencies_of all_names th
         val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
       in File.append path s end
@@ -118,18 +118,17 @@
       |> not include_thy ? filter_out (has_thy thy o snd)
     val ths = facts |> map snd
     val all_names = all_names ths
-    fun is_dep dep (_, th) = Thm.get_name_hint th = dep
+    fun is_dep dep (_, th) = nickname_of th = dep
     fun add_isar_dep facts dep accum =
       if exists (is_dep dep) accum then
         accum
       else case find_first (is_dep dep) facts of
         SOME ((name, status), th) => accum @ [((name, status), th)]
       | NONE => accum (* shouldn't happen *)
-    fun fix_name ((_, stature), th) =
-      ((fn () => th |> Thm.get_name_hint, stature), th)
+    fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
     fun do_thm th =
       let
-        val name = Thm.get_name_hint th
+        val name = nickname_of th
         val goal = goal_of_thm thy th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val deps =
@@ -168,7 +167,7 @@
     val all_names = all_names ths
     fun do_fact ((_, (_, status)), th) prevs =
       let
-        val name = Thm.get_name_hint th
+        val name = nickname_of th
         val feats = features_of ctxt prover thy status [prop_of th]
         val deps = isabelle_dependencies_of all_names th
         val kind = Thm.legacy_get_kind th
@@ -196,7 +195,7 @@
             |>> sort (thm_ord o pairself snd)
     fun do_fact (fact as (_, th)) old_facts =
       let
-        val name = Thm.get_name_hint th
+        val name = nickname_of th
         val goal = goal_of_thm thy th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val kind = Thm.legacy_get_kind th
diff -r 4a11914fd530 -r 9e96486d53ad src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
@@ -25,6 +25,7 @@
   val unescape_meta : string -> string
   val unescape_metas : string -> string list
   val extract_query : string -> string * string list
+  val nickname_of : thm -> string
   val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
   val mesh_facts :
     int -> (('a * thm) list * ('a * thm) list) list -> ('a * thm) list
@@ -122,9 +123,30 @@
     [goal_name, suggs] => (unescape_meta goal_name, unescape_metas suggs)
   | _ => ("", [])
 
+fun parent_of_local_thm th =
+  let
+    val thy = th |> Thm.theory_of_thm
+    val facts = thy |> Global_Theory.facts_of
+    val space = facts |> Facts.space_of
+    fun id_of s = #id (Name_Space.the_entry space s)
+    fun max_id (s', _) (s, id) =
+      let val id' = id_of s' in if id > id' then (s, id) else (s', id') end
+  in ("", ~1) |> Facts.fold_static max_id facts |> fst end
+
+val local_prefix = "local" ^ Long_Name.separator
+
+fun nickname_of th =
+  let val hint = Thm.get_name_hint th in
+    (* FIXME: There must be a better way to detect local facts. *)
+    case try (unprefix local_prefix) hint of
+      SOME suff =>
+      parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
+    | NONE => hint
+  end
+
 fun suggested_facts suggs facts =
   let
-    fun add_fact (fact as (_, th)) = Symtab.default (Thm.get_name_hint th, fact)
+    fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
     val tab = Symtab.empty |> fold add_fact facts
   in map_filter (Symtab.lookup tab) suggs end
 
@@ -468,11 +490,11 @@
 
 fun parents_wrt_facts facts fact_graph =
   let
-    val facts = [] |> fold (cons o Thm.get_name_hint o snd) facts
+    val facts = [] |> fold (cons o nickname_of o snd) facts
     val tab = Symtab.empty |> fold (fn name => Symtab.update (name, ())) facts
     fun insert_not_seen seen name =
       not (member (op =) seen name) ? insert (op =) name
-    fun parents_of seen parents [] = parents
+    fun parents_of _ parents [] = parents
       | parents_of seen parents (name :: names) =
         if Symtab.defined tab name then
           parents_of (name :: seen) (name :: parents) names
@@ -488,7 +510,7 @@
 fun max_suggs_of max_facts = max_facts + Int.min (200, max_facts)
 
 fun is_fact_in_graph fact_graph (_, th) =
-  can (Graph.get_node fact_graph) (Thm.get_name_hint th)
+  can (Graph.get_node fact_graph) (nickname_of th)
 
 fun mash_suggest_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                        concl_t facts =
@@ -545,13 +567,13 @@
         val ths = facts |> map snd
         val all_names =
           ths |> filter_out is_likely_tautology_or_too_meta
-              |> map (rpair () o Thm.get_name_hint)
+              |> map (rpair () o nickname_of)
               |> Symtab.make
         fun trim_deps deps = if length deps > max_dependencies then [] else deps
         fun do_fact _ (accum as (_, true)) = accum
           | do_fact ((_, (_, status)), th) ((parents, upds), false) =
             let
-              val name = Thm.get_name_hint th
+              val name = nickname_of th
               val feats =
                 features_of ctxt prover (theory_of_thm th) status [prop_of th]
               val deps = isabelle_dependencies_of all_names th |> trim_deps
@@ -591,7 +613,7 @@
     val prover = hd provers
     val name = ATP_Util.timestamp () ^ " " ^ serial_string () (* fresh enough *)
     val feats = features_of ctxt prover thy General [t]
-    val deps = used_ths |> map Thm.get_name_hint
+    val deps = used_ths |> map nickname_of
   in
     mash_map ctxt (fn {thys, fact_graph} =>
         let