1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 13 14:04:20 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Dec 13 14:55:42 2011 +0100
     1.3 @@ -107,8 +107,7 @@
     1.4      (string * string) problem -> (string * string) problem
     1.5    val filter_cnf_ueq_problem :
     1.6      (string * string) problem -> (string * string) problem
     1.7 -  val declare_undeclared_syms_in_atp_problem :
     1.8 -    string -> string -> (string * string) problem -> (string * string) problem
     1.9 +  val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
    1.10    val nice_atp_problem :
    1.11      bool -> ('a * (string * string) problem_line list) list
    1.12      -> ('a * string problem_line list) list
    1.13 @@ -613,59 +612,11 @@
    1.14  
    1.15  (** Symbol declarations **)
    1.16  
    1.17 -(* TFF allows implicit declarations of types, function symbols, and predicate
    1.18 -   symbols (with "$i" as the type of individuals), but some provers (e.g.,
    1.19 -   SNARK) require explicit declarations. The situation is similar for THF. *)
    1.20 -fun default_type pred_sym =
    1.21 -  let
    1.22 -    fun typ 0 = if pred_sym then bool_atype else individual_atype
    1.23 -      | typ ary = AFun (individual_atype, typ (ary - 1))
    1.24 -  in typ end
    1.25 -
    1.26  fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
    1.27    | add_declared_syms_in_problem_line _ = I
    1.28  fun declared_syms_in_problem problem =
    1.29    fold (fold add_declared_syms_in_problem_line o snd) problem []
    1.30  
    1.31 -fun nary_type_constr_type n =
    1.32 -  funpow n (curry AFun atype_of_types) atype_of_types
    1.33 -
    1.34 -fun undeclared_syms_in_problem declared problem =
    1.35 -  let
    1.36 -    fun do_sym name ty =
    1.37 -      if member (op =) declared name then I else AList.default (op =) (name, ty)
    1.38 -    fun do_type (AType (name as (s, _), tys)) =
    1.39 -        is_tptp_user_symbol s
    1.40 -        ? do_sym name (fn _ => nary_type_constr_type (length tys))
    1.41 -        #> fold do_type tys
    1.42 -      | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
    1.43 -      | do_type (ATyAbs (_, ty)) = do_type ty
    1.44 -    fun do_term pred_sym (ATerm (name as (s, _), tms)) =
    1.45 -        is_tptp_user_symbol s
    1.46 -        ? do_sym name (fn _ => default_type pred_sym (length tms))
    1.47 -        #> fold (do_term false) tms
    1.48 -      | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
    1.49 -    fun do_formula (AQuant (_, xs, phi)) =
    1.50 -        fold do_type (map_filter snd xs) #> do_formula phi
    1.51 -      | do_formula (AConn (_, phis)) = fold do_formula phis
    1.52 -      | do_formula (AAtom tm) = do_term true tm
    1.53 -    fun do_problem_line (Decl (_, _, ty)) = do_type ty
    1.54 -      | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
    1.55 -  in
    1.56 -    fold (fold do_problem_line o snd) problem []
    1.57 -    |> filter_out (is_built_in_tptp_symbol o fst o fst)
    1.58 -  end
    1.59 -
    1.60 -fun declare_undeclared_syms_in_atp_problem prefix heading problem =
    1.61 -  let
    1.62 -    fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ())
    1.63 -    val declared = problem |> declared_syms_in_problem
    1.64 -    val decls =
    1.65 -      problem |> undeclared_syms_in_problem declared
    1.66 -              |> sort_wrt (fst o fst)
    1.67 -              |> map decl_line
    1.68 -  in (heading, decls) :: problem end
    1.69 -
    1.70  (** Nice names **)
    1.71  
    1.72  fun empty_name_pool readable_names =

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:04:20 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Dec 13 14:55:42 2011 +0100
     2.3 @@ -2333,6 +2333,58 @@
     2.4  val conjsN = "Conjectures"
     2.5  val free_typesN = "Type variables"
     2.6  
     2.7 +(* TFF allows implicit declarations of types, function symbols, and predicate
     2.8 +   symbols (with "$i" as the type of individuals), but some provers (e.g.,
     2.9 +   SNARK) require explicit declarations. The situation is similar for THF. *)
    2.10 +
    2.11 +fun default_type pred_sym s =
    2.12 +  let
    2.13 +    val ind =
    2.14 +      if String.isPrefix type_const_prefix s then atype_of_types
    2.15 +      else individual_atype
    2.16 +    fun typ 0 = if pred_sym then bool_atype else ind
    2.17 +      | typ ary = AFun (ind, typ (ary - 1))
    2.18 +  in typ end
    2.19 +
    2.20 +fun nary_type_constr_type n =
    2.21 +  funpow n (curry AFun atype_of_types) atype_of_types
    2.22 +
    2.23 +fun undeclared_syms_in_problem problem =
    2.24 +  let
    2.25 +    val declared = declared_syms_in_problem problem
    2.26 +    fun do_sym name ty =
    2.27 +      if member (op =) declared name then I else AList.default (op =) (name, ty)
    2.28 +    fun do_type (AType (name as (s, _), tys)) =
    2.29 +        is_tptp_user_symbol s
    2.30 +        ? do_sym name (fn () => nary_type_constr_type (length tys))
    2.31 +        #> fold do_type tys
    2.32 +      | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
    2.33 +      | do_type (ATyAbs (_, ty)) = do_type ty
    2.34 +    fun do_term pred_sym (ATerm (name as (s, _), tms)) =
    2.35 +        is_tptp_user_symbol s
    2.36 +        ? do_sym name (fn _ => default_type pred_sym s (length tms))
    2.37 +        #> fold (do_term false) tms
    2.38 +      | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
    2.39 +    fun do_formula (AQuant (_, xs, phi)) =
    2.40 +        fold do_type (map_filter snd xs) #> do_formula phi
    2.41 +      | do_formula (AConn (_, phis)) = fold do_formula phis
    2.42 +      | do_formula (AAtom tm) = do_term true tm
    2.43 +    fun do_problem_line (Decl (_, _, ty)) = do_type ty
    2.44 +      | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
    2.45 +  in
    2.46 +    fold (fold do_problem_line o snd) problem []
    2.47 +    |> filter_out (is_built_in_tptp_symbol o fst o fst)
    2.48 +  end
    2.49 +
    2.50 +fun declare_undeclared_syms_in_atp_problem problem =
    2.51 +  let
    2.52 +    val decls =
    2.53 +      problem
    2.54 +      |> undeclared_syms_in_problem
    2.55 +      |> sort_wrt (fst o fst)
    2.56 +      |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
    2.57 +  in (implicit_declsN, decls) :: problem end
    2.58 +
    2.59  val explicit_apply_threshold = 50
    2.60  
    2.61  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
    2.62 @@ -2411,8 +2463,7 @@
    2.63            | FOF => I
    2.64            | TFF (_, TPTP_Implicit) => I
    2.65            | THF (_, TPTP_Implicit, _) => I
    2.66 -          | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
    2.67 -                                                        implicit_declsN)
    2.68 +          | _ => declare_undeclared_syms_in_atp_problem)
    2.69      val (problem, pool) = problem |> nice_atp_problem readable_names
    2.70      fun add_sym_ary (s, {min_ary, ...} : sym_info) =
    2.71        min_ary > 0 ? Symtab.insert (op =) (s, min_ary)