1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:35 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:35 2011 +0200
1.3 @@ -1216,58 +1216,40 @@
1.4 end
1.5 handle TYPE _ => T_args
1.6
1.7 -fun enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys =
1.8 +fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
1.9 let
1.10 val thy = Proof_Context.theory_of ctxt
1.11 fun aux arity (CombApp (tm1, tm2)) =
1.12 CombApp (aux (arity + 1) tm1, aux 0 tm2)
1.13 | aux arity (CombConst (name as (s, _), T, T_args)) =
1.14 - let
1.15 - val level = level_of_type_sys type_sys
1.16 - val (T, T_args) =
1.17 - (* Aggressively merge most "hAPPs" if the type system is unsound
1.18 - anyway, by distinguishing overloads only on the homogenized
1.19 - result type. Don't do it for lightweight type systems, though,
1.20 - since it leads to too many unsound proofs. *)
1.21 - if s = prefixed_app_op_name andalso length T_args = 2 andalso
1.22 - not (is_type_sys_virtually_sound type_sys) andalso
1.23 - heaviness_of_type_sys type_sys = Heavyweight then
1.24 - T_args |> map (homogenized_type ctxt nonmono_Ts level 0)
1.25 - |> (fn Ts => let val T = hd Ts --> nth Ts 1 in
1.26 - (T --> T, tl Ts)
1.27 - end)
1.28 - else
1.29 - (T, T_args)
1.30 - in
1.31 - (case strip_prefix_and_unascii const_prefix s of
1.32 - NONE => (name, T_args)
1.33 - | SOME s'' =>
1.34 - let
1.35 - val s'' = invert_const s''
1.36 - fun filtered_T_args false = T_args
1.37 - | filtered_T_args true = filter_type_args thy s'' arity T_args
1.38 - in
1.39 - case type_arg_policy type_sys s'' of
1.40 - Explicit_Type_Args drop_args =>
1.41 - (name, filtered_T_args drop_args)
1.42 - | Mangled_Type_Args drop_args =>
1.43 - (mangled_const_name format type_sys (filtered_T_args drop_args)
1.44 - name, [])
1.45 - | No_Type_Args => (name, [])
1.46 - end)
1.47 - |> (fn (name, T_args) => CombConst (name, T, T_args))
1.48 - end
1.49 + (case strip_prefix_and_unascii const_prefix s of
1.50 + NONE => (name, T_args)
1.51 + | SOME s'' =>
1.52 + let
1.53 + val s'' = invert_const s''
1.54 + fun filtered_T_args false = T_args
1.55 + | filtered_T_args true = filter_type_args thy s'' arity T_args
1.56 + in
1.57 + case type_arg_policy type_sys s'' of
1.58 + Explicit_Type_Args drop_args =>
1.59 + (name, filtered_T_args drop_args)
1.60 + | Mangled_Type_Args drop_args =>
1.61 + (mangled_const_name format type_sys (filtered_T_args drop_args)
1.62 + name, [])
1.63 + | No_Type_Args => (name, [])
1.64 + end)
1.65 + |> (fn (name, T_args) => CombConst (name, T, T_args))
1.66 | aux _ tm = tm
1.67 in aux 0 end
1.68
1.69 -fun repair_combterm ctxt format nonmono_Ts type_sys sym_tab =
1.70 +fun repair_combterm ctxt format type_sys sym_tab =
1.71 not (is_setting_higher_order format type_sys)
1.72 ? (introduce_explicit_apps_in_combterm sym_tab
1.73 #> introduce_predicators_in_combterm sym_tab)
1.74 - #> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys
1.75 -fun repair_fact ctxt format nonmono_Ts type_sys sym_tab =
1.76 + #> enforce_type_arg_policy_in_combterm ctxt format type_sys
1.77 +fun repair_fact ctxt format type_sys sym_tab =
1.78 update_combformula (formula_map
1.79 - (repair_combterm ctxt format nonmono_Ts type_sys sym_tab))
1.80 + (repair_combterm ctxt format type_sys sym_tab))
1.81
1.82 (** Helper facts **)
1.83
1.84 @@ -1441,10 +1423,9 @@
1.85
1.86 val type_pred = `make_fixed_const type_pred_name
1.87
1.88 -fun type_pred_combterm ctxt format nonmono_Ts type_sys T tm =
1.89 - (CombConst (type_pred, T --> @{typ bool}, [T])
1.90 - |> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys, tm)
1.91 - |> CombApp
1.92 +fun type_pred_combterm ctxt format type_sys T tm =
1.93 + CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1.94 + |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
1.95
1.96 fun var_occurs_positively_naked_in_term _ (SOME false) _ accum = accum
1.97 | var_occurs_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1.98 @@ -1458,7 +1439,7 @@
1.99
1.100 fun tag_with_type ctxt format nonmono_Ts type_sys T tm =
1.101 CombConst (type_tag, T --> T, [T])
1.102 - |> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts type_sys
1.103 + |> enforce_type_arg_policy_in_combterm ctxt format type_sys
1.104 |> term_from_combterm ctxt format nonmono_Ts type_sys Top_Level
1.105 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
1.106 and term_from_combterm ctxt format nonmono_Ts type_sys =
1.107 @@ -1497,7 +1478,7 @@
1.108 if should_predicate_on_type ctxt nonmono_Ts type_sys
1.109 (fn () => should_predicate_on_var pos phi universal name) T then
1.110 CombVar (name, T)
1.111 - |> type_pred_combterm ctxt format nonmono_Ts type_sys T
1.112 + |> type_pred_combterm ctxt format type_sys T
1.113 |> do_term |> AAtom |> SOME
1.114 else
1.115 NONE
1.116 @@ -1639,7 +1620,8 @@
1.117 out with monotonicity" paper presented at CADE 2011. *)
1.118 fun add_combterm_nonmonotonic_types _ _ (SOME false) _ = I
1.119 | add_combterm_nonmonotonic_types ctxt level _
1.120 - (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
1.121 + (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
1.122 + tm2)) =
1.123 (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
1.124 (case level of
1.125 Nonmonotonic_Types =>
1.126 @@ -1697,7 +1679,7 @@
1.127 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1.128 CombConst ((s, s'), T, T_args)
1.129 |> fold (curry (CombApp o swap)) bounds
1.130 - |> type_pred_combterm ctxt format nonmono_Ts type_sys res_T
1.131 + |> type_pred_combterm ctxt format type_sys res_T
1.132 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1.133 |> formula_from_combformula ctxt format nonmono_Ts type_sys
1.134 (K (K (K (K true)))) true
1.135 @@ -1832,7 +1814,7 @@
1.136 facts
1.137 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1.138 val nonmono_Ts = conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys
1.139 - val repair = repair_fact ctxt format nonmono_Ts type_sys sym_tab
1.140 + val repair = repair_fact ctxt format type_sys sym_tab
1.141 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1.142 val repaired_sym_tab =
1.143 conjs @ facts |> sym_table_for_facts ctxt (SOME false)