# HG changeset patch # User blanchet # Date 1308141401 -7200 # Node ID e93dfcb53535b8a59d7d7ffa39c6a9cdd0b98fc9 # Parent 3d03f44728832b1395e324c3578b54d8dc632280 fixed soundness bug made more visible by previous change diff -r 3d03f4472883 -r e93dfcb53535 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 15 14:36:41 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 15 14:36:41 2011 +0200 @@ -751,6 +751,9 @@ ATerm ((make_schematic_type_var x, s), []) in term end +fun fo_term_for_type_arg format type_sys T = + if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T) + (* This shouldn't clash with anything else. *) val mangled_type_sep = "\000" @@ -786,7 +789,7 @@ fun mangled_const_name format type_sys T_args (s, s') = let - val ty_args = map (fo_term_from_typ format type_sys) T_args + val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys) fun type_suffix f g = fold_rev (curry (op ^) o g o prefix mangled_type_sep o generic_mangled_type_name f) ty_args "" @@ -1249,11 +1252,9 @@ | res_U_vars => let val U_args = (s, U) |> Sign.const_typargs thy in U_args ~~ T_args - |> map_filter (fn (U, T) => - if member (op =) res_U_vars (dest_TVar U) then - SOME T - else - NONE) + |> map (fn (U, T) => + if member (op =) res_U_vars (dest_TVar U) then T + else dummyT) end end handle TYPE _ => T_args @@ -1474,7 +1475,7 @@ formula_fold pos (var_occurs_positively_naked_in_term name) phi false fun mk_const_aterm format type_sys x T_args args = - ATerm (x, map (fo_term_from_typ format type_sys) T_args @ args) + ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args) fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm = CombConst (type_tag, T --> T, [T]) @@ -1700,7 +1701,7 @@ end fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts - type_sys n s j (s', T_args, T, _, ary, in_conj) = + poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) = let val (kind, maybe_negate) = if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot) @@ -1711,9 +1712,12 @@ 1 upto num_args |> map (`I o make_bound_var o string_of_int) val bounds = bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) + val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args + fun should_keep_arg_type T = + sym_needs_arg_types orelse + not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T) val bound_Ts = - if n > 1 andalso should_drop_arg_type_args type_sys then map SOME arg_Ts - else replicate num_args NONE + arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE) in Formula (preds_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else ""), kind, @@ -1721,7 +1725,7 @@ |> fold (curry (CombApp o swap)) bounds |> type_pred_combterm ctxt format type_sys res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_combformula ctxt format nonmono_Ts type_sys + |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys (K (K (K (K true)))) true |> n > 1 ? bound_tvars type_sys (atyps_of T) |> close_formula_universally @@ -1730,7 +1734,8 @@ end fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) = + poly_nonmono_Ts type_sys n s + (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val ident_base = lightweight_tags_sym_formula_prefix ^ s ^ @@ -1752,12 +1757,12 @@ |> maybe_negate (* See also "should_tag_with_type". *) fun should_encode T = - should_encode_type ctxt nonmono_Ts All_Types T orelse + should_encode_type ctxt poly_nonmono_Ts All_Types T orelse (case type_sys of Tags (Polymorphic, level, Lightweight) => level <> All_Types andalso Monomorph.typ_has_tvars T | _ => false) - val tag_with = tag_with_type ctxt format nonmono_Ts type_sys NONE + val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE val add_formula_for_res = if should_encode res_T then cons (Formula (ident_base ^ "_res", kind, @@ -1785,8 +1790,8 @@ fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd -fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys - (s, decls) = +fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts + poly_nonmono_Ts type_sys (s, decls) = case type_sys of Simple_Types _ => decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s) @@ -1805,13 +1810,13 @@ | _ => decls val n = length decls val decls = - decls - |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true) - o result_type_of_decl) + decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys + (K true) + o result_type_of_decl) in (0 upto length decls - 1, decls) |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind - nonmono_Ts type_sys n s) + nonmono_Ts poly_nonmono_Ts type_sys n s) end | Tags (_, _, heaviness) => (case heaviness of @@ -1820,17 +1825,17 @@ let val n = length decls in (0 upto n - 1 ~~ decls) |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format - conj_sym_kind nonmono_Ts type_sys n s) + conj_sym_kind poly_nonmono_Ts type_sys n s) end) fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts - type_sys sym_decl_tab = + poly_nonmono_Ts type_sys sym_decl_tab = sym_decl_tab |> Symtab.dest |> sort_wrt fst |> rpair [] |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind - nonmono_Ts type_sys) + nonmono_Ts poly_nonmono_Ts type_sys) fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) = poly <> Mangled_Monomorphic andalso @@ -1870,7 +1875,7 @@ val helpers = repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys |> map repair - val lavish_nonmono_Ts = + val poly_nonmono_Ts = if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse polymorphism_of_type_sys type_sys <> Polymorphic then nonmono_Ts @@ -1879,12 +1884,12 @@ val sym_decl_lines = (conjs, helpers @ facts) |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab - |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind - lavish_nonmono_Ts type_sys + |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts + poly_nonmono_Ts type_sys val helper_lines = 0 upto length helpers - 1 ~~ helpers |> map (formula_line_for_fact ctxt format helper_prefix I false - lavish_nonmono_Ts type_sys) + poly_nonmono_Ts type_sys) |> (if needs_type_tag_idempotence type_sys then cons (type_tag_idempotence_fact ()) else