added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS

--- a/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun May 01 18:37:24 2011 +0200
@@ -20,7 +20,7 @@
   datatype 'a problem_line =
     Type_Decl of string * 'a * 'a list * 'a |
     Formula of string * formula_kind * ('a, 'a fo_term) formula
-               * string fo_term option
+               * string fo_term option * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
 
   val timestamp : unit -> string
@@ -51,7 +51,7 @@
 datatype 'a problem_line =
   Type_Decl of string * 'a * 'a list * 'a |
   Formula of string * formula_kind * ('a, 'a fo_term) formula
-             * string fo_term option
+             * string fo_term option * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
 
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
@@ -109,7 +109,7 @@
     "tff(" ^ ident ^ ", type, " ^ sym ^ " : " ^
     string_for_symbol_type arg_tys res_ty ^ ").\n"
   | string_for_problem_line use_conjecture_for_hypotheses
-                            (Formula (ident, kind, phi, source)) =
+                            (Formula (ident, kind, phi, source, useful_info)) =
     let
       val (kind, phi) =
         if kind = Hypothesis andalso use_conjecture_for_hypotheses then
@@ -120,9 +120,12 @@
       (if formula_needs_typed_logic phi then "tff" else "fof") ^
       "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
       string_for_formula phi ^ ")" ^
-      (case source of
-         SOME tm => ", " ^ string_for_term tm
-       | NONE => "") ^ ").\n"
+      (case (source, useful_info) of
+         (NONE, NONE) => ""
+       | (SOME tm, NONE) => ", " ^ string_for_term tm
+       | (_, SOME tm) =>
+         ", " ^ string_for_term (source |> the_default (ATerm ("[]", []))) ^
+         ", " ^ string_for_term tm) ^ ").\n"
     end
 fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
@@ -209,8 +212,9 @@
     ##>> pool_map nice_name arg_tys
     ##>> nice_name res_ty
     #>> (fn ((sym, arg_tys), res_ty) => Type_Decl (ident, sym, arg_tys, res_ty))
-  | nice_problem_line (Formula (ident, kind, phi, source)) =
-    nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
+  | nice_problem_line (Formula (ident, kind, phi, source, useful_info)) =
+    nice_formula phi
+    #>> (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/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -318,7 +318,7 @@
          [Formula (helper_prefix ^ ascii_of "ti_ti", Axiom,
                    AAtom (ATerm (`I "equal",
                                  [tag (tag (var "Y")), tag (var "Y")]))
-                   |> close_formula_universally, NONE)]
+                   |> close_formula_universally, NONE, NONE)]
        end
      else
        [])
@@ -509,14 +509,15 @@
 fun problem_line_for_fact ctxt prefix type_sys
                           (j, formula as {name, kind, ...}) =
   Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name,
-           kind, formula_for_fact ctxt type_sys formula, NONE)
+           kind, formula_for_fact ctxt type_sys formula, NONE, NONE)
 
 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
                                                        superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
-                               AAtom (ATerm (superclass, [ty_arg]))]), NONE)
+                               AAtom (ATerm (superclass, [ty_arg]))]),
+             NONE, NONE)
   end
 
 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
@@ -530,14 +531,14 @@
            mk_ahorn (map (formula_for_fo_literal o apfst not
                           o fo_literal_for_arity_literal) premLits)
                     (formula_for_fo_literal
-                         (fo_literal_for_arity_literal conclLit)), NONE)
+                         (fo_literal_for_arity_literal conclLit)), NONE, NONE)
 
 fun problem_line_for_conjecture ctxt type_sys
         ({name, kind, combformula, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
            formula_for_combformula ctxt type_sys
                                    (close_combformula_universally combformula),
-           NONE)
+           NONE, NONE)
 
 fun free_type_literals type_sys ({ctypes_sorts, ...} : translated_formula) =
   ctypes_sorts |> atp_type_literals_for_types type_sys Conjecture
@@ -545,7 +546,7 @@
 
 fun problem_line_for_free_type j lit =
   Formula (tfree_prefix ^ string_of_int j, Hypothesis,
-           formula_for_fo_literal lit, NONE)
+           formula_for_fo_literal lit, NONE, NONE)
 fun problem_lines_for_free_types type_sys facts =
   let
     val litss = map (free_type_literals type_sys) facts
@@ -574,7 +575,7 @@
   | consider_formula (AAtom tm) = consider_term true tm
 
 fun consider_problem_line (Type_Decl _) = I
-  | consider_problem_line (Formula (_, _, phi, _)) = consider_formula phi
+  | consider_problem_line (Formula (_, _, phi, _, _)) = consider_formula phi
 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
 
 (* needed for helper facts if the problem otherwise does not involve equality *)
@@ -667,8 +668,9 @@
   in aux #> close_formula_universally end
 
 fun repair_problem_line thy type_sys sym_tab
-                        (Formula (ident, kind, phi, source)) =
-    Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source)
+                        (Formula (ident, kind, phi, source, useful_info)) =
+    Formula (ident, kind, repair_formula thy type_sys sym_tab phi, source,
+             useful_info)
   | repair_problem_line _ _ _ _ = raise Fail "unexpected non-formula"
 fun repair_problem thy = map o apsnd o map oo repair_problem_line thy
 
@@ -703,7 +705,7 @@
     val sym_tab = sym_table_for_problem explicit_apply problem
     val problem = problem |> repair_problem thy type_sys sym_tab
     val helper_facts =
-      problem |> maps (map_filter (fn Formula (_, _, phi, _) => SOME phi
+      problem |> maps (map_filter (fn Formula (_, _, phi, _, _) => SOME phi
                                     | _ => NONE) o snd)
               |> get_helper_facts ctxt type_sys
     val helper_lines =
@@ -731,7 +733,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, _, _)) =
     fold_formula (add_term_weights weight) phi
   | add_problem_line_weights _ _ = I