From 34fc12eda0a98738c8be73f1ed2bd05a3bf79fb3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Jul 2016 13:50:21 -0700
Subject: [PATCH] feat(library/tactic/intro_tactic): improve low-level intron

---
 src/library/tactic/intro_tactic.cpp | 22 ++++++++++++++--------
 src/library/tactic/intro_tactic.h   |  6 +++---
 2 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp
index 793ea040a6..5f30eb4e4f 100644
--- a/src/library/tactic/intro_tactic.cpp
+++ b/src/library/tactic/intro_tactic.cpp
@@ -23,8 +23,9 @@ static name mk_aux_name(list<name> & given_names, name const & default_name) {
     }
 }
 
-optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & given_names, buffer<name> & new_Hns) {
+optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & given_names, buffer<name> & new_Hns) {
     lean_assert(is_metavar(mvar));
+    metavar_context mctx     = ctx.mctx();
     optional<metavar_decl> g = mctx.get_metavar_decl(mvar);
     if (!g) return none_expr();
     expr type            = g->get_type();
@@ -38,7 +39,8 @@ optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & m
         }
         lean_assert(is_pi(type) || is_let(type));
         if (is_pi(type)) {
-            expr H  = new_locals.push_local(mk_aux_name(given_names, binding_name(type)), binding_domain(type), binding_info(type));
+            expr H  = new_locals.push_local(mk_aux_name(given_names, binding_name(type)), binding_domain(type),
+                                            binding_info(type));
             type    = instantiate(binding_body(type), H);
             new_Hs.push_back(H);
             new_Hns.push_back(mlocal_name(H));
@@ -52,7 +54,6 @@ optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & m
         }
     }
     local_context lctx   = ctx.lctx();
-    mctx                 = ctx.mctx();
     expr new_M           = mctx.mk_metavar_decl(lctx, type);
     lean_assert(!mctx.is_assigned(new_M));
     expr new_val = abstract_locals(mk_lazy_abstraction_with_locals(new_M, new_Hs), new_Hs.size(), new_Hs.data());
@@ -71,12 +72,18 @@ optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & m
     }
     lean_assert(!mctx.is_assigned(new_M));
     mctx.assign(mvar, new_val);
+    ctx.set_mctx(mctx);
     return some_expr(new_M);
 }
 
-optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & given_names) {
+optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & given_names) {
     buffer<name> tmp;
-    return intron(ctx, mctx, mvar, n, given_names, tmp);
+    return intron(ctx, mvar, n, given_names, tmp);
+}
+
+optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n) {
+    list<name> empty;
+    return intron(ctx, mvar, n, empty);
 }
 
 optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hns) {
@@ -84,11 +91,10 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> &
     optional<expr> mvar  = s.get_main_goal();
     if (!mvar) return none_tactic_state();
     type_context ctx     = mk_type_context_for(s);
-    metavar_context mctx = s.mctx();
     list<name> new_names;
-    if (optional<expr> new_M = intron(ctx, mctx, *mvar, n, new_names, new_Hns)) {
+    if (optional<expr> new_M = intron(ctx, *mvar, n, new_names, new_Hns)) {
         list<expr> new_gs(*new_M, tail(s.goals()));
-        return some_tactic_state(set_mctx_goals(s, mctx, new_gs));
+        return some_tactic_state(set_mctx_goals(s, ctx.mctx(), new_gs));
     } else {
         return none_tactic_state();
     }
diff --git a/src/library/tactic/intro_tactic.h b/src/library/tactic/intro_tactic.h
index be2d689ddb..aaf968645c 100644
--- a/src/library/tactic/intro_tactic.h
+++ b/src/library/tactic/intro_tactic.h
@@ -14,9 +14,9 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s);
    After execution, the buffer \c new_Hns stores the new interal names for the new hypotheses.
 
    \remark new_hs_names is an input/output parameter. The procedure will "consume" n elements from the list. */
-optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
-optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n, list<name> & new_hs_names);
-optional<expr> intron(type_context & ctx, metavar_context & mctx, expr const & mvar, unsigned n);
+optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
+optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n, list<name> & new_hs_names);
+optional<expr> intron(type_context & ctx, expr const & mvar, unsigned n);
 
 void initialize_intro_tactic();
 void finalize_intro_tactic();