# HG changeset patch
# User blanchet
# Date 1354710306 -3600
# Node ID cb564ff43c28bfb5275b16f68fb29451384e15cc
# Parent  3ae4376cb739d45d0de984203233326849a9725e
tuning

diff -r 3ae4376cb739 -r cb564ff43c28 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 11:05:34 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 05 13:25:06 2012 +0100
@@ -57,9 +57,10 @@
   val atp_dependencies_of :
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     -> thm -> bool * string list option
+  val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term
-    -> fact list -> (fact * real) list * fact list
+    -> fact list -> fact list * fact list
   val mash_learn_proof :
     Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
     -> unit
@@ -473,11 +474,11 @@
     EQUAL => string_ord (pairself Context.theory_name p)
   | order => order
 
-fun thm_ord thp =
-  case theory_ord (pairself theory_of_thm thp) of
+fun thm_ord p =
+  case theory_ord (pairself theory_of_thm p) of
     EQUAL =>
     (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
-    string_ord (pairself nickname_of (swap thp))
+    string_ord (pairself nickname_of (swap p))
   | ord => ord
 
 val freezeT = Type.legacy_freeze_type
@@ -708,6 +709,8 @@
 (* factor that controls whether unknown global facts should be included *)
 val include_unk_global_factor = 15
 
+val weight_mash_facts = weight_mepo_facts (* use MePo weights for now *)
+
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
@@ -740,8 +743,7 @@
       ([], unk_global)
       |> include_unk_global_factor * length unk_global <= max_facts ? swap
   in
-    (interleave max_facts (chained @ unk_local @ small_unk_global) sels
-     |> weight_mepo_facts (* use MePo weights for now *),
+    (interleave max_facts (chained @ unk_local @ small_unk_global) sels,
      big_unk_global)
   end
 
@@ -1034,11 +1036,12 @@
          (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
         |> take max_facts
       fun mepo () =
-        facts |> mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts
-                                      concl_t
-              |> weight_mepo_facts
+        mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
+                             facts
+        |> weight_mepo_facts
       fun mash () =
         mash_suggested_facts ctxt params prover max_facts hyp_ts concl_t facts
+        |>> weight_mash_facts
       val mess =
         [] |> (if fact_filter <> mashN then cons (mepo (), []) else I)
            |> (if fact_filter <> mepoN then cons (mash ()) else I)
diff -r 3ae4376cb739 -r cb564ff43c28 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 11:05:34 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Dec 05 13:25:06 2012 +0100
@@ -18,10 +18,10 @@
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
+  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
   val mepo_suggested_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
     -> term list -> term -> fact list -> fact list
-  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
 end;
 
 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
@@ -509,6 +509,12 @@
                       "Total relevant: " ^ string_of_int (length accepts)))
   end
 
+(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
+fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+
+fun weight_mepo_facts facts =
+  facts ~~ map weight_of_fact (0 upto length facts - 1)
+
 fun mepo_suggested_facts ctxt
         ({fact_thresholds = (thres0, thres1), ...} : params) prover
         max_facts fudge hyp_ts concl_t facts =
@@ -535,10 +541,4 @@
            (concl_t |> theory_constify fudge (Context.theory_name thy)))
   end
 
-(* Ad hoc score function roughly based on Blanchette's Ringberg 2011 data. *)
-fun weight_of_fact rank = Math.pow (1.5, 15.5 - 0.05 * Real.fromInt rank) + 15.0
-
-fun weight_mepo_facts facts =
-  facts ~~ map weight_of_fact (0 upto length facts - 1)
-
 end;