1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 15 14:36:41 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 15 14:36:41 2011 +0200
1.3 @@ -751,6 +751,9 @@
1.4 ATerm ((make_schematic_type_var x, s), [])
1.5 in term end
1.6
1.7 +fun fo_term_for_type_arg format type_sys T =
1.8 + if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
1.9 +
1.10 (* This shouldn't clash with anything else. *)
1.11 val mangled_type_sep = "\000"
1.12
1.13 @@ -786,7 +789,7 @@
1.14
1.15 fun mangled_const_name format type_sys T_args (s, s') =
1.16 let
1.17 - val ty_args = map (fo_term_from_typ format type_sys) T_args
1.18 + val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
1.19 fun type_suffix f g =
1.20 fold_rev (curry (op ^) o g o prefix mangled_type_sep
1.21 o generic_mangled_type_name f) ty_args ""
1.22 @@ -1249,11 +1252,9 @@
1.23 | res_U_vars =>
1.24 let val U_args = (s, U) |> Sign.const_typargs thy in
1.25 U_args ~~ T_args
1.26 - |> map_filter (fn (U, T) =>
1.27 - if member (op =) res_U_vars (dest_TVar U) then
1.28 - SOME T
1.29 - else
1.30 - NONE)
1.31 + |> map (fn (U, T) =>
1.32 + if member (op =) res_U_vars (dest_TVar U) then T
1.33 + else dummyT)
1.34 end
1.35 end
1.36 handle TYPE _ => T_args
1.37 @@ -1474,7 +1475,7 @@
1.38 formula_fold pos (var_occurs_positively_naked_in_term name) phi false
1.39
1.40 fun mk_const_aterm format type_sys x T_args args =
1.41 - ATerm (x, map (fo_term_from_typ format type_sys) T_args @ args)
1.42 + ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
1.43
1.44 fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
1.45 CombConst (type_tag, T --> T, [T])
1.46 @@ -1700,7 +1701,7 @@
1.47 end
1.48
1.49 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1.50 - type_sys n s j (s', T_args, T, _, ary, in_conj) =
1.51 + poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
1.52 let
1.53 val (kind, maybe_negate) =
1.54 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1.55 @@ -1711,9 +1712,12 @@
1.56 1 upto num_args |> map (`I o make_bound_var o string_of_int)
1.57 val bounds =
1.58 bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
1.59 + val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
1.60 + fun should_keep_arg_type T =
1.61 + sym_needs_arg_types orelse
1.62 + not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
1.63 val bound_Ts =
1.64 - if n > 1 andalso should_drop_arg_type_args type_sys then map SOME arg_Ts
1.65 - else replicate num_args NONE
1.66 + arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1.67 in
1.68 Formula (preds_sym_formula_prefix ^ s ^
1.69 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1.70 @@ -1721,7 +1725,7 @@
1.71 |> fold (curry (CombApp o swap)) bounds
1.72 |> type_pred_combterm ctxt format type_sys res_T
1.73 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1.74 - |> formula_from_combformula ctxt format nonmono_Ts type_sys
1.75 + |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
1.76 (K (K (K (K true)))) true
1.77 |> n > 1 ? bound_tvars type_sys (atyps_of T)
1.78 |> close_formula_universally
1.79 @@ -1730,7 +1734,8 @@
1.80 end
1.81
1.82 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1.83 - nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1.84 + poly_nonmono_Ts type_sys n s
1.85 + (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1.86 let
1.87 val ident_base =
1.88 lightweight_tags_sym_formula_prefix ^ s ^
1.89 @@ -1752,12 +1757,12 @@
1.90 |> maybe_negate
1.91 (* See also "should_tag_with_type". *)
1.92 fun should_encode T =
1.93 - should_encode_type ctxt nonmono_Ts All_Types T orelse
1.94 + should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
1.95 (case type_sys of
1.96 Tags (Polymorphic, level, Lightweight) =>
1.97 level <> All_Types andalso Monomorph.typ_has_tvars T
1.98 | _ => false)
1.99 - val tag_with = tag_with_type ctxt format nonmono_Ts type_sys NONE
1.100 + val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
1.101 val add_formula_for_res =
1.102 if should_encode res_T then
1.103 cons (Formula (ident_base ^ "_res", kind,
1.104 @@ -1785,8 +1790,8 @@
1.105
1.106 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1.107
1.108 -fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys
1.109 - (s, decls) =
1.110 +fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
1.111 + poly_nonmono_Ts type_sys (s, decls) =
1.112 case type_sys of
1.113 Simple_Types _ =>
1.114 decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
1.115 @@ -1805,13 +1810,13 @@
1.116 | _ => decls
1.117 val n = length decls
1.118 val decls =
1.119 - decls
1.120 - |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys (K true)
1.121 - o result_type_of_decl)
1.122 + decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
1.123 + (K true)
1.124 + o result_type_of_decl)
1.125 in
1.126 (0 upto length decls - 1, decls)
1.127 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1.128 - nonmono_Ts type_sys n s)
1.129 + nonmono_Ts poly_nonmono_Ts type_sys n s)
1.130 end
1.131 | Tags (_, _, heaviness) =>
1.132 (case heaviness of
1.133 @@ -1820,17 +1825,17 @@
1.134 let val n = length decls in
1.135 (0 upto n - 1 ~~ decls)
1.136 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1.137 - conj_sym_kind nonmono_Ts type_sys n s)
1.138 + conj_sym_kind poly_nonmono_Ts type_sys n s)
1.139 end)
1.140
1.141 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1.142 - type_sys sym_decl_tab =
1.143 + poly_nonmono_Ts type_sys sym_decl_tab =
1.144 sym_decl_tab
1.145 |> Symtab.dest
1.146 |> sort_wrt fst
1.147 |> rpair []
1.148 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1.149 - nonmono_Ts type_sys)
1.150 + nonmono_Ts poly_nonmono_Ts type_sys)
1.151
1.152 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1.153 poly <> Mangled_Monomorphic andalso
1.154 @@ -1870,7 +1875,7 @@
1.155 val helpers =
1.156 repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
1.157 |> map repair
1.158 - val lavish_nonmono_Ts =
1.159 + val poly_nonmono_Ts =
1.160 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1.161 polymorphism_of_type_sys type_sys <> Polymorphic then
1.162 nonmono_Ts
1.163 @@ -1879,12 +1884,12 @@
1.164 val sym_decl_lines =
1.165 (conjs, helpers @ facts)
1.166 |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
1.167 - |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind
1.168 - lavish_nonmono_Ts type_sys
1.169 + |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1.170 + poly_nonmono_Ts type_sys
1.171 val helper_lines =
1.172 0 upto length helpers - 1 ~~ helpers
1.173 |> map (formula_line_for_fact ctxt format helper_prefix I false
1.174 - lavish_nonmono_Ts type_sys)
1.175 + poly_nonmono_Ts type_sys)
1.176 |> (if needs_type_tag_idempotence type_sys then
1.177 cons (type_tag_idempotence_fact ())
1.178 else