# HG changeset patch # User blanchet # Date 1381304879 -7200 # Node ID b6b41e1d568912fa72ba681949b21394c3139fdd # Parent c2782ec22cc6841af82423dbea87dc9e4c9dedb4 optimized built-in const check diff -r c2782ec22cc6 -r b6b41e1d5689 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Oct 09 08:28:36 2013 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Oct 09 09:47:59 2013 +0200 @@ -72,6 +72,7 @@ fun generate_features ctxt prover thys file_name = let + val is_built_in_const = Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover val path = file_name |> Path.explode val _ = File.write path "" val facts = all_facts ctxt |> filter_out (has_thys thys o snd) @@ -79,8 +80,7 @@ let val name = nickname_of_thm th val feats = - features_of ctxt prover (theory_of_thm th) 0 Symtab.empty stature - [prop_of th] + features_of ctxt is_built_in_const (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" @@ -150,6 +150,7 @@ fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys linearize max_suggs file_name = let + val is_built_in_const = Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val path = file_name |> Path.explode val facts = all_facts ctxt @@ -164,8 +165,8 @@ 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 prover (theory_of_thm th) (num_old_facts + j) - const_tab stature [prop_of th] + features_of ctxt is_built_in_const (theory_of_thm th) (num_old_facts + j) const_tab + stature [prop_of th] |> sort_wrt fst val access_facts = (if linearize then take (j - 1) new_facts @@ -176,8 +177,8 @@ val parents = if linearize then prevs else parents fun extra_features_of (((_, stature), th), weight) = [prop_of th] - |> features_of ctxt prover (theory_of_thm th) (num_old_facts + j) - const_tab stature + |> features_of ctxt is_built_in_const (theory_of_thm th) (num_old_facts + j) const_tab + stature |> map (apsnd (fn r => weight * extra_feature_factor * r)) val query = if do_query then diff -r c2782ec22cc6 -r b6b41e1d5689 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Oct 09 08:28:36 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Oct 09 09:47:59 2013 +0200 @@ -63,8 +63,8 @@ val run_prover_for_mash : Proof.context -> params -> string -> fact list -> thm -> prover_result val features_of : - Proof.context -> string -> theory -> int -> int Symtab.table -> stature - -> term list -> (string * real) list + Proof.context -> (string * typ -> term list -> bool * term list) -> theory -> + int -> int Symtab.table -> stature -> term list -> (string * real) list val trim_dependencies : string list -> string list option val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list @@ -608,14 +608,14 @@ val max_pat_breadth = 10 (* FUDGE *) -fun term_features_of ctxt prover thy_name num_facts const_tab term_max_depth +fun term_features_of ctxt is_built_in_const thy_name num_facts const_tab term_max_depth type_max_depth ts = let val thy = Proof_Context.theory_of ctxt fun is_built_in (x as (s, _)) args = if member (op =) logical_consts s then (true, args) - else is_built_in_const_of_prover ctxt prover x args + else is_built_in_const x args val fixes = map snd (Variable.dest_fixes ctxt) val classes = Sign.classes_of thy @@ -715,11 +715,11 @@ val type_max_depth = 1 (* TODO: Generate type classes for types? *) -fun features_of ctxt prover thy num_facts const_tab (scope, _) ts = +fun features_of ctxt is_built_in_const thy num_facts const_tab (scope, _) ts = let val thy_name = Context.theory_name thy in thy_feature_of thy_name :: - term_features_of ctxt prover thy_name num_facts const_tab term_max_depth - type_max_depth ts + term_features_of ctxt is_built_in_const thy_name num_facts const_tab term_max_depth + type_max_depth ts |> scope <> Global ? cons local_feature end @@ -961,16 +961,19 @@ let val thy = Proof_Context.theory_of ctxt val thy_name = Context.theory_name thy + val is_built_in_const = is_built_in_const_of_prover ctxt prover val facts = facts |> sort (crude_thm_ord o pairself snd o swap) val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) val num_facts = length facts val const_tab = fold (add_const_counts o prop_of o snd) facts Symtab.empty + fun fact_has_right_theory (_, th) = thy_name = Context.theory_name (theory_of_thm th) fun chained_or_extra_features_of factor (((_, stature), th), weight) = [prop_of th] - |> features_of ctxt prover (theory_of_thm th) num_facts const_tab stature + |> features_of ctxt is_built_in_const (theory_of_thm th) num_facts const_tab stature |> map (apsnd (fn r => weight * factor * r)) + val (access_G, suggs) = peek_state ctxt overlord (fn {access_G, ...} => if Graph.is_empty access_G then @@ -979,8 +982,8 @@ let val parents = maximal_wrt_access_graph access_G facts val goal_feats = - features_of ctxt prover thy num_facts const_tab (Local, General) - (concl_t :: hyp_ts) + features_of ctxt is_built_in_const thy num_facts const_tab (Local, General) + (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) @@ -1050,7 +1053,8 @@ val thy = Proof_Context.theory_of ctxt val name = freshish_name () val feats = - features_of ctxt prover thy 0 Symtab.empty (Local, General) [t] + features_of ctxt (is_built_in_const_of_prover ctxt prover) thy 0 Symtab.empty + (Local, General) [t] |> map fst in peek_state ctxt overlord (fn {access_G, ...} => @@ -1096,6 +1100,7 @@ "" else let + val is_built_in_const = is_built_in_const_of_prover ctxt prover val name_tabs = build_name_tables nickname_of_thm facts fun deps_of status th = if no_dependencies_for_status status then @@ -1150,8 +1155,8 @@ let val name = nickname_of_thm th val feats = - features_of ctxt prover (theory_of_thm th) 0 Symtab.empty - stature [prop_of th] + features_of ctxt is_built_in_const (theory_of_thm th) 0 Symtab.empty stature + [prop_of th] |> map fst val deps = deps_of status th |> these val n = n |> not (null deps) ? Integer.add 1