diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 8aa0f480d..9e057e9fc 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -82,15 +82,12 @@ environment end_scoped_cmd(parser & p) { environment check_cmd(parser & p) { expr e = p.parse_expr(); - buffer locals; - e = abstract_locals(e, p, locals); + list ctx = locals_to_context(e, p); level_param_names ls = to_level_param_names(collect_univ_params(e)); level_param_names new_ls; - std::tie(e, new_ls) = p.elaborate_relaxed(e); + std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx); auto tc = mk_type_checker_with_hints(p.env(), p.mk_ngen()); expr type = tc->check(e, append(ls, new_ls)); - e = instantiate_locals(e, locals); - type = instantiate_locals(type, locals); auto reg = p.regular_stream(); formatter const & fmt = reg.get_formatter(); options opts = p.ios().get_options(); diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index e6c5a06e9..028dd1d8f 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -138,7 +138,8 @@ environment variable_cmd_core(parser & p, bool is_axiom) { ls = to_list(ls_buffer.begin(), ls_buffer.end()); } level_param_names new_ls; - std::tie(type, new_ls) = p.elaborate_type(type); + list ctx = locals_to_context(type, p); + std::tie(type, new_ls) = p.elaborate_type(type, ctx); update_section_local_levels(p, new_ls); return declare_var(p, p.env(), n, append(ls, new_ls), type, is_axiom, bi, pos); } @@ -317,7 +318,8 @@ static environment variables_cmd(parser & p) { p.parse_close_binder_info(bi); level_param_names ls = to_level_param_names(collect_univ_params(type)); level_param_names new_ls; - std::tie(type, new_ls) = p.elaborate_type(type); + list ctx = locals_to_context(type, p); + std::tie(type, new_ls) = p.elaborate_type(type, ctx); update_section_local_levels(p, new_ls); ls = append(ls, new_ls); environment env = p.env(); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index ba4719de2..f45fffdda 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -376,13 +376,14 @@ class elaborator { } public: - elaborator(environment const & env, local_decls const & lls, io_state const & ios, name_generator const & ngen, + elaborator(environment const & env, local_decls const & lls, list const & ctx, io_state const & ios, name_generator const & ngen, pos_info_provider * pp, bool check_unassigned): m_env(env), m_lls(lls), m_ios(ios), m_ngen(ngen), m_tc(mk_type_checker_with_hints(env, m_ngen.mk_child())), m_pos_provider(pp) { m_check_unassigned = check_unassigned; m_use_local_instances = get_elaborator_local_instances(ios.get_options()); + set_ctx(ctx); } expr mk_local(name const & n, expr const & t, binder_info const & bi) { @@ -1147,6 +1148,7 @@ public: } std::tuple operator()(expr const & t, expr const & v, name const & n) { + lean_assert(!has_local(t)); lean_assert(!has_local(v)); expr r_t = ensure_type(visit(t)); expr r_v = visit(v); expr r_v_type = infer_type(r_v); @@ -1169,13 +1171,14 @@ public: static name g_tmp_prefix = name::mk_internal_unique_name(); -std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, - expr const & e, pos_info_provider * pp, bool check_unassigned, bool ensure_type) { - return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type); +std::tuple elaborate(environment const & env, local_decls const & lls, list const & ctx, + io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned, + bool ensure_type) { + return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type); } std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, name const & n, expr const & t, expr const & v, pos_info_provider * pp) { - return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, true)(t, v, n); + return elaborator(env, lls, list(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n); } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 8d88c0bde..5cd9155fa 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -13,8 +13,10 @@ Author: Leonardo de Moura #include "frontends/lean/local_decls.h" namespace lean { -std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, expr const & e, - pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false); -std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, - name const & n, expr const & t, expr const & v, pos_info_provider * pp = nullptr); +std::tuple elaborate(environment const & env, local_decls const & lls, list const & ctx, + io_state const & ios, expr const & e, pos_info_provider * pp = nullptr, + bool check_unassigned = true, bool ensure_type = false); +std::tuple elaborate(environment const & env, local_decls const & lls, + io_state const & ios, name const & n, expr const & t, expr const & v, + pos_info_provider * pp = nullptr); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index d4cc53339..580d4bf07 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -474,19 +474,19 @@ level parser::parse_level(unsigned rbp) { return left; } -std::tuple parser::elaborate_relaxed(expr const & e) { +std::tuple parser::elaborate_relaxed(expr const & e, list const & ctx) { parser_pos_provider pp = get_pos_provider(); - return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, false); + return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, false); } -std::tuple parser::elaborate_type(expr const & e) { +std::tuple parser::elaborate_type(expr const & e, list const & ctx) { parser_pos_provider pp = get_pos_provider(); - return ::lean::elaborate(m_env, m_local_level_decls, m_ios, e, &pp, true, true); + return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, &pp, true, true); } std::tuple parser::elaborate_at(environment const & env, expr const & e) { parser_pos_provider pp = get_pos_provider(); - return ::lean::elaborate(env, m_local_level_decls, m_ios, e, &pp); + return ::lean::elaborate(env, m_local_level_decls, list(), m_ios, e, &pp); } std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v) { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index b43cb71bd..1d41f9c79 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -258,9 +258,9 @@ public: struct no_undef_id_error_scope { parser & m_p; bool m_old; no_undef_id_error_scope(parser &); ~no_undef_id_error_scope(); }; /** \brief Elaborate \c e, and tolerate metavariables in the result. */ - std::tuple elaborate_relaxed(expr const & e); + std::tuple elaborate_relaxed(expr const & e, list const & ctx = list()); /** \brief Elaborate \c e, and ensure it is a type. */ - std::tuple elaborate_type(expr const & e); + std::tuple elaborate_type(expr const & e, list const & ctx = list()); /** \brief Elaborate \c e in the given environment. */ std::tuple elaborate_at(environment const & env, expr const & e); /** \brief Elaborate \c e (making sure the result does not have metavariables). */ diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 8433e7302..b72edace1 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -59,18 +59,12 @@ void collect_section_locals(expr const & type, expr const & value, parser const sort_section_params(ls, p, section_ps); } -expr abstract_locals(expr const & e, parser const & p, buffer & locals) { +list locals_to_context(expr const & e, parser const & p) { expr_struct_set ls; collect_locals(e, ls); + buffer locals; sort_section_params(ls, p, locals); - return Fun(locals, e); -} - -expr instantiate_locals(expr const & b, buffer & locals) { - expr _b = b; - unsigned sz = locals.size(); - for (unsigned i = 0; i < sz; i++) - _b = binding_body(_b); - return instantiate_rev(_b, locals.size(), locals.data()); + std::reverse(locals.begin(), locals.end()); + return to_list(locals.begin(), locals.end()); } } diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 72516170b..5717c9c58 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -19,8 +19,5 @@ levels collect_section_levels(level_param_names const & ls, parser & p); void collect_section_locals(expr const & type, expr const & value, parser const & p, buffer & section_ps); /** \brief Copy the local parameters to \c section_ps, then sort \c section_ps (using the order in which they were declared). */ void sort_section_params(expr_struct_set const & locals, parser const & p, buffer & section_ps); -/** \brief collect all locals in \c e and store and locals, and return Fun(locals, e) */ -expr abstract_locals(expr const & e, parser const & p, buffer & locals); -/** \brief 'inverse' of \c abstract_locals, given a binding \c b instantiate it using locals */ -expr instantiate_locals(expr const & b, buffer & locals); +list locals_to_context(expr const & e, parser const & p); } diff --git a/tests/lean/run/section1.lean b/tests/lean/run/section1.lean new file mode 100644 index 000000000..9b009525b --- /dev/null +++ b/tests/lean/run/section1.lean @@ -0,0 +1,14 @@ +import standard +using tactic + +section + set_option pp.universes true + set_option pp.implicit true + parameter {A : Type} + parameters {a b : A} + parameter H : a = b + parameters H1 H2 : b = a + check H1 + check H + check H2 +end \ No newline at end of file