--- 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