# HG changeset patch # User wenzelm # Date 1435927903 -7200 # Node ID 58326c4a3ea2f355a539649430924ff0872611e4 # Parent 6686a410842a464c91720580a2d0363e91b04004 tuned signature; diff -r 6686a410842a -r 58326c4a3ea2 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri Jul 03 14:41:55 2015 +0200 +++ b/src/HOL/TPTP/mash_export.ML Fri Jul 03 14:51:43 2015 +0200 @@ -98,7 +98,7 @@ fun do_fact ((_, stature), th) = let val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of 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 File.append path s @@ -188,14 +188,14 @@ val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) val isar_deps = isar_dependencies_of 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_of_thm th) stature [Thm.prop_of th] + 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 val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps fun extra_features_of (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_of_thm th) stature + |> features_of ctxt (Thm.theory_name_of_thm th) stature |> map (rpair (weight * extra_feature_factor)) val query = diff -r 6686a410842a -r 58326c4a3ea2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 03 14:41:55 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 03 14:51:43 2015 +0200 @@ -52,7 +52,7 @@ 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 -> theory -> stature -> term list -> string list + 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 prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list -> @@ -922,12 +922,10 @@ val type_max_depth = 1 (* TODO: Generate type classes for types? *) -fun features_of ctxt thy (scope, _) ts = - let val thy_name = Context.theory_name thy in - thy_feature_of thy_name :: - term_features_of ctxt thy_name term_max_depth type_max_depth ts - |> scope <> Global ? cons local_feature - end +fun features_of ctxt thy_name (scope, _) ts = + thy_feature_of thy_name :: + term_features_of ctxt thy_name term_max_depth type_max_depth ts + |> scope <> Global ? cons local_feature (* Too many dependencies is a sign that a decision procedure is at work. There is not much to learn from such proofs. *) @@ -1160,13 +1158,14 @@ fun chained_or_extra_features_of factor (((_, stature), th), weight) = [Thm.prop_of th] - |> features_of ctxt (Thm.theory_of_thm th) stature + |> features_of ctxt (Thm.theory_name_of_thm th) stature |> map (rpair (weight * factor)) val {access_G, xtabs = ((num_facts, fact_tab), (num_feats, feat_tab)), ffds, freqs, ...} = peek_state ctxt - val goal_feats0 = features_of ctxt thy (Local, General) (concl_t :: hyp_ts) + val goal_feats0 = + features_of ctxt (Context.theory_name thy) (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) @@ -1263,7 +1262,7 @@ launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt - val feats = features_of ctxt thy (Local, General) [t] + 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 in map_state ctxt @@ -1373,7 +1372,7 @@ (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th - val feats = features_of ctxt (Thm.theory_of_thm th) stature [Thm.prop_of 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 val learns = (name, parents, feats, deps) :: learns