# 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>\type\)) + val tvars = args |> map_index (fn (j, _) => TVar ((tvar_a_str, j + 1), \<^sort>\type\)) 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