made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support

--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:25 2011 +0200
@@ -15,20 +15,21 @@
     AConn of connective * ('a, 'b, 'c) formula list |
     AAtom of 'c
 
-  datatype logic = Fof | Tff
+  datatype format = Fof | Tff
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
     Decl of string * 'a * 'a list * 'a |
-    Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
+    Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
                * string fo_term option * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
 
+  val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
   val timestamp : unit -> string
   val hashw : word * word -> word
   val hashw_string : string * word -> word
   val is_atp_variable : string -> bool
   val tptp_strings_for_atp_problem :
-    bool -> (string * string problem_line list) list -> string list
+    formula_kind -> format -> string problem -> string list
   val nice_atp_problem :
     bool -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
@@ -48,11 +49,13 @@
   AConn of connective * ('a, 'b, 'c) formula list |
   AAtom of 'c
 
-datatype logic = Fof | Tff
+fun mk_anot phi = AConn (ANot, [phi])
+
+datatype format = Fof | Tff
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
   Decl of string * 'a * 'a list * 'a |
-  Formula of logic * string * formula_kind * ('a, 'a, 'a fo_term) formula
+  Formula of string * formula_kind * ('a, 'a, 'a fo_term) formula
              * string fo_term option * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
 
@@ -108,19 +111,19 @@
   | string_for_symbol_type arg_tys res_ty =
     string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
 
-fun string_for_problem_line _ (Decl (ident, sym, arg_tys, res_ty)) =
+fun string_for_problem_line _ _ (Decl (ident, sym, arg_tys, res_ty)) =
     "tff(" ^ ident ^ ", type,\n    " ^ sym ^ " : " ^
     string_for_symbol_type arg_tys res_ty ^ ").\n"
-  | string_for_problem_line use_conjecture_for_hypotheses
-        (Formula (logic, ident, kind, phi, source, useful_info)) =
+  | string_for_problem_line hypothesis_kind format
+                            (Formula (ident, kind, phi, source, useful_info)) =
     let
       val (kind, phi) =
-        if kind = Hypothesis andalso use_conjecture_for_hypotheses then
-          (Conjecture, AConn (ANot, [phi]))
+        if kind = Hypothesis then
+          (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot)
         else
           (kind, phi)
     in
-      (case logic of Fof => "fof" | Tff => "tff") ^
+      (case format of Fof => "fof" | Tff => "tff") ^
       "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
       string_for_formula phi ^ ")" ^
       (case (source, useful_info) of
@@ -130,13 +133,13 @@
          ", " ^ string_for_term (source |> the_default (ATerm ("[]", []))) ^
          ", " ^ string_for_term tm) ^ ").\n"
     end
-fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
+fun tptp_strings_for_atp_problem hypothesis_kind format problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   \% " ^ timestamp () ^ "\n" ::
   maps (fn (_, []) => []
          | (heading, lines) =>
            "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
-           map (string_for_problem_line use_conjecture_for_hypotheses) lines)
+           map (string_for_problem_line hypothesis_kind format) lines)
        problem
 
 fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
@@ -221,9 +224,9 @@
     ##>> pool_map nice_name arg_tys
     ##>> nice_name res_ty
     #>> (fn ((sym, arg_tys), res_ty) => Decl (ident, sym, arg_tys, res_ty))
-  | nice_problem_line (Formula (logic, ident, kind, phi, source, useful_info)) =
+  | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) =
     nice_formula phi
-    #>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))
+    #>> (fn phi => Formula (ident, kind, phi, source, useful_info))
 fun nice_problem problem =
   pool_map (fn (heading, lines) =>
                pool_map nice_problem_line lines #>> pair heading) problem

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 01 18:37:25 2011 +0200
@@ -7,6 +7,8 @@
 
 signature ATP_SYSTEMS =
 sig
+  type format = ATP_Problem.format
+  type formula_kind = ATP_Problem.formula_kind
   type failure = ATP_Proof.failure
 
   type atp_config =
@@ -16,7 +18,8 @@
      slices: unit -> (real * (bool * int)) list,
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
-     use_conjecture_for_hypotheses: bool}
+     hypothesis_kind: formula_kind,
+     formats: format list}
 
   datatype e_weight_method =
     E_Slices | E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
@@ -40,7 +43,8 @@
   val remote_prefix : string
   val remote_atp :
     string -> string -> string list -> (string * string) list
-    -> (failure * string) list -> (unit -> int) -> bool -> string * atp_config
+    -> (failure * string) list -> (unit -> int) -> formula_kind -> format list
+    -> string * atp_config
   val add_atp : string * atp_config -> theory -> theory
   val get_atp : theory -> string -> atp_config
   val supported_atps : theory -> string list
@@ -52,6 +56,7 @@
 structure ATP_Systems : ATP_SYSTEMS =
 struct
 
+open ATP_Problem
 open ATP_Proof
 
 (* ATP configuration *)
@@ -63,7 +68,8 @@
    slices: unit -> (real * (bool * int)) list,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
-   use_conjecture_for_hypotheses: bool}
+   hypothesis_kind: formula_kind,
+   formats: format list}
 
 val known_perl_failures =
   [(CantConnect, "HTTP error"),
@@ -188,7 +194,8 @@
        "# Cannot determine problem status within resource limit"),
       (OutOfResources, "SZS status: ResourceOut"),
       (OutOfResources, "SZS status ResourceOut")],
