--- a/src/HOL/Tools/ATP/atp_problem.ML Fri May 06 13:34:59 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri May 06 13:34:59 2011 +0200
@@ -23,13 +23,11 @@
* 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 :
- formula_kind -> format -> string problem -> string list
+ val tptp_strings_for_atp_problem : format -> string problem -> string list
val nice_atp_problem :
bool -> ('a * (string * string) problem_line list) list
-> ('a * string problem_line list) list
@@ -49,8 +47,6 @@
AConn of connective * ('a, 'b, 'c) formula list |
AAtom of 'c
-fun mk_anot phi = AConn (ANot, [phi])
-
datatype format = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
@@ -114,35 +110,27 @@
val default_source =
ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
-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 hypothesis_kind format
+ | string_for_problem_line format
(Formula (ident, kind, phi, source, useful_info)) =
- let
- val (kind, phi) =
- if kind = Hypothesis then
- (hypothesis_kind, phi |> hypothesis_kind = Conjecture ? mk_anot)
- else
- (kind, phi)
- in
- (case format of Fof => "fof" | Tff => "tff") ^
- "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
- string_for_formula phi ^ ")" ^
- (case (source, useful_info) of
- (NONE, NONE) => ""
- | (SOME tm, NONE) => ", " ^ string_for_term tm
- | (_, SOME tm) =>
- ", " ^ string_for_term (source |> the_default default_source) ^
- ", " ^ string_for_term tm) ^ ").\n"
- end
-fun tptp_strings_for_atp_problem hypothesis_kind format problem =
+ (case format of Fof => "fof" | Tff => "tff") ^
+ "(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
+ string_for_formula phi ^ ")" ^
+ (case (source, useful_info) of
+ (NONE, NONE) => ""
+ | (SOME tm, NONE) => ", " ^ string_for_term tm
+ | (_, SOME tm) =>
+ ", " ^ string_for_term (source |> the_default default_source) ^
+ ", " ^ string_for_term tm) ^ ").\n"
+fun tptp_strings_for_atp_problem 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 hypothesis_kind format) lines)
+ map (string_for_problem_line format) lines)
problem
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))