max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(frontends/lean/{vm_,}elaborator): move name resolution over to parser locals

Browse source 
In the end I wasn't quite sure whether this is necessary, but it's at least simpler.
This commit is contained in:
Sebastian Ullrich 2019-01-12 13:58:02 +01:00
parent e0da13128e
commit da865fc33a
4 changed files with 69 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

111
src/frontends/lean/elaborator.cpp
View file

@ -4036,117 +4036,6 @@ elaborate(environment & env, options const & opts, name const & decl_name,
return p;
}
static optional<expr> 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<names> 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<names> 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<expr> & 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<expr> 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");

5
src/frontends/lean/elaborator.h
View file

@ -360,11 +360,6 @@ pair<expr, names> 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();
}

6
src/frontends/lean/parser.h
View file

@ -183,9 +183,6 @@ class parser : public abstract_parser {
void push_local_scope(bool save_options = true);
void pop_local_scope();
optional<expr> 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<expr> locals_to_context() const;
/** \brief Return all local declarations and aliases */
list<pair<name, expr>> const & get_local_entries() const { return m_local_decls.get_entries(); }
optional<expr> 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);

68
src/frontends/lean/vm_elaborator.cpp
View file

@ -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<names> 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<names> 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<expr> 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<expr> 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<binder_info>(), const_name(fn), type, ls_buffer));
}