1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 14 17:49:42 2011 +0100
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Dec 14 18:07:32 2011 +0100
1.3 @@ -2338,11 +2338,14 @@
1.4 symbols (with "$i" as the type of individuals), but some provers (e.g.,
1.5 SNARK) require explicit declarations. The situation is similar for THF. *)
1.6
1.7 -fun default_type pred_sym s =
1.8 +fun default_type type_enc pred_sym s =
1.9 let
1.10 val ind =
1.11 - if String.isPrefix type_const_prefix s then atype_of_types
1.12 - else individual_atype
1.13 + case type_enc of
1.14 + Simple_Types _ =>
1.15 + if String.isPrefix type_const_prefix s then atype_of_types
1.16 + else individual_atype
1.17 + | _ => individual_atype
1.18 fun typ 0 = if pred_sym then bool_atype else ind
1.19 | typ ary = AFun (ind, typ (ary - 1))
1.20 in typ end
1.21 @@ -2350,7 +2353,7 @@
1.22 fun nary_type_constr_type n =
1.23 funpow n (curry AFun atype_of_types) atype_of_types
1.24
1.25 -fun undeclared_syms_in_problem problem =
1.26 +fun undeclared_syms_in_problem type_enc problem =
1.27 let
1.28 val declared = declared_syms_in_problem problem
1.29 fun do_sym name ty =
1.30 @@ -2363,7 +2366,7 @@
1.31 | do_type (ATyAbs (_, ty)) = do_type ty
1.32 fun do_term pred_sym (ATerm (name as (s, _), tms)) =
1.33 is_tptp_user_symbol s
1.34 - ? do_sym name (fn _ => default_type pred_sym s (length tms))
1.35 + ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
1.36 #> fold (do_term false) tms
1.37 | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
1.38 fun do_formula (AQuant (_, xs, phi)) =
1.39 @@ -2377,11 +2380,11 @@
1.40 |> filter_out (is_built_in_tptp_symbol o fst o fst)
1.41 end
1.42
1.43 -fun declare_undeclared_syms_in_atp_problem problem =
1.44 +fun declare_undeclared_syms_in_atp_problem type_enc problem =
1.45 let
1.46 val decls =
1.47 problem
1.48 - |> undeclared_syms_in_problem
1.49 + |> undeclared_syms_in_problem type_enc
1.50 |> sort_wrt (fst o fst)
1.51 |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
1.52 in (implicit_declsN, decls) :: problem end
1.53 @@ -2464,7 +2467,7 @@
1.54 | FOF => I
1.55 | TFF (_, TPTP_Implicit) => I
1.56 | THF (_, TPTP_Implicit, _) => I
1.57 - | _ => declare_undeclared_syms_in_atp_problem)
1.58 + | _ => declare_undeclared_syms_in_atp_problem type_enc)
1.59 val (problem, pool) = problem |> nice_atp_problem readable_names
1.60 fun add_sym_ary (s, {min_ary, ...} : sym_info) =
1.61 min_ary > 0 ? Symtab.insert (op =) (s, min_ary)