# HG changeset patch
# User blanchet
# Date 1300357111 -3600
# Node ID 7f2793d51efcd709b4b6e753ed55d2da95f8f08e
# Parent  c1d560db15ec40237e87193e8941256be734782f
add option to function to keep trivial  ATP formulas, needed for some experiments

diff -r c1d560db15ec -r 7f2793d51efc src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 17 11:18:31 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Mar 17 11:18:31 2011 +0100
@@ -23,7 +23,7 @@
   val types_dangerous_types : type_system -> bool
   val num_atp_type_args : theory -> type_system -> string -> int
   val translate_atp_fact :
-    Proof.context -> (string * 'a) * thm
+    Proof.context -> bool -> (string * 'a) * thm
     -> translated_formula option * ((string * 'a) * thm)
   val prepare_atp_problem :
     Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
@@ -241,10 +241,12 @@
      ctypes_sorts = ctypes_sorts}
   end
 
-fun make_fact ctxt eq_as_iff presimp ((name, _), th) =
-  case make_formula ctxt eq_as_iff presimp name Axiom (prop_of th) of
-    {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
-  | formula => SOME formula
+fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), th) =
+  case (keep_trivial,
+        make_formula ctxt eq_as_iff presimp name Axiom (prop_of th)) of
+    (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
+    NONE
+  | (_, formula) => SOME formula
 fun make_conjecture ctxt ts =
   let val last = length ts - 1 in
     map2 (fn j => make_formula ctxt true true (string_of_int j)
@@ -276,7 +278,7 @@
     fun dub c needs_full_types (th, j) =
       ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
         false), th)
-    fun make_facts eq_as_iff = map_filter (make_fact ctxt eq_as_iff false)
+    fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false)
   in
     (metis_helpers
      |> filter (is_used o fst)
@@ -300,7 +302,8 @@
        [])
   end
 
-fun translate_atp_fact ctxt = `(make_fact ctxt true true)
+fun translate_atp_fact ctxt keep_trivial =
+  `(make_fact ctxt keep_trivial true true)
 
 fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   let
diff -r c1d560db15ec -r 7f2793d51efc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 17 11:18:31 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Mar 17 11:18:31 2011 +0100
@@ -308,7 +308,7 @@
   | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
 fun atp_translated_fact _ (ATP_Translated_Fact p) = p
   | atp_translated_fact ctxt fact =
-    translate_atp_fact ctxt (untranslated_fact fact)
+    translate_atp_fact ctxt false (untranslated_fact fact)
 fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
   | smt_weighted_fact thy num_facts (fact, j) =
     (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
diff -r c1d560db15ec -r 7f2793d51efc src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 17 11:18:31 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Mar 17 11:18:31 2011 +0100
@@ -246,7 +246,7 @@
         else
           launch_provers state
               (get_facts "ATP" no_dangerous_types atp_relevance_fudge o K atps)
-              (ATP_Translated_Fact oo K (translate_atp_fact ctxt o fst))
+              (ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
               (K (K NONE)) atps
       fun launch_smts accum =
         if null smts then