# HG changeset patch # User blanchet # Date 1323784542 -3600 # Node ID 3b8606fba2ddb235da4be2a76bac81952a304fcd # Parent 67110d6c66dee6279c7328824015ee7d661dd797 correctly declare implicit TFF1 types that appear first as type arguments with "$tType" and not "$i diff -r 67110d6c66de -r 3b8606fba2dd src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Dec 13 14:04:20 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Dec 13 14:55:42 2011 +0100 @@ -107,8 +107,7 @@ (string * string) problem -> (string * string) problem val filter_cnf_ueq_problem : (string * string) problem -> (string * string) problem - val declare_undeclared_syms_in_atp_problem : - string -> string -> (string * string) problem -> (string * string) problem + val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list val nice_atp_problem : bool -> ('a * (string * string) problem_line list) list -> ('a * string problem_line list) list @@ -613,59 +612,11 @@ (** Symbol declarations **) -(* TFF allows implicit declarations of types, function symbols, and predicate - symbols (with "$i" as the type of individuals), but some provers (e.g., - SNARK) require explicit declarations. The situation is similar for THF. *) -fun default_type pred_sym = - let - fun typ 0 = if pred_sym then bool_atype else individual_atype - | typ ary = AFun (individual_atype, typ (ary - 1)) - in typ end - fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym | add_declared_syms_in_problem_line _ = I fun declared_syms_in_problem problem = fold (fold add_declared_syms_in_problem_line o snd) problem [] -fun nary_type_constr_type n = - funpow n (curry AFun atype_of_types) atype_of_types - -fun undeclared_syms_in_problem declared problem = - let - fun do_sym name ty = - if member (op =) declared name then I else AList.default (op =) (name, ty) - fun do_type (AType (name as (s, _), tys)) = - is_tptp_user_symbol s - ? do_sym name (fn _ => nary_type_constr_type (length tys)) - #> fold do_type tys - | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 - | do_type (ATyAbs (_, ty)) = do_type ty - fun do_term pred_sym (ATerm (name as (s, _), tms)) = - is_tptp_user_symbol s - ? do_sym name (fn _ => default_type pred_sym (length tms)) - #> fold (do_term false) tms - | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm - fun do_formula (AQuant (_, xs, phi)) = - fold do_type (map_filter snd xs) #> do_formula phi - | do_formula (AConn (_, phis)) = fold do_formula phis - | do_formula (AAtom tm) = do_term true tm - fun do_problem_line (Decl (_, _, ty)) = do_type ty - | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi - in - fold (fold do_problem_line o snd) problem [] - |> filter_out (is_built_in_tptp_symbol o fst o fst) - end - -fun declare_undeclared_syms_in_atp_problem prefix heading problem = - let - fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ()) - val declared = problem |> declared_syms_in_problem - val decls = - problem |> undeclared_syms_in_problem declared - |> sort_wrt (fst o fst) - |> map decl_line - in (heading, decls) :: problem end - (** Nice names **) fun empty_name_pool readable_names = diff -r 67110d6c66de -r 3b8606fba2dd src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Dec 13 14:04:20 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Dec 13 14:55:42 2011 +0100 @@ -2333,6 +2333,58 @@ val conjsN = "Conjectures" val free_typesN = "Type variables" +(* TFF allows implicit declarations of types, function symbols, and predicate + symbols (with "$i" as the type of individuals), but some provers (e.g., + SNARK) require explicit declarations. The situation is similar for THF. *) + +fun default_type pred_sym s = + let + val ind = + if String.isPrefix type_const_prefix s then atype_of_types + else individual_atype + fun typ 0 = if pred_sym then bool_atype else ind + | typ ary = AFun (ind, typ (ary - 1)) + in typ end + +fun nary_type_constr_type n = + funpow n (curry AFun atype_of_types) atype_of_types + +fun undeclared_syms_in_problem problem = + let + val declared = declared_syms_in_problem problem + fun do_sym name ty = + if member (op =) declared name then I else AList.default (op =) (name, ty) + fun do_type (AType (name as (s, _), tys)) = + is_tptp_user_symbol s + ? do_sym name (fn () => nary_type_constr_type (length tys)) + #> fold do_type tys + | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 + | do_type (ATyAbs (_, ty)) = do_type ty + fun do_term pred_sym (ATerm (name as (s, _), tms)) = + is_tptp_user_symbol s + ? do_sym name (fn _ => default_type pred_sym s (length tms)) + #> fold (do_term false) tms + | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm + fun do_formula (AQuant (_, xs, phi)) = + fold do_type (map_filter snd xs) #> do_formula phi + | do_formula (AConn (_, phis)) = fold do_formula phis + | do_formula (AAtom tm) = do_term true tm + fun do_problem_line (Decl (_, _, ty)) = do_type ty + | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi + in + fold (fold do_problem_line o snd) problem [] + |> filter_out (is_built_in_tptp_symbol o fst o fst) + end + +fun declare_undeclared_syms_in_atp_problem problem = + let + val decls = + problem + |> undeclared_syms_in_problem + |> sort_wrt (fst o fst) + |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ())) + in (implicit_declsN, decls) :: problem end + val explicit_apply_threshold = 50 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter @@ -2411,8 +2463,7 @@ | FOF => I | TFF (_, TPTP_Implicit) => I | THF (_, TPTP_Implicit, _) => I - | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix - implicit_declsN) + | _ => declare_undeclared_syms_in_atp_problem) val (problem, pool) = problem |> nice_atp_problem readable_names fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary)