tuning
authorblanchet
Thu, 19 Dec 2013 19:37:43 +0100
changeset 54830 152539a103d8
parent 54829 157c7dfcbcd8
child 54831 3587689271dd
tuning
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