# HG changeset patch # User blanchet # Date 1308143478 -7200 # Node ID b35ff420d72094399f9ce14ecfc0306da23fc20a # Parent e93dfcb53535b8a59d7d7ffa39c6a9cdd0b98fc9# Parent 7ee98a3802af513cc7a01fabe6878949672c54bd merge diff -r 7ee98a3802af -r b35ff420d720 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Jun 14 17:24:23 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 15 15:11:18 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]) @@ -1699,22 +1700,24 @@ |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary)) end -fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false - 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) else (Axiom, I) val (arg_Ts, res_T) = chop_fun ary T + val num_args = length arg_Ts val bound_names = - 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int) + 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 = - arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T - else 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, @@ -1722,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 @@ -1731,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 ^ @@ -1753,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, @@ -1786,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) @@ -1806,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 @@ -1821,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 @@ -1871,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 @@ -1880,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 diff -r 7ee98a3802af -r b35ff420d720 src/HOL/ex/ATP_Export.thy --- a/src/HOL/ex/ATP_Export.thy Tue Jun 14 17:24:23 2011 +0200 +++ b/src/HOL/ex/ATP_Export.thy Wed Jun 15 15:11:18 2011 +0200 @@ -4,23 +4,31 @@ begin ML {* -val do_it = false; (* switch to true to generate files *) +val do_it = false; (* switch to "true" to generate files *) val thy = @{theory Complex_Main}; val ctxt = @{context} *} ML {* if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy true - "/tmp/infs_full_types.tptp" + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds" + "/tmp/infs_poly_preds.tptp" else () *} ML {* if do_it then - ATP_Export.generate_tptp_inference_file_for_theory ctxt thy false - "/tmp/infs_partial_types.tptp" + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags" + "/tmp/infs_poly_tags.tptp" +else + () +*} + +ML {* +if do_it then + ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy" + "/tmp/infs_poly_tags_heavy.tptp" else () *} diff -r 7ee98a3802af -r b35ff420d720 src/HOL/ex/atp_export.ML --- a/src/HOL/ex/atp_export.ML Tue Jun 14 17:24:23 2011 +0200 +++ b/src/HOL/ex/atp_export.ML Wed Jun 15 15:11:18 2011 +0200 @@ -11,7 +11,7 @@ val generate_tptp_graph_file_for_theory : Proof.context -> theory -> string -> unit val generate_tptp_inference_file_for_theory : - Proof.context -> theory -> bool -> string -> unit + Proof.context -> theory -> string -> string -> unit end; structure ATP_Export : ATP_EXPORT = @@ -87,15 +87,10 @@ val add_inferences_to_problem = map o apsnd o map o add_inferences_to_problem_line -fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name = +fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name = let val format = ATP_Problem.FOF - val type_sys = - ATP_Translate.Preds - (ATP_Translate.Polymorphic, - if full_types then ATP_Translate.All_Types - else ATP_Translate.Const_Arg_Types, - ATP_Translate.Heavyweight) + val type_sys = type_sys |> ATP_Translate.type_sys_from_string val path = file_name |> Path.explode val _ = File.write path "" val facts0 = facts_of thy