# HG changeset patch # User blanchet # Date 1387478263 -3600 # Node ID 152539a103d8cd58033bf0c8ad9c05cfd33b0826 # Parent 157c7dfcbcd87d50ca57c3408d2e4bdc957920ec tuning diff -r 157c7dfcbcd8 -r 152539a103d8 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 19 19:35:50 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 19 19:37:43 2013 +0100 @@ -2577,8 +2577,7 @@ | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 | do_type (APi (_, ty)) = do_type ty fun do_term pred_sym (ATerm ((name, tys), tms)) = - apsnd (do_sym name - (fn _ => default_type pred_sym (length tys) (length tms))) + apsnd (do_sym name (fn _ => default_type pred_sym (length tys) (length tms))) #> fold do_type tys #> fold (do_term false) tms | do_term _ (AAbs (((_, ty), tm), args)) = do_type ty #> do_term false tm #> fold (do_term false) args @@ -2608,17 +2607,11 @@ val ((cls, tys), syms) = undeclared_in_problem problem val decls = Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) - | (s, (cls, ())) => - cons (Class_Decl (class_decl_prefix ^ s, cls, []))) - cls [] @ + | (s, (cls, ())) => cons (Class_Decl (class_decl_prefix ^ s, cls, []))) cls [] @ Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) - | (s, (ty, ary)) => - cons (Type_Decl (type_decl_prefix ^ s, ty, ary))) - tys [] @ + | (s, (ty, ary)) => cons (Type_Decl (type_decl_prefix ^ s, ty, ary))) tys [] @ Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *) - | (s, (sym, ty)) => - cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) - syms [] + | (s, (sym, ty)) => cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) syms [] in (heading, decls) :: problem end fun all_ctrss_of_datatypes ctxt = @@ -2653,14 +2646,13 @@ val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish val ctrss = all_ctrss_of_datatypes ctxt fun firstorderize in_helper = - firstorderize_fact thy ctrss type_enc - (uncurried_aliases andalso not in_helper) completish sym_tab0 + firstorderize_fact thy ctrss type_enc (uncurried_aliases andalso not in_helper) completish + sym_tab0 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 ctrss mono type_enc - uncurried_aliases sym_tab0 sym_tab + uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab) |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false) @@ -2670,9 +2662,7 @@ |> map (firstorderize true) val all_facts = helpers @ conjs @ facts val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts - val datatypes = - datatypes_of_sym_table ctxt ctrss format type_enc uncurried_aliases - sym_tab + val datatypes = datatypes_of_sym_table ctxt ctrss format type_enc uncurried_aliases sym_tab val class_decl_lines = decl_lines_of_classes type_enc classes val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms) @@ -2691,8 +2681,7 @@ val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc - (K default_rank)) + |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank)) val free_type_lines = lines_of_free_types type_enc (facts @ conjs) val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs (* Reordering these might confuse the proof reconstruction code. *) @@ -2706,18 +2695,17 @@ (free_typesN, free_type_lines), (conjsN, conj_lines)] val problem = - problem |> (case format of - CNF => ensure_cnf_problem - | CNF_UEQ => filter_cnf_ueq_problem - | FOF => I - | _ => declare_undeclared_in_problem implicit_declsN) + problem + |> (case format of + CNF => ensure_cnf_problem + | CNF_UEQ => filter_cnf_ueq_problem + | FOF => I + | _ => declare_undeclared_in_problem implicit_declsN) val (problem, pool) = problem |> nice_atp_problem readable_names format - fun add_sym_ary (s, {min_ary, ...} : sym_info) = - min_ary > 0 ? Symtab.insert (op =) (s, min_ary) + fun add_sym_ary (s, {min_ary, ...} : sym_info) = min_ary > 0 ? Symtab.insert (op =) (s, min_ary) in - (problem, pool |> Option.map snd |> the_default Symtab.empty, - fact_names |> Vector.fromList, lifted, - Symtab.empty |> Symtab.fold add_sym_ary sym_tab) + (problem, pool |> Option.map snd |> the_default Symtab.empty, fact_names |> Vector.fromList, + lifted, Symtab.empty |> Symtab.fold add_sym_ary sym_tab) end (* FUDGE *) @@ -2731,8 +2719,7 @@ fun atp_problem_selection_weights problem = let fun add_term_weights weight (ATerm ((s, _), tms)) = - is_tptp_user_symbol s ? Symtab.default (s, weight) - #> fold (add_term_weights weight) tms + is_tptp_user_symbol s ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms | add_term_weights weight (AAbs ((_, tm), args)) = add_term_weights weight tm #> fold (add_term_weights weight) args fun add_line_weights weight (Formula (_, _, phi, _, _)) = @@ -2770,13 +2757,11 @@ fun may_be_predicator s = member (op =) [predicator_name, prefixed_predicator_name] s -fun strip_predicator (tm as ATerm ((s, _), [tm'])) = - if may_be_predicator s then tm' else tm +fun strip_predicator (tm as ATerm ((s, _), [tm'])) = if may_be_predicator s then tm' else tm | strip_predicator tm = tm fun make_head_roll (ATerm ((s, _), tms)) = - if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms) - else (s, tms) + if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms) else (s, tms) | make_head_roll _ = ("", []) fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi