src/HOL/Tools/ATP/atp_problem_generate.ML

   val helper_table : ((string * bool) * (status * thm) list) list
   val trans_lams_of_string :
     Proof.context -> type_enc -> string -> term list -> term list * term list
   val string_of_status : status -> string
   val factsN : string
-  val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode ->
-    string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list ->
-    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
+  val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc ->
+    mode -> string -> bool -> bool -> bool -> term list -> term ->
+    ((string * stature) * term) list -> string atp_problem * string Symtab.table
+    * (string * term) list * int Symtab.table
   val atp_problem_selection_weights : string atp_problem -> (string * real) list
   val atp_problem_term_order_info : string atp_problem -> (string * int) list
 end;
 
 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =

   | string_of_status Rec_Def = rec_defN
 
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP forbids name clashes, and some of the remote
    provers might care. *)
-fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank
+fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank
         (j, {name, stature = (_, status), role, iformula, atomic_types}) =
   Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
             encode name, alt name),
            role,
            iformula
            |> formula_of_iformula ctxt mono type_enc
                   should_guard_var_in_formula (if pos then SOME true else NONE)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types,
-           NONE, isabelle_info (string_of_status status) (rank j))
-
-fun lines_of_subclass type_enc sub super =
+           NONE, isabelle_info generate_info (string_of_status status) (rank j))
+
+fun lines_of_subclass generate_info type_enc sub super =
   Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
            AConn (AImplies,
                   [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
            |> bound_tvars type_enc false [tvar_a],
-           NONE, isabelle_info inductiveN helper_rank)
-
-fun lines_of_subclass_pair type_enc (sub, supers) =
+           NONE, isabelle_info generate_info inductiveN helper_rank)
+
+fun lines_of_subclass_pair generate_info type_enc (sub, supers) =
   if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
-    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
-                 map (`make_class) supers)]
+    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)]
   else
-    map (lines_of_subclass type_enc sub) supers
-
-fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
+    map (lines_of_subclass generate_info type_enc sub) supers
+
+fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) =
   if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
     Class_Memb (class_memb_prefix ^ name,
       map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
       native_atp_type_of_typ type_enc false 0 T, `make_class cl)
   else
     Formula ((tcon_clause_prefix ^ name, ""), Axiom,
              mk_ahorn (maps (class_atoms type_enc) prems)
                       (class_atom type_enc (cl, T))
              |> bound_tvars type_enc true (snd (dest_Type T)),
-             NONE, isabelle_info inductiveN helper_rank)
-
-fun line_of_conjecture ctxt mono type_enc
-                       ({name, role, iformula, atomic_types, ...} : ifact) =
+             NONE, isabelle_info generate_info inductiveN helper_rank)
+
+fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =
   Formula ((conjecture_prefix ^ name, ""), role,
            iformula
-           |> formula_of_iformula ctxt mono type_enc
-                  should_guard_var_in_formula (SOME false)
+           |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types, NONE, [])
 
 fun lines_of_free_types type_enc (facts : ifact list) =
   if is_type_enc_polymorphic type_enc then

     [] |> (is_type_enc_polymorphic type_enc andalso
            is_type_level_monotonicity_based level)
           ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
   end
 
-fun line_of_guards_mono_type ctxt mono type_enc T =
+fun line_of_guards_mono_type ctxt generate_info mono type_enc T =
   Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
            Axiom,
            IConst (`make_bound_var "X", T, [])
            |> type_guard_iterm type_enc T
            |> AAtom
            |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula
                                   (SOME true)
            |> close_formula_universally
            |> bound_tvars type_enc true (atomic_types_of T),
-           NONE, isabelle_info inductiveN helper_rank)
-
-fun line_of_tags_mono_type ctxt mono type_enc T =
+           NONE, isabelle_info generate_info inductiveN helper_rank)
+
+fun line_of_tags_mono_type ctxt generate_info mono type_enc T =
   let val x_var = ATerm ((`make_bound_var "X", []), []) in
     Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom,
              eq_formula type_enc (atomic_types_of T) [] false
                   (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
-             NONE, isabelle_info non_rec_defN helper_rank)
+             NONE, isabelle_info generate_info non_rec_defN helper_rank)
   end
 
-fun lines_of_mono_types ctxt mono type_enc =
+fun lines_of_mono_types ctxt generate_info mono type_enc =
   (case type_enc of
     Native _ => K []
-  | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc)
-  | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc))
+  | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc)
+  | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc))
 
 fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
   let
     val thy = Proof_Context.theory_of ctxt
     val (T, T_args) =

                    ? curry APi (map (tvar_name o dest_TVar) T_args))
   end
 
 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
 
-fun line_of_guards_sym_decl ctxt mono type_enc n s j
-                            (s', T_args, T, _, ary, in_conj) =
+fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j
+    (s', T_args, T, _, ary, in_conj) =
   let
     val thy = Proof_Context.theory_of ctxt
     val (role, maybe_negate) = honor_conj_sym_role in_conj
     val (arg_Ts, res_T) = chop_fun ary T
     val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int)

              |> formula_of_iformula ctxt mono type_enc
                                     always_guard_var_in_formula (SOME true)
              |> close_formula_universally
              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
              |> maybe_negate,
-             NONE, isabelle_info inductiveN helper_rank)
+             NONE, isabelle_info generate_info inductiveN helper_rank)
   end
 
