--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Apr 24 21:00:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Apr 25 11:58:10 2014 +0200
@@ -50,7 +50,8 @@
Class_Decl of string * 'a * 'a list |
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a atp_type |
- Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
+ Datatype_Decl of
+ string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
Formula of (string * string) * atp_formula_role
* ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -194,7 +195,8 @@
Class_Decl of string * 'a * 'a list |
Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a atp_type |
- Datatype_Decl of string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list |
+ Datatype_Decl of
+ string * ('a * 'a list) list * 'a atp_type * ('a, 'a atp_type) atp_term list * bool |
Class_Memb of string * ('a * 'a list) list * 'a atp_type * 'a |
Formula of (string * string) * atp_formula_role
* ('a, 'a atp_type, ('a, 'a atp_type) atp_term, 'a) atp_formula
@@ -613,7 +615,9 @@
(if null xs then "" else "[" ^ commas (map bound_tvar xs) ^ "], ") ^
typ ty
fun sort_decl xs ty cl = "sort(" ^ binder_typ xs ty ^ ", " ^ cl ^ ")."
- fun datatype_decl xs ty tms = "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
+ 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
@@ -661,7 +665,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 =
@@ -938,9 +943,9 @@
nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
| 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 Thu Apr 24 21:00:00 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Apr 25 11:58:10 2014 +0200
@@ -2462,21 +2462,19 @@
fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
let val ctrs' = map do_ctr ctrs in
- if forall is_some ctrs' then
- SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
- else
- NONE
+ (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs',
+ forall is_some ctrs')
end
in
- map_filter datatype_of_ctrs ctrss
+ ctrss |> map datatype_of_ctrs |> filter_out (null o #2)
end
else
[]
| datatypes_of_sym_table _ _ _ _ _ _ = []
-fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs) =
+fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs, exhaust) =
let val xs = map (fn AType ((name, _), []) => name) ty_args in
- Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs)
+ Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs, exhaust)
end
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2589,7 +2587,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
| do_line (Formula (_, _, phi, _, _)) = do_formula phi