-   use_conjecture_for_hypotheses = true}
+   hypothesis_kind = Conjecture,
+   formats = [Fof]}
 
 val e = (eN, e_config)
 
@@ -216,7 +223,8 @@
       (MalformedInput, "Free Variable"),
       (SpassTooOld, "tptp2dfg"),
       (InternalError, "Please report this error")],
-   use_conjecture_for_hypotheses = true}
+   hypothesis_kind = Conjecture,
+   formats = [Fof]}
 
 val spass = (spassN, spass_config)
 
@@ -249,7 +257,8 @@
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
       (Interrupted, "Aborted by signal SIGINT")],
-   use_conjecture_for_hypotheses = true}
+   hypothesis_kind = Conjecture,
+   formats = [Fof]}
 
 val vampire = (vampireN, vampire_config)
 
@@ -269,7 +278,8 @@
       (IncompleteUnprovable, "SZS status Satisfiable"),
       (ProofMissing, "\nunsat"),
       (ProofMissing, "SZS status Unsatisfiable")],
-   use_conjecture_for_hypotheses = false}
+   hypothesis_kind = Hypothesis,
+   formats = [Fof]}
 
 val z3_atp = (z3_atpN, z3_atp_config)
 
@@ -307,8 +317,7 @@
 val max_remote_secs = 240 (* give Geoff Sutcliffe's servers a break *)
 
 fun remote_config system_name system_versions proof_delims known_failures
-                  default_max_relevant use_conjecture_for_hypotheses
-                  : atp_config =
+                  default_max_relevant hypothesis_kind formats : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn timeout => fn _ =>
@@ -320,21 +329,22 @@
      known_failures @ known_perl_failures @
      [(IncompleteUnprovable, "says Unknown"),
       (TimedOut, "says Timeout")],
-   use_conjecture_for_hypotheses = use_conjecture_for_hypotheses}
+   hypothesis_kind = hypothesis_kind,
+   formats = formats}
 
 fun int_average f xs = fold (Integer.add o f) xs 0 div length xs
 
 fun remotify_config system_name system_versions
-        ({proof_delims, slices, known_failures, use_conjecture_for_hypotheses,
-          ...} : atp_config) : atp_config =
+                    ({proof_delims, slices, known_failures, hypothesis_kind,
+                      formats, ...} : atp_config) : atp_config =
   remote_config system_name system_versions proof_delims known_failures
-                (int_average (snd o snd) o slices) use_conjecture_for_hypotheses
+                (int_average (snd o snd) o slices) hypothesis_kind formats
 
 fun remote_atp name system_name system_versions proof_delims known_failures
-               default_max_relevant use_conjecture_for_hypotheses =
+               default_max_relevant hypothesis_kind formats =
   (remote_prefix ^ name,
    remote_config system_name system_versions proof_delims known_failures
-                 default_max_relevant use_conjecture_for_hypotheses)
+                 default_max_relevant hypothesis_kind formats)
 fun remotify_atp (name, config) system_name system_versions =
   (remote_prefix ^ name, remotify_config system_name system_versions config)
 
@@ -343,12 +353,13 @@
 val remote_z3_atp = remotify_atp z3_atp "Z3" ["2.18"]
 val remote_tofof_e =
   remote_atp tofof_eN "ToFoF" ["0.1"] [] (#known_failures e_config)
-             (K 200 (* FUDGE *)) true
+             (K 200 (* FUDGE *)) Conjecture [Tff]
 val remote_sine_e =
-  remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) true
+  remote_atp sine_eN "SInE" ["0.4"] [] [] (K 500 (* FUDGE *)) Conjecture [Fof]
 val remote_snark =
   remote_atp snarkN "SNARK" ["20080805r024"]
-             [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *)) true
+             [("refutation.", "end_refutation.")] [] (K 250 (* FUDGE *))
+             Conjecture [Tff, Fof]
 
 (* Setup *)
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:25 2011 +0200
@@ -156,7 +156,6 @@
        |> filter (fn TyLitVar _ => kind <> Conjecture
                    | TyLitFree _ => kind = Conjecture)
 
-fun mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
 fun mk_aconns c phis =
   let val (phis', phi') = split_last phis in
