feat(library/tactic,frontends/lean): propagate new options back to elaborator

src/frontends/lean/elaborator.cpp

@@ -1742,14 +1742,21 @@ optional<expr> elaborator::get_pre_tactic_for(expr const & mvar) {
 
 optional<tactic> elaborator::pre_tactic_to_tactic(expr const & pre_tac) {
     try {
-        auto fn = [=](goal const & g, name_generator && ngen, expr const & e, optional<expr> const & expected_type,
+        auto fn = [=](goal const & g, options const & o, name_generator && ngen, expr const & e, optional<expr> const & expected_type,
                       substitution const & subst, bool report_unassigned) {
-            elaborator aux_elaborator(m_ctx, std::move(ngen));
             // Disable tactic hints when processing expressions nested in tactics.
             // We must do it otherwise, it is easy to make the system loop.
             bool use_tactic_hints = false;
-            return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
+            if (o == m_ctx.m_options) {
-                                                   use_tactic_hints, subst, report_unassigned);
+                elaborator aux_elaborator(m_ctx, std::move(ngen));
+                return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
+                                                       use_tactic_hints, subst, report_unassigned);
+            } else {
+                elaborator_context aux_ctx(m_ctx, o);
+                elaborator aux_elaborator(aux_ctx, std::move(ngen));
+                return aux_elaborator.elaborate_nested(g.to_context(), expected_type, e,
+                                                       use_tactic_hints, subst, report_unassigned);
+            }
         };
         return optional<tactic>(expr_to_tactic(env(), fn, pre_tac, pip()));
     } catch (expr_to_tactic_exception & ex) {

src/frontends/lean/elaborator_context.cpp

@@ -67,15 +67,23 @@ bool get_elaborator_lift_coercions(options const & opts) {
 elaborator_context::elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
                                        pos_info_provider const * pp, info_manager * info, bool check_unassigned):
     m_env(env), m_ios(ios), m_lls(lls), m_pos_provider(pp), m_info_manager(info), m_check_unassigned(check_unassigned) {
-    m_use_local_instances = get_elaborator_local_instances(ios.get_options());
+    set_options(ios.get_options());
-    m_ignore_instances    = get_elaborator_ignore_instances(ios.get_options());
-    m_flycheck_goals      = get_elaborator_flycheck_goals(ios.get_options());
-    m_fail_missing_field  = get_elaborator_fail_missing_field(ios.get_options());
-    m_lift_coercions      = get_elaborator_lift_coercions(ios.get_options());
-    init_options(ios.get_options());
 }
 
-void elaborator_context::init_options(options const & opts) {
+elaborator_context::elaborator_context(elaborator_context const & ctx, options const & o):
+    m_env(ctx.m_env), m_ios(ctx.m_ios), m_lls(ctx.m_lls), m_pos_provider(ctx.m_pos_provider),
+    m_info_manager(ctx.m_info_manager), m_check_unassigned(ctx.m_check_unassigned) {
+    set_options(o);
+}
+
+void elaborator_context::set_options(options const & opts) {
+    m_options             = opts;
+    m_use_local_instances = get_elaborator_local_instances(opts);
+    m_ignore_instances    = get_elaborator_ignore_instances(opts);
+    m_flycheck_goals      = get_elaborator_flycheck_goals(opts);
+    m_fail_missing_field  = get_elaborator_fail_missing_field(opts);
+    m_lift_coercions      = get_elaborator_lift_coercions(opts);
+
     if (has_show_goal(opts, m_show_goal_line, m_show_goal_col)) {
         m_show_goal_at = true;
     } else {

src/frontends/lean/elaborator_context.h

@@ -20,6 +20,7 @@ class elaborator_context {
     pos_info_provider const * m_pos_provider;
     info_manager *            m_info_manager;
     // configuration
+    options                   m_options;
     bool                      m_check_unassigned;
     bool                      m_use_local_instances;
     bool                      m_ignore_instances;
@@ -36,8 +37,9 @@ class elaborator_context {
     unsigned m_show_hole_line;
     unsigned m_show_hole_col;
 
+    void set_options(options const & opts);
+
     /** \brief Support for showing information using hot-keys */
-    void init_options(options const & opts);
     bool has_show_goal_at(unsigned & line, unsigned & col) const;
     void reset_show_goal_at();
 
@@ -46,6 +48,7 @@ class elaborator_context {
 public:
     elaborator_context(environment const & env, io_state const & ios, local_decls<level> const & lls,
                        pos_info_provider const * pp = nullptr, info_manager * info = nullptr, bool check_unassigned = true);
+    elaborator_context(elaborator_context const & ctx, options const & o);
 };
 void initialize_elaborator_context();
 void finalize_elaborator_context();

src/frontends/lean/info_tactic.cpp

@@ -32,11 +32,11 @@ struct scoped_info_tactic_proof_state {
 };
 
 tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
-    return tactic1([=](environment const &, io_state const &, proof_state const & ps) -> proof_state {
+    return tactic1([=](environment const &, io_state const & ios, proof_state const & ps) -> proof_state {
             // create dummy variable just to communicate position to the elaborator
             expr dummy = mk_sort(mk_level_zero(), e.get_tag());
             scoped_info_tactic_proof_state scope(ps);
-            fn(goal(), name_generator("dummy"), dummy, none_expr(), substitution(), false);
+            fn(goal(), ios.get_options(), name_generator("dummy"), dummy, none_expr(), substitution(), false);
             return ps;
         });
 }

src/library/simplifier/simp_tactic.cpp

@@ -196,7 +196,7 @@ private:
             try {
                 expr new_l; constraints cs;
                 bool report_unassigned = true;
-                std::tie(new_l, m_subst, cs) = m_elab(m_g, m_ngen.mk_child(), l, none_expr(), m_subst, report_unassigned);
+                std::tie(new_l, m_subst, cs) = m_elab(m_g, m_ios.get_options(), m_ngen.mk_child(), l, none_expr(), m_subst, report_unassigned);
                 if (cs)
                     throw tactic_exception("invalid 'simp' tactic, fail to resolve generated constraints");
                 expr new_e = head_beta_reduce(m_elab_tc.infer(new_l).first);

src/library/tactic/apply_tactic.cpp

@@ -208,7 +208,7 @@ tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kin
             name_generator ngen = s.get_ngen();
             expr       new_e; substitution new_subst; constraints cs_;
             try {
-                auto ecs = elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false);
+                auto ecs = elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), s.get_subst(), false);
                 std::tie(new_e, new_subst, cs_) = ecs;
                 buffer<constraint> cs;
                 to_buffer(cs_, cs);

src/library/tactic/check_expr_tactic.cpp

@@ -21,7 +21,7 @@ tactic check_expr_tactic(elaborate_fn const & elab, expr const & e,
             }
             goal const & g      = head(gs);
             name_generator ngen = s.get_ngen();
-            expr new_e = std::get<0>(elab(g, ngen.mk_child(), e, none_expr(), s.get_subst(), false));
+            expr new_e = std::get<0>(elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), s.get_subst(), false));
             auto tc = mk_type_checker(env, ngen.mk_child());
             expr new_t = tc->infer(new_e).first;
             auto out = regular(env, ios);

src/library/tactic/elaborate.cpp

@@ -45,7 +45,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
     optional<expr> elab_expected_type;
     if (enforce_type_during_elaboration)
         elab_expected_type = expected_type;
-    auto esc   = elab(head(gs), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned);
+    auto esc   = elab(head(gs), ios.get_options(), ngen.mk_child(), e, elab_expected_type, subst, report_unassigned);
     expr new_e; substitution new_subst; constraints cs_;
     std::tie(new_e, new_subst, cs_) = esc;
     buffer<constraint> cs;

src/library/tactic/elaborate.h

@@ -25,7 +25,7 @@ bool solve_constraints(environment const & env, io_state const & ios, proof_stat
     3- postponed constraints
 */
 typedef std::tuple<expr, substitution, constraints> elaborate_result;
-typedef std::function<elaborate_result(goal const &, name_generator &&, expr const &,
+typedef std::function<elaborate_result(goal const &, options const &, name_generator &&, expr const &,
                                        optional<expr> const &, substitution const &, bool)> elaborate_fn;
 
 /** \brief Try to elaborate expression \c e using the elaboration function \c elab. The elaboration is performed

src/library/tactic/exact_tactic.cpp

@@ -99,7 +99,7 @@ static tactic assumption_tactic_core(bool conservative) {
             goal g = head(gs);
             buffer<expr> hs;
             g.get_hyps(hs);
-            auto elab = [](goal const &, name_generator const &, expr const & H,
+            auto elab = [](goal const &, options const &, name_generator const &, expr const & H,
                            optional<expr> const &, substitution const & s, bool) -> elaborate_result {
                 return elaborate_result(H, s, constraints());
             };

src/library/tactic/let_tactic.cpp

@@ -19,7 +19,7 @@ expr mk_let_tactic_expr(name const & id, expr const & e) {
 }
 
 tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
-    return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
+    return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
             proof_state new_s = s;
             goals const & gs  = new_s.get_goals();
             if (!gs) {
@@ -29,7 +29,7 @@ tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
             goal const & g         = head(gs);
             name_generator ngen    = s.get_ngen();
             bool report_unassigned = true;
-            elaborate_result esc = elab(g, ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned);
+            elaborate_result esc = elab(g, ios.get_options(), ngen.mk_child(), e, none_expr(), new_s.get_subst(), report_unassigned);
             expr new_e; substitution new_subst; constraints cs;
             std::tie(new_e, new_subst, cs) = esc;
             if (cs)

src/library/tactic/rewrite_tactic.cpp

@@ -747,7 +747,7 @@ class rewrite_fn {
 
     optional<pair<expr, constraints>> elaborate_core(expr const & e, bool fail_if_cnstrs) {
         expr new_expr; substitution new_subst; constraints cs;
-        std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false);
+        std::tie(new_expr, new_subst, cs) = m_elab(m_g, m_ios.get_options(), m_ngen.mk_child(), e, none_expr(), m_ps.get_subst(), false);
         if (fail_if_cnstrs && cs)
             return optional<pair<expr, constraints>>();
         m_ps = proof_state(m_ps, new_subst);

tests/lean/hott/disable_instances.hlean

@@ -0,0 +1,13 @@
+open is_equiv
+constants (A B : Type) (f : A → B)
+
+definition H : is_equiv f := sorry
+
+
+definition loop [instance] [h : is_equiv f] : is_equiv f :=
+h
+
+example (a : A) : let H' : is_equiv f := H in @(inv f) H' (f a) = a :=
+begin
+  with_options [elaborator.ignore_instances true] (apply left_inv f a)
+end