added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Apr 20 16:04:36 2010 +0200
@@ -15,6 +15,7 @@
      overlord: bool,
      atps: string list,
      full_types: bool,
+     explicit_apply: bool,
      respect_no_atp: bool,
      relevance_threshold: real,
      convergence: real,
@@ -69,6 +70,7 @@
    overlord: bool,
    atps: string list,
    full_types: bool,
+   explicit_apply: bool,
    respect_no_atp: bool,
    relevance_threshold: real,
    convergence: real,

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Tue Apr 20 16:04:36 2010 +0200
@@ -67,7 +67,7 @@
   | (failure :: _) => SOME failure
 
 fun generic_prover overlord get_facts prepare write_file cmd args failure_strs
-        proof_text name ({debug, full_types, ...} : params)
+        proof_text name ({debug, full_types, explicit_apply, ...} : params)
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -128,7 +128,7 @@
       if Config.get ctxt measure_runtime then split_time s else (s, 0)
     fun run_on probfile =
       if File.exists cmd then
-        write_file full_types probfile clauses
+        write_file full_types explicit_apply probfile clauses
         |> pair (apfst split_time' (bash_output (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd ^ ".");
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Apr 20 16:04:36 2010 +0200
@@ -34,10 +34,10 @@
   val get_helper_clauses : bool -> theory -> bool ->
        hol_clause list * (thm * (axiom_name * hol_clause_id)) list * string list ->
        hol_clause list
-  val write_tptp_file : bool -> bool -> Path.T ->
+  val write_tptp_file : bool -> bool -> bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list -> unit
-  val write_dfg_file : bool -> Path.T ->
+  val write_dfg_file : bool -> bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list -> unit
 end
@@ -50,19 +50,19 @@
 open Sledgehammer_Fact_Preprocessor
 
 (* Parameter "full_types" below indicates that full type information is to be
-exported *)
+   exported.
 
-(* If true, each function will be directly applied to as many arguments as
-   possible, avoiding use of the "apply" operator. Use of hBOOL is also
-   minimized. *)
-val minimize_applies = true;
+   If "explicit_apply" is false, each function will be directly applied to as
+   many arguments as possible, avoiding use of the "apply" operator. Use of
+   hBOOL is also minimized.
+*)
 
 fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
 
 (*True if the constant ever appears outside of the top-level position in literals.
   If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL const_needs_hBOOL c =
-  not minimize_applies orelse
+fun needs_hBOOL explicit_apply const_needs_hBOOL c =
+  explicit_apply orelse
     the_default false (Symtab.lookup const_needs_hBOOL c);
 
 
@@ -211,9 +211,10 @@
 
 val type_wrapper = "ti";
 
-fun head_needs_hBOOL const_needs_hBOOL (CombConst((c, _), _, _)) =
-    needs_hBOOL const_needs_hBOOL c
-  | head_needs_hBOOL _ _ = true;
+fun head_needs_hBOOL explicit_apply const_needs_hBOOL
+                     (CombConst ((c, _), _, _)) =
+    needs_hBOOL explicit_apply const_needs_hBOOL c
+  | head_needs_hBOOL _ _ _ = true
 
 fun wrap_type full_types (s, ty) pool =
   if full_types then
@@ -223,8 +224,11 @@
   else
     (s, pool)
 
-fun wrap_type_if full_types cnh (head, s, tp) =
-  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else pair s
+fun wrap_type_if full_types explicit_apply cnh (head, s, tp) =
+  if head_needs_hBOOL explicit_apply cnh head then
+    wrap_type full_types (s, tp)
+  else
+    pair s
 
 fun apply ss = "hAPP" ^ paren_pack ss;
 
@@ -252,18 +256,22 @@
   | string_of_application _ _ (CombVar (name, _), args) pool =
     nice_name name pool |>> (fn s => string_apply (s, args))
 
-fun string_of_combterm (params as (full_types, cma, cnh)) t pool =
+fun string_of_combterm (params as (full_types, explicit_apply, cma, cnh)) t
+                       pool =
   let
     val (head, args) = strip_combterm_comb t
     val (ss, pool) = pool_map (string_of_combterm params) args pool
     val (s, pool) = string_of_application full_types cma (head, ss) pool
-  in wrap_type_if full_types cnh (head, s, type_of_combterm t) pool end
+  in
+    wrap_type_if full_types explicit_apply cnh (head, s, type_of_combterm t)
+                 pool
+  end
 
 (*Boolean-valued terms are here converted to literals.*)
 fun boolify params c =
   string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
 
-fun string_of_predicate (params as (_, _, cnh)) t =
+fun string_of_predicate (params as (_, explicit_apply, _, cnh)) t =
   case t of
     (CombApp (CombApp (CombConst (("equal", _), _, _), t1), t2)) =>
     (* DFG only: new TPTP prefers infix equality *)
@@ -272,7 +280,8 @@
   | _ =>
     case #1 (strip_combterm_comb t) of
       CombConst ((s, _), _, _) =>
-      (if needs_hBOOL cnh s then boolify else string_of_combterm) params t
+      (if needs_hBOOL explicit_apply cnh s then boolify else string_of_combterm)
+          params t
     | _ => boolify params t
 
 
@@ -342,8 +351,8 @@
 
 fun add_types tvars = fold add_fol_type_funcs tvars
 
-fun add_decls (full_types, cma, cnh) (CombConst ((c, _), _, tvars))
-              (funcs, preds) =
+fun add_decls (full_types, explicit_apply, cma, cnh)
+              (CombConst ((c, _), _, tvars)) (funcs, preds) =
       if c = "equal" then
         (add_types tvars funcs, preds)
       else
@@ -351,8 +360,10 @@
             val ntys = if not full_types then length tvars else 0
             val addit = Symtab.update(c, arity+ntys)
         in
-            if needs_hBOOL cnh c then (add_types tvars (addit funcs), preds)
-            else (add_types tvars funcs, addit preds)
+            if needs_hBOOL explicit_apply cnh c then
+              (add_types tvars (addit funcs), preds)
+            else
+              (add_types tvars funcs, addit preds)
         end
   | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
       (add_fol_type_funcs ctp funcs, preds)
@@ -458,18 +469,23 @@
                            (const_min_arity, const_needs_hBOOL) =
   fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
 
-fun display_arity const_needs_hBOOL (c,n) =
+fun display_arity explicit_apply const_needs_hBOOL (c,n) =
   trace_msg (fn () => "Constant: " ^ c ^
                 " arity:\t" ^ Int.toString n ^
-                (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
+                (if needs_hBOOL explicit_apply const_needs_hBOOL c then
+                   " needs hBOOL"
+                 else
+                   ""))
 
-fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
-  if minimize_applies then
+fun count_constants explicit_apply
+                    (conjectures, _, extra_clauses, helper_clauses, _, _) =
+  if not explicit_apply then
      let val (const_min_arity, const_needs_hBOOL) =
           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
        |> fold count_constants_clause extra_clauses
        |> fold count_constants_clause helper_clauses
-     val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
+     val _ = List.app (display_arity explicit_apply const_needs_hBOOL)
+                      (Symtab.dest (const_min_arity))
      in (const_min_arity, const_needs_hBOOL) end
   else (Symtab.empty, Symtab.empty);
 
@@ -479,15 +495,15 @@
 
 (* TPTP format *)
 
-fun write_tptp_file readable_names full_types file clauses =
+fun write_tptp_file readable_names full_types explicit_apply file clauses =
   let
     fun section _ [] = []
       | section name ss = "\n% " ^ name ^ plural_s (length ss) ^ "\n" :: ss
     val pool = empty_name_pool readable_names
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses
-    val (cma, cnh) = count_constants clauses
-    val params = (full_types, cma, cnh)
+    val (cma, cnh) = count_constants explicit_apply clauses
+    val params = (full_types, explicit_apply, cma, cnh)
     val ((conjecture_clss, tfree_litss), pool) =
       pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
     val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])
