From 5fdc737dfc252854837b6838cdf652be65434a2c Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 27 Jan 2017 14:49:02 +0100 Subject: [PATCH] feat(library/tactic): store name of current declaration in tactic_state --- library/init/meta/tactic.lean | 3 ++ src/api/parser.cpp | 2 +- src/frontends/lean/builtin_cmds.cpp | 12 ++--- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/decl_attributes.cpp | 2 +- src/frontends/lean/decl_cmds.cpp | 4 +- src/frontends/lean/definition_cmds.cpp | 8 ++-- src/frontends/lean/elaborator.cpp | 32 ++++--------- src/frontends/lean/elaborator.h | 12 +++-- src/frontends/lean/inductive_cmds.cpp | 2 +- src/frontends/lean/notation_cmd.cpp | 2 +- src/frontends/lean/parser.cpp | 30 ++++++------ src/frontends/lean/parser.h | 13 +++--- src/frontends/lean/structure_cmd.cpp | 4 +- src/frontends/lean/util.cpp | 8 ++-- src/frontends/lean/util.h | 2 +- src/frontends/smt2/parser.cpp | 2 +- src/library/tactic/cases_tactic.cpp | 4 +- src/library/tactic/dsimplify.cpp | 6 +-- src/library/tactic/elaborate.cpp | 24 ++++------ src/library/tactic/elaborate.h | 14 ------ src/library/tactic/simp_lemmas.cpp | 14 +++--- src/library/tactic/simplify.cpp | 9 ++-- src/library/tactic/subst_tactic.cpp | 2 +- src/library/tactic/tactic_state.cpp | 46 +++++++++++-------- src/library/tactic/tactic_state.h | 18 +++++--- src/library/tactic/user_attribute.cpp | 2 +- src/library/tactic/vm_monitor.cpp | 2 +- .../interactive/do_info.lean.expected.out | 6 +-- 29 files changed, 134 insertions(+), 153 deletions(-) diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index e417efeac8..e6467c034e 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -405,6 +405,9 @@ try $ do prio ← has_attribute attr_name src, set_basic_attribute_core attr_name tgt p (some prio) +/-- Name of the declaration currently being elaborated. -/ +meta constant decl_name : tactic name + /- (save_type_info e ref) save (typeof e) at position associated with ref -/ meta constant save_type_info : expr → expr → tactic unit meta constant save_info_thunk : nat → nat → (unit → format) → tactic unit diff --git a/src/api/parser.cpp b/src/api/parser.cpp index 341f05af6f..8c2183411b 100644 --- a/src/api/parser.cpp +++ b/src/api/parser.cpp @@ -56,7 +56,7 @@ lean_bool lean_parse_expr(lean_env env, lean_ios ios, char const * str, lean_exp parser p(_env, _ios, mk_dummy_loader(), in, strname, use_exceptions); expr e = p.parse_expr(); expr _e; level_param_names _ps; - std::tie(_e, _ps) = p.elaborate(list(), e); + std::tie(_e, _ps) = p.elaborate(strname, list(), e); *new_expr = of_expr(new expr(_e)); *new_ps = of_list_name(new list(_ps)); LEAN_CATCH; diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index c5ca78259b..33b08240fb 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -163,7 +163,7 @@ environment end_scoped_cmd(parser & p) { environment check_cmd(parser & p) { expr e; level_param_names ls; - std::tie(e, ls) = parse_local_expr(p); + std::tie(e, ls) = parse_local_expr(p, "_check"); type_checker tc(p.env(), true, false); expr type = tc.check(e, ls); auto out = p.mk_message(p.cmd_pos(), INFORMATION); @@ -184,7 +184,7 @@ environment eval_cmd(parser & p) { whnf = true; } expr e; level_param_names ls; - std::tie(e, ls) = parse_local_expr(p); + std::tie(e, ls) = parse_local_expr(p, "_eval"); expr r; if (whnf) { type_checker tc(p.env(), true, false); @@ -380,10 +380,10 @@ static expr convert_metavars(metavar_context & ctx, expr const & e) { static environment unify_cmd(parser & p) { environment const & env = p.env(); expr e1; level_param_names ls1; - std::tie(e1, ls1) = parse_local_expr(p); + std::tie(e1, ls1) = parse_local_expr(p, "_unify"); p.check_token_next(get_comma_tk(), "invalid #unify command, proper usage \"#unify e1, e2\""); expr e2; level_param_names ls2; - std::tie(e2, ls2) = parse_local_expr(p); + std::tie(e2, ls2) = parse_local_expr(p, "_unify"); metavar_context mctx; local_context lctx; e1 = convert_metavars(mctx, e1); @@ -436,7 +436,7 @@ static void vm_eval_core(vm_state & s, name const & main, optional const static environment vm_eval_cmd(parser & p) { auto pos = p.pos(); expr e; level_param_names ls; - std::tie(e, ls) = parse_local_expr(p); + std::tie(e, ls) = parse_local_expr(p, "_eval"); if (has_metavar(e)) throw parser_error("invalid vm_eval command, expression contains metavariables", pos); type_context tc(p.env(), transparency_mode::All); @@ -533,7 +533,7 @@ static environment run_command_cmd(parser & p) { tactic = mk_app(mk_constant(get_pre_monad_and_then_name()), tactic, try_triv); expr val = mk_typed_expr(mk_true(), mk_by(tactic)); bool check_unassigned = false; - elaborate(env, opts, mctx, local_context(), val, check_unassigned); + elaborate(env, opts, "_run_command", mctx, local_context(), val, check_unassigned); return env; } diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 9e1a005093..7b51137890 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -830,7 +830,7 @@ static expr parse_proj(parser & p, unsigned, expr const * args, pos_info const & try { metavar_context mctx; bool check_unassigned = false; - lhs = p.elaborate(mctx, lhs, check_unassigned).first; + lhs = p.elaborate({}, mctx, lhs, check_unassigned).first; type_checker tc(p.env(), true, false); lhs_type = tc.infer(lhs); } catch (exception &) { diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index 4c231bcba4..6fe5b87d2e 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -49,7 +49,7 @@ void decl_attributes::parse_core(parser & p, bool compact) { auto pos = p.pos(); expr pre_val = p.parse_expr(); pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val); - expr val = p.elaborate(list(), pre_val).first; + expr val = p.elaborate("_attribute", list(), pre_val).first; val = normalize(p.env(), val); if (optional mpz_val = to_num_core(val)) { if (!mpz_val->is_unsigned_int()) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index bab1858aa1..9f3b794188 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -266,7 +266,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, decl_modifiers } level_param_names new_ls; list ctx = p.locals_to_context(); - std::tie(type, new_ls) = p.elaborate_type(ctx, type); + std::tie(type, new_ls) = p.elaborate_type("_variable", ctx, type); if (k == variable_kind::Variable || k == variable_kind::Parameter) update_local_levels(p, new_ls, k == variable_kind::Variable); return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, modifiers); @@ -369,7 +369,7 @@ static environment variables_cmd_core(parser & p, variable_kind k, decl_modifier level_param_names new_ls; expr new_type; check_command_period_open_binder_or_eof(p); - std::tie(new_type, new_ls) = p.elaborate_type(ctx, type); + std::tie(new_type, new_ls) = p.elaborate_type("_variables", ctx, type); if (k == variable_kind::Variable || k == variable_kind::Parameter) update_local_levels(p, new_ls, k == variable_kind::Variable); new_ls = append(ls, new_ls); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 69d604cb5b..822abefe53 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -157,7 +157,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif buffer fns, params; declaration_info_scope scope(p, kind, modifiers); expr val = parse_mutual_definition(p, lp_names, fns, params); - elaborator elab(p.env(), p.get_options(), metavar_context(), local_context()); + elaborator elab(p.env(), p.get_options(), local_pp_name(fns[0]), metavar_context(), local_context()); buffer new_params; elaborate_params(elab, params, new_params); val = replace_locals_preserving_pos_info(val, params, new_params); @@ -650,7 +650,7 @@ public: auto_reporting_info_manager_scope scope4(get_module_id(), m_use_info_manager); try { - elaborator elab(m_decl_env, m_opts, m_mctx, m_lctx); + elaborator elab(m_decl_env, m_opts, local_pp_name(m_fn), m_mctx, m_lctx); expr val, type; std::tie(val, type) = elaborate_proof(elab); if (is_equations_result(val)) @@ -721,7 +721,7 @@ public: auto_reporting_info_manager_scope scope4(get_module_id(), m_use_info_manager); try { - elaborator elab(m_decl_env, m_opts, m_mctx, m_lctx); + elaborator elab(m_decl_env, m_opts, "example", m_mctx, m_lctx); expr val, type; std::tie(val, type) = elab.elaborate_with_type(m_val, mlocal_type(m_fn)); @@ -778,7 +778,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif if (p.get_break_at_pos()) return p.env(); - elaborator elab(p.env(), p.get_options(), metavar_context(), local_context()); + elaborator elab(p.env(), p.get_options(), local_pp_name(fn), metavar_context(), local_context()); buffer new_params; elaborate_params(elab, params, new_params); elab.set_instance_fingerprint(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 73d97c65b6..51eda793d6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -109,9 +109,9 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const #define trace_elab_detail(CODE) lean_trace("elaborator_detail", scope_trace_env _scope(m_env, m_ctx); CODE) #define trace_elab_debug(CODE) lean_trace("elaborator_debug", scope_trace_env _scope(m_env, m_ctx); CODE) -elaborator::elaborator(environment const & env, options const & opts, metavar_context const & mctx, - local_context const & lctx): - m_env(env), m_opts(opts), +elaborator::elaborator(environment const & env, options const & opts, name const & decl_name, + metavar_context const & mctx, local_context const & lctx): + m_env(env), m_opts(opts), m_decl_name(decl_name), m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible), m_uses_infom(get_global_info_manager() != nullptr) { } @@ -186,7 +186,7 @@ expr elaborator::mk_instance_core(local_context const & lctx, expr const & C, ex metavar_context mctx = m_ctx.mctx(); local_context new_lctx = lctx.instantiate_mvars(mctx); new_lctx = erase_inaccessible_annotations(new_lctx); - tactic_state s = ::lean::mk_tactic_state_for(m_env, m_opts, mctx, new_lctx, C); + tactic_state s = ::lean::mk_tactic_state_for(m_env, m_opts, m_decl_name, mctx, new_lctx, C); throw elaborator_exception(ref, format("failed to synthesize type class instance for") + line() + s.pp()); } return *inst; @@ -2544,7 +2544,7 @@ tactic_state elaborator::mk_tactic_state_for(expr const & mvar) { expr type = mctx.instantiate_mvars(mdecl.get_type()); type = erase_inaccessible_annotations(type); m_ctx.set_mctx(mctx); - return ::lean::mk_tactic_state_for(m_env, m_opts, mctx, lctx, type); + return ::lean::mk_tactic_state_for(m_env, m_opts, m_decl_name, mctx, lctx, type); } void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) { @@ -2567,8 +2567,6 @@ void elaborator::synthesize_using_tactics() { buffer to_process; to_buffer(m_tactics, to_process); m_tactics = list(); - elaborate_fn fn(nested_elaborate); - scope_elaborate_fn scope(fn); for (expr_pair const & p : to_process) { lean_assert(is_metavar(p.first)); invoke_tactic(p.first, p.second); @@ -2916,10 +2914,10 @@ expr elaborator::finalize_theorem_proof(expr const & val, theorem_finalization_i } pair -elaborate(environment & env, options const & opts, +elaborate(environment & env, options const & opts, name const & decl_name, metavar_context & mctx, local_context const & lctx, expr const & e, bool check_unassigned) { - elaborator elab(env, opts, mctx, lctx); + elaborator elab(env, opts, decl_name, mctx, lctx); expr r = elab.elaborate(e); auto p = elab.finalize(r, check_unassigned, true); mctx = elab.mctx(); @@ -3004,10 +3002,7 @@ vm_obj tactic_resolve_local_name(vm_obj const & vm_id, vm_obj const & vm_s) { } } -/** \brief Translated local constants (and undefined constants) occurring in \c e into - local constants provided by \c ctx. - Throw exception is \c ctx does not contain the local constant. */ -static expr resolve_names(environment const & env, local_context const & lctx, expr const & e) { +expr resolve_names(environment const & env, local_context const & lctx, expr const & e) { auto fn = [&](expr const & e) { if (is_placeholder(e) || is_by(e) || is_as_is(e)) { return some_expr(e); // ignore placeholders, nested tactics and as_is terms @@ -3029,17 +3024,6 @@ static expr resolve_names(environment const & env, local_context const & lctx, e return replace(e, fn); } -expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, - expr const & e, bool relaxed) { - elaborator elab(env, opts, mctx, lctx); - expr r = elab.elaborate(resolve_names(env, lctx, e)); - if (!relaxed) - elab.ensure_no_unassigned_metavars(r); - mctx = elab.mctx(); - env = elab.env(); - return r; -} - static vm_obj tactic_save_type_info(vm_obj const & _e, vm_obj const & ref, vm_obj const & _s) { expr const & e = to_expr(_e); tactic_state const & s = to_tactic_state(_s); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 06d813016a..6a5678e7e9 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/local_context.h" #include "library/type_context.h" #include "library/tactic/tactic_state.h" +#include "library/tactic/elaborate.h" #include "frontends/lean/elaborator_exception.h" #include "frontends/lean/info_manager.h" @@ -34,6 +35,7 @@ private: }; environment m_env; options m_opts; + name m_decl_name; type_context m_ctx; info_manager m_info; @@ -248,7 +250,7 @@ private: void finalize_core(sanitize_param_names_fn & S, buffer & es, bool check_unassigned, bool to_simple_metavar, bool collect_local_ctx); public: - elaborator(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx); + elaborator(environment const & env, options const & opts, name const & decl_name, metavar_context const & mctx, local_context const & lctx); ~elaborator(); metavar_context const & mctx() const { return m_ctx.mctx(); } local_context const & lctx() const { return m_ctx.lctx(); } @@ -303,12 +305,14 @@ public: } }; -pair elaborate(environment & env, options const & opts, +pair elaborate(environment & env, options const & opts, name const & decl_name, metavar_context & mctx, local_context const & lctx, expr const & e, bool check_unassigend); -expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, - expr const & e, bool relaxed); +/** \brief Translated local constants (and undefined constants) occurring in \c e into + local constants provided by \c ctx. + Throw exception is \c ctx does not contain the local constant. */ +expr resolve_names(environment const & env, local_context const & lctx, expr const & e); void initialize_elaborator(); void finalize_elaborator(); diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index 75c9c87289..524136fd1d 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -289,7 +289,7 @@ class inductive_cmd_fn { void elaborate_inductive_decls(buffer const & params, buffer const & inds, buffer > const & intro_rules, buffer & new_params, buffer & new_inds, buffer > & new_intro_rules) { options opts = m_p.get_options(); - elaborator elab(m_env, opts, metavar_context(), local_context()); + elaborator elab(m_env, opts, local_pp_name(inds[0]), metavar_context(), local_context()); buffer params_no_inds; for (expr const & p : params) { diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 13e159c326..a4fee34f84 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -47,7 +47,7 @@ static unsigned parse_precedence_core(parser & p) { parser::local_scope scope(p, env); expr pre_val = p.parse_expr(get_max_prec()); pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val); - expr val = p.elaborate(list(), pre_val).first; + expr val = p.elaborate("notation", list(), pre_val).first; val = normalize(p.env(), val); if (optional mpz_val = to_num_core(val)) { if (!mpz_val->is_unsigned_int()) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ba2a29288a..dcd54d4fab 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -805,47 +805,43 @@ level parser::parse_level(unsigned rbp) { return left; } -pair parser::elaborate(metavar_context & mctx, local_context_adapter const & adapter, +pair parser::elaborate(name const & decl_name, + metavar_context & mctx, local_context_adapter const & adapter, expr const & e, bool check_unassigned) { expr tmp_e = adapter.translate_to(e); pair r = - ::lean::elaborate(m_env, get_options(), mctx, adapter.lctx(), tmp_e, check_unassigned); + ::lean::elaborate(m_env, get_options(), decl_name, mctx, adapter.lctx(), tmp_e, check_unassigned); expr new_e = r.first; new_e = adapter.translate_from(new_e); return mk_pair(new_e, r.second); } -pair parser::elaborate(metavar_context & mctx, list const & lctx, expr const & e, bool check_unassigned) { +pair parser::elaborate(name const & decl_name, metavar_context & mctx, list const & lctx, expr const & e, bool check_unassigned) { local_context_adapter adapter(lctx); - return elaborate(mctx, adapter, e, check_unassigned); + return elaborate(decl_name, mctx, adapter, e, check_unassigned); } -pair parser::elaborate(metavar_context & mctx, expr const & e, bool check_unassigned) { +pair parser::elaborate(name const & decl_name, metavar_context & mctx, expr const & e, bool check_unassigned) { local_context_adapter adapter(m_local_decls); - return elaborate(mctx, adapter, e, check_unassigned); + return elaborate(decl_name, mctx, adapter, e, check_unassigned); } -pair parser::elaborate(expr const & e) { +pair parser::elaborate(name const & decl_name, list const & ctx, expr const & e) { metavar_context mctx; - return elaborate(mctx, list(), e, true); + return elaborate(decl_name, mctx, ctx, e, true); } -pair parser::elaborate(list const & ctx, expr const & e) { - metavar_context mctx; - return elaborate(mctx, ctx, e, true); -} - -pair parser::elaborate_type(list const & ctx, expr const & e) { +pair parser::elaborate_type(name const & decl_name, list const & ctx, expr const & e) { metavar_context mctx; expr Type = copy_tag(e, mk_sort(mk_level_placeholder())); expr new_e = copy_tag(e, mk_typed_expr(Type, e)); - return elaborate(mctx, ctx, new_e, true); + return elaborate(decl_name, mctx, ctx, new_e, true); } -pair parser::elaborate_type(metavar_context & mctx, expr const & e) { +pair parser::elaborate_type(name const & decl_name, metavar_context & mctx, expr const & e) { expr Type = copy_tag(e, mk_sort(mk_level_placeholder())); expr new_e = copy_tag(e, mk_typed_expr(Type, e)); - return elaborate(mctx, new_e, true); + return elaborate(decl_name, mctx, new_e, true); } [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index ed595653c9..9825bccb97 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -506,18 +506,17 @@ public: expr const & get_undef_id(unsigned i) const { return m_undef_ids[i]; } private: - pair elaborate(metavar_context & mctx, local_context_adapter const & adapter, + pair elaborate(name const & decl_name, metavar_context & mctx, local_context_adapter const & adapter, expr const & e, bool check_unassigned = true); public: local_context_adapter mk_local_context_adapter() { return local_context_adapter(m_local_decls); } - pair elaborate(expr const & e); - pair elaborate(metavar_context & mctx, expr const & e, bool check_unassigned = true); - pair elaborate(metavar_context & mctx, list const & lctx, expr const & e, bool check_unassigned); - pair elaborate(list const & ctx, expr const & e); - pair elaborate_type(list const & lctx, expr const & e); + pair elaborate(name const & decl_name, metavar_context & mctx, expr const & e, bool check_unassigned = true); + pair elaborate(name const & decl_name, metavar_context & mctx, list const & lctx, expr const & e, bool check_unassigned); + pair elaborate(name const & decl_name, list const & ctx, expr const & e); + pair elaborate_type(name const & decl_name, list const & lctx, expr const & e); /* Elaborate \c e as a type using the given metavariable context, and using m_local_decls as the local context */ - pair elaborate_type(metavar_context & mctx, expr const & e); + pair elaborate_type(name const & decl_name, metavar_context & mctx, expr const & e); expr mk_sorry(pos_info const & p); bool used_sorry() const { return m_used_sorry; } diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 2c1203ba99..b814a9d24a 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -389,7 +389,7 @@ struct structure_cmd_fn { expr tmp = Pi_as_is(ctx, Pi(tmp_locals, m_type, m_p), m_p); level_param_names new_ls; expr new_tmp; - std::tie(new_tmp, new_ls) = m_p.elaborate_type(list(), tmp); + std::tie(new_tmp, new_ls) = m_p.elaborate_type(m_name, list(), tmp); levels new_meta_ls = map2(new_ls, [&](name const &) { return m_ctx.mk_univ_metavar_decl(); }); new_tmp = instantiate_univ_params(new_tmp, new_ls, new_meta_ls); new_tmp = update_locals(new_tmp, ctx); @@ -682,7 +682,7 @@ struct structure_cmd_fn { level_param_names new_ls; expr new_tmp; metavar_context mctx = m_ctx.mctx(); - std::tie(new_tmp, new_ls) = m_p.elaborate_type(mctx, tmp); + std::tie(new_tmp, new_ls) = m_p.elaborate_type(m_name, mctx, tmp); m_ctx.set_mctx(mctx); for (auto new_l : new_ls) m_level_names.push_back(new_l); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index fa15e55424..57e08bf898 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -262,19 +262,19 @@ level mk_result_level(buffer const & r_lvls) { } } -std::tuple parse_local_expr(parser & p, metavar_context & mctx, bool relaxed) { +std::tuple parse_local_expr(parser & p, name const & decl_name, metavar_context & mctx, bool relaxed) { expr e = p.parse_expr(); p.declare_sorry_if_used(); bool check_unassigend = !relaxed; expr new_e; level_param_names ls; - std::tie(new_e, ls) = p.elaborate(mctx, e, check_unassigend); + std::tie(new_e, ls) = p.elaborate(decl_name, mctx, e, check_unassigend); level_param_names new_ls = to_level_param_names(collect_univ_params(new_e)); return std::make_tuple(new_e, new_ls); } -std::tuple parse_local_expr(parser & p, bool relaxed) { +std::tuple parse_local_expr(parser & p, name const & decl_name, bool relaxed) { metavar_context mctx; - return parse_local_expr(p, mctx, relaxed); + return parse_local_expr(p, decl_name, mctx, relaxed); } optional is_uniquely_aliased(environment const & env, name const & n) { diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 298ae8d503..9f7c4961fc 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -84,7 +84,7 @@ expr Pi_as_is(expr const & local, expr const & e); level mk_result_level(buffer const & r_lvls); /** \brief Auxiliary function for check/eval/find_decl */ -std::tuple parse_local_expr(parser & p, bool relaxed = true); +std::tuple parse_local_expr(parser & p, name const & decl_name, bool relaxed = true); optional is_uniquely_aliased(environment const & env, name const & n); diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp index ca176ccfb0..17316015f3 100644 --- a/src/frontends/smt2/parser.cpp +++ b/src/frontends/smt2/parser.cpp @@ -478,7 +478,7 @@ private: metavar_context mctx; expr goal_mvar = mctx.mk_metavar_decl(lctx(), mk_constant(get_false_name())); - vm_obj s = to_obj(mk_tactic_state_for_metavar(env(), ios().get_options(), mctx, goal_mvar)); + vm_obj s = to_obj(mk_tactic_state_for_metavar(env(), ios().get_options(), "check-sat", mctx, goal_mvar)); vm_state state(env(), ios().get_options()); scope_vm_state scope(state); diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index ea91bd0b47..22d6867bd7 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -56,7 +56,7 @@ struct cases_tactic_fn { /* throw exception that stores the intermediate state */ [[ noreturn ]] void throw_exception(expr const & mvar, char const * msg) { - throw cases_tactic_exception(mk_tactic_state_for_metavar(m_env, m_opts, m_mctx, mvar), msg); + throw cases_tactic_exception(mk_tactic_state_for_metavar(m_env, m_opts, "cases", m_mctx, mvar), msg); } #define lean_cases_trace(MVAR, CODE) lean_trace(name({"tactic", "cases"}), type_context TMP_CTX = mk_type_context_for(MVAR); scope_trace_env _scope1(m_env, TMP_CTX); CODE) @@ -232,7 +232,7 @@ struct cases_tactic_fn { } format pp_goal(expr const & mvar) { - tactic_state tmp = mk_tactic_state_for_metavar(m_env, m_opts, m_mctx, mvar); + tactic_state tmp = mk_tactic_state_for_metavar(m_env, m_opts, "cases", m_mctx, mvar); return tmp.pp_goal(mvar); } diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp index d8a11ce573..bd021b582c 100644 --- a/src/library/tactic/dsimplify.cpp +++ b/src/library/tactic/dsimplify.cpp @@ -295,12 +295,12 @@ class tactic_dsimplify_fn : public dsimplify_core_fn { public: tactic_dsimplify_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, bool visit_instances, - vm_obj const & a, vm_obj const & pre, vm_obj const & post): + vm_obj const & a, vm_obj const & pre, vm_obj const & post, tactic_state const & s): dsimplify_core_fn(ctx, dcs, max_steps, visit_instances), m_a(a), m_pre(pre), m_post(post), - m_s(mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx(), mk_true())) { + m_s(s) { } vm_obj const & get_a() const { return m_a; } @@ -314,7 +314,7 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a, type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); tactic_dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits::max()), - to_bool(visit_instances), a, pre, post); + to_bool(visit_instances), a, pre, post, s); expr new_e = F(to_expr(e)); tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs); return mk_tactic_success(mk_vm_pair(F.get_a(), to_obj(new_e)), new_s); diff --git a/src/library/tactic/elaborate.cpp b/src/library/tactic/elaborate.cpp index 81cc728870..7a89e01aaf 100644 --- a/src/library/tactic/elaborate.cpp +++ b/src/library/tactic/elaborate.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "kernel/for_each_fn.h" #include "library/annotation.h" #include "library/vm/vm_expr.h" @@ -17,28 +18,21 @@ expr mk_by(expr const & e) { return mk_annotation(*g_by_name, e); } bool is_by(expr const & e) { return is_annotation(e, *g_by_name); } expr const & get_by_arg(expr const & e) { lean_assert(is_by(e)); return get_annotation_arg(e); } -LEAN_THREAD_PTR(elaborate_fn const, g_elaborate); - -scope_elaborate_fn::scope_elaborate_fn(elaborate_fn const & fn) { - m_old = g_elaborate; - g_elaborate = &fn; -} - -scope_elaborate_fn::~scope_elaborate_fn() { - g_elaborate = m_old; -} - vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj const & _s) { tactic_state const & s = to_tactic_state(_s); optional g = s.get_main_goal_decl(); if (!g) return mk_no_goals_exception(s); - if (!g_elaborate) { - return mk_tactic_exception("elaborator is not available", s); - } metavar_context mctx = s.mctx(); try { environment env = s.env(); - expr r = (*g_elaborate)(env, s.get_options(), mctx, g->get_context(), to_expr(qe), to_bool(relaxed)); + auto e = to_expr(qe); + elaborator elab(env, s.get_options(), s.decl_name(), mctx, g->get_context()); + expr r = elab.elaborate(resolve_names(env, g->get_context(), e)); + if (!to_bool(relaxed)) + elab.ensure_no_unassigned_metavars(r); + mctx = elab.mctx(); + env = elab.env(); + r = mctx.instantiate_mvars(r); if (to_bool(relaxed) && has_expr_metavar(r)) { buffer new_goals; diff --git a/src/library/tactic/elaborate.h b/src/library/tactic/elaborate.h index fdb63d02d4..89c6d63ef4 100644 --- a/src/library/tactic/elaborate.h +++ b/src/library/tactic/elaborate.h @@ -13,20 +13,6 @@ expr mk_by(expr const & e); bool is_by(expr const & e); expr const & get_by_arg(expr const & e); -/* Elaboration function. - \remark The boolean flag indicates whether metavariables should be tolerated in the result or not. - \remark The metavariable context is input/output. */ -typedef std::function elaborate_fn; - -/** \brief Auxiliary function for setting the thread local elaboration - procedure used by the tactic framework. */ -class scope_elaborate_fn { - elaborate_fn const * m_old; -public: - scope_elaborate_fn(elaborate_fn const &); - ~scope_elaborate_fn(); -}; - void initialize_elaborate(); void finalize_elaborate(); } diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index cb2388691e..5492eae0a3 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1317,8 +1317,8 @@ vm_obj simp_lemmas_erase(vm_obj const & lemmas, vm_obj const & lemma_list) { return to_obj(new_lemmas); } -static optional prove(type_context & ctx, vm_obj const & prove_fn, expr const & e) { - tactic_state s = mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.lctx(), e); +static optional prove(type_context & ctx, vm_obj const & prove_fn, expr const & e, tactic_state s) { + s = mk_tactic_state_for(s.env(), s.get_options(), s.decl_name(), ctx.lctx(), e); vm_obj r_obj = invoke(prove_fn, to_obj(s)); optional s_new = is_tactic_success(r_obj); if (!s_new || s_new->goals()) return none_expr(); @@ -1329,7 +1329,7 @@ static optional prove(type_context & ctx, vm_obj const & prove_fn, expr co return some_expr(result); } -static bool instantiate_emetas(type_context & ctx, vm_obj const & prove_fn, unsigned num_emeta, list const & emetas, list const & instances) { +static bool instantiate_emetas(type_context & ctx, vm_obj const & prove_fn, unsigned num_emeta, list const & emetas, list const & instances, tactic_state const & s) { environment const & env = ctx.env(); bool failed = false; unsigned i = num_emeta; @@ -1364,7 +1364,7 @@ static bool instantiate_emetas(type_context & ctx, vm_obj const & prove_fn, unsi // Note: m_type has no metavars if (ctx.is_prop(m_type)) { - if (auto pf = prove(ctx, prove_fn, m_type)) { + if (auto pf = prove(ctx, prove_fn, m_type, s)) { lean_verify(ctx.is_def_eq(m, *pf)); return; } @@ -1381,14 +1381,14 @@ static bool instantiate_emetas(type_context & ctx, vm_obj const & prove_fn, unsi } -static simp_result simp_lemma_rewrite(type_context & ctx, simp_lemma const & sl, vm_obj const & prove_fn, expr const & e) { +static simp_result simp_lemma_rewrite(type_context & ctx, simp_lemma const & sl, vm_obj const & prove_fn, expr const & e, tactic_state const & s) { type_context::tmp_mode_scope scope(ctx, sl.get_num_umeta(), sl.get_num_emeta()); if (!ctx.is_def_eq(e, sl.get_lhs())) { lean_trace("simp_lemmas", tout() << "fail to unify: " << sl.get_id() << "\n";); return simp_result(e); } - if (!instantiate_emetas(ctx, prove_fn, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances())) { + if (!instantiate_emetas(ctx, prove_fn, sl.get_num_emeta(), sl.get_emetas(), sl.get_instances(), s)) { lean_trace("simp_lemmas", tout() << "fail to instantiate emetas: " << sl.get_id() << "\n";); return simp_result(e); } @@ -1426,7 +1426,7 @@ vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & type_context ctx = mk_type_context_for(s, m); for (simp_lemma const & lemma : *srs) { - simp_result r = simp_lemma_rewrite(ctx, lemma, prove_fn, e); + simp_result r = simp_lemma_rewrite(ctx, lemma, prove_fn, e, s); if (!is_eqp(r.get_new(), e)) { lean_trace("simp_lemmas", scope_trace_env scope(ctx.env(), ctx); tout() << "[" << lemma.get_id() << "]: " << e << " ==> " << r.get_new() << "\n";); diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 1be2c435f1..867005de24 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -1024,7 +1024,7 @@ class vm_simplify_fn : public simplify_ext_core_fn { } virtual optional prove(expr const & e) override { - tactic_state s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_ctx.lctx(), e); + auto s = mk_tactic_state_for(m_ctx.env(), m_ctx.get_options(), m_s.decl_name(), m_ctx.lctx(), e); vm_obj r_obj = invoke(m_prove, m_a, to_obj(s)); optional s_new = is_tactic_success(r_obj); if (!s_new || s_new->goals()) return none_expr(); @@ -1040,11 +1040,12 @@ public: vm_simplify_fn(type_context & ctx, defeq_can_state & dcs, simp_lemmas const & slss, unsigned max_steps, bool contextual, bool lift_eq, bool canonize_instances, bool canonize_proofs, bool use_axioms, - vm_obj const & prove, vm_obj const & pre, vm_obj const & post): + vm_obj const & prove, vm_obj const & pre, vm_obj const & post, + tactic_state const & s): simplify_ext_core_fn(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, use_axioms), m_prove(prove), m_pre(pre), m_post(post), - m_s(mk_tactic_state_for(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx(), mk_true())) {} + m_s(s) {} pair operator()(vm_obj const & a, name const & rel, expr const & e) { m_a = a; @@ -1110,7 +1111,7 @@ static vm_obj ext_simplify_core(vm_obj const & a, vm_obj const & c, simp_lemmas type_context ctx = mk_type_context_for(s, transparency_mode::Reducible); defeq_can_state dcs = s.dcs(); vm_simplify_fn simp(ctx, dcs, slss, max_steps, contextual, lift_eq, canonize_instances, canonize_proofs, - use_axioms, prove, pre, post); + use_axioms, prove, pre, post, s); pair p = simp(a, r, e); if (p.second.get_new() != e) { vm_obj const & a = p.first; diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index db2ed1b291..7bdc081e0a 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -34,7 +34,7 @@ bool check_hypothesis_in_context(metavar_context const & mctx, expr const & mvar expr subst(environment const & env, options const & opts, transparency_mode const & m, metavar_context & mctx, expr const & mvar, expr const & H, bool symm, hsubstitution * subst) { #define lean_subst_trace(CODE) lean_trace(name({"tactic", "subst"}), CODE) -#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S = mk_tactic_state_for_metavar(env, opts, mctx, MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp_core() << "\n";) +#define lean_subst_trace_state(MVAR, MSG) lean_trace(name({"tactic", "subst"}), tactic_state S = mk_tactic_state_for_metavar(env, opts, "subst", mctx, MVAR); type_context TMP_CTX = mk_type_context_for(S, m); scope_trace_env _scope1(env, TMP_CTX); tout() << MSG << S.pp_core() << "\n";) lean_subst_trace_state(mvar, "initial:\n"); lean_assert(mctx.get_metavar_decl(mvar)); diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 1adf9e64b7..639916e204 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -48,9 +48,9 @@ void tactic_state_cell::dealloc() { delete this; } -tactic_state::tactic_state(environment const & env, options const & o, metavar_context const & ctx, +tactic_state::tactic_state(environment const & env, options const & o, name const & decl_name, metavar_context const & ctx, list const & gs, expr const & main, defeq_canonizer::state const & dcs) { - m_ptr = new tactic_state_cell(env, o, ctx, gs, main, dcs); + m_ptr = new tactic_state_cell(env, o, decl_name, ctx, gs, main, dcs); m_ptr->inc_ref(); } @@ -64,40 +64,42 @@ optional tactic_state::get_main_goal_decl() const { return mctx().get_metavar_decl(head(goals())); } -tactic_state mk_tactic_state_for(environment const & env, options const & o, metavar_context mctx, local_context const & lctx, expr const & type) { +tactic_state mk_tactic_state_for(environment const & env, options const & o, name const & decl_name, + metavar_context mctx, local_context const & lctx, expr const & type) { expr main = mctx.mk_metavar_decl(lctx, type); - return tactic_state(env, o, mctx, list(main), main, defeq_canonizer::state()); + return tactic_state(env, o, decl_name, mctx, list(main), main, defeq_canonizer::state()); } -tactic_state mk_tactic_state_for(environment const & env, options const & o, local_context const & lctx, expr const & type) { - metavar_context mctx; - return mk_tactic_state_for(env, o, mctx, lctx, type); +tactic_state mk_tactic_state_for(environment const & env, options const & o, name const & decl_name, + local_context const & lctx, expr const & type) { + return mk_tactic_state_for(env, o, decl_name, {}, lctx, type); } -tactic_state mk_tactic_state_for_metavar(environment const & env, options const & opts, metavar_context const & mctx, expr const & mvar) { - return tactic_state(env, opts, mctx, list(mvar), mvar, defeq_canonizer::state()); +tactic_state mk_tactic_state_for_metavar(environment const & env, options const & opts, name const & decl_name, + metavar_context const & mctx, expr const & mvar) { + return tactic_state(env, opts, decl_name, mctx, list(mvar), mvar, defeq_canonizer::state()); } tactic_state set_options(tactic_state const & s, options const & o) { - return tactic_state(s.env(), o, s.mctx(), s.goals(), s.main(), s.dcs()); + return tactic_state(s.env(), o, s.decl_name(), s.mctx(), s.goals(), s.main(), s.dcs()); } tactic_state set_env(tactic_state const & s, environment const & env) { - return tactic_state(env, s.get_options(), s.mctx(), s.goals(), s.main(), s.dcs()); + return tactic_state(env, s.get_options(), s.decl_name(), s.mctx(), s.goals(), s.main(), s.dcs()); } tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx) { if (is_eqp(s.mctx(), mctx)) return s; - return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main(), s.dcs()); + return tactic_state(s.env(), s.get_options(), s.decl_name(), mctx, s.goals(), s.main(), s.dcs()); } tactic_state set_mctx_dcs(tactic_state const & s, metavar_context const & mctx, defeq_can_state const & dcs) { if (is_eqp(s.mctx(), mctx) && is_eqp(s.dcs(), dcs)) return s; - return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main(), dcs); + return tactic_state(s.env(), s.get_options(), s.decl_name(), mctx, s.goals(), s.main(), dcs); } tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx) { - return tactic_state(env, s.get_options(), mctx, s.goals(), s.main(), s.dcs()); + return tactic_state(env, s.get_options(), s.decl_name(), mctx, s.goals(), s.main(), s.dcs()); } static list consume_solved_prefix(metavar_context const & mctx, list const & gs) { @@ -110,11 +112,11 @@ static list consume_solved_prefix(metavar_context const & mctx, list } tactic_state set_goals(tactic_state const & s, list const & gs) { - return tactic_state(s.env(), s.get_options(), s.mctx(), consume_solved_prefix(s.mctx(), gs), s.main(), s.dcs()); + return tactic_state(s.env(), s.get_options(), s.decl_name(), s.mctx(), consume_solved_prefix(s.mctx(), gs), s.main(), s.dcs()); } tactic_state set_mctx_goals_dcs(tactic_state const & s, metavar_context const & mctx, list const & gs, defeq_can_state const & dcs) { - return tactic_state(s.env(), s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main(), dcs); + return tactic_state(s.env(), s.get_options(), s.decl_name(), mctx, consume_solved_prefix(mctx, gs), s.main(), dcs); } tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list const & gs) { @@ -123,7 +125,7 @@ tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env, metavar_context const & mctx, list const & gs) { - return tactic_state(env, s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main(), s.dcs()); + return tactic_state(env, s.get_options(), s.decl_name(), mctx, consume_solved_prefix(mctx, gs), s.main(), s.dcs()); } tactic_state set_mctx_lctx_dcs(tactic_state const & s, metavar_context const & mctx, local_context const & lctx, defeq_can_state const & dcs) { @@ -134,7 +136,7 @@ tactic_state set_mctx_lctx_dcs(tactic_state const & s, metavar_context const & m } metavar_context new_mctx = mctx; expr mvar = new_mctx.mk_metavar_decl(lctx, mk_true()); - return tactic_state(s.env(), s.get_options(), new_mctx, to_list(mvar), mvar, s.dcs()); + return tactic_state(s.env(), s.get_options(), s.decl_name(), new_mctx, to_list(mvar), mvar, s.dcs()); } tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, local_context const & lctx) { @@ -143,7 +145,7 @@ tactic_state set_mctx_lctx(tactic_state const & s, metavar_context const & mctx, tactic_state set_defeq_can_state(tactic_state const & s, defeq_can_state const & dcs) { if (is_eqp(s.dcs(), dcs)) return s; - return tactic_state(s.env(), s.get_options(), s.mctx(), s.goals(), s.main(), dcs); + return tactic_state(s.env(), s.get_options(), s.decl_name(), s.mctx(), s.goals(), s.main(), dcs); } format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const { @@ -742,6 +744,11 @@ vm_obj tactic_module_doc_strings(vm_obj const & _s) { return mk_tactic_success(r, s); } +vm_obj tactic_decl_name(vm_obj const & _s) { + auto & s = to_tactic_state(_s); + return mk_tactic_success(to_obj(s.decl_name()), s); +} + format tactic_state::pp() const { type_context ctx = mk_type_context_for(*this, transparency_mode::Semireducible); expr ts_expr = mk_constant("tactic_state"); @@ -806,6 +813,7 @@ void initialize_tactic_state() { DECLARE_VM_BUILTIN(name({"tactic", "add_doc_string"}), tactic_add_doc_string); DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}), tactic_module_doc_strings); DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}), tactic_open_namespaces); + DECLARE_VM_BUILTIN(name({"tactic", "decl_name"}), tactic_decl_name); g_pp_instantiate_goal_mvars = new name{"pp", "instantiate_goal_mvars"}; register_bool_option(*g_pp_instantiate_goal_mvars, LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS, "(pretty printer) instantiate assigned metavariables before pretty printing goals"); diff --git a/src/library/tactic/tactic_state.h b/src/library/tactic/tactic_state.h index afd41c9193..a6d96b5aae 100644 --- a/src/library/tactic/tactic_state.h +++ b/src/library/tactic/tactic_state.h @@ -20,6 +20,7 @@ class tactic_state_cell { MK_LEAN_RC(); environment m_env; options m_options; + name m_decl_name; metavar_context m_mctx; list m_goals; expr m_main; @@ -27,9 +28,11 @@ class tactic_state_cell { friend class tactic_state; void dealloc(); public: - tactic_state_cell(environment const & env, options const & o, metavar_context const & ctx, list const & gs, + tactic_state_cell(environment const & env, options const & o, name const & decl_name, + metavar_context const & ctx, list const & gs, expr const & main, defeq_can_state const & s): - m_rc(0), m_env(env), m_options(o), m_mctx(ctx), m_goals(gs), m_main(main), m_defeq_can_state(s) {} + m_rc(0), m_env(env), m_options(o), m_decl_name(decl_name), + m_mctx(ctx), m_goals(gs), m_main(main), m_defeq_can_state(s) {} }; class tactic_state { @@ -41,7 +44,8 @@ private: explicit tactic_state(tactic_state_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } format pp_goal(formatter_factory const & fmtf, expr const & g) const; public: - tactic_state(environment const & env, options const & o, metavar_context const & ctx, list const & gs, + tactic_state(environment const & env, options const & o, name const & decl_name, + metavar_context const & ctx, list const & gs, expr const & main, defeq_can_state const & s); tactic_state(tactic_state const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } tactic_state(tactic_state && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } @@ -55,6 +59,7 @@ public: metavar_context const & mctx() const { lean_assert(m_ptr); return m_ptr->m_mctx; } list const & goals() const { lean_assert(m_ptr); return m_ptr->m_goals; } expr const & main() const { lean_assert(m_ptr); return m_ptr->m_main; } + name const & decl_name() const { lean_assert(m_ptr); return m_ptr->m_decl_name; } defeq_can_state const & get_defeq_canonizer_state() const { return m_ptr->m_defeq_can_state; } defeq_can_state const & dcs() const { return get_defeq_canonizer_state(); } @@ -80,11 +85,12 @@ inline optional none_tactic_state() { return optional some_tactic_state(tactic_state const & e) { return optional(e); } inline optional some_tactic_state(tactic_state && e) { return optional(std::forward(e)); } -tactic_state mk_tactic_state_for(environment const & env, options const & opts, metavar_context mctx, +tactic_state mk_tactic_state_for(environment const & env, options const & opts, name const & decl_name, metavar_context mctx, local_context const & lctx, expr const & type); -tactic_state mk_tactic_state_for(environment const & env, options const & opts, +tactic_state mk_tactic_state_for(environment const & env, options const & opts, name const & decl_name, local_context const & lctx, expr const & type); -tactic_state mk_tactic_state_for_metavar(environment const & env, options const & opts, metavar_context const & mctx, expr const & mvar); +tactic_state mk_tactic_state_for_metavar(environment const & env, options const & opts, name const & decl_name, + metavar_context const & mctx, expr const & mvar); tactic_state set_options(tactic_state const & s, options const & o); tactic_state set_env(tactic_state const & s, environment const & env); diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp index f8719dd2c0..6db8659943 100644 --- a/src/library/tactic/user_attribute.cpp +++ b/src/library/tactic/user_attribute.cpp @@ -184,7 +184,7 @@ vm_obj caching_user_attribute_get_cache(vm_obj const &, vm_obj const & vm_attr, lean_trace("user_attributes_cache", tout() << "recomputing cache for [" << attr.get_name() << "]\n";); buffer instances; attr.get_instances(env, instances); - tactic_state s0 = mk_tactic_state_for(env, options(), local_context(), mk_true()); + tactic_state s0 = mk_tactic_state_for(env, options(), {}, local_context(), mk_true()); vm_obj result = invoke(cache_handler, to_obj(to_list(instances)), to_obj(s0)); if (is_tactic_success(result)) { user_attr_cache::entry entry; diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index b2ddef3e7c..fa535e3419 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -161,7 +161,7 @@ vm_obj vm_obj_to_tactic_state(vm_obj const & o) { if (is_tactic_state(o)) return o; else - return to_obj(mk_tactic_state_for(environment(), options(), local_context(), mk_Prop())); + return to_obj(mk_tactic_state_for(environment(), options(), {}, local_context(), mk_Prop())); } vm_obj vm_obj_to_format(vm_obj const & o) { diff --git a/tests/lean/interactive/do_info.lean.expected.out b/tests/lean/interactive/do_info.lean.expected.out index 9b29c2bfed..ef767a9fe1 100644 --- a/tests/lean/interactive/do_info.lean.expected.out +++ b/tests/lean/interactive/do_info.lean.expected.out @@ -1,7 +1,7 @@ {"msg":{"caption":"trace output","file_name":"f","pos_col":0,"pos_line":3,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"} {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":456},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6} +{"record":{"full-id":"tactic.intro","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":459},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6} {"record":{"full-id":"tactic.transitivity","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":30},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":9} -{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":563},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12} +{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":566},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":12} {"record":{"full-id":"tactic.symmetry","source":{"column":9,"file":"/library/init/meta/relation_tactics.lean","line":27},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":14} -{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":563},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16} +{"record":{"full-id":"tactic.assumption","source":{"column":9,"file":"/library/init/meta/tactic.lean","line":566},"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"tactic unit"},"response":"ok","seq_num":16}