# HG changeset patch # User blanchet # Date 1403881522 -7200 # Node ID e844dcf57debf128b36bdf5851fcbfc0fa9e61ea # Parent 1f49da059947b613d35cc79dc1ddaabb2b4919b7 killed dead code diff -r 1f49da059947 -r e844dcf57deb src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Fri Jun 27 16:52:50 2014 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Fri Jun 27 17:05:22 2014 +0200 @@ -15,8 +15,8 @@ val MeSh_IsarN : string val MeSh_ProverN : string val IsarN : string - val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> bool -> - string list -> string option -> string -> string -> string -> string -> string -> string -> unit + val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> string list -> + string option -> string -> string -> string -> string -> string -> string -> unit end; structure MaSh_Eval : MASH_EVAL = @@ -41,9 +41,9 @@ fun in_range (from, to) j = j >= from andalso (to = NONE orelse j <= the to) -fun evaluate_mash_suggestions ctxt params range linearize methods prob_dir_name - mepo_file_name mash_isar_file_name mash_prover_file_name - mesh_isar_file_name mesh_prover_file_name report_file_name = +fun evaluate_mash_suggestions ctxt params range methods prob_dir_name mepo_file_name + mash_isar_file_name mash_prover_file_name mesh_isar_file_name mesh_prover_file_name + report_file_name = let val thy = Proof_Context.theory_of ctxt val zeros = [0, 0, 0, 0, 0, 0] @@ -112,11 +112,7 @@ 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 facts = - facts - |> filter (fn (_, th') => - if linearize then crude_thm_ord (th', th) = LESS - else thm_less (th', th)) + val facts = facts |> filter (fn (_, th') => thm_less (th', th)) (* adapted from "mirabelle_sledgehammer.ML" *) fun set_file_name method (SOME dir) = let diff -r 1f49da059947 -r e844dcf57deb src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri Jun 27 16:52:50 2014 +0200 +++ b/src/HOL/TPTP/mash_export.ML Fri Jun 27 17:05:22 2014 +0200 @@ -54,9 +54,9 @@ let val path = Path.explode file_name - fun do_fact (parents, fact) prevs = + fun do_fact (parents, fact) = let val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" in - File.append path s; [fact] + File.append path s end val facts = @@ -66,7 +66,7 @@ |> map (apsnd (nickname_of_thm o snd)) in File.write path ""; - ignore (fold do_fact facts []) + List.app do_fact facts end fun generate_features ctxt thys file_name = @@ -78,8 +78,7 @@ fun do_fact ((_, stature), th) = let val name = nickname_of_thm th - val feats = - features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] |> map fst + val feats = features_of ctxt (theory_of_thm th) stature [prop_of th] val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n" in File.append path s @@ -161,26 +160,23 @@ 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 num_old_facts = length old_facts val name_tabs = build_name_tables nickname_of_thm facts - fun do_fact (j, (((name, (parents, ((_, stature), th))), prevs), const_tab)) = + fun do_fact (j, ((name, (parents, ((_, stature), th))), prevs)) = 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 do_query = not (is_bad_query ctxt ho_atp step j th isar_deps) - val goal_feats = - features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th] - |> sort_wrt fst + val goal_feats = features_of ctxt (theory_of_thm th) stature [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) = [prop_of th] - |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature - |> map (apsnd (fn r => weight * extra_feature_factor * r)) + |> features_of ctxt (theory_of_thm th) stature + |> map (rpair (weight * extra_feature_factor)) val query = if do_query then @@ -192,7 +188,8 @@ |> rev |> weight_facts_steeply |> map extra_features_of - |> rpair goal_feats |-> fold (union (eq_fst (op =))) + |> rpair (map (rpair 1.0) goal_feats) + |-> fold (union (eq_fst (op =))) in "? " ^ string_of_int max_suggs ^ " # " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_features query_feats ^ "\n" @@ -200,8 +197,8 @@ else "" val update = - "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ - encode_strs (map fst goal_feats) ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n" + "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^ encode_strs goal_feats ^ + "; " ^ marker ^ " " ^ encode_strs deps ^ "\n" in query ^ update end else "" @@ -210,10 +207,7 @@ new_facts |> attach_parents_to_facts old_facts |> map (`(nickname_of_thm o snd o snd)) val hd_prevs = map (nickname_of_thm o snd) (the_list (try List.last old_facts)) val prevss = hd_prevs :: map (single o fst) new_facts |> split_last |> fst - val hd_const_tabs = fold (add_const_counts o prop_of o snd) old_facts Symtab.empty - val (const_tabs, _) = - fold_map (`I oo add_const_counts o prop_of o snd o snd o snd) new_facts hd_const_tabs - val lines = map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs)) + val lines = map do_fact (tag_list 1 (new_facts ~~ prevss)) in File.write_list path lines end diff -r 1f49da059947 -r e844dcf57deb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 16:52:50 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 17:05:22 2014 +0200 @@ -54,8 +54,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 -> int -> int Symtab.table -> stature -> term list -> - string list + val features_of : Proof.context -> theory -> 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 -> @@ -68,7 +67,6 @@ val weight_facts_steeply : 'a list -> ('a * real) list val find_mash_suggestions : Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list * ('b * thm) list - val add_const_counts : term -> int Symtab.table -> int Symtab.table val mash_suggested_facts : Proof.context -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list val mash_learn_proof : Proof.context -> params -> term -> ('a * thm) list -> thm list -> unit @@ -320,10 +318,10 @@ structure MaSh_SML = struct -exception BOTTOM of int - fun heap cmp bnd al a = let + exception BOTTOM of int + fun maxson l i = let val i31 = i + i + i + 1 in if i31 + 2 < l then @@ -395,10 +393,10 @@ Array.update (recommends, at, (j, big_number + ov)) end) -exception EXIT of unit - fun k_nearest_neighbors dffreq num_facts depss feat_facts max_suggs visible_facts goal_feats = let + exception EXIT of unit + val ln_afreq = Math.ln (Real.fromInt num_facts) fun tfidf feat = ln_afreq - Math.ln (Real.fromInt (Vector.sub (dffreq, feat))) @@ -968,7 +966,7 @@ val max_pat_breadth = 10 (* FUDGE *) -fun term_features_of ctxt thy_name num_facts const_tab term_max_depth type_max_depth ts = +fun term_features_of ctxt thy_name term_max_depth type_max_depth ts = let val thy = Proof_Context.theory_of ctxt @@ -1060,10 +1058,10 @@ val type_max_depth = 1 (* TODO: Generate type classes for types? *) -fun features_of ctxt thy num_facts const_tab (scope, _) ts = +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 num_facts const_tab term_max_depth type_max_depth ts + term_features_of ctxt thy_name term_max_depth type_max_depth ts |> scope <> Global ? cons local_feature end @@ -1291,9 +1289,6 @@ (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown) end -fun add_const_counts t = - fold (fn s => Symtab.map_default (s, 0) (Integer.add 1)) (Term.add_const_names t []) - fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) max_suggs hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt @@ -1302,26 +1297,20 @@ 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 - - (* Weights appear to hurt kNN more than they help. *) - val const_tab = Symtab.empty |> engine <> MaSh_SML_kNN - ? fold (add_const_counts o prop_of o snd) facts 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 (theory_of_thm th) num_facts const_tab stature + |> features_of ctxt (theory_of_thm th) stature |> map (rpair (weight * factor)) fun query_args access_G = let val parents = maximal_wrt_access_graph access_G facts - val goal_feats = - features_of ctxt thy num_facts const_tab (Local, General) (concl_t :: hyp_ts) + val goal_feats = features_of ctxt thy (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) @@ -1435,7 +1424,7 @@ launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt - val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] + val feats = features_of ctxt thy (Local, General) [t] in map_state ctxt overlord (fn state as {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => @@ -1554,7 +1543,7 @@ (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th - val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th] + val feats = features_of ctxt (theory_of_thm th) stature [prop_of th] val deps = deps_of status th |> these val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1 val learns = (name, parents, feats, deps) :: learns