# HG changeset patch
# User blanchet
# Date 1283329614 -7200
# Node ID 542474156c661c2c3ed08dbc63e0aff049d64344
# Parent  0e2798f30087573783d228596ed0aea9fda8374a
introduce fudge factors to deal with "theory const"

diff -r 0e2798f30087 -r 542474156c66 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- 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)
diff -r 0e2798f30087 -r 542474156c66 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- 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