From da865fc33a1cadca8a57d7eb81225c8f22308ca3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 12 Jan 2019 13:58:02 +0100 Subject: [PATCH] refactor(frontends/lean/{vm_,}elaborator): move name resolution over to parser locals In the end I wasn't quite sure whether this is necessary, but it's at least simpler. --- src/frontends/lean/elaborator.cpp | 111 --------------------------- src/frontends/lean/elaborator.h | 5 -- src/frontends/lean/parser.h | 6 +- src/frontends/lean/vm_elaborator.cpp | 68 +++++++++++++++- 4 files changed, 69 insertions(+), 121 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7e210d3bf1..9b7dda2638 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -4036,117 +4036,6 @@ elaborate(environment & env, options const & opts, name const & decl_name, return p; } -static optional resolve_local_name_core(environment const & env, local_context const & lctx, name const & id, - expr const & src, names const & extra_locals) { - // extra locals - unsigned vidx = 0; - for (name const & extra : extra_locals) { - if (id == extra) - return some_expr(copy_pos(src, mk_bvar(vidx))); - vidx++; - } - - /* check local context */ - if (auto decl = lctx.find_local_decl_from_user_name(id)) { - return some_expr(copy_pos(src, decl->mk_ref())); - } - - /* check local_refs */ - if (auto ref = get_local_ref(env, id)) { - /* ref may contain local references that have new names at lctx. */ - return some_expr(copy_pos(src, replace(*ref, [&](expr const & e, unsigned) { - if (is_local(e)) { - if (auto decl = lctx.find_local_decl_from_user_name(local_pp_name(e))) { - return some_expr(decl->mk_ref()); - } - } - return none_expr(); - }))); - } - - if (!id.is_atomic() && id.is_string()) { - if (auto r = resolve_local_name_core(env, lctx, id.get_prefix(), src, extra_locals)) { - return some_expr(copy_pos(src, mk_field_notation_compact(*r, id.get_string().data()))); // HACK: accessing Lean string as C String - } else { - return none_expr(); - } - } else { - return none_expr(); - } -} - -struct resolve_names_fn : public replace_visitor { - environment const & m_env; - local_context const & m_lctx; - names m_locals; - - - resolve_names_fn(environment const & env, local_context const & lctx): - m_env(env), m_lctx(lctx) {} - - virtual expr visit_constant(expr const & e) override { - lean_unreachable(); - } - - virtual expr visit_local(expr const & e) override { - lean_unreachable(); - } - - virtual expr visit_binding(expr const & e) override { - expr new_d = visit(binding_domain(e)); - flet set(m_locals, cons(binding_name(e), m_locals)); - expr new_b = visit(binding_body(e)); - return update_binding(e, new_d, new_b); - } - - virtual expr visit_let(expr const & e) override { - expr new_type = visit(let_type(e)); - expr new_val = visit(let_value(e)); - flet set(m_locals, cons(let_name(e), m_locals)); - expr new_body = visit(let_body(e)); - return update_let(e, new_type, new_val, new_body); - } - - void push_new_arg(buffer & new_args, expr const & arg) { - if (is_choice(arg)) { - for (unsigned i = 0; i < get_num_choices(arg); i++) - push_new_arg(new_args, get_choice(arg, i)); - } else if (std::find(new_args.begin(), new_args.end(), arg) == new_args.end()) { - new_args.push_back(arg); - } - } - - virtual expr visit(expr const & e) override { - if (is_placeholder(e) || is_as_is(e) || is_emptyc_or_emptys(e) || is_as_atomic(e)) { - return e; - } else if (is_annotation(e, "preresolved")) { - auto m = mdata_data(e); - expr id = mdata_expr(e); - if (auto l = resolve_local_name_core(m_env, m_lctx, const_name(id), id, m_locals)) { - return copy_pos(e, *l); - } else { - buffer new_args; - for (unsigned i = 0;; i++) { - if (auto n = get_name(m, name(name(), i))) { - new_args.push_back(copy_pos(e, mk_const(*n, const_levels(id)))); - } else { - break; - } - } - if (new_args.empty()) - throw elaborator_exception(e, format("unknown identifier '") + format(const_name(id).escape()) + format("'")); - return mk_choice(new_args.size(), new_args.data()); - } - } else { - return replace_visitor::visit(e); - } - } -}; - -expr resolve_names(environment const & env, local_context const & lctx, expr const & e) { - return resolve_names_fn(env, lctx)(e); -} - void initialize_elaborator() { g_elab_strategy = new name("elab_strategy"); register_trace_class("elaborator"); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 7cf18b00d4..30a5943cae 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -360,11 +360,6 @@ pair elaborate(environment & env, options const & opts, name const metavar_context & mctx, local_context const & lctx, expr const & e, bool check_unassigned, bool recover_from_errors); -/** \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/parser.h b/src/frontends/lean/parser.h index 093cb9d5a4..d4192bf48a 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -183,9 +183,6 @@ class parser : public abstract_parser { void push_local_scope(bool save_options = true); void pop_local_scope(); - optional resolve_local(name const & id, pos_info const & p, names const & extra_locals, - bool allow_field_notation = true); - friend class patexpr_to_expr_fn; struct backtracking_exception {}; @@ -494,6 +491,9 @@ public: list locals_to_context() const; /** \brief Return all local declarations and aliases */ list> const & get_local_entries() const { return m_local_decls.get_entries(); } + optional resolve_local(name const & id, pos_info const & p, names const & extra_locals, + bool allow_field_notation = true); + void maybe_throw_error(parser_error && err); level parser_error_or_level(parser_error && err); diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index abe485974c..de16b51d41 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -19,8 +19,72 @@ Lean interface to the old elaborator/elaboration parts of the parser #include "frontends/lean/elaborator.h" #include "frontends/lean/parser.h" #include "frontends/lean/decl_cmds.h" +#include "frontends/lean/definition_cmds.h" +#include "frontends/lean/brackets.h" +#include "frontends/lean/choice.h" namespace lean { +struct resolve_names_fn : public replace_visitor { + parser & m_p; + names m_locals; + + resolve_names_fn(parser & p) : m_p(p) {} + + virtual expr visit_constant(expr const & e) override { + lean_unreachable(); + } + + virtual expr visit_local(expr const & e) override { + lean_unreachable(); + } + + virtual expr visit_binding(expr const & e) override { + expr new_d = visit(binding_domain(e)); + flet set(m_locals, cons(binding_name(e), m_locals)); + expr new_b = visit(binding_body(e)); + return update_binding(e, new_d, new_b); + } + + virtual expr visit_let(expr const & e) override { + expr new_type = visit(let_type(e)); + expr new_val = visit(let_value(e)); + flet set(m_locals, cons(let_name(e), m_locals)); + expr new_body = visit(let_body(e)); + return update_let(e, new_type, new_val, new_body); + } + + virtual expr visit(expr const & e) override { + if (is_placeholder(e) || is_as_is(e) || is_emptyc_or_emptys(e) || is_as_atomic(e)) { + return e; + } else if (is_annotation(e, "preresolved")) { + auto m = mdata_data(e); + expr id = mdata_expr(e); + if (auto l = m_p.resolve_local(const_name(id), m_p.pos_of(e), m_locals)) { + return copy_pos(e, *l); + } else { + buffer new_args; + for (unsigned i = 0;; i++) { + if (auto n = get_name(m, name(name(), i))) { + new_args.push_back(copy_pos(e, mk_const(*n, const_levels(id)))); + } else { + break; + } + } + if (new_args.empty()) + throw elaborator_exception(e, format("unknown identifier '") + format(const_name(id).escape()) + format("'")); + return mk_choice(new_args.size(), new_args.data()); + } + } else { + return replace_visitor::visit(e); + } + } +}; + +static expr resolve_names(parser & p, expr const & e) { + return resolve_names_fn(p)(e); +} + + decl_attributes to_decl_attributes(environment const & env, expr const & e, bool local) { decl_attributes attributes(!local); buffer args; @@ -62,7 +126,7 @@ void elab_check_cmd(parser & p, expr const & cmd) { bool check_unassigend = false; names ls; metavar_context mctx; - e = resolve_names(p.env(), p.mk_local_context_adapter().lctx(), e); + e = resolve_names(p, e); std::tie(e, ls) = p.elaborate("_check", mctx, e, check_unassigend); names new_ls = to_names(collect_univ_params(e)); type_context_old tc(p.env()); @@ -89,7 +153,7 @@ void elab_constant_cmd(parser & p, expr const & cmd) { for (auto const & e : ls) ls_buffer.push_back(const_name(e)); expr type = args[2]; - type = resolve_names(p.env(), p.mk_local_context_adapter().lctx(), type); + type = resolve_names(p, type); p.set_env(elab_var(p, variable_kind::Constant, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd), optional(), const_name(fn), type, ls_buffer)); }