--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 00:07:31 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 10:26:54 2010 +0200
@@ -5,21 +5,25 @@
structure Mirabelle_Sledgehammer_Filter : MIRABELLE_ACTION =
struct
+structure SF = Sledgehammer_Filter
+
val relevance_filter_args =
- [("worse_irrel_freq", Sledgehammer_Filter.worse_irrel_freq),
- ("higher_order_irrel_weight", Sledgehammer_Filter.higher_order_irrel_weight),
- ("abs_rel_weight", Sledgehammer_Filter.abs_rel_weight),
- ("abs_irrel_weight", Sledgehammer_Filter.abs_irrel_weight),
- ("skolem_irrel_weight", Sledgehammer_Filter.skolem_irrel_weight),
- ("intro_bonus", Sledgehammer_Filter.intro_bonus),
- ("elim_bonus", Sledgehammer_Filter.elim_bonus),
- ("simp_bonus", Sledgehammer_Filter.simp_bonus),
- ("local_bonus", Sledgehammer_Filter.local_bonus),
- ("chained_bonus", Sledgehammer_Filter.chained_bonus),
- ("max_imperfect", Sledgehammer_Filter.max_imperfect),
- ("max_imperfect_exp", Sledgehammer_Filter.max_imperfect_exp),
- ("threshold_divisor", Sledgehammer_Filter.threshold_divisor),
- ("ridiculous_threshold", Sledgehammer_Filter.ridiculous_threshold)]
+ [("worse_irrel_freq", SF.worse_irrel_freq),
+ ("higher_order_irrel_weight", SF.higher_order_irrel_weight),
+ ("abs_rel_weight", SF.abs_rel_weight),
+ ("abs_irrel_weight", SF.abs_irrel_weight),
+ ("skolem_irrel_weight", SF.skolem_irrel_weight),
+ ("theory_const_rel_weight", SF.theory_const_rel_weight),
+ ("theory_const_irrel_weight", SF.theory_const_irrel_weight),
+ ("intro_bonus", SF.intro_bonus),
+ ("elim_bonus", SF.elim_bonus),
+ ("simp_bonus", SF.simp_bonus),
+ ("local_bonus", SF.local_bonus),
+ ("chained_bonus", SF.chained_bonus),
+ ("max_imperfect", SF.max_imperfect),
+ ("max_imperfect_exp", SF.max_imperfect_exp),
+ ("threshold_divisor", SF.threshold_divisor),
+ ("ridiculous_threshold", SF.ridiculous_threshold)]
structure Prooftab =
Table(type key = int * int val ord = prod_ord int_ord int_ord);
@@ -103,7 +107,7 @@
val subgoal = 1
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
- Sledgehammer_Filter.relevant_facts ctxt full_types
+ SF.relevant_facts ctxt full_types
relevance_thresholds
(the_default default_max_relevant max_relevant)
(the_default false theory_relevant)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 01 00:07:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 01 10:26:54 2010 +0200
@@ -18,6 +18,8 @@
val abs_rel_weight : real Unsynchronized.ref
val abs_irrel_weight : real Unsynchronized.ref
val skolem_irrel_weight : real Unsynchronized.ref
+ val theory_const_rel_weight : real Unsynchronized.ref
+ val theory_const_irrel_weight : real Unsynchronized.ref
val intro_bonus : real Unsynchronized.ref
val elim_bonus : real Unsynchronized.ref
val simp_bonus : real Unsynchronized.ref
@@ -56,6 +58,9 @@
only: bool}
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
+val abs_name = "Sledgehammer.abs"
+val skolem_prefix = "Sledgehammer.sko"
+val theory_const_suffix = Long_Name.separator ^ " 1"
fun repair_name reserved multi j name =
(name |> Symtab.defined reserved name ? quote) ^
@@ -139,9 +144,6 @@
fun string_for_hyper_pconst (s, ps) =
s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
-val abs_name = "Sledgehammer.abs"
-val skolem_prefix = "Sledgehammer.sko"
-
(* These are typically simplified away by "Meson.presimplify". Equality is
handled specially via "fequal". *)
val boring_consts =
@@ -228,7 +230,7 @@
if theory_relevant then
let
val name = Context.theory_name (theory_of_thm th)
- val t = Const (name ^ ". 1", @{typ bool})
+ val t = Const (name ^ theory_const_suffix, @{typ bool})
in t $ prop_of th end
else
prop_of th
@@ -306,19 +308,23 @@
val abs_rel_weight = Unsynchronized.ref 0.5
val abs_irrel_weight = Unsynchronized.ref 2.0
val skolem_irrel_weight = Unsynchronized.ref 0.75
+val theory_const_rel_weight = Unsynchronized.ref 0.5
+val theory_const_irrel_weight = Unsynchronized.ref 0.25
(* Computes a constant's weight, as determined by its frequency. *)
-fun generic_pconst_weight abs_weight skolem_weight weight_for f const_tab
- (c as (s, PType (m, _))) =
+fun generic_pconst_weight abs_weight skolem_weight theory_const_weight
+ weight_for f const_tab (c as (s, PType (m, _))) =
if s = abs_name then abs_weight
else if String.isPrefix skolem_prefix s then skolem_weight
+ else if String.isSuffix theory_const_suffix s then theory_const_weight
else weight_for m (pconst_freq (match_ptype o f) const_tab c)
fun rel_pconst_weight const_tab =
- generic_pconst_weight (!abs_rel_weight) 0.0 rel_weight_for I const_tab
+ generic_pconst_weight (!abs_rel_weight) 0.0 (!theory_const_rel_weight)
+ rel_weight_for I const_tab
fun irrel_pconst_weight const_tab =
generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight)
- irrel_weight_for swap const_tab
+ (!theory_const_irrel_weight) irrel_weight_for swap const_tab
(* FUDGE *)
val intro_bonus = Unsynchronized.ref 0.15