--- 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
--- 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
--- 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