fix(frontends/lean): bug in section management

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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<expr> locals;
+    list<expr> ctx = locals_to_context(e, p);
-    e = abstract_locals(e, p, locals);
     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();

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<expr> 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<expr> 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();

src/frontends/lean/elaborator.cpp

@@ -376,13 +376,14 @@ class elaborator {
     }
 
 public:
-    elaborator(environment const & env, local_decls<level> const & lls, io_state const & ios, name_generator const & ngen,
+    elaborator(environment const & env, local_decls<level> const & lls, list<expr> 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<expr, expr, level_param_names> 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<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
+std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              expr const & e, pos_info_provider * pp, bool check_unassigned, bool ensure_type) {
+                                              io_state const & ios, expr const & e, pos_info_provider * pp, bool check_unassigned,
-    return elaborator(env, lls, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
+                                              bool ensure_type) {
+    return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type);
 }
 
 std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> 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<expr>(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n);
 }
 }

src/frontends/lean/elaborator.h

@@ -13,8 +13,10 @@ Author: Leonardo de Moura
 #include "frontends/lean/local_decls.h"
 
 namespace lean {
-std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios, expr const & e,
+std::tuple<expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, list<expr> const & ctx,
-                                              pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false);
+                                              io_state const & ios, expr const & e, pos_info_provider * pp = nullptr,
-std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls, io_state const & ios,
+                                              bool check_unassigned = true, bool ensure_type = false);
-                                                    name const & n, expr const & t, expr const & v, pos_info_provider * pp = nullptr);
+std::tuple<expr, expr, level_param_names> elaborate(environment const & env, local_decls<level> const & lls,
+                                                    io_state const & ios, name const & n, expr const & t, expr const & v,
+                                                    pos_info_provider * pp = nullptr);
 }

src/frontends/lean/parser.cpp

@@ -474,19 +474,19 @@ level parser::parse_level(unsigned rbp) {
     return left;
 }
 
-std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e) {
+std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, list<expr> 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<expr, level_param_names> parser::elaborate_type(expr const & e) {
+std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> 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<expr, level_param_names> 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<expr>(), m_ios, e, &pp);
 }
 
 std::tuple<expr, expr, level_param_names> parser::elaborate_definition(name const & n, expr const & t, expr const & v) {

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<expr, level_param_names> elaborate_relaxed(expr const & e);
+    std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>());
     /** \brief Elaborate \c e, and ensure it is a type. */
-    std::tuple<expr, level_param_names> elaborate_type(expr const & e);
+    std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>());
     /** \brief Elaborate \c e in the given environment. */
     std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
     /** \brief Elaborate \c e (making sure the result does not have metavariables). */

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<expr> & locals) {
+list<expr> locals_to_context(expr const & e, parser const & p) {
     expr_struct_set ls;
     collect_locals(e, ls);
+    buffer<expr> locals;
     sort_section_params(ls, p, locals);
-    return Fun(locals, e);
+    std::reverse(locals.begin(), locals.end());
-}
+    return to_list(locals.begin(), locals.end());
-
-expr instantiate_locals(expr const & b, buffer<expr> & 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());
 }
 }

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<expr> & 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<expr> & section_ps);
-/** \brief collect all locals in \c e and store and locals, and return Fun(locals, e) */
+list<expr> locals_to_context(expr const & e, parser const & p);
-expr abstract_locals(expr const & e, parser const & p, buffer<expr> & locals);
-/** \brief 'inverse' of \c abstract_locals, given a binding \c b instantiate it using locals */
-expr instantiate_locals(expr const & b, buffer<expr> & locals);
 }

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