refined experimental option of Sledgehammer

--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Mar 26 18:51:58 2016 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -185,7 +185,7 @@
     val thy = Proof_Context.theory_of ctxt
     val assm_ths0 = map (Skip_Proof.make_thm thy) assms
     val ((assm_name, _), ctxt) = ctxt
-      |> Config.put Sledgehammer_Prover_ATP.atp_completish (completeness > 0)
+      |> Config.put Sledgehammer_Prover_ATP.atp_completish (if completeness > 0 then 2 else 0)
       |> Local_Theory.note ((@{binding thms}, []), assm_ths0)
 
     fun ref_of th = (Facts.named (Thm.derivation_name th), [])

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 26 18:51:58 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -15,7 +15,7 @@
   type atp_formula_role = ATP_Problem.atp_formula_role
   type 'a atp_problem = 'a ATP_Problem.atp_problem
 
-  datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
+  datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator
 
   datatype scope = Global | Local | Assum | Chained
   datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
@@ -126,7 +126,7 @@
 open ATP_Util
 open ATP_Problem
 
-datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter | Translator
+datatype mode = Metis | Sledgehammer | Sledgehammer_Completish of int | Exporter | Translator
 
 datatype scope = Global | Local | Assum | Chained
 datatype status = General | Induction | Intro | Inductive | Elim | Simp | Non_Rec_Def | Rec_Def
@@ -1530,7 +1530,7 @@
 val predicator_iconst = IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
 
 fun predicatify completish tm =
-  if completish then
+  if completish > 0 then
     IApp (IApp (IConst (`I tptp_equal, @{typ "bool => bool => bool"}, []), tm), fTrue_iconst)
   else
     IApp (predicator_iconst, tm)
@@ -1734,14 +1734,14 @@
       fold (fn ((helper_s, needs_sound), ths) =>
                if (needs_sound andalso not sound) orelse
                   (helper_s <> unmangled_s andalso
-                   (not completish orelse could_specialize)) then
+                   (completish < 2 orelse could_specialize)) then
                  I
                else
                  ths ~~ (1 upto length ths)
                  |> maps (dub_and_inst needs_sound o apfst (apsnd Thm.prop_of))
                  |> make_facts
                  |> union (op = o apply2 #iformula))
-           (if completish then completish_helper_table else helper_table)
+           (if completish >= 2 then completish_helper_table else helper_table)
     end
   | NONE => I)
 fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
@@ -2169,7 +2169,7 @@
 fun default_mono level completish =
   {maybe_finite_Ts = [@{typ bool}],
    surely_infinite_Ts = (case level of Nonmono_Types (Strict, _) => [] | _ => known_infinite_types),
-   maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
+   maybe_nonmono_Ts = [if completish >= 2 then tvar_a else @{typ bool}]}
 
 (* This inference is described in section 4 of Blanchette et al., "Encoding
    monomorphic and polymorphic types", TACAS 2013. *)
@@ -2572,13 +2572,13 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
-    val completish = (mode = Sledgehammer_Completish)
+    val completish = (case mode of Sledgehammer_Completish k => k | _ => 0)
     (* Forcing explicit applications is expensive for polymorphic encodings,
        because it takes only one existential variable ranging over "'a => 'b" to
        ruin everything. Hence we do it only if there are few facts (which is
        normally the case for "metis" and the minimizer). *)
     val app_op_level =
-      if completish then
+      if completish > 0 then
         Full_App_Op_And_Predicator
       else if length facts + length hyp_ts >= app_op_and_predicator_threshold then
         if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Mar 26 18:51:58 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Mar 28 12:05:47 2016 +0200
@@ -13,7 +13,7 @@
 
   val atp_dest_dir : string Config.T
   val atp_problem_prefix : string Config.T
-  val atp_completish : bool Config.T
+  val atp_completish : int Config.T
   val atp_full_names : bool Config.T
 
   val is_ho_atp : Proof.context -> string -> bool
@@ -41,7 +41,7 @@
 val atp_dest_dir = Attrib.setup_config_string @{binding sledgehammer_atp_dest_dir} (K "")
 val atp_problem_prefix =
   Attrib.setup_config_string @{binding sledgehammer_atp_problem_prefix} (K "prob")
-val atp_completish = Attrib.setup_config_bool @{binding sledgehammer_atp_completish} (K false)
+val atp_completish = Attrib.setup_config_int @{binding sledgehammer_atp_completish} (K 0)
 (* In addition to being easier to read, readable names are often much shorter, especially if types
    are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short
    names are enabled by default. *)
@@ -146,7 +146,8 @@
     val waldmeister_new = (local_name = waldmeister_newN)
     val spassy = (local_name = pirateN orelse local_name = spassN)
 
-    val atp_mode = if Config.get ctxt atp_completish then Sledgehammer_Completish else Sledgehammer
+    val completish = Config.get ctxt atp_completish
+    val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_of_prover name