@@ -532,7 +531,7 @@
     fun var s = ATerm (`I s, [])
     fun tag tm = ATerm (`I type_tag_name, [var "X", tm])
   in
-    Formula (Fof, helper_prefix ^ ascii_of "ti_ti", Axiom,
+    Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
              AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
              |> close_formula_universally, NONE, NONE)
   end
@@ -690,22 +689,18 @@
                 (close_combformula_universally combformula))
   |> close_formula_universally
 
-fun logic_for_type_sys Many_Typed = Tff
-  | logic_for_type_sys _ = Fof
-
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
 fun formula_line_for_fact ctxt prefix type_sys
                           (j, formula as {name, kind, ...}) =
-  Formula (logic_for_type_sys type_sys,
-           prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
+  Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
            formula_for_fact ctxt type_sys formula, NONE, NONE)
 
 fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
                                                        superclass, ...}) =
   let val ty_arg = ATerm (`I "T", []) in
-    Formula (Fof, class_rel_clause_prefix ^ ascii_of name, Axiom,
+    Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
                                AAtom (ATerm (superclass, [ty_arg]))])
              |> close_formula_universally, NONE, NONE)
@@ -718,7 +713,7 @@
 
 fun formula_line_for_arity_clause (ArityClause {name, conclLit, premLits,
                                                 ...}) =
-  Formula (Fof, arity_clause_prefix ^ ascii_of name, Axiom,
+  Formula (arity_clause_prefix ^ ascii_of name, Axiom,
            mk_ahorn (map (formula_from_fo_literal o apfst not
                           o fo_literal_from_arity_literal) premLits)
                     (formula_from_fo_literal
@@ -727,7 +722,7 @@
 
 fun formula_line_for_conjecture ctxt type_sys
         ({name, kind, combformula, ...} : translated_formula) =
-  Formula (logic_for_type_sys type_sys, conjecture_prefix ^ name, kind,
+  Formula (conjecture_prefix ^ name, kind,
            formula_from_combformula ctxt type_sys
                                     (close_combformula_universally combformula)
            |> close_formula_universally, NONE, NONE)
@@ -737,7 +732,7 @@
                |> map fo_literal_from_type_literal
 
 fun formula_line_for_free_type j lit =
-  Formula (Fof, tfree_prefix ^ string_of_int j, Hypothesis,
+  Formula (tfree_prefix ^ string_of_int j, Hypothesis,
            formula_from_fo_literal lit, NONE, NONE)
 fun formula_lines_for_free_types type_sys facts =
   let
@@ -803,7 +798,7 @@
       val freshener =
         case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
     in
-      Formula (Fof, sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
+      Formula (sym_decl_prefix ^ freshener ^ "_" ^ ascii_of s, Axiom,
                CombConst ((s, s'), T, T_args)
                |> fold (curry (CombApp o swap)) bound_tms
                |> type_pred_combatom type_sys res_T
@@ -837,7 +832,7 @@
 
 fun add_tff_types_in_problem_line (Decl (_, _, arg_Ts, res_T)) =
     union (op =) (res_T :: arg_Ts)
-  | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
+  | add_tff_types_in_problem_line (Formula (_, _, phi, _, _)) =
     add_tff_types_in_formula phi
 
 fun tff_types_in_problem problem =
@@ -914,7 +909,7 @@
 fun add_term_weights weight (ATerm (s, tms)) =
   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
-fun add_problem_line_weights weight (Formula (_, _, _, phi, _, _)) =
+fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
     formula_fold (add_term_weights weight) phi
   | add_problem_line_weights _ _ = I
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
@@ -340,7 +340,7 @@
 
 fun run_atp auto name
         ({exec, required_execs, arguments, slices, proof_delims, known_failures,
-          use_conjecture_for_hypotheses, ...} : atp_config)
+          hypothesis_kind, ...} : atp_config)
         ({debug, verbose, overlord, type_sys, max_relevant, monomorphize,
           monomorphize_limit, explicit_apply, isar_proof, isar_shrink_factor,
           slicing, timeout, ...} : params)
@@ -348,6 +348,7 @@
   let
     val thy = Proof.theory_of state
     val ctxt = Proof.context_of state
+    val format = if type_sys = Many_Typed then Tff else Fof
     val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
     val (dest_dir, problem_prefix) =
       if overlord then overlord_file_location_for_prover name
@@ -452,7 +453,7 @@
                      "exec " ^ core) ^ " 2>&1"
                 val _ =
                   atp_problem
-                  |> tptp_strings_for_atp_problem use_conjecture_for_hypotheses
+                  |> tptp_strings_for_atp_problem hypothesis_kind format
                   |> cons ("% " ^ command ^ "\n")
                   |> File.write_list prob_file
                 val conjecture_shape =