fix(frontends/lean): more bugs in section management

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

src/frontends/lean/builtin_exprs.cpp

@@ -353,7 +353,7 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co
     for (auto old_l : locals) {
         binder_info bi = local_info(old_l);
         bi = bi.update_contextual(true);
-        expr new_l     = p.save_pos(mk_local(local_pp_name(old_l), mlocal_type(old_l), bi), pos);
+        expr new_l     = p.save_pos(mk_local(local_pp_name(old_l), mk_as_is(mlocal_type(old_l)), bi), pos);
         p.add_local(new_l);
         new_locals.push_back(new_l);
     }

src/frontends/lean/decl_cmds.cpp

@@ -255,8 +255,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
     if (in_section(env)) {
         buffer<expr> section_ps;
         collect_section_locals(type, value, p, section_ps);
-        type = Pi(section_ps, type, p);
-        value = Fun(section_ps, value, p);
+        type = Pi_as_is(section_ps, type, p);
+        value = Fun_as_is(section_ps, value, p);
         levels section_ls = collect_section_levels(ls, p);
         expr ref = mk_app(mk_explicit(mk_constant(real_n, section_ls)), section_ps);
         p.add_local_expr(n, ref);

src/frontends/lean/elaborator.cpp

@@ -827,6 +827,9 @@ public:
     }
 
     expr visit_macro(expr const & e) {
+        if (is_as_is(e)) {
+            return get_as_is_arg(e);
+        } else {
             // Remark: Macros are not meant to be used in the front end.
             // Perhaps, we should throw error.
             buffer<expr> args;
@@ -834,6 +837,7 @@ public:
                 args.push_back(visit(macro_arg(e, i)));
             return update_macro(e, args.size(), args.data());
         }
+    }
 
     expr visit_constant(expr const & e) {
         auto it = m_cache.find(e);

src/frontends/lean/inductive_cmd.cpp

@@ -375,7 +375,7 @@ struct inductive_cmd_fn {
             for (auto const & ir : inductive_decl_intros(d)) {
                 expr type = intro_rule_type(ir);
                 type = fix_inductive_occs(type, decls, section_params);
-                type = Pi(section_params, type, m_p);
+                type = Pi_as_is(section_params, type, m_p);
                 bool strict = m_relaxed_implicit_infer.contains(intro_rule_name(ir));
                 type = infer_implicit(type, section_params.size(), strict);
                 new_irs.push_back(update_intro_rule(ir, type));

src/frontends/lean/util.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "library/scoped_ext.h"
 #include "library/locals.h"
+#include "library/explicit.h"
 #include "frontends/lean/parser.h"
 
 namespace lean {
@@ -75,4 +76,28 @@ expr Fun(buffer<expr> const & locals, expr const & e, parser & p) {
 expr Pi(buffer<expr> const & locals, expr const & e, parser & p) {
     return p.rec_save_pos(Pi(locals, e), p.pos_of(e));
 }
+
+template<bool is_lambda>
+static expr mk_binding_as_is(unsigned num, expr const * locals, expr const & b) {
+    expr r     = abstract_locals(b, num, locals);
+    unsigned i = num;
+    while (i > 0) {
+        --i;
+        expr const & l = locals[i];
+        expr t = abstract_locals(mlocal_type(l), i, locals);
+        if (is_lambda)
+            r = mk_lambda(local_pp_name(l), mk_as_is(t), r, local_info(l));
+        else
+            r = mk_pi(local_pp_name(l), mk_as_is(t), r, local_info(l));
+    }
+    return r;
+}
+
+expr Fun_as_is(buffer<expr> const & locals, expr const & e, parser & p) {
+    return p.rec_save_pos(mk_binding_as_is<true>(locals.size(), locals.data(), e), p.pos_of(e));
+}
+
+expr Pi_as_is(buffer<expr> const & locals, expr const & e, parser & p) {
+    return p.rec_save_pos(mk_binding_as_is<false>(locals.size(), locals.data(), e), p.pos_of(e));
+}
 }

src/frontends/lean/util.h

@@ -24,4 +24,8 @@ list<expr> locals_to_context(expr const & e, parser const & p);
 expr Fun(buffer<expr> const & locals, expr const & e, parser & p);
 /** \brief Pi(locals, e), but also propagate \c e position to result */
 expr Pi(buffer<expr> const & locals, expr const & e, parser & p);
+/** \brief Similar to Fun(locals, e, p), but the types are marked as 'as-is' (i.e., they are not processed by the elaborator. */
+expr Fun_as_is(buffer<expr> const & locals, expr const & e, parser & p);
+/** \brief Similar to Pi(locals, e, p), but the types are marked as 'as-is' (i.e., they are not processed by the elaborator. */
+expr Pi_as_is(buffer<expr> const & locals, expr const & e, parser & p);
 }

src/library/explicit.cpp

@@ -10,7 +10,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 static name g_explicit_name("@");
-[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of '@' expression"); }
+static name g_as_is_name("as_is");
+[[ noreturn ]] static void throw_ex(name const & n) { throw exception(sstream() << "unexpected occurrence of '" << n << "' expression"); }
 
 // We encode the 'explicit' expression mark '@' using a macro.
 // This is a trick to avoid creating a new kind of expression.
@@ -18,25 +19,27 @@ static name g_explicit_name("@");
 // and have no semantic significance.
 class explicit_macro_cell : public macro_definition_cell {
 public:
+    virtual bool operator==(macro_definition_cell const & other) const { return this == &other; }
     virtual name get_name() const { return g_explicit_name; }
-    virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); }
-    virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
-    virtual void write(serializer &) const { throw_ex(); }
+    virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(get_name()); }
+    virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(get_name()); }
+    virtual void write(serializer &) const { throw_ex(get_name()); }
+};
+
+class as_is_macro_cell : public explicit_macro_cell {
+public:
+    virtual name get_name() const { return g_as_is_name; }
 };
 
 static macro_definition g_explicit(new explicit_macro_cell());
