# HG changeset patch # User blanchet # Date 1368702352 -7200 # Node ID 47b9302325f087a7fe44bf93f9c54f93eca8d550 # Parent 78e7a007ba28a46c0e18f3297cc59efcdbe3f1f3 tuning diff -r 78e7a007ba28 -r 47b9302325f0 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200 @@ -850,7 +850,7 @@ chop_fun (n - 1) ran_T |>> cons dom_T | chop_fun _ T = ([], T) -fun filter_type_args thy ctrs type_enc s ary T_args = +fun filter_type_args thy ctrss type_enc s ary T_args = let val poly = polymorphism_of_type_enc type_enc in if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *) T_args @@ -890,7 +890,7 @@ | Tags _ => [] else if level = Undercover_Types then noninfer_type_args T_args - else if member (op =) ctrs s andalso + else if exists (exists (curry (op =) s)) ctrss andalso level <> Const_Types Without_Ctr_Optim then ctr_infer_type_args T_args else @@ -1173,18 +1173,19 @@ I fun filter_type_args_in_const _ _ _ _ _ [] = [] - | filter_type_args_in_const thy ctrs type_enc ary s T_args = + | filter_type_args_in_const thy ctrss type_enc ary s T_args = case unprefix_and_unascii const_prefix s of NONE => if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] else T_args | SOME s'' => - filter_type_args thy ctrs type_enc (unmangled_invert_const s'') ary T_args -fun filter_type_args_in_iterm thy ctrs type_enc = + filter_type_args thy ctrss type_enc (unmangled_invert_const s'') ary + T_args +fun filter_type_args_in_iterm thy ctrss type_enc = let fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) | filt ary (IConst (name as (s, _), T, T_args)) = - filter_type_args_in_const thy ctrs type_enc ary s T_args + filter_type_args_in_const thy ctrss type_enc ary s T_args |> (fn T_args => IConst (name, T, T_args)) | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) | filt _ tm = tm @@ -1642,7 +1643,7 @@ |> mangle_type_args_in_iterm type_enc in list_app app [head, arg] end -fun firstorderize_fact thy ctrs type_enc sym_tab uncurried_aliases completish = +fun firstorderize_fact thy ctrss type_enc sym_tab uncurried_aliases completish = let fun do_app arg head = mk_app_op type_enc head arg fun list_app_ops (head, args) = fold do_app args head @@ -1690,7 +1691,7 @@ val do_iterm = not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators) - #> filter_type_args_in_iterm thy ctrs type_enc + #> filter_type_args_in_iterm thy ctrss type_enc in update_iformula (formula_map do_iterm) end (** Helper facts **) @@ -2565,7 +2566,7 @@ fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 sym_tab +fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab base_s0 types in_conj = let fun do_alias ary = @@ -2579,7 +2580,7 @@ mangle_type_args_in_const type_enc base_name T_args val base_ary = min_ary_of sym_tab0 base_s fun do_const name = IConst (name, T, T_args) - val filter_ty_args = filter_type_args_in_iterm thy ctrs type_enc + val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true) val name1 as (s1, _) = base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1) @@ -2610,7 +2611,7 @@ else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 sym_tab +fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => @@ -2618,19 +2619,19 @@ let val base_s0 = mangled_s |> unmangled_invert_const in - do_uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 sym_tab - base_s0 types in_conj min_ary + do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 + sym_tab base_s0 types in_conj min_ary end else ([], []) | NONE => ([], []) -fun uncurried_alias_lines_of_sym_table ctxt ctrs mono type_enc uncurried_aliases - sym_tab0 sym_tab = +fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc + uncurried_aliases sym_tab0 sym_tab = ([], []) |> uncurried_aliases ? Symtab.fold_rev (pair_append - o uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 + o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab) sym_tab val implicit_declsN = "Should-be-implicit typings" @@ -2716,11 +2717,9 @@ | is_poly_ctr (Datatype.DtType (_, Us)) = exists is_poly_ctr Us | is_poly_ctr _ = false -fun all_ctrs_of_polymorphic_datatypes thy = - Symtab.fold (snd #> #descr #> maps (#3 o snd) - #> (fn cs => exists (exists is_poly_ctr o snd) cs - ? append (map fst cs))) - (Datatype.get_all thy) [] +fun all_ctrss_of_datatypes thy = + Symtab.fold (snd #> #descr #> map (snd #> #3 #> map fst) #> append) + (Datatype.get_all thy) [] val app_op_and_predicator_threshold = 45 @@ -2759,15 +2758,15 @@ sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish - val ctrs = all_ctrs_of_polymorphic_datatypes thy + val ctrss = all_ctrss_of_datatypes thy fun firstorderize in_helper = - firstorderize_fact thy ctrs type_enc sym_tab0 + firstorderize_fact thy ctrss type_enc sym_tab0 (uncurried_aliases andalso not in_helper) completish val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) val (ho_stuff, sym_tab) = sym_table_of_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = - uncurried_alias_lines_of_sym_table ctxt ctrs mono type_enc + uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab)