--- a/src/HOL/Tools/ATP/atp_problem.ML Thu May 16 11:35:07 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 * bool |
+ * ('a, 'a ho_type) ho_term list |
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
@@ -125,6 +125,7 @@
-> 'e -> 'e
val formula_map :
('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
+ val strip_atype : 'a ho_type -> 'a list * ('a ho_type list * 'a ho_type)
val is_format_higher_order : atp_format -> bool
val tptp_string_of_line : atp_format -> string problem_line -> string
val lines_of_atp_problem :
@@ -193,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 * bool |
+ * ('a, 'a ho_type) ho_term list |
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
@@ -315,11 +316,16 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
-fun strip_atype (APi (tys, ty)) = strip_atype ty |>> apfst (append tys)
- | strip_atype (AFun (ty1, ty2)) = strip_atype ty2 |>> apsnd (cons ty1)
- | strip_atype ty = (([], []), ty)
+fun strip_api (APi (tys, ty)) = strip_api ty |>> append tys
+ | strip_api ty = ([], ty)
-fun is_function_atype ty = snd (strip_atype ty) <> AType (tptp_bool_type, [])
+fun strip_afun (AFun (ty1, ty2)) = strip_afun ty2 |>> cons ty1
+ | strip_afun ty = ([], ty)
+
+fun strip_atype ty = ty |> strip_api ||> strip_afun
+
+fun is_function_atype ty =
+ snd (snd (strip_atype ty)) <> AType (tptp_bool_type, [])
fun is_predicate_atype ty = not (is_function_atype ty)
fun is_nontrivial_predicate_atype (AType _) = false
| is_nontrivial_predicate_atype ty = is_predicate_atype ty
@@ -347,15 +353,15 @@
else
func ^ "(" ^ commas args ^ ")"
-fun flatten_type (APi (tys, ty)) = APi (tys, flatten_type ty)
- | flatten_type (ty as AFun (ty1 as AType _, ty2)) =
- (case flatten_type ty2 of
+fun uncurry_type (APi (tys, ty)) = APi (tys, uncurry_type ty)
+ | uncurry_type (ty as AFun (ty1 as AType _, ty2)) =
+ (case uncurry_type ty2 of
AFun (ty' as AType (s, tys), ty) =>
AFun (AType (tptp_product_type,
ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
| _ => ty)
- | flatten_type (ty as AType _) = ty
- | flatten_type _ =
+ | uncurry_type (ty as AType _) = ty
+ | uncurry_type _ =
raise Fail "unexpected higher-order type in first-order format"
val dfg_individual_type = "iii" (* cannot clash *)
@@ -390,7 +396,7 @@
in str true ty end
fun string_of_type (format as THF _) ty = str_of_type format ty
- | string_of_type format ty = str_of_type format (flatten_type ty)
+ | string_of_type format ty = str_of_type format (uncurry_type ty)
fun tptp_string_of_quantifier AForall = tptp_forall
| tptp_string_of_quantifier AExists = tptp_exists
@@ -585,9 +591,9 @@
fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ typ ty ^ ")."
fun pred_typ sym ty =
let
- val (ty_vars, tys) =
- strip_atype ty |> fst
- |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
+ val (ty_vars, (tys, _)) =
+ strip_atype ty
+ |>> (fn [] => [] | xs => ["[" ^ commas xs ^ "]"])
in "predicate(" ^ commas (sym :: ty_vars @ map typ tys) ^ ")." end
fun bound_tvar (ty, []) = ty
| bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
@@ -595,9 +601,8 @@
(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 exhaust =
- "datatype(" ^ commas (binder_typ xs ty :: map term tms @
- (if exhaust then [] else ["..."])) ^ ")."
+ fun datatype_decl xs ty tms =
+ "datatype(" ^ commas (binder_typ xs ty :: map term tms) ^ ")."
fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
if pred kind then
@@ -645,8 +650,8 @@
else NONE
| _ => NONE) |> flat
val datatype_decls =
- filt (try (fn Datatype_Decl (_, xs, ty, tms, exhaust) =>
- datatype_decl xs ty tms exhaust)) |> flat
+ filt (try (fn Datatype_Decl (_, xs, ty, tms) => datatype_decl xs ty tms))
+ |> flat
val sort_decls =
filt (try (fn Class_Memb (_, xs, ty, cl) => sort_decl xs ty cl)) |> flat
val subclass_decls =
@@ -924,9 +929,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, exhaust)) =
+ | nice_line (Datatype_Decl (ident, xs, ty, tms)) =
nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
- #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms, exhaust))
+ #>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
| 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 May 16 11:35:07 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200
@@ -426,7 +426,7 @@
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 100 (* arbitrary *)), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
val tvar_a = TVar tvar_a_z
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}
@@ -2539,17 +2539,32 @@
val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
in mono_lines @ decl_lines end
-fun datatypes_of_facts ctxt (DFG Polymorphic) (type_enc as Native _) facts =
- if is_type_enc_polymorphic type_enc then
- [(@{typ nat}, [@{term "0::nat"}, @{term Suc}], true)]
- else
- []
+fun datatypes_of_facts ctxt (DFG Polymorphic) (type_enc as Native (_, _, level))
+ facts =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val mono = default_mono level false
+ val ho_term_from_term =
+ iterm_from_term thy type_enc []
+ #> fst #> ho_term_from_iterm ctxt mono type_enc NONE
+ 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}]) (*,
+ (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}]) *)]
+ else
+ []
+ end
| 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 decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) =
+ let
+ val xs = map (fn AType (name, []) => name) ty_args
+ in
+ Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty,
+ ctrs)
+ end
fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
@@ -2668,7 +2683,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
@@ -2772,7 +2787,7 @@
(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 = map_filter decl_line_of_datatype datatypes
+ val datatype_decl_lines = map 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 =