fully support all type system encodings in typed formats (TFF, THF)
authorblanchet
Fri May 27 10:30:07 2011 +0200 (2011-05-27)
changeset 429981c80902d0456
parent 42997 038bb26d74b0
child 42999 0db96016bdbf
fully support all type system encodings in typed formats (TFF, THF)
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Fri May 27 10:30:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri May 27 10:30:07 2011 +0200
     1.3 @@ -29,13 +29,12 @@
     1.4    val tptp_fof : string
     1.5    val tptp_tff : string
     1.6    val tptp_thf : string
     1.7 -  val tptp_special_prefix : string
     1.8    val tptp_has_type : string
     1.9    val tptp_type_of_types : string
    1.10    val tptp_bool_type : string
    1.11    val tptp_individual_type : string
    1.12    val tptp_fun_type : string
    1.13 -  val tptp_prod_type : string
    1.14 +  val tptp_product_type : string
    1.15    val tptp_forall : string
    1.16    val tptp_exists : string
    1.17    val tptp_not : string
    1.18 @@ -50,18 +49,32 @@
    1.19    val tptp_equal : string
    1.20    val tptp_false : string
    1.21    val tptp_true : string
    1.22 -  val is_atp_variable : string -> bool
    1.23 +  val is_built_in_tptp_symbol : string -> bool
    1.24 +  val is_tptp_variable : string -> bool
    1.25 +  val is_tptp_user_symbol : string -> bool
    1.26    val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
    1.27    val mk_aconn :
    1.28      connective -> ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
    1.29      -> ('a, 'b, 'c) formula
    1.30 +  val aconn_fold :
    1.31 +    bool option -> (bool option -> 'a -> 'b -> 'b) -> connective * 'a list
    1.32 +    -> 'b -> 'b
    1.33 +  val aconn_map :
    1.34 +    bool option -> (bool option -> 'a -> ('b, 'c, 'd) formula)
    1.35 +    -> connective * 'a list -> ('b, 'c, 'd) formula
    1.36 +  val formula_fold :
    1.37 +    bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
    1.38 +    -> 'd -> 'd
    1.39    val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
    1.40 +  val is_format_typed : format -> bool
    1.41    val timestamp : unit -> string
    1.42    val hashw : word * word -> word
    1.43    val hashw_string : string * word -> word
    1.44    val tptp_strings_for_atp_problem : format -> string problem -> string list
    1.45    val filter_cnf_ueq_problem :
    1.46      (string * string) problem -> (string * string) problem
    1.47 +  val declare_undeclared_syms_in_atp_problem :
    1.48 +    string -> string -> (string * string) problem -> (string * string) problem
    1.49    val nice_atp_problem :
    1.50      bool -> ('a * (string * string) problem_line list) list
    1.51      -> ('a * string problem_line list) list
    1.52 @@ -96,13 +109,12 @@
    1.53  val tptp_fof = "fof"
    1.54  val tptp_tff = "tff"
    1.55  val tptp_thf = "thf"
    1.56 -val tptp_special_prefix = "$"
    1.57  val tptp_has_type = ":"
    1.58  val tptp_type_of_types = "$tType"
    1.59  val tptp_bool_type = "$o"
    1.60  val tptp_individual_type = "$i"
    1.61  val tptp_fun_type = ">"
    1.62 -val tptp_prod_type = "*"
    1.63 +val tptp_product_type = "*"
    1.64  val tptp_forall = "!"
    1.65  val tptp_exists = "?"
    1.66  val tptp_not = "~"
    1.67 @@ -118,16 +130,42 @@
    1.68  val tptp_false = "$false"
    1.69  val tptp_true = "$true"
    1.70  
    1.71 -fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
    1.72 +fun is_built_in_tptp_symbol "equal" = true (* deprecated *)
    1.73 +  | is_built_in_tptp_symbol s = not (Char.isAlpha (String.sub (s, 0)))
    1.74 +fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
    1.75 +val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
    1.76  
    1.77  fun mk_anot (AConn (ANot, [phi])) = phi
    1.78    | mk_anot phi = AConn (ANot, [phi])
    1.79  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    1.80  
    1.81 +fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
    1.82 +  | aconn_fold pos f (AImplies, [phi1, phi2]) =
    1.83 +    f (Option.map not pos) phi1 #> f pos phi2
    1.84 +  | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
    1.85 +  | aconn_fold pos f (AOr, phis) = fold (f pos) phis
    1.86 +  | aconn_fold _ f (_, phis) = fold (f NONE) phis
    1.87 +
    1.88 +fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
    1.89 +  | aconn_map pos f (AImplies, [phi1, phi2]) =
    1.90 +    AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
    1.91 +  | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
    1.92 +  | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
    1.93 +  | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
    1.94 +
    1.95 +fun formula_fold pos f =
    1.96 +  let
    1.97 +    fun aux pos (AQuant (_, _, phi)) = aux pos phi
    1.98 +      | aux pos (AConn conn) = aconn_fold pos aux conn
    1.99 +      | aux pos (AAtom tm) = f pos tm
   1.100 +  in aux pos end
   1.101 +
   1.102  fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   1.103    | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   1.104    | formula_map f (AAtom tm) = AAtom (f tm)
   1.105  
   1.106 +val is_format_typed = member (op =) [TFF, THF]
   1.107 +
   1.108  val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
   1.109  
   1.110  (* This hash function is recommended in "Compilers: Principles, Techniques, and
   1.111 @@ -160,7 +198,7 @@
   1.112         ([], s) => s
   1.113       | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s
   1.114       | (ss, s) =>
   1.115 -       "(" ^ space_implode (" " ^ tptp_prod_type ^ " ") ss ^ ") " ^
   1.116 +       "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^
   1.117         tptp_fun_type ^ " " ^ s)
   1.118    | string_for_type _ _ = raise Fail "unexpected type in untyped format"
   1.119  
   1.120 @@ -256,7 +294,7 @@
   1.121    | is_problem_line_cnf_ueq _ = false
   1.122  
   1.123  fun open_conjecture_term (ATerm ((s, s'), tms)) =
   1.124 -  ATerm (if is_atp_variable s then (s |> Name.desymbolize false, s')
   1.125 +  ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
   1.126           else (s, s'), tms |> map open_conjecture_term)
   1.127  fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi
   1.128    | open_formula true (AAtom t) = AAtom (open_conjecture_term t)
   1.129 @@ -280,6 +318,58 @@
   1.130           in if length conjs = 1 then problem else [] end)
   1.131  
   1.132  
   1.133 +(** Symbol declarations **)
   1.134 +
   1.135 +(* TFF allows implicit declarations of types, function symbols, and predicate
   1.136 +   symbols (with "$i" as the type of individuals), but some provers (e.g.,
   1.137 +   SNARK) require explicit declarations. The situation is similar for THF. *)
   1.138 +
   1.139 +val atype_of_types = AType (`I tptp_type_of_types)
   1.140 +val bool_atype = AType (`I tptp_bool_type)
   1.141 +val individual_atype = AType (`I tptp_individual_type)
   1.142 +
   1.143 +fun default_type pred_sym =
   1.144 +  let
   1.145 +    fun typ 0 = if pred_sym then bool_atype else individual_atype
   1.146 +      | typ ary = AFun (individual_atype, typ (ary - 1))
   1.147 +  in typ end
   1.148 +
   1.149 +fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
   1.150 +  | add_declared_syms_in_problem_line _ = I
   1.151 +fun declared_syms_in_problem problem =
   1.152 +  fold (fold add_declared_syms_in_problem_line o snd) problem []
   1.153 +
   1.154 +fun undeclared_syms_in_problem declared problem =
   1.155 +  let
   1.156 +    fun do_sym name ty =
   1.157 +      if member (op =) declared name then I else AList.default (op =) (name, ty)
   1.158 +    fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
   1.159 +      | do_type (AType name) = do_sym name (K atype_of_types)
   1.160 +    fun do_term pred_sym (ATerm (name as (s, _), tms)) =
   1.161 +      is_tptp_user_symbol s
   1.162 +      ? do_sym name (fn _ => default_type pred_sym (length tms))
   1.163 +      #> fold (do_term false) tms
   1.164 +    fun do_formula (AQuant (_, xs, phi)) =
   1.165 +        fold do_type (map_filter snd xs) #> do_formula phi
   1.166 +      | do_formula (AConn (_, phis)) = fold do_formula phis
   1.167 +      | do_formula (AAtom tm) = do_term true tm
   1.168 +    fun do_problem_line (Decl (_, _, ty)) = do_type ty
   1.169 +      | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
   1.170 +  in
   1.171 +    fold (fold do_problem_line o snd) problem []
   1.172 +    |> filter_out (is_built_in_tptp_symbol o fst o fst)
   1.173 +  end
   1.174 +
   1.175 +fun declare_undeclared_syms_in_atp_problem prefix heading problem =
   1.176 +  let
   1.177 +    fun decl_line (x as (s, _), ty) = Decl (prefix ^ s, x, ty ())
   1.178 +    val declared = problem |> declared_syms_in_problem
   1.179 +    val decls =
   1.180 +      problem |> undeclared_syms_in_problem declared
   1.181 +              |> sort_wrt (fst o fst)
   1.182 +              |> map decl_line
   1.183 +  in (heading, decls) :: problem end
   1.184 +
   1.185  (** Nice names **)
   1.186  
   1.187  fun empty_name_pool readable_names =
   1.188 @@ -325,7 +415,7 @@
   1.189  
   1.190  fun nice_name (full_name, _) NONE = (full_name, NONE)
   1.191    | nice_name (full_name, desired_name) (SOME the_pool) =
   1.192 -    if String.isPrefix tptp_special_prefix full_name then
   1.193 +    if is_built_in_tptp_symbol full_name then
   1.194        (full_name, SOME the_pool)
   1.195      else case Symtab.lookup (fst the_pool) full_name of
   1.196        SOME nice_name => (nice_name, SOME the_pool)
   1.197 @@ -362,8 +452,7 @@
   1.198      pool_map nice_formula phis #>> curry AConn c
   1.199    | nice_formula (AAtom tm) = nice_term tm #>> AAtom
   1.200  fun nice_problem_line (Decl (ident, sym, ty)) =
   1.201 -    nice_name sym ##>> nice_type ty
   1.202 -    #>> (fn (sym, ty) => Decl (ident, sym, ty))
   1.203 +    nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Decl (ident, sym, ty))
   1.204    | nice_problem_line (Formula (ident, kind, phi, source, info)) =
   1.205      nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
   1.206  fun nice_problem problem =
     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:07 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri May 27 10:30:07 2011 +0200
     2.3 @@ -378,7 +378,7 @@
     2.4    let
     2.5      fun do_term_pair _ NONE = NONE
     2.6        | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
     2.7 -        case pairself is_atp_variable (s1, s2) of
     2.8 +        case pairself is_tptp_variable (s1, s2) of
     2.9            (true, true) =>
    2.10            (case AList.lookup (op =) subst s1 of
    2.11               SOME s2' => if s2' = s2 then SOME subst else NONE
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:07 2011 +0200
     3.3 @@ -364,7 +364,7 @@
     3.4    | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
     3.5    | add_type_constraint _ _ = I
     3.6  
     3.7 -fun repair_atp_variable_name f s =
     3.8 +fun repair_tptp_variable_name f s =
     3.9    let
    3.10      fun subscript_name s n = s ^ nat_subscript n
    3.11      val s = String.map f s
    3.12 @@ -445,11 +445,11 @@
    3.13                  case strip_prefix_and_unascii schematic_var_prefix a of
    3.14                    SOME b => Var ((b, 0), T)
    3.15                  | NONE =>
    3.16 -                  if is_atp_variable a then
    3.17 -                    Var ((repair_atp_variable_name Char.toLower a, 0), T)
    3.18 +                  if is_tptp_variable a then
    3.19 +                    Var ((repair_tptp_variable_name Char.toLower a, 0), T)
    3.20                    else
    3.21                      (* Skolem constants? *)
    3.22 -                    Var ((repair_atp_variable_name Char.toUpper a, 0), T)
    3.23 +                    Var ((repair_tptp_variable_name Char.toUpper a, 0), T)
    3.24            in list_comb (t, ts) end
    3.25    in aux (SOME HOLogic.boolT) [] end
    3.26  
    3.27 @@ -514,7 +514,7 @@
    3.28          #>> quantify_over_var (case q of
    3.29                                   AForall => forall_of
    3.30                                 | AExists => exists_of)
    3.31 -                              (repair_atp_variable_name Char.toLower s)
    3.32 +                              (repair_tptp_variable_name Char.toLower s)
    3.33        | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
    3.34        | AConn (c, [phi1, phi2]) =>
    3.35          do_formula (pos |> c = AImplies ? not) phi1
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:07 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 27 10:30:07 2011 +0200
     4.3 @@ -81,8 +81,9 @@
     4.4  val readable_names =
     4.5    Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true)
     4.6  
     4.7 -val type_decl_prefix = "type_"
     4.8 -val sym_decl_prefix = "sym_"
     4.9 +val type_decl_prefix = "ty_"
    4.10 +val sym_decl_prefix = "sy_"
    4.11 +val sym_formula_prefix = "sym_"
    4.12  val fact_prefix = "fact_"
    4.13  val conjecture_prefix = "conj_"
    4.14  val helper_prefix = "help_"
    4.15 @@ -184,27 +185,6 @@
    4.16  fun is_setting_higher_order THF (Simple_Types _) = true
    4.17    | is_setting_higher_order _ _ = false
    4.18  
    4.19 -fun aconn_fold pos f (ANot, [phi]) = f (Option.map not pos) phi
    4.20 -  | aconn_fold pos f (AImplies, [phi1, phi2]) =
    4.21 -    f (Option.map not pos) phi1 #> f pos phi2
    4.22 -  | aconn_fold pos f (AAnd, phis) = fold (f pos) phis
    4.23 -  | aconn_fold pos f (AOr, phis) = fold (f pos) phis
    4.24 -  | aconn_fold _ f (_, phis) = fold (f NONE) phis
    4.25 -
    4.26 -fun aconn_map pos f (ANot, [phi]) = AConn (ANot, [f (Option.map not pos) phi])
    4.27 -  | aconn_map pos f (AImplies, [phi1, phi2]) =
    4.28 -    AConn (AImplies, [f (Option.map not pos) phi1, f pos phi2])
    4.29 -  | aconn_map pos f (AAnd, phis) = AConn (AAnd, map (f pos) phis)
    4.30 -  | aconn_map pos f (AOr, phis) = AConn (AOr, map (f pos) phis)
    4.31 -  | aconn_map _ f (c, phis) = AConn (c, map (f NONE) phis)
    4.32 -
    4.33 -fun formula_fold pos f =
    4.34 -  let
    4.35 -    fun aux pos (AQuant (_, _, phi)) = aux pos phi
    4.36 -      | aux pos (AConn conn) = aconn_fold pos aux conn
    4.37 -      | aux pos (AAtom tm) = f pos tm
    4.38 -  in aux pos end
    4.39 -
    4.40  type translated_formula =
    4.41    {name: string,
    4.42     locality: locality,
    4.43 @@ -282,8 +262,7 @@
    4.44  fun close_combformula_universally phi = close_universally combterm_vars phi
    4.45  
    4.46  fun term_vars (ATerm (name as (s, _), tms)) =
    4.47 -  is_atp_variable s ? insert (op =) (name, NONE)
    4.48 -  #> fold term_vars tms
    4.49 +  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
    4.50  fun close_formula_universally phi = close_universally term_vars phi
    4.51  
    4.52  val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
    4.53 @@ -311,14 +290,15 @@
    4.54      f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
    4.55      ^ ")"
    4.56  
    4.57 +val bool_atype = AType (`I tptp_bool_type)
    4.58 +
    4.59  fun ho_type_from_fo_term higher_order pred_sym ary =
    4.60    let
    4.61      fun to_atype ty =
    4.62        AType ((make_simple_type (generic_mangled_type_name fst ty),
    4.63                generic_mangled_type_name snd ty))
    4.64      fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
    4.65 -    fun to_fo 0 ty =
    4.66 -        if pred_sym then AType (`I tptp_bool_type) else to_atype ty
    4.67 +    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
    4.68        | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
    4.69      fun to_ho (ty as ATerm ((s, _), tys)) =
    4.70        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
    4.71 @@ -1013,8 +993,7 @@
    4.72    end
    4.73  
    4.74  fun should_declare_sym type_sys pred_sym s =
    4.75 -  not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
    4.76 -  not (String.isPrefix tptp_special_prefix s) andalso
    4.77 +  is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
    4.78    (case type_sys of
    4.79       Simple_Types _ => true
    4.80     | Tags (_, _, Light) => true
    4.81 @@ -1086,7 +1065,7 @@
    4.82          Simple_Types level => (format = THF, [], level)
    4.83        | _ => (false, replicate (length T_args) homo_infinite_type, No_Types)
    4.84    in
    4.85 -    Decl (type_decl_prefix ^ s, (s, s'),
    4.86 +    Decl (sym_decl_prefix ^ s, (s, s'),
    4.87            (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
    4.88            |> mangled_type higher_order pred_sym (length T_arg_Ts + ary))
    4.89    end
    4.90 @@ -1108,7 +1087,7 @@
    4.91        arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
    4.92                               else NONE)
    4.93    in
    4.94 -    Formula (sym_decl_prefix ^ s ^
    4.95 +    Formula (sym_formula_prefix ^ s ^
    4.96               (if n > 1 then "_" ^ string_of_int j else ""), kind,
    4.97               CombConst ((s, s'), T, T_args)
    4.98               |> fold (curry (CombApp o swap)) bounds
    4.99 @@ -1126,7 +1105,7 @@
   4.100          n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   4.101    let
   4.102      val ident_base =
   4.103 -      sym_decl_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
   4.104 +      sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
   4.105      val (kind, maybe_negate) =
   4.106        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
   4.107        else (Axiom, I)
   4.108 @@ -1173,74 +1152,50 @@
   4.109  
   4.110  fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
   4.111                                  (s, decls) =
   4.112 -  (if member (op =) [TFF, THF] format then
   4.113 -     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
   4.114 -   else
   4.115 -     []) @
   4.116 -  (case type_sys of
   4.117 -     Simple_Types _ => []
   4.118 -   | Preds _ =>
   4.119 -     let
   4.120 -       val decls =
   4.121 -         case decls of
   4.122 -           decl :: (decls' as _ :: _) =>
   4.123 -           let val T = result_type_of_decl decl in
   4.124 -             if forall (curry (type_instance ctxt o swap) T
   4.125 -                        o result_type_of_decl) decls' then
   4.126 -               [decl]
   4.127 -             else
   4.128 -               decls
   4.129 -           end
   4.130 -         | _ => decls
   4.131 -       val n = length decls
   4.132 -       val decls =
   4.133 -         decls
   4.134 -         |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
   4.135 -                    o result_type_of_decl)
   4.136 -     in
   4.137 -       (0 upto length decls - 1, decls)
   4.138 -       |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
   4.139 -                                                nonmono_Ts type_sys n s)
   4.140 -     end
   4.141 -   | Tags (_, _, heaviness) =>
   4.142 -     (case heaviness of
   4.143 -        Heavy => []
   4.144 -      | Light =>
   4.145 -        let val n = length decls in
   4.146 -          (0 upto n - 1 ~~ decls)
   4.147 -          |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
   4.148 -                                                  nonmono_Ts type_sys n s)
   4.149 -        end))
   4.150 +  case type_sys of
   4.151 +    Simple_Types _ =>
   4.152 +    decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
   4.153 +  | Preds _ =>
   4.154 +    let
   4.155 +      val decls =
   4.156 +        case decls of
   4.157 +          decl :: (decls' as _ :: _) =>
   4.158 +          let val T = result_type_of_decl decl in
   4.159 +            if forall (curry (type_instance ctxt o swap) T
   4.160 +                       o result_type_of_decl) decls' then
   4.161 +              [decl]
   4.162 +            else
   4.163 +              decls
   4.164 +          end
   4.165 +        | _ => decls
   4.166 +      val n = length decls
   4.167 +      val decls =
   4.168 +        decls
   4.169 +        |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
   4.170 +                   o result_type_of_decl)
   4.171 +    in
   4.172 +      (0 upto length decls - 1, decls)
   4.173 +      |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
   4.174 +                                               nonmono_Ts type_sys n s)
   4.175 +    end
   4.176 +  | Tags (_, _, heaviness) =>
   4.177 +    (case heaviness of
   4.178 +       Heavy => []
   4.179 +     | Light =>
   4.180 +       let val n = length decls in
   4.181 +         (0 upto n - 1 ~~ decls)
   4.182 +         |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
   4.183 +                                                 nonmono_Ts type_sys n s)
   4.184 +       end)
   4.185  
   4.186  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
   4.187                                       type_sys sym_decl_tab =
   4.188 -  Symtab.fold_rev
   4.189 -      (append o problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
   4.190 -                                            type_sys)
   4.191 -      sym_decl_tab []
   4.192 -
   4.193 -fun add_simple_types_in_type (AFun (ty1, ty2)) =
   4.194 -    fold add_simple_types_in_type [ty1, ty2]
   4.195 -  | add_simple_types_in_type (AType name) = insert (op =) name
   4.196 -
   4.197 -fun add_simple_types_in_formula (AQuant (_, xs, phi)) =
   4.198 -    fold add_simple_types_in_type (map_filter snd xs)
   4.199 -    #> add_simple_types_in_formula phi
   4.200 -  | add_simple_types_in_formula (AConn (_, phis)) =
   4.201 -    fold add_simple_types_in_formula phis
   4.202 -  | add_simple_types_in_formula (AAtom _) = I
   4.203 -
   4.204 -fun add_simple_types_in_problem_line (Decl (_, _, ty)) =
   4.205 -    add_simple_types_in_type ty
   4.206 -  | add_simple_types_in_problem_line (Formula (_, _, phi, _, _)) =
   4.207 -    add_simple_types_in_formula phi
   4.208 -
   4.209 -fun simple_types_in_problem problem =
   4.210 -  fold (fold add_simple_types_in_problem_line o snd) problem []
   4.211 -  |> filter_out (String.isPrefix tptp_special_prefix o fst)
   4.212 -
   4.213 -fun decl_line_for_simple_type (s, s') =
   4.214 -  Decl (type_decl_prefix ^ s, (s, s'), AType (`I tptp_type_of_types))
   4.215 +  sym_decl_tab
   4.216 +  |> Symtab.dest
   4.217 +  |> sort_wrt fst
   4.218 +  |> rpair []
   4.219 +  |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
   4.220 +                                                     nonmono_Ts type_sys)
   4.221  
   4.222  fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) =
   4.223      level = Nonmonotonic_Types orelse level = Finite_Types
   4.224 @@ -1251,8 +1206,8 @@
   4.225      if heading = needle then j
   4.226      else offset_of_heading_in_problem needle problem (j + length lines)
   4.227  
   4.228 -val type_declsN = "Types"
   4.229 -val sym_declsN = "Symbol types"
   4.230 +val implicit_declsN = "Should-be-implicit typings"
   4.231 +val explicit_declsN = "Explicit typings"
   4.232  val factsN = "Relevant facts"
   4.233  val class_relsN = "Class relationships"
   4.234  val aritiesN = "Arities"
   4.235 @@ -1293,7 +1248,7 @@
   4.236      (* Reordering these might confuse the proof reconstruction code or the SPASS
   4.237         Flotter hack. *)
   4.238      val problem =
   4.239 -      [(sym_declsN, sym_decl_lines),
   4.240 +      [(explicit_declsN, sym_decl_lines),
   4.241         (factsN,
   4.242          map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
   4.243              (0 upto length facts - 1 ~~ facts)),
   4.244 @@ -1307,13 +1262,12 @@
   4.245          formula_lines_for_free_types format type_sys (facts @ conjs))]
   4.246      val problem =
   4.247        problem
   4.248 -      |> (case type_sys of
   4.249 -            Simple_Types _ =>
   4.250 -            cons (type_declsN, problem |> simple_types_in_problem
   4.251 -                                       |> map decl_line_for_simple_type)
   4.252 -          | _ => I)
   4.253 -    val problem =
   4.254 -      problem |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
   4.255 +      |> (if format = CNF_UEQ then filter_cnf_ueq_problem else I)
   4.256 +      |> (if is_format_typed format then
   4.257 +            declare_undeclared_syms_in_atp_problem type_decl_prefix
   4.258 +                                                   implicit_declsN
   4.259 +          else
   4.260 +            I)
   4.261      val (problem, pool) =
   4.262        problem |> nice_atp_problem (Config.get ctxt readable_names)
   4.263      val helpers_offset = offset_of_heading_in_problem helpersN problem 0
   4.264 @@ -1348,8 +1302,7 @@
   4.265  val type_info_default_weight = 0.8
   4.266  
   4.267  fun add_term_weights weight (ATerm (s, tms)) =
   4.268 -  (not (is_atp_variable s) andalso s <> "equal" andalso
   4.269 -   not (String.isPrefix tptp_special_prefix s)) ? Symtab.default (s, weight)
   4.270 +  is_tptp_user_symbol s ? Symtab.default (s, weight)
   4.271    #> fold (add_term_weights weight) tms
   4.272  fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
   4.273      formula_fold NONE (K (add_term_weights weight)) phi
   4.274 @@ -1380,7 +1333,7 @@
   4.275      |> add_conjectures_weights (get free_typesN @ get conjsN)
   4.276      |> add_facts_weights (get factsN)
   4.277      |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
   4.278 -            [sym_declsN, class_relsN, aritiesN]
   4.279 +            [explicit_declsN, class_relsN, aritiesN]
   4.280      |> Symtab.dest
   4.281      |> sort (prod_ord Real.compare string_ord o pairself swap)
   4.282    end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:07 2011 +0200
     5.3 @@ -446,20 +446,14 @@
     5.4      else
     5.5        adjust_dumb_type_sys formats (Preds (Mangled_Monomorphic, level, Heavy))
     5.6    | adjust_dumb_type_sys formats type_sys =
     5.7 -    if member (op =) formats FOF then
     5.8 -      (FOF, type_sys)
     5.9 -    else if member (op =) formats CNF_UEQ then
    5.10 -      (CNF_UEQ, case type_sys of
    5.11 -                  Preds stuff =>
    5.12 -                  (if is_type_sys_fairly_sound type_sys then Preds else Tags)
    5.13 -                      stuff
    5.14 -                | _ => type_sys)
    5.15 -    else
    5.16 -      (* We could return "type_sys" unchanged for TFF but this would require the
    5.17 -         TFF and THF provers to accept problems in which some constants are
    5.18 -         implicitly declared. Today only ToFoF-E seems to meet this
    5.19 -         criterion. *)
    5.20 -      (hd formats, Simple_Types All_Types)
    5.21 +    (case hd formats of
    5.22 +       CNF_UEQ =>
    5.23 +       (CNF_UEQ, case type_sys of
    5.24 +                   Preds stuff =>
    5.25 +                   (if is_type_sys_fairly_sound type_sys then Preds else Tags)
    5.26 +                       stuff
    5.27 +                 | _ => type_sys)
    5.28 +     | format => (format, type_sys))
    5.29  
    5.30  fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
    5.31      adjust_dumb_type_sys formats type_sys