@@ -511,7 +527,7 @@
 
 (* DFG format *)
 
-fun write_dfg_file full_types file clauses =
+fun write_dfg_file full_types explicit_apply file clauses =
   let
     (* Some of the helper functions below are not name-pool-aware. However,
        there's no point in adding name pool support if the DFG format is on its
@@ -519,8 +535,8 @@
     val pool = NONE
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses
-    val (cma, cnh) = count_constants clauses
-    val params = (full_types, cma, cnh)
+    val (cma, cnh) = count_constants explicit_apply clauses
+    val params = (full_types, explicit_apply, cma, cnh)
     val ((conjecture_clss, tfree_litss), pool) =
       pool_map (dfg_clause params) conjectures pool |>> ListPair.unzip
     and probname = Path.implode (Path.base file)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 20 14:39:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Apr 20 16:04:36 2010 +0200
@@ -41,6 +41,7 @@
   [("debug", "false"),
    ("verbose", "false"),
    ("overlord", "false"),
+   ("explicit_apply", "false"),
    ("respect_no_atp", "true"),
    ("relevance_threshold", "50"),
    ("convergence", "320"),
@@ -58,6 +59,7 @@
   [("no_debug", "debug"),
    ("quiet", "verbose"),
    ("no_overlord", "overlord"),
+   ("implicit_apply", "explicit_apply"),
    ("ignore_no_atp", "respect_no_atp"),
    ("partial_types", "full_types"),
    ("theory_irrelevant", "theory_relevant"),
@@ -146,6 +148,7 @@
     val overlord = lookup_bool "overlord"
     val atps = lookup_string "atps" |> space_explode " "
     val full_types = lookup_bool "full_types"
+    val explicit_apply = lookup_bool "explicit_apply"
     val respect_no_atp = lookup_bool "respect_no_atp"
     val relevance_threshold =
       0.01 * Real.fromInt (lookup_int "relevance_threshold")
@@ -160,11 +163,12 @@
     val minimize_timeout = lookup_time "minimize_timeout"
   in
     {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
-     full_types = full_types, respect_no_atp = respect_no_atp,
-     relevance_threshold = relevance_threshold, convergence = convergence,
-     theory_relevant = theory_relevant, higher_order = higher_order,
-     follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
-     sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
+     full_types = full_types, explicit_apply = explicit_apply,
+     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
+     convergence = convergence, theory_relevant = theory_relevant,
+     higher_order = higher_order, follow_defs = follow_defs,
+     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
+     timeout = timeout, minimize_timeout = minimize_timeout}
   end
 
 fun get_params thy = extract_params thy (default_raw_params thy)