# HG changeset patch # User blanchet # Date 1368635960 -7200 # Node ID 6f3cab60621faba97c10d8db5d466723510966cd # Parent eb3571cf938707ac64a47be2fac376aa040e22f8 more work on SPASS datatypes diff -r eb3571cf9387 -r 6f3cab60621f src/HOL/Tools/ATP/atp_problem.ML --- 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)) diff -r eb3571cf9387 -r 6f3cab60621f src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 =