# HG changeset patch # User blanchet # Date 1368702352 -7200 # Node ID 78e7a007ba28a46c0e18f3297cc59efcdbe3f1f3 # Parent 97dd505ee058687cc3402e5c7dc53a36f6f2b214 reintroduced syntax for "nonexhaustive" datatypes diff -r 97dd505ee058 -r 78e7a007ba28 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu May 16 13:05:52 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu May 16 13:05:52 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 @@ -194,7 +194,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 @@ -601,8 +601,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 @@ -650,8 +651,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 = @@ -929,9 +930,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)) diff -r 97dd505ee058 -r 78e7a007ba28 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200 @@ -2546,20 +2546,21 @@ in if is_type_enc_polymorphic type_enc then [(native_ho_type_from_typ type_enc false 0 @{typ nat}, - map ho_term_from_term [@{term "0::nat"}, @{term Suc}]), + map ho_term_from_term [@{term "0::nat"}, @{term Suc}], true), (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}), - map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}])] + map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}], + true)] else [] end | 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) + ctrs, exhaust) end fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) @@ -2679,7 +2680,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