# HG changeset patch
# User blanchet
# Date 1401703190 -7200
# Node ID f591096a9c941d1150e63e6d98ac171a89143e5c
# Parent  7524b440686c339a0be8ec8fc8c664cc20694115
add option to keep duplicates, for more precise evaluation of relevance filters

diff -r 7524b440686c -r f591096a9c94 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Mon Jun 02 11:59:49 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Mon Jun 02 11:59:50 2014 +0200
@@ -14,6 +14,7 @@
   [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
    lam_trans = lifting, timeout = 2, dont_preplay, minimize]
 
+declare [[sledgehammer_fact_duplicates = true]]
 declare [[sledgehammer_instantiate_inducts = false]]
 
 hide_fact (open) HOL.ext
diff -r 7524b440686c -r f591096a9c94 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Mon Jun 02 11:59:49 2014 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Mon Jun 02 11:59:50 2014 +0200
@@ -15,10 +15,8 @@
   val MeSh_IsarN : string
   val MeSh_ProverN : string
   val IsarN : string
-  val evaluate_mash_suggestions :
-    Proof.context -> params -> int * int option -> bool -> string list
-    -> string option -> string -> string -> string -> string -> string -> string
-    -> unit
+  val evaluate_mash_suggestions : Proof.context -> params -> int * int option -> bool ->
+    string list -> string option -> string -> string -> string -> string -> string -> string -> unit
 end;
 
 structure MaSh_Eval : MASH_EVAL =
diff -r 7524b440686c -r f591096a9c94 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Mon Jun 02 11:59:49 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Mon Jun 02 11:59:50 2014 +0200
@@ -263,7 +263,7 @@
 val generate_mepo_suggestions =
   generate_mepo_or_mash_suggestions
     (fn ctxt => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
-       Sledgehammer_Fact.drop_duplicate_facts
+       not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
        #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
 
 fun generate_mash_suggestions ctxt params =
diff -r 7524b440686c -r f591096a9c94 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jun 02 11:59:49 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Jun 02 11:59:50 2014 +0200
@@ -15,6 +15,7 @@
   type prover_result = Sledgehammer_Prover.prover_result
 
   val trace : bool Config.T
+  val duplicates : bool Config.T
   val MePoN : string
   val MaShN : string
   val MeShN : string
@@ -117,9 +118,12 @@
 open Sledgehammer_MePo
 
 val trace = Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
+val duplicates = Attrib.setup_config_bool @{binding sledgehammer_fact_duplicates} (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
+fun gen_eq_thm ctxt = if Config.get ctxt duplicates then Thm.eq_thm_strict else Thm.eq_thm_prop
+
 val MePoN = "MePo"
 val MaShN = "MaSh"
 val MeShN = "MeSh"
@@ -1264,7 +1268,7 @@
     val unknown = raw_unknown
       |> fold (subtract (eq_snd Thm.eq_thm_prop)) [unknown_chained, unknown_proximate]
   in
-    (mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess, unknown)
+    (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown)
   end
 
 fun add_const_counts t =
@@ -1633,9 +1637,7 @@
   if not (subset (op =) (the_list fact_filter, fact_filters)) then
     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   else if only then
-    let val facts = facts |> map fact_of_raw_fact in
-      [("", facts)]
-    end
+    [("", map fact_of_raw_fact facts)]
   else if max_facts <= 0 orelse null facts then
     [("", [])]
   else
@@ -1689,8 +1691,8 @@
       fun add_and_take accepts =
         (case add_ths of
            [] => accepts
-         | _ => (unique_facts |> filter in_add |> map fact_of_raw_fact) @
-                (accepts |> filter_out in_add))
+         | _ =>
+           (unique_facts |> filter in_add |> map fact_of_raw_fact) @ (accepts |> filter_out in_add))
         |> take max_facts
 
       fun mepo () =
@@ -1706,7 +1708,7 @@
         [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)
            |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo)
            |> Par_List.map (apsnd (fn f => f ()))
-      val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take
+      val mesh = mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess |> add_and_take
     in
       if the_mash_engine () = MaSh_Py andalso save then MaSh_Py.save ctxt overlord else ();
       (case (fact_filter, mess) of