# HG changeset patch # User blanchet # Date 1304279612 -7200 # Node ID fa2cf11d63516bc77263577f9063e720d736a486 # Parent f139d0ac2d448c31b95a225af70d270f88e1b959 beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type) diff -r f139d0ac2d44 -r fa2cf11d6351 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:57:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 21:53:32 2011 +0200 @@ -779,6 +779,8 @@ if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T) end +fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false + fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) = let val (arg_Ts, res_T) = n_ary_strip_type ary T @@ -787,7 +789,8 @@ val bound_tms = bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) val bound_Ts = - arg_Ts |> map (if n > 1 then SOME else K NONE) + arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T + else NONE) in Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom, CombConst ((s, s'), T, T_args) @@ -807,11 +810,13 @@ val decls = case decls of decl :: (decls' as _ :: _) => - if forall (curry (op =) (result_type_of_decl decl) - o result_type_of_decl) decls' then - [decl] - else - decls + let val T = result_type_of_decl decl in + if forall ((fn T' => Type.raw_instance (T', T)) + o result_type_of_decl) decls' then + [decl] + else + decls + end | _ => decls val n = length decls val decls =