--- a/src/HOL/Tools/ATP/atp_problem.ML Wed May 15 17:49:39 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed May 15 18:05:46 2013 +0200
@@ -784,8 +784,7 @@
(** Nice names **)
fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
-fun pool_map f xs =
- pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
+fun pool_map f xs = pool_fold (fn x => fn ys => f x #>> (fn y => y :: ys)) xs []
val no_qualifiers =
let
@@ -890,6 +889,10 @@
| DFG _ => avoid_clash_with_dfg_keywords
| _ => I
val nice_name = nice_name avoid_clash
+ fun nice_bound_tvars xs =
+ pool_map nice_name (map fst xs)
+ ##>> pool_map (pool_map nice_name) (map snd xs)
+ #>> op ~~
fun nice_type (AType (name, tys)) =
nice_name name ##>> pool_map nice_type tys #>> AType
| nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
@@ -923,12 +926,12 @@
| nice_line (Sym_Decl (ident, sym, ty)) =
nice_name sym ##>> nice_type ty
#>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
+ | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
+ nice_bound_tvars xs ##>> nice_type ty ##>> pool_map nice_term tms
+ #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
| nice_line (Class_Memb (ident, xs, ty, cl)) =
- pool_map nice_name (map fst xs)
- ##>> pool_map (pool_map nice_name) (map snd xs)
- ##>> nice_type ty ##>> nice_name cl
- #>> (fn (((tys, cls), ty), cl) =>
- Class_Memb (ident, tys ~~ cls, ty, cl))
+ nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
+ #>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
| nice_line (Formula (ident, kind, phi, source, info)) =
nice_formula phi
#>> (fn phi => Formula (ident, kind, phi, source, info))
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 15 17:49:39 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 15 18:05:46 2013 +0200
@@ -2534,6 +2534,13 @@
val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
in mono_lines @ decl_lines end
+fun decl_lines_of_datatypes (DFG Polymorphic) (type_enc as Native _) =
+ if is_type_enc_polymorphic type_enc then
+ [Datatype_Decl ("nat", [], AType (("naT", @{type_name nat}), []), [])] (*###*)
+ else
+ []
+ | decl_lines_of_datatypes _ _ = []
+
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
fun do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 sym_tab
@@ -2630,6 +2637,7 @@
fun do_sym (name as (s, _)) value =
if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
fun do_class name = apfst (apfst (do_sym name ()))
+ val do_bound_tvars = fold do_class o snd
fun do_type (AType (name, tys)) =
apfst (apsnd (do_sym name (length tys))) #> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
@@ -2650,8 +2658,10 @@
fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
| do_line (Type_Decl _) = I
| do_line (Sym_Decl (_, _, ty)) = do_type ty
+ | do_line (Datatype_Decl (_, xs, ty, tms)) =
+ fold do_bound_tvars xs #> do_type ty #> fold (do_term false) tms
| do_line (Class_Memb (_, xs, ty, cl)) =
- fold (fold do_class o snd) xs #> do_type ty #> do_class cl
+ fold do_bound_tvars xs #> do_type ty #> do_class cl
| do_line (Formula (_, _, phi, _, _)) = do_formula phi
val ((cls, tys), syms) = declared_in_atp_problem problem
in
@@ -2751,6 +2761,8 @@
(conjs, helpers @ facts, uncurried_alias_eq_tms)
|> sym_decl_table_of_facts thy type_enc sym_tab
|> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
+ val datatype_decl_lines = decl_lines_of_datatypes format type_enc
+ val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
val num_facts = length facts
val fact_lines =
map (line_of_fact ctxt fact_prefix ascii_of I (not exporter)
@@ -2766,7 +2778,7 @@
val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
(* Reordering these might confuse the proof reconstruction code. *)
val problem =
- [(explicit_declsN, class_decl_lines @ sym_decl_lines),
+ [(explicit_declsN, decl_lines),
(uncurried_alias_eqsN, uncurried_alias_eq_lines),
(factsN, fact_lines),
(subclassesN, subclass_lines),