# HG changeset patch # User blanchet # Date 1403871650 -7200 # Node ID a68ae60c15049a239b4397608e8a30dfd0471e7f # Parent 5e65e3d108a168df99c6d0562f6477a86976963a got rid of hard-coded weights, now that we have TFIDF diff -r 5e65e3d108a1 -r a68ae60c1504 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 12:06:22 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jun 27 14:20:50 2014 +0200 @@ -55,7 +55,7 @@ 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 * real) 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 -> @@ -896,12 +896,11 @@ |> map snd |> take max_facts end -val default_weight = 1.0 -fun free_feature_of s = ("f" ^ s, 40.0 (* FUDGE *)) -fun thy_feature_of s = ("y" ^ s, 8.0 (* FUDGE *)) -fun type_feature_of s = ("t" ^ s, 4.0 (* FUDGE *)) -fun class_feature_of s = ("s" ^ s, 1.0 (* FUDGE *)) -val local_feature = ("local", 16.0 (* FUDGE *)) +fun free_feature_of s = "f" ^ s +fun thy_feature_of s = "y" ^ s +fun type_feature_of s = "t" ^ s +fun class_feature_of s = "s" ^ s +val local_feature = "local" fun crude_theory_ord p = if Theory.subthy p then @@ -982,7 +981,7 @@ #> swap #> op :: #> subtract (op =) @{sort type} #> map massage_long_name #> map class_feature_of - #> union (eq_fst (op =))) S + #> union (op =)) S fun pattify_type 0 _ = [] | pattify_type _ (Type (s, [])) = @@ -1001,11 +1000,10 @@ maybe_singleton_str pat_tvar_prefix (crude_str_of_sort S) fun add_type_pat depth T = - union (eq_fst (op =)) (map type_feature_of (pattify_type depth T)) + union (op =) (map type_feature_of (pattify_type depth T)) fun add_type_pats 0 _ = I - | add_type_pats depth t = - add_type_pat depth t #> add_type_pats (depth - 1) t + | add_type_pats depth t = add_type_pat depth t #> add_type_pats (depth - 1) t fun add_type T = add_type_pats type_max_depth T @@ -1014,44 +1012,28 @@ fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts | add_subtypes T = add_type T - val base_weight_of_const = 16.0 (* FUDGE *) - val weight_of_const = - (if num_facts = 0 orelse Symtab.is_empty const_tab then - K base_weight_of_const - else - fn s => - let val count = Symtab.lookup const_tab s |> the_default 1 in - base_weight_of_const + Real.fromInt num_facts / Real.fromInt count - end) - fun pattify_term _ 0 _ = [] | pattify_term _ _ (Const (s, _)) = - if is_widely_irrelevant_const s then [] else [(massage_long_name s, weight_of_const s)] + if is_widely_irrelevant_const s then [] else [massage_long_name s] | pattify_term _ _ (Free (s, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T) - |> map (rpair 1.0) |> (if member (op =) fixes s then - cons (free_feature_of (massage_long_name - (thy_name ^ Long_Name.separator ^ s))) + cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s))) else I) - | pattify_term _ _ (Var (_, T)) = - maybe_singleton_str pat_var_prefix (crude_str_of_typ T) |> map (rpair default_weight) + | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T) | pattify_term Ts _ (Bound j) = maybe_singleton_str pat_var_prefix (crude_str_of_typ (nth Ts j)) - |> map (rpair default_weight) | pattify_term Ts depth (t $ u) = let val ps = take max_pat_breadth (pattify_term Ts depth t) - val qs = take max_pat_breadth (("", default_weight) :: pattify_term Ts (depth - 1) u) + val qs = take max_pat_breadth ("" :: pattify_term Ts (depth - 1) u) in - map_product (fn ppw as (p, pw) => - fn ("", _) => ppw - | (q, qw) => (p ^ "(" ^ q ^ ")", pw + qw)) ps qs + map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end | pattify_term _ _ _ = [] - fun add_term_pat Ts = union (eq_fst (op =)) oo pattify_term Ts + fun add_term_pat Ts = union (op =) oo pattify_term Ts fun add_term_pats _ 0 _ = I | add_term_pats Ts depth t = add_term_pat Ts depth t #> add_term_pats Ts (depth - 1) t @@ -1062,8 +1044,7 @@ (case strip_comb t of (Const (s, T), args) => (not (is_widely_irrelevant_const s) ? add_term Ts t) - #> add_subtypes T - #> fold (add_subterms Ts) args + #> add_subtypes T #> fold (add_subterms Ts) args | (head, args) => (case head of Free (_, T) => add_term Ts t #> add_subtypes T @@ -1333,7 +1314,7 @@ 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 - |> map (apsnd (fn r => weight * factor * r)) + |> map (rpair (weight * factor)) fun query_args access_G = let @@ -1352,7 +1333,8 @@ |> weight_facts_steeply |> map (chained_or_extra_features_of extra_feature_factor) |> rpair [] |-> fold (union (eq_fst (op =))) - val feats = fold (union (eq_fst (op =))) [chained_feats, extra_feats] goal_feats + val feats = + fold (union (eq_fst (op =))) [chained_feats, extra_feats] (map (rpair 1.0) goal_feats) |> debug ? sort (Real.compare o swap o pairself snd) in (parents, feats) @@ -1453,7 +1435,7 @@ launch_thread timeout (fn () => let val thy = Proof_Context.theory_of ctxt - val feats = map fst (features_of ctxt thy 0 Symtab.empty (Local, General) [t]) + val feats = features_of ctxt thy 0 Symtab.empty (Local, General) [t] in map_state ctxt overlord (fn state as {access_G, xtabs as ((num_facts0, _), _), ffds, freqs, dirty_facts} => @@ -1572,8 +1554,7 @@ (learns, (num_nontrivial, next_commit, _)) = let val name = nickname_of_thm th - val feats = - map fst (features_of ctxt (theory_of_thm th) 0 Symtab.empty stature [prop_of th]) + val feats = features_of ctxt (theory_of_thm th) 0 Symtab.empty 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