-expr mk_explicit(expr const & e) {
-    return mk_macro(g_explicit, 1, &e);
-}
+static macro_definition g_as_is(new as_is_macro_cell());
 
-bool is_explicit(expr const & e) {
-    return is_macro(e) && macro_def(e) == g_explicit;
-}
-
-expr const & get_explicit_arg(expr const & e) {
-    lean_assert(is_explicit(e));
-    return macro_arg(e, 0);
-}
+expr mk_explicit(expr const & e) { return mk_macro(g_explicit, 1, &e); }
+bool is_explicit(expr const & e) { return is_macro(e) && macro_def(e) == g_explicit; }
+expr mk_as_is(expr const & e) { return mk_macro(g_as_is, 1, &e); }
+bool is_as_is(expr const & e) { return is_macro(e) && macro_def(e) == g_as_is; }
+expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return macro_arg(e, 0); }
+expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return macro_arg(e, 0); }
 
 static int mk_explicit(lua_State * L) { return push_expr(L, mk_explicit(to_expr(L, 1))); }
 static int is_explicit(lua_State * L) { return push_boolean(L, is_explicit(to_expr(L, 1))); }

src/library/explicit.h

@@ -16,10 +16,22 @@ namespace lean {
 expr mk_explicit(expr const & e);
 /** \brief Return true iff \c e is an explicit expression. */
 bool is_explicit(expr const & e);
+/**
+    \brief Create an explicit expression that is accepted as is
+    by the elaborator.
+*/
+expr mk_as_is(expr const & e);
+/** \brief Return true iff \c e was created with mk_as_is. */
+bool is_as_is(expr const & e);
 /**
    \brief Return the argument of an explicit expression.
    \pre is_explicit(e)
 */
 expr const & get_explicit_arg(expr const & e);
+/**
+   \brief Return the argument of an expression created using mk_as_is.
+   \pre is_as_is(e)
+*/
+expr const & get_as_is_arg(expr const & e);
 void open_explicit(lua_State * L);
 }

tests/lean/run/tactic29.lean

@@ -0,0 +1,18 @@
+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
+  theorem test : a = b ∧ a = a
+  := by apply and_intro; apply H; apply refl
+end
+
+check @test

tests/lean/run/tactic30.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
+  theorem test : a = b ∧ a = a
+  := including H, by apply and_intro; assumption; apply refl
+end
+
+check @test