# HG changeset patch
# User desharna
# Date 1642856436 -3600
# Node ID 4106bc2a9cc8d348e145d97b1781cc2916b10d5d
# Parent  8dc52ba4155b6f8ef943625e8f2c50e5c673d90b
optimized app_op_level selection in TPTP generation

diff -r 8dc52ba4155b -r 4106bc2a9cc8 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jan 22 12:05:09 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jan 22 14:00:36 2022 +0100
@@ -2834,7 +2834,8 @@
     val app_op_level =
       if completish > 0 then
         Full_App_Op_And_Predicator
-      else if length facts + length hyp_ts >= app_op_and_predicator_threshold then
+      else if is_greater_equal
+        (compare_length_with facts (app_op_and_predicator_threshold - length hyp_ts)) then
         if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op
       else
         Sufficient_App_Op_And_Predicator
diff -r 8dc52ba4155b -r 4106bc2a9cc8 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Sat Jan 22 12:05:09 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Jan 22 14:00:36 2022 +0100
@@ -49,6 +49,7 @@
   val extract_lambda_def : (term -> string * typ) -> term -> string * term
   val short_thm_name : Proof.context -> thm -> string
   val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
+  val compare_length_with : 'a list -> int -> order
 end;
 
 structure ATP_Util : ATP_UTIL =
@@ -412,6 +413,11 @@
     else long
   end
 
-  val map_prod = Ctr_Sugar_Util.map_prod
+val map_prod = Ctr_Sugar_Util.map_prod
+
+(* Compare the length of a list with an integer n while traversing at most n elements of the list.
+*)
+fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS
+  | compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1)
 
 end;