--- 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,7 +18,7 @@
datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Type_Decl of string * 'a * 'a list * 'a |
+ Decl of string * 'a * 'a list * 'a |
Formula of logic * 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
@@ -49,7 +49,7 @@
datatype logic = Fof | Tff
datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
- Type_Decl of string * 'a * 'a list * 'a |
+ Decl of string * 'a * 'a list * 'a |
Formula of logic * 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
@@ -99,7 +99,7 @@
| 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)) =
+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
@@ -201,11 +201,11 @@
| 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 (Type_Decl (ident, sym, arg_tys, res_ty)) =
+fun nice_problem_line (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))
+ #>> (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_formula phi
#>> (fn phi => Formula (logic, ident, kind, phi, source, useful_info))
--- a/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Sun May 01 18:37:24 2011 +0200
@@ -237,6 +237,7 @@
fun parse_term x =
(scan_general_id
+ --| Scan.option ($$ ":" -- scan_general_id) (* ignore TFF types for now *)
-- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms)
--| $$ ")") []
--| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
--- 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
@@ -45,11 +45,12 @@
open Metis_Translate
open Sledgehammer_Util
+val type_decl_prefix = "type_"
+val sym_decl_prefix = "sym_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
-val type_decl_prefix = "type_"
-val class_rel_clause_prefix = "clrel_";
+val class_rel_clause_prefix = "crel_";
val arity_clause_prefix = "arity_"
val tfree_prefix = "tfree_"
@@ -61,6 +62,7 @@
fun make_type ty = type_prefix ^ ascii_of ty
(* official TPTP TFF syntax *)
+val tff_type_of_types = "$tType"
val tff_bool_type = "$o"
(* Freshness almost guaranteed! *)
@@ -778,14 +780,14 @@
| _ => ([], f ty))
| strip_and_map_combtyp f ty = ([], f ty)
-fun type_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
+fun sym_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
if type_sys = Many_Typed then
let
val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty
val (s, s') = (s, s') |> mangled_const_name ty_args
in
- Type_Decl (type_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
- if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
+ Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
+ if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
end
else
let
@@ -796,7 +798,7 @@
val bound_tms =
map (fn (name, ty) => CombConst (name, the ty, [])) bounds
in
- Formula (Fof, type_decl_prefix ^ ascii_of s, Axiom,
+ Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
CombConst ((s, s'), ty, ty_args)
|> fold (curry (CombApp o swap)) bound_tms
|> type_pred_combatom type_sys res_ty
@@ -804,13 +806,31 @@
|> formula_for_combformula ctxt type_sys,
NONE, NONE)
end
-fun type_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
- map (type_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
+fun sym_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
+ map (sym_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
+
+fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
+ union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
+ | add_tff_types_in_formula (AConn (_, phis)) =
+ fold add_tff_types_in_formula phis
+ | add_tff_types_in_formula (AAtom _) = I
-val type_declsN = "Type declarations"
+fun add_tff_types_in_problem_line (Decl (_, _, arg_tys, res_ty)) =
+ union (op =) (res_ty :: arg_tys)
+ | add_tff_types_in_problem_line (Formula (_, _, _, phi, _, _)) =
+ add_tff_types_in_formula phi
+
+fun tff_types_in_problem problem =
+ fold (fold add_tff_types_in_problem_line o snd) problem []
+
+fun problem_line_for_tff_type (s, s') =
+ Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
+
+val type_declsN = "Types"
+val sym_declsN = "Symbols"
val factsN = "Relevant facts"
val class_relsN = "Class relationships"
-val aritiesN = "Arity declarations"
+val aritiesN = "Arities"
val helpersN = "Helper facts"
val conjsN = "Conjectures"
val free_typesN = "Type variables"
@@ -832,6 +852,7 @@
Flotter hack. *)
val problem =
[(type_declsN, []),
+ (sym_declsN, []),
(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
(0 upto length facts - 1 ~~ facts)),
(class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
@@ -845,17 +866,24 @@
|> get_helper_facts ctxt type_sys
|>> map (hrepair_fact type_sys hrepairs)
val const_tab = const_table_for_facts type_sys hrepairs (conjs @ facts)
- val type_decl_lines =
- Symtab.fold_rev (append o type_decl_lines_for_const ctxt type_sys
- hrepairs)
+ val sym_decl_lines =
+ Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys hrepairs)
const_tab []
val helper_lines =
helper_facts
|>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys)
|> op @
- val (problem, pool) =
+ val problem =
problem |> fold (AList.update (op =))
- [(type_declsN, type_decl_lines), (helpersN, helper_lines)]
+ [(sym_declsN, sym_decl_lines),
+ (helpersN, helper_lines)]
+ val type_decl_lines =
+ if type_sys = Many_Typed then
+ problem |> tff_types_in_problem |> map problem_line_for_tff_type
+ else
+ []
+ val (problem, pool) =
+ problem |> AList.update (op =) (type_declsN, type_decl_lines)
|> nice_atp_problem readable_names
in
(problem,