--- a/src/HOL/TPTP/mash_eval.ML Thu Dec 27 15:46:27 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Dec 27 16:49:12 2012 +0100
@@ -46,7 +46,7 @@
val lines = sugg_path |> File.read_lines
val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Symtab.empty [] [] css
- val all_names = build_all_names nickname_of facts
+ val all_names = build_all_names nickname_of_thm facts
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
fun index_string (j, s) = s ^ "@" ^ string_of_int j
fun str_of_res label facts ({outcome, run_time, used_facts, ...}
@@ -74,7 +74,7 @@
let
val (name, suggs) = extract_query line
val th =
- case find_first (fn (_, th) => nickname_of th = name) facts of
+ case find_first (fn (_, th) => nickname_of_thm th = name) facts of
SOME (_, th) => th
| NONE => error ("No fact called \"" ^ name ^ "\".")
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
@@ -107,7 +107,7 @@
fun prove heading get facts =
let
fun nickify ((_, stature), th) =
- ((K (escape_meta (nickname_of th)), stature), th)
+ ((K (escape_meta (nickname_of_thm th)), stature), th)
val facts =
facts
|> map (get #> nickify)
--- a/src/HOL/TPTP/mash_export.ML Thu Dec 27 15:46:27 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Thu Dec 27 16:49:12 2012 +0100
@@ -59,7 +59,7 @@
val facts =
all_facts ctxt
|> not include_thys ? filter_out (has_thys thys o snd)
- |> map (snd #> nickname_of)
+ |> map (snd #> nickname_of_thm)
in fold do_fact facts []; () end
fun generate_features ctxt prover thys include_thys file_name =
@@ -71,7 +71,7 @@
|> not include_thys ? filter_out (has_thys thys o snd)
fun do_fact ((_, stature), th) =
let
- val name = nickname_of th
+ val name = nickname_of_thm th
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val s =
@@ -96,11 +96,11 @@
val path = file_name |> Path.explode
val facts =
all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
- val all_names = build_all_names nickname_of facts
+ val all_names = build_all_names nickname_of_thm facts
fun do_fact (j, (_, th)) =
if in_range range j then
let
- val name = nickname_of th
+ val name = nickname_of_thm th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val deps =
isar_or_prover_dependencies_of ctxt params_opt facts all_names th
@@ -128,7 +128,7 @@
val path = file_name |> Path.explode
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
- val all_names = build_all_names nickname_of facts
+ val all_names = build_all_names nickname_of_thm facts
fun do_fact (j, ((name, ((_, stature), th)), prevs)) =
if in_range range j then
let
@@ -149,8 +149,9 @@
in query ^ update end
else
""
- val parents = map (nickname_of o snd) (the_list (try List.last old_facts))
- val new_facts = new_facts |> map (`(nickname_of o snd))
+ val parents =
+ map (nickname_of_thm o snd) (the_list (try List.last old_facts))
+ val new_facts = new_facts |> map (`(nickname_of_thm o snd))
val prevss = fst (split_last (parents :: map (single o fst) new_facts))
val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss))
in File.write_list path lines end
@@ -168,10 +169,10 @@
val path = file_name |> Path.explode
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
- val all_names = build_all_names nickname_of facts
+ val all_names = build_all_names nickname_of_thm facts
fun do_fact ((_, th), old_facts) =
let
- val name = nickname_of th
+ val name = nickname_of_thm th
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of all_names th
@@ -184,7 +185,7 @@
old_facts
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
max_facts NONE hyp_ts concl_t
- |> map (nickname_of o snd)
+ |> map (nickname_of_thm o snd)
in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end
end
fun accum x (yss as ys :: _) = (x :: ys) :: yss
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 27 15:46:27 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 27 16:49:12 2012 +0100
@@ -40,7 +40,7 @@
Proof.context -> bool -> int -> string list * (string * real) list
-> (string * real) list
val mash_unlearn : Proof.context -> unit
- val nickname_of : thm -> string
+ val nickname_of_thm : thm -> string
val find_suggested_facts :
(string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
val mesh_facts :
@@ -403,7 +403,7 @@
val local_prefix = "local" ^ Long_Name.separator
-fun nickname_of th =
+fun nickname_of_thm th =
if Thm.has_name_hint th then
let val hint = Thm.get_name_hint th in
(* FIXME: There must be a better way to detect local facts. *)
@@ -417,7 +417,7 @@
fun find_suggested_facts suggs facts =
let
- fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
+ fun add_fact (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
val tab = Symtab.empty |> fold add_fact facts
fun find_sugg (name, weight) =
Symtab.lookup tab name |> Option.map (rpair weight)
@@ -489,8 +489,12 @@
fun thm_ord p =
case theory_ord (pairself theory_of_thm p) of
EQUAL =>
- (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
- string_ord (pairself nickname_of (swap p))
+ let val q = pairself nickname_of_thm p in
+ (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
+ case bool_ord (pairself (String.isSuffix "_def") (swap q)) of
+ EQUAL => string_ord q
+ | ord => ord
+ end
| ord => ord
val freezeT = Type.legacy_freeze_type
@@ -604,7 +608,7 @@
val prover_dependency_default_max_facts = 50
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
-val typedef_deps = [@{thm CollectI} |> nickname_of]
+val typedef_deps = [@{thm CollectI} |> nickname_of_thm]
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
val typedef_ths =
@@ -614,12 +618,12 @@
type_definition.Abs_cases type_definition.Rep_induct
type_definition.Abs_induct type_definition.Rep_range
type_definition.Abs_image}
- |> map nickname_of
+ |> map nickname_of_thm
fun is_size_def [dep] th =
(case first_field ".recs" dep of
SOME (pref, _) =>
- (case first_field ".size" (nickname_of th) of
+ (case first_field ".size" (nickname_of_thm th) of
SOME (pref', _) => pref = pref'
| NONE => false)
| NONE => false)
@@ -649,8 +653,9 @@
val goal = goal_of_thm thy th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- fun fix_name ((_, stature), th) = ((fn () => nickname_of th, stature), th)
- fun is_dep dep (_, th) = nickname_of th = dep
+ fun nickify ((_, stature), th) =
+ ((fn () => nickname_of_thm th, stature), th)
+ fun is_dep dep (_, th) = nickname_of_thm th = dep
fun add_isar_dep facts dep accum =
if exists (is_dep dep) accum then
accum
@@ -663,11 +668,11 @@
(max_facts |> the_default prover_dependency_default_max_facts)
NONE hyp_ts concl_t
|> fold (add_isar_dep facts) (these isar_deps)
- |> map fix_name
+ |> map nickify
in
if verbose andalso auto_level = 0 then
let val num_facts = length facts in
- "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of th) ^
+ "MaSh: " ^ quote prover ^ " on " ^ quote (nickname_of_thm th) ^
" with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
"."
|> Output.urgent_message
@@ -697,7 +702,7 @@
fun maximal_in_graph access_G facts =
let
- val facts = [] |> fold (cons o nickname_of o snd) facts
+ val facts = [] |> fold (cons o nickname_of_thm o snd) facts
val tab = Symtab.empty |> fold (fn name => Symtab.default (name, ())) facts
fun insert_new seen name =
not (Symtab.defined seen name) ? insert (op =) name
@@ -726,7 +731,7 @@
in find_maxes Symtab.empty ([], Graph.maximals access_G) end
fun is_fact_in_graph access_G (_, th) =
- can (Graph.get_node access_G) (nickname_of th)
+ can (Graph.get_node access_G) (nickname_of_thm th)
val weight_raw_mash_facts = weight_mepo_facts
val weight_mash_facts = weight_raw_mash_facts
@@ -825,7 +830,7 @@
val thy = Proof_Context.theory_of ctxt
val name = freshish_name ()
val feats = features_of ctxt prover thy (Local, General) [t]
- val deps = used_ths |> map nickname_of
+ val deps = used_ths |> map nickname_of_thm
in
peek_state ctxt (fn {access_G, ...} =>
let val parents = maximal_in_graph access_G facts in
@@ -863,7 +868,7 @@
""
else
let
- val all_names = build_all_names nickname_of facts
+ val all_names = build_all_names nickname_of_thm facts
fun deps_of status th =
if status = Non_Rec_Def orelse status = Rec_Def then
SOME []
@@ -911,7 +916,7 @@
| learn_new_fact ((_, stature as (_, status)), th)
(adds, (parents, n, next_commit, _)) =
let
- val name = nickname_of th
+ val name = nickname_of_thm th
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val deps = deps_of status th |> these
@@ -946,7 +951,7 @@
| relearn_old_fact ((_, (_, status)), th)
((reps, flops), (n, next_commit, _)) =
let
- val name = nickname_of th
+ val name = nickname_of_thm th
val (n, reps, flops) =
case deps_of status th of
SOME deps => (n + 1, (name, deps) :: reps, flops)
@@ -968,7 +973,7 @@
let
val max_isar = 1000 * max_dependencies
fun kind_of_proof th =
- try (Graph.get_node access_G) (nickname_of th)
+ try (Graph.get_node access_G) (nickname_of_thm th)
|> the_default Isar_Proof
fun priority_of (_, th) =
random_range 0 max_isar