# HG changeset patch
# User blanchet
# Date 1377166372 -7200
# Node ID a1235e90da5f05d07e6abd950c07187655975fe6
# Parent  07a6e11f163122d92d1e940e872e2c4236177b42
pour extra features from proximate facts into goal, in exporter

diff -r 07a6e11f1631 -r a1235e90da5f src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Aug 22 12:12:51 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Aug 22 12:12:52 2013 +0200
@@ -174,11 +174,29 @@
             smart_dependencies_of ctxt params_opt access_facts name_tabs th
                                   (SOME isar_deps)
           val parents = if linearize then prevs else parents
+          fun extra_features_of (((_, stature), th), weight) =
+            [prop_of th]
+            |> features_of ctxt prover (theory_of_thm th) (num_old_facts + j)
+                           const_tab stature
+            |> map (apsnd (fn r => weight * extra_feature_weight_factor * r))
           val query =
             if do_query then
-              "? " ^ string_of_int max_suggs ^ " # " ^
-              encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
-              encode_features feats ^ "\n"
+              let
+                val extra_featss =
+                  new_facts
+                  |> drop (j - num_extra_feature_facts)
+                  |> take num_extra_feature_facts
+                  |> rev
+                  |> weight_facts_steeply
+                  |> map extra_features_of
+                val extra_feats =
+                  fold_rev (union (op = o pairself fst)) extra_featss []
+                val query_feats = union (op = o pairself fst) extra_feats feats
+              in
+                "? " ^ string_of_int max_suggs ^ " # " ^
+                encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
+                encode_features query_feats ^ "\n"
+              end
             else
               ""
           val update =
@@ -254,10 +272,10 @@
       let
         val (name, mash_suggs) =
           extract_suggestions mash_line
-          ||> weight_mash_facts
+          ||> weight_facts_steeply
         val (name', mepo_suggs) =
           extract_suggestions mepo_line
-          ||> weight_mepo_facts
+          ||> weight_facts_steeply
         val _ = if name = name' then () else error "Input files out of sync."
         val mess =
           [(mepo_weight, (mepo_suggs, [])),
diff -r 07a6e11f1631 -r a1235e90da5f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Aug 22 12:12:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Aug 22 12:12:52 2013 +0200
@@ -73,8 +73,10 @@
     -> bool * string list
   val attach_parents_to_facts :
     ('a * thm) list -> ('a * thm) list -> (string list * ('a * thm)) list
-  val weight_mepo_facts : 'a list -> ('a * real) list
-  val weight_mash_facts : 'a list -> ('a * real) list
+  val num_extra_feature_facts : int
+  val extra_feature_weight_factor : real
+  val weight_facts_smoothly : 'a list -> ('a * real) list
+  val weight_facts_steeply : 'a list -> ('a * real) list
   val find_mash_suggestions :
     Proof.context -> int -> string list -> ('b * thm) list -> ('b * thm) list
     -> ('b * thm) list -> ('b * thm) list * ('b * thm) list
@@ -903,23 +905,23 @@
 
 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
 
-(* FUDGE *)
-fun weight_of_mepo_fact rank =
-  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
-
-fun weight_mepo_facts facts =
-  facts ~~ map weight_of_mepo_fact (0 upto length facts - 1)
-
-val weight_raw_mash_facts = weight_mepo_facts
-val weight_mash_facts = weight_raw_mash_facts
+val num_extra_feature_facts = 10 (* FUDGE *)
+val extra_feature_weight_factor = 0.1
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =
   Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
 
-fun weight_proximity_facts facts =
+fun weight_facts_smoothly facts =
   facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
 
+(* FUDGE *)
+fun steep_weight_of_fact rank =
+  Math.pow (0.62, log2 (Real.fromInt (rank + 1)))
+
+fun weight_facts_steeply facts =
+  facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
+
 val max_proximity_facts = 100
 
 fun find_mash_suggestions _ _ [] _ _ raw_unknown = ([], raw_unknown)
@@ -933,8 +935,8 @@
               |> take max_proximity_facts
       val mess =
         [(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
-         (0.08 (* FUDGE *), (weight_raw_mash_facts raw_mash, raw_unknown)),
-         (0.02 (* FUDGE *), (weight_proximity_facts proximity, []))]
+         (0.08 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown)),
+         (0.02 (* FUDGE *), (weight_facts_smoothly proximity, []))]
       val unknown =
         raw_unknown
         |> fold (subtract (Thm.eq_thm_prop o pairself snd))
@@ -1289,11 +1291,11 @@
       fun mepo () =
         mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
                              facts
-        |> weight_mepo_facts
+        |> weight_facts_steeply
       fun mash () =
         mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
             hyp_ts concl_t facts
-        |>> weight_mash_facts
+        |>> weight_facts_steeply
       val mess =
         (* the order is important for the "case" expression below *)
         [] |> (if effective_fact_filter <> mepoN then