--- a/src/HOL/Tools/ATP/atp_problem.ML Wed May 15 18:09:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed May 15 18:39:20 2013 +0200
@@ -51,7 +51,7 @@
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a ho_type |
Datatype_Decl of string * ('a * 'a list) list * 'a ho_type
- * ('a, 'a ho_type) ho_term list |
+ * ('a, 'a ho_type) ho_term list * bool |
Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
Formula of (string * string) * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -193,7 +193,7 @@
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a ho_type |
Datatype_Decl of string * ('a * 'a list) list * 'a ho_type
- * ('a, 'a ho_type) ho_term list |
+ * ('a, 'a ho_type) ho_term list * bool |
Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
Formula of (string * string) * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
@@ -591,12 +591,13 @@
in "predicate(" ^ commas (sym :: ty_vars @ map typ tys) ^ ")." end
fun bound_tvar (ty, []) = ty
| bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
- fun foo xs ty =
+ fun binder_typ xs ty =
(if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
typ ty
- fun sort_decl xs ty cl = "sort(" ^ foo xs ty ^ ", " ^ cl ^ ")."
- fun datatype_decl xs ty tms =
- "datatype(" ^ foo xs ty ^ ", " ^ commas (map term tms) ^ ")."
+ fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
+ fun datatype_decl xs ty tms exhaust =
+ "datatype(" ^ commas (binder_typ xs ty :: map term tms @
+ (if exhaust then [] else ["..."])) ^ ")."
fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
if pred kind then
@@ -644,8 +645,8 @@
else NONE
| _ => NONE) |> flat
val datatype_decls =
- filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms))
- |> flat
+ filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) =>
+ datatype_decl xs ty tms exhaust)) |> flat
val sort_decls =
filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
val subclass_decls =
@@ -923,9 +924,9 @@
| 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_line (Datatype_Decl (ident, xs, ty, tms, exhaust)) =
nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
- #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
+ #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
| nice_line (Class_Memb (ident, xs, ty, cl)) =
nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
#>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 15 18:09:20 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 15 18:39:20 2013 +0200
@@ -59,6 +59,7 @@
val class_decl_prefix : string
val type_decl_prefix : string
val sym_decl_prefix : string
+ val datatype_decl_prefix : string
val class_memb_prefix : string
val guards_sym_formula_prefix : string
val tags_sym_formula_prefix : string
@@ -229,7 +230,8 @@
val class_decl_prefix = "cl_"
val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
-val class_memb_prefix = "clmb_"
+val datatype_decl_prefix = "dt_"
+val class_memb_prefix = "cm_"
val guards_sym_formula_prefix = "gsy_"
val tags_sym_formula_prefix = "tsy_"
val uncurried_alias_eq_prefix = "unc_"
@@ -2180,6 +2182,7 @@
fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
+ (* ### FIXME: is the list of type variables exhaustive? *)
Class_Memb (class_memb_prefix ^ name,
map (fn (cls, T) =>
(T |> dest_TVar |> tvar_name, map (`make_class) cls))
@@ -2534,12 +2537,17 @@
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 _) =
+fun datatypes_of_facts ctxt (DFG Polymorphic) (type_enc as Native _) facts =
if is_type_enc_polymorphic type_enc then
- [Datatype_Decl ("nat", [], AType (("naT", @{type_name nat}), []), [])] (*###*)
+ [(@{typ nat}, [@{term "0::nat"}, @{term Suc}], true)]
else
[]
- | decl_lines_of_datatypes _ _ = []
+ | datatypes_of_facts _ _ _ _ = []
+
+fun decl_line_of_datatype (_, [], _) = NONE
+ | decl_line_of_datatype (T as Type (s, _), ctrs, exhaust) =
+ SOME (Datatype_Decl (datatype_decl_prefix ^ ascii_of s, [],
+ AType (("naT", @{type_name nat}), []), [], exhaust)) (*###*)
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2658,7 +2666,7 @@
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)) =
+ | 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 do_bound_tvars xs #> do_type ty #> do_class cl
@@ -2754,14 +2762,15 @@
val helpers =
sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
|> map (firstorderize true)
- val mono_Ts =
- helpers @ conjs @ facts |> monotonic_types_of_facts ctxt mono type_enc
+ val all_facts = helpers @ conjs @ facts
+ val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts
+ val datatypes = datatypes_of_facts ctxt format type_enc all_facts
val class_decl_lines = decl_lines_of_classes type_enc classes
val sym_decl_lines =
(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 datatype_decl_lines = map_filter decl_line_of_datatype datatypes
val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
val num_facts = length facts
val fact_lines =