refactor(kernel/metavar): add method instantiate as alias for instantiate_metavars_wo_jst

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

src/frontends/lean/elaborator.cpp

@@ -628,7 +628,7 @@ public:
 
     optional<tactic> get_tactic_for(substitution const & substitution, expr const & mvar) {
         if (auto it = m_tactic_hints.find(mlocal_name(mvar))) {
-            expr pre_tac = substitution.instantiate_metavars_wo_jst(*it);
+            expr pre_tac = substitution.instantiate(*it);
             try {
                 return optional<tactic>(expr_to_tactic(m_env, pre_tac, m_pos_provider));
             } catch (expr_to_tactic_exception & ex) {
@@ -658,8 +658,8 @@ public:
                 buffer<expr> locals;
                 get_app_args(*meta, locals);
                 for (expr & l : locals)
-                    l = subst.instantiate_metavars_wo_jst(l);
+                    l = subst.instantiate(l);
-                mvar = update_mlocal(mvar, subst.instantiate_metavars_wo_jst(mlocal_type(mvar)));
+                mvar = update_mlocal(mvar, subst.instantiate(mlocal_type(mvar)));
                 meta = ::lean::mk_app(mvar, locals);
                 expr type = m_tc.infer(*meta);
                 proof_state ps(goals(goal(*meta, type)), subst, m_ngen.mk_child());
@@ -671,7 +671,7 @@ public:
                                 display_unsolved_proof_state(mvar, r->first, "unsolved subgoals");
                             } else {
                                 subst = r->first.get_subst();
-                                expr v = subst.instantiate_metavars_wo_jst(mvar);
+                                expr v = subst.instantiate(mvar);
                                 subst = subst.assign(mlocal_name(mvar), v);
                             }
                         } else {
@@ -686,12 +686,12 @@ public:
                 }
             }
         }
-        return subst.instantiate_metavars_wo_jst(e);
+        return subst.instantiate(e);
     }
 
     /** \brief Apply substitution and solve remaining metavariables using tactics. */
     expr apply(substitution & s, expr const & e) {
-        expr r = s.instantiate_metavars_wo_jst(e);
+        expr r = s.instantiate(e);
         return solve_unassigned_mvars(s, r);
     }
 
