--- 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
@@ -18,6 +18,7 @@
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
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
type 'a problem = (string * 'a problem_line list) list
@@ -48,6 +49,7 @@
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
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
type 'a problem = (string * 'a problem_line list) list
@@ -98,22 +100,30 @@
exists formula_needs_typed_logic phis
| formula_needs_typed_logic (AAtom _) = false
-fun string_for_problem_line use_conjecture_for_hypotheses
+fun string_for_symbol_type [] res_ty = res_ty
+ | string_for_symbol_type [arg_ty] res_ty = arg_ty ^ " > " ^ res_ty
+ | string_for_symbol_type arg_tys res_ty =
+ string_for_symbol_type ["(" ^ space_implode " * " arg_tys ^ ")"] res_ty
+
+fun string_for_problem_line _ (Type_Decl (ident, sym, arg_tys, res_ty)) =
+ "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)) =
- let
- val (kind, phi) =
- if kind = Hypothesis andalso use_conjecture_for_hypotheses then
- (Conjecture, AConn (ANot, [phi]))
- else
- (kind, phi)
- in
- (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"
- end
+ let
+ val (kind, phi) =
+ if kind = Hypothesis andalso use_conjecture_for_hypotheses then
+ (Conjecture, AConn (ANot, [phi]))
+ else
+ (kind, phi)
+ in
+ (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"
+ end
fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
@@ -194,8 +204,13 @@
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Formula (ident, kind, phi, source)) =
- nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source))
+fun nice_problem_line (Type_Decl (ident, sym, arg_tys, res_ty)) =
+ nice_name sym
+ ##>> 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))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
pool_map nice_problem_line lines #>> pair heading) problem