--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Sep 12 10:40:53 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Sep 12 11:05:19 2013 +0200
@@ -452,7 +452,7 @@
end
fun mash_unlearn ctxt ({overlord, ...} : params) =
- (clear_state ctxt overlord; Output.urgent_message "Reset MaSh")
+ (clear_state ctxt overlord; Output.urgent_message "Reset MaSh.")
(*** Isabelle helpers ***)
@@ -951,14 +951,17 @@
fold (fn s => Symtab.map_default (s, 0) (Integer.add 1))
(Term.add_const_names t [])
-fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
- concl_t facts =
+fun mash_suggested_facts ctxt ({debug, overlord, ...} : params) prover max_facts
+ hyp_ts concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
+ val thy_name = Context.theory_name thy
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
@@ -971,8 +974,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 prover thy num_facts const_tab (Local, General)
+ (concl_t :: hyp_ts)
val chained_feats =
chained
|> map (rpair 1.0)
@@ -981,12 +984,14 @@
val extra_feats =
facts
|> take (Int.max (0, num_extra_feature_facts - length chained))
+ |> filter fact_has_right_theory
|> 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
+ |> debug ? sort (Real.compare o swap o pairself snd)
val hints =
chained |> filter (is_fact_in_graph access_G o snd)
|> map (nickname_of_thm o snd)