@@ -717,9 +717,7 @@ public:
         expr r_type = infer_type(r);
         environment env = m_env;
         justification j = mk_justification(e, [=](formatter const & fmt, options const & opts, substitution const & subst) {
-                return pp_type_mismatch(fmt, env, opts,
+                return pp_type_mismatch(fmt, env, opts, subst.instantiate(expected_type), subst.instantiate(r_type));
-                                        subst.instantiate_metavars_wo_jst(expected_type),
-                                        subst.instantiate_metavars_wo_jst(r_type));
             });
         if (!m_tc.is_def_eq(r_type, expected_type, j)) {
             throw_kernel_exception(env, e,
@@ -739,9 +737,7 @@ public:
         expr r_v_type = infer_type(r_v);
         environment env = m_env;
         justification j = mk_justification(v, [=](formatter const & fmt, options const & o, substitution const & subst) {
-                return pp_def_type_mismatch(fmt, env, o, n,
+                return pp_def_type_mismatch(fmt, env, o, n, subst.instantiate(r_t), subst.instantiate(r_v_type));
-                                            subst.instantiate_metavars_wo_jst(r_t),
-                                            subst.instantiate_metavars_wo_jst(r_v_type));
             });
         if (!m_tc.is_def_eq(r_v_type, r_t, j)) {
             throw_kernel_exception(env, v,

src/kernel/metavar.cpp

@@ -181,7 +181,7 @@ protected:
                     m_subst.d_assign(m_name, r);
                     return r;
                 } else {
-                    return m_subst.instantiate_metavars_wo_jst(p1->first);
+                    return m_subst.instantiate(p1->first);
                 }
             }
         } else {

src/kernel/metavar.h

@@ -100,6 +100,7 @@ public:
        but does not return a justification object for the new expression.
     */
     expr instantiate_metavars_wo_jst(expr const & e) const;
+    expr instantiate(expr const & e) const { return instantiate_metavars_wo_jst(e); }
 
     std::pair<expr, substitution> updt_instantiate_metavars_wo_jst(expr const & e) const;
 

src/kernel/type_checker.cpp

@@ -129,7 +129,7 @@ expr type_checker::ensure_sort_core(expr e, expr const & s) {
         expr r = mk_sort(mk_meta_univ(m_gen.next()));
         justification j = mk_justification(s,
                                            [=](formatter const & fmt, options const & o, substitution const & subst) {
-                                               return pp_type_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
+                                               return pp_type_expected(fmt, m_env, o, subst.instantiate(s));
                                            });
         add_cnstr(mk_eq_cnstr(e, r, j));
         return r;
@@ -170,7 +170,7 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) {
         expr r      = mk_pi(g_x_name, A_args, B_args);
         justification j = mk_justification(s,
                                            [=](formatter const & fmt, options const & o, substitution const & subst) {
-                                               return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));
+                                               return pp_function_expected(fmt, m_env, o, subst.instantiate(s));
                                            });
         add_cnstr(mk_eq_cnstr(e, r, j));
         return r;
@@ -202,10 +202,7 @@ app_delayed_justification::app_delayed_justification(environment const & env, ex
 
 justification mk_app_justification(environment const & env, expr const & e, expr const & d_type, expr const & a_type) {
     auto pp_fn = [=](formatter const & fmt, options const & o, substitution const & subst) {
-        return pp_app_type_mismatch(fmt, env, o,
+        return pp_app_type_mismatch(fmt, env, o, subst.instantiate(e), subst.instantiate(d_type), subst.instantiate(a_type));
-                                    subst.instantiate_metavars_wo_jst(e),
-                                    subst.instantiate_metavars_wo_jst(d_type),
-                                    subst.instantiate_metavars_wo_jst(a_type));
     };
     return mk_justification(e, pp_fn);
 }

src/library/kernel_bindings.cpp

@@ -1389,7 +1389,7 @@ static int mk_justification(lua_State * L) {
         environment env = to_environment(L, 2);
         expr e          = to_expr(L, 3);
         justification j = mk_justification(some_expr(e), [=](formatter const & fmt, options const & opts, substitution const & subst) {
-                expr new_e = subst.instantiate_metavars_wo_jst(e);
+                expr new_e = subst.instantiate(e);
                 format r;
                 r += format(s.c_str());
                 r += pp_indent_expr(fmt, env, opts, new_e);

src/library/tactic/apply_tactic.cpp

@@ -98,7 +98,7 @@ tactic apply_tactic(expr const & _e) {
             return map2<proof_state>(substs, [=](substitution const & subst) -> proof_state {
                     name_generator new_ngen(ngen);
                     type_checker tc(env, new_ngen.mk_child());
-                    expr new_e = subst.instantiate_metavars_wo_jst(e);
+                    expr new_e = subst.instantiate(e);
                     expr new_p = g.abstract(new_e);
                     check_has_no_local(new_p, _e);
                     substitution new_subst = subst.assign(g.get_name(), new_p);
@@ -108,7 +108,7 @@ tactic apply_tactic(expr const & _e) {
                     unsigned i = metas.size();
                     while (i > 0) {
                         --i;
-                        new_gs = cons(goal(metas[i], subst.instantiate_metavars_wo_jst(tc.infer(metas[i]))), new_gs);
+                        new_gs = cons(goal(metas[i], subst.instantiate(tc.infer(metas[i]))), new_gs);
                     }
                     return proof_state(new_gs, new_subst, new_ngen);
                 });

src/library/tactic/goal.cpp

@@ -91,11 +91,6 @@ expr goal::mk_meta(name const & n, expr const & type, bool only_contextual) cons
     return copy_tag(m_meta, mk_app(mvar, locals));
 }
 
-goal goal::instantiate_metavars(substitution const & s) const {
-    return goal(s.instantiate_metavars_wo_jst(m_meta),
-                s.instantiate_metavars_wo_jst(m_type));
-}
-
 static bool validate_locals(expr const & r, unsigned num_locals, expr const * locals) {
     bool failed = false;
     for_each(r, [&](expr const & e, unsigned) {
@@ -169,7 +164,6 @@ static int goal_pp(lua_State * L) {
 }
 static int goal_validate_locals(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate_locals()); }
 static int goal_validate(lua_State * L) { return push_boolean(L, to_goal(L, 1).validate(to_environment(L, 2))); }
-static int goal_instantiate(lua_State * L) { return push_goal(L, to_goal(L, 1).instantiate_metavars(to_substitution(L, 2))); }
 static int goal_abstract(lua_State * L) { return push_expr(L, to_goal(L, 1).abstract(to_expr(L, 2))); }
 static int goal_name(lua_State * L) { return push_name(L, to_goal(L, 1).get_name()); }
 
@@ -181,7 +175,6 @@ static const struct luaL_Reg goal_m[] = {
     {"pp",              safe_function<goal_pp>},
     {"validate",        safe_function<goal_validate>},
     {"validate_locals", safe_function<goal_validate_locals>},
-    {"instantiate",     safe_function<goal_instantiate>},
     {"meta",            safe_function<goal_meta>},
     {"type",            safe_function<goal_type>},
     {"name",            safe_function<goal_name>},

src/library/tactic/goal.h

@@ -70,9 +70,6 @@ public:
     */
     bool validate(environment const & env) const;
 
-    /** \brief Instatiate the metavariables in this goal using the given substitution */
-    goal instantiate_metavars(substitution const & s) const;
-
     format pp(environment const & env, formatter const & fmt, options const & opts) const;
 };