--- a/src/HOL/TPTP/mash_eval.ML Fri Jul 03 14:51:43 2015 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 03 16:19:45 2015 +0200
@@ -54,7 +54,7 @@
val css = clasimpset_rule_table_of ctxt
val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css
- val name_tabs = build_name_tables nickname_of_thm facts
+ val name_tabs = build_name_tables (nickname_of_thm ctxt) facts
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
fun index_str (j, s) = s ^ "@" ^ string_of_int j
@@ -90,12 +90,12 @@
[name] => name
| names => error ("Input files out of sync: facts " ^ commas (map quote names) ^ "."))
val th =
- case find_first (fn (_, th) => nickname_of_thm th = name) facts of
+ case find_first (fn (_, th) => nickname_of_thm ctxt th = name) facts of
SOME (_, th) => th
| NONE => error ("No fact called \"" ^ name ^ "\".")
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
- val isar_deps = these (isar_dependencies_of name_tabs th)
+ val isar_deps = these (isar_dependencies_of ctxt name_tabs th)
val suggss = isar_deps :: suggss0
val facts = facts |> filter (fn (_, th') => thm_less (th', th))
@@ -116,7 +116,7 @@
else
let
fun nickify ((_, stature), th) =
- ((K (encode_str (nickname_of_thm th)), stature), th)
+ ((K (encode_str (nickname_of_thm ctxt th)), stature), th)
val facts =
suggs
--- a/src/HOL/TPTP/mash_export.ML Fri Jul 03 14:51:43 2015 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 03 16:19:45 2015 +0200
@@ -65,7 +65,7 @@
fun all_facts ctxt =
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css
- |> sort (crude_thm_ord o apply2 snd)
+ |> sort (crude_thm_ord ctxt o apply2 snd)
end
fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th))
@@ -82,8 +82,8 @@
val facts =
all_facts ctxt
|> filter_out (has_thys thys o snd)
- |> attach_parents_to_facts []
- |> map (apsnd (nickname_of_thm o snd))
+ |> attach_parents_to_facts ctxt []
+ |> map (apsnd (nickname_of_thm ctxt o snd))
in
File.write path "";
List.app do_fact facts
@@ -97,7 +97,7 @@
fun do_fact ((_, stature), th) =
let
- val name = nickname_of_thm th
+ val name = nickname_of_thm ctxt th
val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
in
@@ -124,7 +124,7 @@
let
val deps =
(case isar_deps_opt of
- NONE => isar_dependencies_of name_tabs th
+ NONE => isar_dependencies_of ctxt name_tabs th
| deps => deps)
in
(case deps of
@@ -142,12 +142,12 @@
let
val path = Path.explode file_name
val facts = filter_out (has_thys thys o snd) (all_facts ctxt)
- val name_tabs = build_name_tables nickname_of_thm facts
+ val name_tabs = build_name_tables (nickname_of_thm ctxt) facts
fun do_fact (j, (_, th)) =
if in_range range j then
let
- val name = nickname_of_thm th
+ val name = nickname_of_thm ctxt th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val access_facts = filter_accessible_from th facts
val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE
@@ -180,13 +180,13 @@
val path = Path.explode file_name
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
- val name_tabs = build_name_tables nickname_of_thm facts
+ val name_tabs = build_name_tables (nickname_of_thm ctxt) facts
fun do_fact (j, (name, (parents, ((_, stature), th)))) =
if in_range range j then
let
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
- val isar_deps = isar_dependencies_of name_tabs th
+ val isar_deps = isar_dependencies_of ctxt name_tabs th
val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
val goal_feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
val access_facts = filter_accessible_from th new_facts @ old_facts
@@ -224,7 +224,9 @@
""
val new_facts =
- new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd))
+ new_facts
+ |> attach_parents_to_facts ctxt old_facts
+ |> map (`(nickname_of_thm ctxt o snd o snd))
val lines = map do_fact (tag_list 1 new_facts)
in
File.write_list path lines
@@ -243,16 +245,16 @@
val path = Path.explode file_name
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
- val name_tabs = build_name_tables nickname_of_thm facts
+ val name_tabs = build_name_tables (nickname_of_thm ctxt) facts
fun do_fact (j, ((_, th), old_facts)) =
if in_range range j then
let
- val name = nickname_of_thm th
+ val name = nickname_of_thm ctxt th
val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
- val isar_deps = isar_dependencies_of name_tabs th
+ val isar_deps = isar_dependencies_of ctxt name_tabs th
in
if is_bad_query ctxt ho_atp step j th isar_deps then
""
@@ -263,7 +265,7 @@
|> filter_accessible_from th
|> mepo_or_mash_suggested_facts ctxt (Thm.theory_of_thm th) params max_suggs hyp_ts
concl_t
- |> map (nickname_of_thm o snd)
+ |> map (nickname_of_thm ctxt o snd)
in
encode_str name ^ ": " ^ encode_strs suggs ^ "\n"
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 03 14:51:43 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 03 16:19:45 2015 +0200
@@ -45,19 +45,20 @@
val str_of_mash_algorithm : mash_algorithm -> string
val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
- val nickname_of_thm : thm -> string
+ val nickname_of_thm : Proof.context -> thm -> string
val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
- val crude_thm_ord : thm * thm -> order
+ val crude_thm_ord : Proof.context -> thm * thm -> order
val thm_less : thm * thm -> bool
val goal_of_thm : theory -> thm -> thm
val run_prover_for_mash : Proof.context -> params -> string -> string -> fact list -> thm ->
prover_result
val features_of : Proof.context -> string -> stature -> term list -> string list
val trim_dependencies : string list -> string list option
- val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
+ val isar_dependencies_of : Proof.context -> string Symtab.table * string Symtab.table ->
+ thm -> string list option
val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
string Symtab.table * string Symtab.table -> thm -> bool * string list
- val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
+ val attach_parents_to_facts : Proof.context -> ('a * thm) list -> ('a * thm) list ->
(string list * ('a * thm)) list
val num_extra_feature_facts : int
val extra_feature_factor : real
@@ -737,23 +738,24 @@
(*** Isabelle helpers ***)
-fun elided_backquote_thm threshold th =
- elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
+fun elided_backquote_thm ctxt threshold th =
+ elide_string threshold (backquote_thm ctxt th)
-fun nickname_of_thm th =
+fun nickname_of_thm ctxt th =
if Thm.has_name_hint th then
let val hint = Thm.get_name_hint th in
(* There must be a better way to detect local facts. *)
(case Long_Name.dest_local hint of
- SOME suf => Long_Name.implode [Thm.theory_name_of_thm th, suf, elided_backquote_thm 50 th]
+ SOME suf =>
+ Long_Name.implode [Thm.theory_name_of_thm th, suf, elided_backquote_thm ctxt 50 th]
| NONE => hint)
end
else
- elided_backquote_thm 200 th
+ elided_backquote_thm ctxt 200 th
fun find_suggested_facts ctxt facts =
let
- fun add (fact as (_, th)) = Symtab.default (nickname_of_thm th, fact)
+ fun add (fact as (_, th)) = Symtab.default (nickname_of_thm ctxt th, fact)
val tab = fold add facts Symtab.empty
fun lookup nick =
Symtab.lookup tab nick
@@ -776,12 +778,12 @@
EQUAL => string_ord (apply2 Context.theory_name p)
| order => order)
-fun crude_thm_ord p =
+fun crude_thm_ord ctxt p =
(case crude_theory_ord (apply2 Thm.theory_of_thm p) of
EQUAL =>
(* The hack below is necessary because of odd dependencies that are not reflected in the theory
comparison. *)
- let val q = apply2 nickname_of_thm p in
+ let val q = apply2 (nickname_of_thm ctxt) p in
(* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
(case bool_ord (apply2 (String.isSuffix "_def") (swap q)) of
EQUAL => string_ord q
@@ -934,14 +936,14 @@
val prover_default_max_facts = 25
(* "type_definition_xxx" facts are characterized by their use of "CollectI". *)
-val typedef_dep = nickname_of_thm @{thm CollectI}
+val typedef_dep = nickname_of_thm @{context} @{thm CollectI}
(* Mysterious parts of the class machinery create lots of proofs that refer exclusively to
"someI_ex" (and to some internal constructions). *)
-val class_some_dep = nickname_of_thm @{thm someI_ex}
+val class_some_dep = nickname_of_thm @{context} @{thm someI_ex}
val fundef_ths =
@{thms fundef_ex1_existence fundef_ex1_uniqueness fundef_ex1_iff fundef_default_value}
- |> map nickname_of_thm
+ |> map (nickname_of_thm @{context})
(* "Rep_xxx_inject", "Abs_xxx_inverse", etc., are derived using these facts. *)
val typedef_ths =
@@ -949,46 +951,46 @@
type_definition.Rep_inject type_definition.Abs_inject type_definition.Rep_cases
type_definition.Abs_cases type_definition.Rep_induct type_definition.Abs_induct
type_definition.Rep_range type_definition.Abs_image}
- |> map nickname_of_thm
+ |> map (nickname_of_thm @{context})
-fun is_size_def [dep] th =
+fun is_size_def ctxt [dep] th =
(case first_field ".rec" dep of
SOME (pref, _) =>
- (case first_field ".size" (nickname_of_thm th) of
+ (case first_field ".size" (nickname_of_thm ctxt th) of
SOME (pref', _) => pref = pref'
| NONE => false)
| NONE => false)
- | is_size_def _ _ = false
+ | is_size_def _ _ _ = false
fun trim_dependencies deps =
if length deps > max_dependencies then NONE else SOME deps
-fun isar_dependencies_of name_tabs th =
+fun isar_dependencies_of ctxt name_tabs th =
thms_in_proof max_dependencies (SOME name_tabs) th
|> Option.map (fn deps =>
if deps = [typedef_dep] orelse deps = [class_some_dep] orelse
exists (member (op =) fundef_ths) deps orelse exists (member (op =) typedef_ths) deps orelse
- is_size_def deps th then
+ is_size_def ctxt deps th then
[]
else
deps)
fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover auto_level facts
name_tabs th =
- (case isar_dependencies_of name_tabs th of
+ (case isar_dependencies_of ctxt name_tabs th of
SOME [] => (false, [])
| isar_deps0 =>
let
val isar_deps = these isar_deps0
val thy = Proof_Context.theory_of ctxt
val goal = goal_of_thm thy th
- val name = nickname_of_thm th
+ val name = nickname_of_thm ctxt th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal 1 ctxt
val facts = facts |> filter (fn (_, th') => thm_less (th', th))
- fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
+ fun nickify ((_, stature), th) = ((nickname_of_thm ctxt th, stature), th)
- fun is_dep dep (_, th) = nickname_of_thm th = dep
+ fun is_dep dep (_, th) = nickname_of_thm ctxt th = dep
fun add_isar_dep facts dep accum =
if exists (is_dep dep) accum then
@@ -1032,7 +1034,7 @@
(* In the following functions, chunks are risers w.r.t. "thm_less_eq". *)
-fun chunks_and_parents_for chunks th =
+fun chunks_and_parents_for ctxt chunks th =
let
fun insert_parent new parents =
let val parents = parents |> filter_out (fn p => thm_less_eq (p, new)) in
@@ -1056,11 +1058,11 @@
in
fold_rev do_chunk chunks ([], [])
|>> cons []
- ||> map nickname_of_thm
+ ||> map (nickname_of_thm ctxt)
end
-fun attach_parents_to_facts _ [] = []
- | attach_parents_to_facts old_facts (facts as (_, th) :: _) =
+fun attach_parents_to_facts _ _ [] = []
+ | attach_parents_to_facts ctxt old_facts (facts as (_, th) :: _) =
let
fun do_facts _ [] = []
| do_facts (_, parents) [fact] = [(parents, fact)]
@@ -1071,14 +1073,14 @@
val chunks_and_parents' =
if thm_less_eq (th, th') andalso
Thm.theory_name_of_thm th = Thm.theory_name_of_thm th'
- then (chunks, [nickname_of_thm th])
- else chunks_and_parents_for chunks th'
+ then (chunks, [nickname_of_thm ctxt th])
+ else chunks_and_parents_for ctxt chunks th'
in
(parents, fact) :: do_facts chunks_and_parents' facts
end
in
old_facts @ facts
- |> do_facts (chunks_and_parents_for [[]] th)
+ |> do_facts (chunks_and_parents_for ctxt [[]] th)
|> drop (length old_facts)
end
@@ -1110,15 +1112,15 @@
fun strict_subthy thyp = Theory.subthy thyp andalso not (Theory.subthy (swap thyp))
-fun maximal_wrt_access_graph _ [] = []
- | maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) =
+fun maximal_wrt_access_graph _ _ [] = []
+ | maximal_wrt_access_graph ctxt access_G ((fact as (_, th)) :: facts) =
let val thy = Thm.theory_of_thm th in
fact :: filter_out (fn (_, th') => strict_subthy (Thm.theory_of_thm th', thy)) facts
- |> map (nickname_of_thm o snd)
+ |> map (nickname_of_thm ctxt o snd)
|> maximal_wrt_graph access_G
end
-fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
+fun is_fact_in_graph ctxt access_G = can (Graph.get_node access_G) o nickname_of_thm ctxt
val chained_feature_factor = 0.5 (* FUDGE *)
val extra_feature_factor = 0.1 (* FUDGE *)
@@ -1149,7 +1151,7 @@
val algorithm = the_mash_algorithm ()
val facts = facts
- |> rev_sort_list_prefix (crude_thm_ord o apply2 snd)
+ |> rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd)
(Int.max (num_extra_feature_facts, max_proximity_facts))
val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
@@ -1181,7 +1183,7 @@
fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats0)
|> debug ? sort (Real.compare o swap o apply2 snd)
- val parents = maximal_wrt_access_graph access_G facts
+ val parents = maximal_wrt_access_graph ctxt access_G facts
val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
val suggs =
@@ -1201,7 +1203,7 @@
goal_feats int_goal_feats
end
- val unknown = filter_out (is_fact_in_graph access_G o snd) facts
+ val unknown = filter_out (is_fact_in_graph ctxt access_G o snd) facts
in
find_mash_suggestions ctxt max_suggs suggs facts chained unknown
|> apply2 (map fact_of_raw_fact)
@@ -1263,15 +1265,15 @@
let
val thy = Proof_Context.theory_of ctxt
val feats = features_of ctxt (Context.theory_name thy) (Local, General) [t]
- val facts = rev_sort_list_prefix (crude_thm_ord o apply2 snd) 1 facts
+ val facts = rev_sort_list_prefix (crude_thm_ord ctxt o apply2 snd) 1 facts
in
map_state ctxt
(fn {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} =>
let
- val parents = maximal_wrt_access_graph access_G facts
+ val parents = maximal_wrt_access_graph ctxt access_G facts
val deps = used_ths
- |> filter (is_fact_in_graph access_G)
- |> map nickname_of_thm
+ |> filter (is_fact_in_graph ctxt access_G)
+ |> map (nickname_of_thm ctxt)
val name = learned_proof_name ()
val (access_G', xtabs', rev_learns) =
@@ -1300,7 +1302,7 @@
fun next_commit_time () = Time.+ (Timer.checkRealTimer timer, commit_timeout)
val {access_G, ...} = peek_state ctxt
- val is_in_access_G = is_fact_in_graph access_G o snd
+ val is_in_access_G = is_fact_in_graph ctxt access_G o snd
val no_new_facts = forall is_in_access_G facts
in
if no_new_facts andalso not run_prover then
@@ -1314,7 +1316,7 @@
""
else
let
- val name_tabs = build_name_tables nickname_of_thm facts
+ val name_tabs = build_name_tables (nickname_of_thm ctxt) facts
fun deps_of status th =
if status = Non_Rec_Def orelse status = Rec_Def then
@@ -1323,7 +1325,7 @@
prover_dependencies_of ctxt params prover auto_level facts name_tabs th
|> (fn (false, _) => NONE | (true, deps) => trim_dependencies deps)
else
- isar_dependencies_of name_tabs th
+ isar_dependencies_of ctxt name_tabs th
fun do_commit [] [] [] state = state
| do_commit learns relearns flops
@@ -1371,7 +1373,7 @@
| learn_new_fact (parents, ((_, stature as (_, status)), th))
(learns, (num_nontrivial, next_commit, _)) =
let
- val name = nickname_of_thm th
+ val name = nickname_of_thm ctxt th
val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
val deps = these (deps_of status th)
val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
@@ -1392,8 +1394,8 @@
else
let
val new_facts = facts
- |> sort (crude_thm_ord o apply2 snd)
- |> attach_parents_to_facts []
+ |> sort (crude_thm_ord ctxt o apply2 snd)
+ |> attach_parents_to_facts ctxt []
|> filter_out (is_in_access_G o snd)
val (learns, (num_nontrivial, _, _)) =
([], (0, next_commit_time (), false))
@@ -1406,7 +1408,7 @@
| relearn_old_fact ((_, (_, status)), th)
((relearns, flops), (num_nontrivial, next_commit, _)) =
let
- val name = nickname_of_thm th
+ val name = nickname_of_thm ctxt th
val (num_nontrivial, relearns, flops) =
(case deps_of status th of
SOME deps => (num_nontrivial + 1, (name, deps) :: relearns, flops)
@@ -1430,7 +1432,7 @@
fun priority_of th =
Random.random_range 0 max_isar +
- (case try (Graph.get_node access_G) (nickname_of_thm th) of
+ (case try (Graph.get_node access_G) (nickname_of_thm ctxt th) of
SOME (Isar_Proof, _, deps) => ~100 * length deps
| SOME (Automatic_Proof, _, _) => 2 * max_isar
| SOME (Isar_Proof_wegen_Prover_Flop, _, _) => max_isar
@@ -1464,7 +1466,7 @@
val ctxt = ctxt |> Config.put instantiate_inducts false
val facts =
nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] @{prop True}
- |> sort (crude_thm_ord o apply2 snd o swap)
+ |> sort (crude_thm_ord ctxt o apply2 snd o swap)
val num_facts = length facts
val prover = hd provers
@@ -1532,7 +1534,7 @@
fun please_learn () =
let
val {access_G, xtabs = ((num_facts0, _), _), ...} = peek_state ctxt
- val is_in_access_G = is_fact_in_graph access_G o snd
+ val is_in_access_G = is_fact_in_graph ctxt access_G o snd
val min_num_facts_to_learn = length facts - num_facts0
in
if min_num_facts_to_learn <= max_facts_to_learn_before_query then