refactor(kernel/instantiate): rename instantiate_params to instantiate_univ_params

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/converter.cpp

@@ -167,7 +167,7 @@ struct default_converter : public converter {
         if (is_constant(e)) {
             if (auto d = m_env.find(const_name(e))) {
                 if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w)
-                    return unfold_name_core(instantiate_params(d->get_value(), d->get_univ_params(), const_levels(e)), w);
+                    return unfold_name_core(instantiate_univ_params(d->get_value(), d->get_univ_params(), const_levels(e)), w);
             }
         }
         return e;

src/kernel/inductive/inductive.cpp

@@ -799,7 +799,7 @@ optional<expr> inductive_normalizer_extension::operator()(expr const & e, extens
         ACebu.push_back(intro_args[it1->m_num_params + i]);
     std::reverse(ACebu.begin(), ACebu.end());
     expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data());
-    r = instantiate_params(r, it1->m_level_names, const_levels(elim_fn));
+    r = instantiate_univ_params(r, it1->m_level_names, const_levels(elim_fn));
     return some_expr(r);
 }
 

src/kernel/instantiate.cpp

@@ -130,7 +130,7 @@ expr beta_reduce(expr t) {
     }
 }
 
-expr instantiate_params(expr const & e, level_param_names const & ps, levels const & ls) {
+expr instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls) {
     if (!has_param_univ(e))
         return e;
     return replace(e, [&](expr const & e, unsigned) -> optional<expr> {

src/kernel/instantiate.h

@@ -31,5 +31,5 @@ expr beta_reduce(expr t);
 
     \pre length(ps) == length(ls)
 */
-expr instantiate_params(expr const & e, level_param_names const & ps, levels const & ls);
+expr instantiate_univ_params(expr const & e, level_param_names const & ps, levels const & ls);
 }

src/kernel/type_checker.cpp

@@ -260,7 +260,7 @@ expr type_checker::infer_type_core(expr const & e, bool infer_only) {
             for (level const & l : ls)
                 check_level(l, e);
         }
-        r = instantiate_params(d.get_type(), ps, ls);
+        r = instantiate_univ_params(d.get_type(), ps, ls);
         break;
     }
     case expr_kind::Macro: {

src/library/coercion.cpp

@@ -177,12 +177,12 @@ struct add_coercion_fn {
         if (length(const_levels(D_cnst)) != length(g_level_params))
             return;
         // C >-> D >-> E
-        g  = instantiate_params(g, g_level_params, const_levels(D_cnst));
+        g  = instantiate_univ_params(g, g_level_params, const_levels(D_cnst));
         expr gf = apply_beta(g, gf_args.size(), gf_args.data());
         expr gf_type = g_type;
         while (is_pi(gf_type))
             gf_type = binding_body(gf_type);
-        gf_type = instantiate(instantiate_params(gf_type, g_level_params, const_levels(D_cnst)), gf_args.size(), gf_args.data());
+        gf_type = instantiate(instantiate_univ_params(gf_type, g_level_params, const_levels(D_cnst)), gf_args.size(), gf_args.data());
         unsigned i = f_arg_types.size();
         while (i > 0) {
             --i;
@@ -380,7 +380,7 @@ optional<expr> get_coercion(environment const & env, expr const & C, coercion_cl
         return none_expr();
     for (coercion_info const & info : *it) {
         if (info.m_to == D && info.m_num_args == args.size() && length(info.m_level_params) == length(const_levels(C_fn))) {
-            expr f = instantiate_params(info.m_fun, info.m_level_params, const_levels(C_fn));
+            expr f = instantiate_univ_params(info.m_fun, info.m_level_params, const_levels(C_fn));
             return some_expr(apply_beta(f, args.size(), args.data()));
         }
     }
@@ -413,9 +413,9 @@ bool get_user_coercions(environment const & env, expr const & C, buffer<std::tup
         if (info.m_to.kind() == coercion_class_kind::User &&
             info.m_num_args == args.size() &&
             length(info.m_level_params) == length(const_levels(C_fn))) {
-            expr f = instantiate_params(info.m_fun, info.m_level_params, const_levels(C_fn));
+            expr f = instantiate_univ_params(info.m_fun, info.m_level_params, const_levels(C_fn));
             expr c = apply_beta(f, args.size(), args.data());
-            expr t = instantiate_params(info.m_fun_type, info.m_level_params, const_levels(C_fn));
+            expr t = instantiate_univ_params(info.m_fun_type, info.m_level_params, const_levels(C_fn));
             for (unsigned i = 0; i < args.size(); i++) t = binding_body(t);
             t = instantiate(t, args.size(), args.data());
             result.emplace_back(info.m_to.get_name(), c, t);

src/library/kernel_bindings.cpp

@@ -646,8 +646,8 @@ static int expr_instantiate(lua_State * L) {
     }
 }
 
-static int expr_instantiate_level_params(lua_State * L) {
+static int expr_instantiate_univ_params(lua_State * L) {
-    return push_expr(L, instantiate_params(to_expr(L, 1), to_level_param_names(L, 2), to_list_level_ext(L, 3)));
+    return push_expr(L, instantiate_univ_params(to_expr(L, 1), to_level_param_names(L, 2), to_list_level_ext(L, 3)));
 }
 
 static int expr_abstract(lua_State * L) {
@@ -732,7 +732,7 @@ static const struct luaL_Reg expr_m[] = {
     {"lift_free_vars",   safe_function<expr_lift_free_vars>},
     {"lower_free_vars",  safe_function<expr_lower_free_vars>},
     {"instantiate",      safe_function<expr_instantiate>},
-    {"instantiate_levels", safe_function<expr_instantiate_level_params>},
+    {"instantiate_univs", safe_function<expr_instantiate_univ_params>},
     {"abstract",         safe_function<expr_abstract>},
     {"occurs",           safe_function<expr_occurs>},
     {"is_eqp",           safe_function<expr_is_eqp>},

src/library/tactic/tactic.cpp

@@ -328,7 +328,7 @@ protected:
     virtual expr visit_constant(expr const & c) {
         if (const_name(c) == m_name) {
             m_unfolded = true;
-            return instantiate_params(m_def, m_ps, const_levels(c));
+            return instantiate_univ_params(m_def, m_ps, const_levels(c));
         } else {
             return c;
         }
@@ -346,7 +346,7 @@ protected:
         optional<declaration> d = m_env.find(const_name(c));
         if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) {
             m_unfolded = true;
-            return instantiate_params(d->get_value(), d->get_univ_params(), const_levels(c));
+            return instantiate_univ_params(d->get_value(), d->get_univ_params(), const_levels(c));
         } else {
             return c;
         }