-fun lines_of_tags_sym_decl ctxt mono type_enc n s
-                           (j, (s', T_args, T, pred_sym, ary, in_conj)) =
+fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s
+    (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   let
     val thy = Proof_Context.theory_of ctxt
     val level = level_of_type_enc type_enc
     val ident =
       tags_sym_formula_prefix ^ s ^

     val cst = mk_aterm type_enc (s, s') T_args
     val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym
     val tag_with = tag_with_type ctxt mono type_enc NONE
     fun formula c =
       [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
-                isabelle_info non_rec_defN helper_rank)]
+                isabelle_info generate_info non_rec_defN helper_rank)]
   in
     if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
       []
     else if level = Undercover_Types then
       let

       if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
       else decls
     end
   | rationalize_decls _ decls = decls
 
-fun lines_of_sym_decls ctxt mono type_enc (s, decls) =
+fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) =
   (case type_enc of
     Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)]
   | Guards (_, level) =>
     let
       val thy = Proof_Context.theory_of ctxt
       val decls = decls |> rationalize_decls thy
       val n = length decls
       val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
     in
-      (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
+      (0 upto length decls - 1, decls)
+      |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)
     end
   | Tags (_, level) =>
     if is_type_level_uniform level then
       []
     else
       let val n = length decls in
-        (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
+        (0 upto n - 1 ~~ decls)
+        |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
       end)
 
-fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
+fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab =
   let
     val syms = sym_decl_tab |> Symtab.dest |> sort_by fst
-    val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts
-    val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
+    val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts
+    val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms
   in mono_lines @ decl_lines end
 
 fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
       sym_tab =
     if is_type_enc_polymorphic type_enc then

     Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs, exhaust)
   end
 
 fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
 
-fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
-                                    base_s0 types in_conj =
+fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0
+    types in_conj =
   let
     fun do_alias ary =
       let
         val thy = Proof_Context.theory_of ctxt
         val (role, maybe_negate) = honor_conj_sym_role in_conj

           eq_formula type_enc (atomic_types_of T) (map (apsnd do_bound_type) bounds) false
             (atp_term_of tm1) (atp_term_of tm2)
       in
         ([tm1, tm2],
          [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE,
-            isabelle_info non_rec_defN helper_rank)])
+            isabelle_info generate_info non_rec_defN helper_rank)])
         |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
             else pair_append (do_alias (ary - 1)))
       end
   in do_alias end
 
-fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
+fun uncurried_alias_lines_of_sym ctxt generate_info 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 =>
     if String.isSubstring uncurried_alias_sep mangled_s then
       let val base_s0 = mangled_s |> unmangled_invert_const in
-        do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab base_s0 types
-          in_conj min_ary
+        do_uncurried_alias_lines_of_sym ctxt generate_info 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 ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab =
+fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
+    sym_tab0 sym_tab =
   ([], [])
   |> uncurried_aliases
-    ? Symtab.fold_rev
-        (pair_append o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab)
-        sym_tab
+    ? Symtab.fold_rev (pair_append
+        o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab)
+      sym_tab
 
 val implicit_declsN = "Could-be-implicit typings"
 val explicit_declsN = "Explicit typings"
 val uncurried_alias_eqsN = "Uncurried aliases"
 val factsN = "Relevant facts"

 
 val all_ctrss_of_datatypes = map (map_filter (try dest_Const) o #ctrs) o Ctr_Sugar.ctr_sugars_of
 
 val app_op_and_predicator_threshold = 45
 
-fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
-    readable_names presimp hyp_ts concl_t facts =
+fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans
+    uncurried_aliases readable_names presimp hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
     val type_enc = type_enc |> adjust_type_enc format
     val completish = (mode = Sledgehammer_Completish)
     (* Forcing explicit applications is expensive for polymorphic encodings,

         sym_tab0
     val (conjs, facts) = (conjs, facts) |> apply2 (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 generate_info 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)
               uncurried_alias_eq_tms
     val helpers =

     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)
       |> sym_decl_table_of_facts thy type_enc sym_tab
-      |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
+      |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts
     val datatype_decl_lines = map decl_line_of_datatype datatypes
     val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
     val num_facts = length facts
     val freshen = mode <> Exporter andalso mode <> Translator
     val pos = mode <> Exporter
     val rank_of = rank_of_fact_num num_facts
     val fact_lines =
-      map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of)
+      map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of)
         (0 upto num_facts - 1 ~~ facts)
-    val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
-    val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
+    val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs
+    val tcon_lines = map (line_of_tcon_clause generate_info 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 generate_info 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. *)
     val problem =
       [(explicit_declsN, decl_lines),