# HG changeset patch
# User blanchet
# Date 1328104426 -3600
# Node ID a7538ad74997c79257179a7875b13d1ddeee65d7
# Parent  e7445478d90b923c7033466922aa5abd71488fa9
tuning

diff -r e7445478d90b -r a7538ad74997 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Feb 01 12:47:43 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Feb 01 14:53:46 2012 +0100
@@ -1377,6 +1377,8 @@
              {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
               in_conj = false})
 
+datatype explicit_apply = Incomplete_Apply | Sufficient_Apply | Full_Apply
+
 fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts =
   let
     fun consider_var_ary const_T var_T max_ary =
@@ -1389,7 +1391,7 @@
             iter (ary + 1) (range_type T)
       in iter 0 const_T end
     fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
-      if explicit_apply = NONE andalso
+      if explicit_apply = Sufficient_Apply andalso
          (can dest_funT T orelse T = @{typ bool}) then
         let
           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
@@ -1431,11 +1433,11 @@
                         val types' = types |> insert_type ctxt I T
                         val in_conj = in_conj orelse conj_fact
                         val min_ary =
-                          if is_some explicit_apply orelse
-                             pointer_eq (types', types) then
+                          if explicit_apply = Sufficient_Apply andalso
+                             not (pointer_eq (types', types)) then
+                            fold (consider_var_ary T) fun_var_Ts min_ary
+                          else
                             min_ary
-                          else
-                            fold (consider_var_ary T) fun_var_Ts min_ary
                       in
                         Symtab.update (s, {pred_sym = pred_sym,
                                            min_ary = Int.min (ary, min_ary),
@@ -1448,9 +1450,10 @@
                         val pred_sym = top_level andalso not bool_vars
                         val min_ary =
                           case explicit_apply of
-                            SOME true => 0
-                          | SOME false => ary
-                          | NONE => fold (consider_var_ary T) fun_var_Ts ary
+                            Incomplete_Apply => ary
+                          | Sufficient_Apply =>
+                            fold (consider_var_ary T) fun_var_Ts ary
+                          | Full_Apply => 0
                       in
                         Symtab.update_new (s,
                             {pred_sym = pred_sym, min_ary = min_ary,
@@ -2436,10 +2439,6 @@
   |> List.partition is_poly_constr
   |> pairself (map fst)
 
-(* Forcing explicit applications is expensive for polymorphic encodings, because
-   it takes only one existential variable ranging over "'a => 'b" to ruin
-   everything. Hence we do it only if there are few facts (which is normally the
-   case for "metis" and the minimizer). *)
 val explicit_apply_threshold = 50
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
@@ -2447,12 +2446,16 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
+    (* Forcing explicit applications is expensive for polymorphic encodings,
+       because it takes only one existential variable ranging over "'a => 'b" to
+       ruin everything. Hence we do it only if there are few facts (which is
+       normally the case for "metis" and the minimizer). *)
     val explicit_apply =
       if polymorphism_of_type_enc type_enc = Polymorphic andalso
          length facts >= explicit_apply_threshold then
-        SOME false
+        Incomplete_Apply
       else
-        NONE
+        Sufficient_Apply
     val lam_trans =
       if lam_trans = keep_lamsN andalso
          not (is_type_enc_higher_order type_enc) then
@@ -2472,7 +2475,7 @@
     val firstorderize =
       firstorderize_fact thy monom_constrs format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
-    val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts
+    val sym_tab = sym_table_for_facts ctxt type_enc Incomplete_Apply conjs facts
     val helpers =
       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
               |> map firstorderize