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

fix(frontends/lean): pass around info_manager at more locations

Browse source
This commit is contained in:
Sebastian Ullrich 2016-11-07 11:44:47 +01:00 • committed by Leonardo de Moura
parent 1f9554a014
commit bbb06dec70
4 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/definition_cmds.cpp
View file

@ -144,7 +144,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
buffer<expr> 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(), metavar_context(), local_context(), p.infom());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
val = replace_locals_preserving_pos_info(val, params, new_params);
@ -562,7 +562,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
if (is_instance)
attrs.set_attribute(p.env(), "instance");
std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance);
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context());
elaborator elab(p.env(), p.get_options(), metavar_context(), local_context(), p.infom());
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
elab.set_instance_fingerprint();

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

@ -104,7 +104,7 @@ elaborator_strategy get_elaborator_strategy(environment const & env, name const
#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, optional<info_manager> infom):
local_context const & lctx, optional<info_manager> & infom):
m_env(env), m_opts(opts),
m_ctx(env, opts, mctx, lctx, get_tcm(), transparency_mode::Semireducible), m_infom(infom) {
unsigned line, col;
@ -656,8 +656,10 @@ expr elaborator::visit_const_core(expr const & e) {
/** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
void elaborator::save_identifier_info(expr const & f) {
if (!m_no_info && m_infom && get_pos_info_provider() && is_constant(f)) {
if (auto p = get_pos_info_provider()->get_pos_info(f))
if (auto p = get_pos_info_provider()->get_pos_info(f)) {
m_infom->add_identifier_info(p->first, p->second, const_name(f));
m_infom->add_type_info(p->first, p->second, infer_type(f));
}
}
}
@ -680,7 +682,7 @@ expr elaborator::visit_function(expr const & fn, bool has_args, expr const & ref
case expr_kind::Lambda: r = visit_lambda(fn, none_expr()); break;
case expr_kind::Let: r = visit_let(fn, none_expr()); break;
}
save_identifier_info(fn);
save_identifier_info(r);
if (has_args)
r = ensure_function(r, ref);
return r;
@ -2734,10 +2736,6 @@ elaborate(environment & env, options const & opts,
auto p = elab.finalize(r, check_unassigned, true);
mctx = elab.mctx();
env = elab.env();
if (infom) {
lean_assert(elab.infom());
infom = *elab.infom();
}
return p;
}
@ -2781,7 +2779,9 @@ static expr translate(environment const & env, local_context const & lctx, expr
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);
// TODO(sullrich): pass through info_manager?
optional<info_manager> infom;
elaborator elab(env, opts, mctx, lctx, infom);
expr r = elab.elaborate(translate(env, lctx, e));
if (!relaxed)
elab.ensure_no_unassigned_metavars(r);

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

@ -88,7 +88,7 @@ private:
/* Position information for show goal feature */
optional<pos_info> m_show_goal_pos;
optional<info_manager> m_infom;
optional<info_manager> & m_infom;
expr get_default_numeral_type();
@ -239,7 +239,7 @@ private:
void unassigned_uvars_to_params(expr const & e);
public:
elaborator(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
optional<info_manager> infom = optional<info_manager>());
optional<info_manager> & infom);
metavar_context const & mctx() const { return m_ctx.mctx(); }
local_context const & lctx() const { return m_ctx.lctx(); }
expr push_local(name const & n, expr const & type, binder_info const & bi = binder_info()) {

2
src/frontends/lean/inductive_cmds.cpp
View file

@ -286,7 +286,7 @@ class inductive_cmd_fn {
void elaborate_inductive_decls(buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules,
buffer<expr> & new_params, buffer<expr> & new_inds, buffer<buffer<expr> > & new_intro_rules) {
options opts = m_p.get_options();
elaborator elab(m_env, opts, metavar_context(), local_context());
elaborator elab(m_env, opts, metavar_context(), local_context(), m_p.infom());
buffer<expr> params_no_inds;
for (expr const & p : params) {