# HG changeset patch
# User desharna
# Date 1639142427 -3600
# Node ID 68a0f9a8561dcfcefcb7593ad64305869ad70430
# Parent  89318c9131e840919adc1ab6e67a9f774fdb9650
tuned ATP to use map_index

diff -r 89318c9131e8 -r 68a0f9a8561d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Dec 12 20:38:47 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Dec 10 14:20:27 2021 +0100
@@ -458,8 +458,7 @@
 fun make_axiom_tcon_clause (s, name, (cl, args)) =
   let
     val args = args |> map normalize_classes
-    val tvars =
-      1 upto length args |> map (fn j => TVar ((tvar_a_str, j), \<^sort>\<open>type\<close>))
+    val tvars = args |> map_index (fn (j, _) => TVar ((tvar_a_str, j + 1), \<^sort>\<open>type\<close>))
   in (name, args ~~ tvars, (cl, Type (s, tvars))) end
 
 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
@@ -857,12 +856,9 @@
   | do_cheaply_conceal_lambdas _ t = t
 
 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
-fun conceal_bounds Ts t =
-  subst_bounds (map (Free o apfst concealed_bound_name)
-                    (0 upto length Ts - 1 ~~ Ts), t)
+fun conceal_bounds Ts t = subst_bounds (map_index (Free o apfst concealed_bound_name) Ts, t)
 fun reveal_bounds Ts =
-  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
-                    (0 upto length Ts - 1 ~~ Ts))
+  subst_atomic (map_index (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) Ts)
 
 fun do_introduce_combinators ctxt Ts t =
   (t |> conceal_bounds Ts
@@ -917,7 +913,7 @@
       val head_T = fastype_of head
       val n = length args
       val arg_Ts = head_T |> binder_types |> take n |> rev
-      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
+      val u = u |> subst_atomic (map_index (swap o apfst Bound) args)
     in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
   | intentionalize_def t = t
 
@@ -1429,11 +1425,9 @@
     val (facts, lambda_ts) =
       facts |> map (snd o snd) |> trans_lams
             |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts
-    val lam_facts =
-      map2 (fn t => fn j =>
-               ((lam_fact_prefix ^ Int.toString j,
-                 (Global, Non_Rec_Def)), (Axiom, t)))
-           lambda_ts (1 upto length lambda_ts)
+    val lam_facts = lambda_ts
+      |> map_index (fn (j, t) =>
+         ((lam_fact_prefix ^ Int.toString (j + 1), (Global, Non_Rec_Def)), (Axiom, t)))
   in (facts, lam_facts) end
 
 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to
@@ -1525,7 +1519,7 @@
       if forall null footprint then
         []
       else
-        0 upto length footprint - 1 ~~ footprint
+        map_index I footprint
         |> sort (rev_order o list_ord Term_Ord.indexname_ord o apply2 snd)
         |> cover []
     end
@@ -2094,7 +2088,7 @@
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
       map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
-      |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
+      |> map_index (apfst (rpair (Local, General) o string_of_int))
     val ((conjs, facts), lam_facts) =
       (conjs, facts)
       |> presimp ? apply2 (map (apsnd (apsnd (presimp_prop simp_options ctxt type_enc))))
@@ -2145,8 +2139,7 @@
           val ary = length tms
           val cover = type_arg_cover thy pos s ary
         in
-          exists (fn (j, tm) => tm = var andalso member (op =) cover j)
-                 (0 upto ary - 1 ~~ tms) orelse
+          exists (fn (j, tm) => tm = var andalso member (op =) cover j) (map_index I tms) orelse
           exists is_undercover tms
         end
       | is_undercover _ = true
@@ -2199,7 +2192,7 @@
               val ary = length args
               fun arg_site j = if is_tptp_equal s then Eq_Arg pos else Arg (s, j, ary)
             in
-              map2 (fn j => term (arg_site j)) (0 upto ary - 1) args
+              map_index (fn (j, arg) => term (arg_site j) arg) args
               |> mk_aterm type_enc name T_args
             end
           | IVar (name, _) =>
@@ -2313,7 +2306,7 @@
   if is_type_enc_polymorphic type_enc then
     let
       val type_classes = (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
-      fun line j (cl, T) =
+      fun line (j, (cl, T)) =
         if type_classes then
           Class_Memb (class_memb_prefix ^ string_of_int j, [],
             native_atp_type_of_typ type_enc false 0 T, `make_class cl)
@@ -2324,7 +2317,7 @@
         fold (union (op =)) (map #atomic_types facts) []
         |> class_membs_of_types type_enc add_sorts_on_tfree
     in
-      map2 line (0 upto length membs - 1) membs
+      map_index line membs
     end
   else
     []
@@ -2543,14 +2536,13 @@
     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)
-    val bounds =
-      bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
+    val bounds = map2 (fn name => fn T => IConst (name, T, [])) bound_names arg_Ts
     val bound_Ts =
       (case level_of_type_enc type_enc of
         All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts
       | Undercover_Types =>
         let val cover = type_arg_cover thy NONE s ary in
-          map2 (fn j => if member (op =) cover j then SOME else K NONE) (0 upto ary - 1) arg_Ts
+          map_index (fn (j, arg_T) => if member (op =) cover j then SOME arg_T else NONE) arg_Ts
         end
       | _ => replicate ary NONE)
   in
@@ -2594,7 +2586,7 @@
       let
         val cover = type_arg_cover thy NONE s ary
         fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T
-        val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts)
+        val bounds = bounds |> map2 maybe_tag (map_index I arg_Ts)
       in formula (cst bounds) end
     else
       formula (cst bounds)
@@ -2621,15 +2613,14 @@
       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 generate_info mono type_enc n s)
+      map_index (uncurry (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)) decls
     end
   | Tags (_, level) =>
     if is_type_level_uniform level then
       []
     else
       let val n = length decls in
-        (0 upto n - 1 ~~ decls)
+        map_index I decls
         |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
       end)
 
@@ -2883,15 +2874,15 @@
     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 generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of)
-        (0 upto num_facts - 1 ~~ facts)
+    val fact_lines = facts
+      |> map_index (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc
+         rank_of)
+
     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 generate_info helper_prefix I (K "") false true mono type_enc
-        (K default_rank))
+    val helper_lines = helpers
+      |> map_index (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. *)
@@ -2948,7 +2939,7 @@
           fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
                             / Real.fromInt num_facts
       in
-        map weight_of (0 upto num_facts - 1) ~~ facts
+        map_index (apfst weight_of) facts
         |> fold (uncurry add_line_weights)
       end
     val get = these o AList.lookup (op =) problem