refactor(frontends/lean): eliminate the abstract method 'family' from parser

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

src/frontends/lean/builtin_exprs.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/calc.h"
 #include "frontends/lean/proof_qed_ext.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
 
 namespace lean {
 namespace notation {
@@ -109,8 +110,8 @@ static expr parse_let(parser & p, pos_info const & pos) {
             p.check_token_next(g_assign, "invalid let declaration, ':=' expected");
             value = p.parse_scoped_expr(ps, lenv);
             if (is_opaque)
-                type  = p.pi_abstract(ps, type);
+                type  = Pi(ps, type, p);
-            value = p.lambda_abstract(ps, value);
+            value = Fun(ps, value, p);
         }
         if (is_opaque) {
             expr l = p.save_pos(mk_local(id, type), pos);
@@ -356,7 +357,7 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co
         p.add_local(new_l);
         new_locals.push_back(new_l);
     }
-    expr r = p.rec_save_pos(Fun(new_locals, p.parse_expr()), pos);
+    expr r = Fun(new_locals, p.parse_expr(), p);
     r = p.rec_save_pos(mk_app(r, locals), pos);
     return r;
 }

src/frontends/lean/decl_cmds.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include "util/sstream.h"
 #include "kernel/type_checker.h"
+#include "kernel/abstract.h"
 #include "library/scoped_ext.h"
 #include "library/aliases.h"
 #include "library/private.h"
@@ -124,7 +125,7 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
         auto lenv = p.parse_binders(ps);
         p.check_token_next(g_colon, "invalid declaration, ':' expected");
         type = p.parse_scoped_expr(ps, lenv);
-        type = p.pi_abstract(ps, type);
+        type = Pi(ps, type, p);
     } else {
         p.next();
         type = p.parse_expr();
@@ -230,9 +231,9 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
             buffer<expr> ps;
             optional<local_environment> lenv;
             lenv = p.parse_binders(ps);
+            auto pos = p.pos();
             if (p.curr_is_token(g_colon)) {
                 p.next();
-                auto pos = p.pos();
                 type = p.parse_scoped_expr(ps, *lenv);
                 if (is_theorem && !p.curr_is_token(g_assign)) {
                     value = p.save_pos(mk_expr_placeholder(), pos);
@@ -245,8 +246,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
                 p.check_token_next(g_assign, "invalid declaration, ':=' expected");
                 value = p.parse_scoped_expr(ps, *lenv);
             }
-            type = p.pi_abstract(ps, type);
+            type  = Pi(ps, type, p);
-            value = p.lambda_abstract(ps, value);
+            value = Fun(ps, value, p);
         }
         update_univ_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);
         ls = to_list(ls_buffer.begin(), ls_buffer.end());
@@ -254,14 +255,12 @@ 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 = p.pi_abstract(section_ps, type);
+        type = Pi(section_ps, type, p);
-        value = p.lambda_abstract(section_ps, value);
+        value = Fun(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);
     }
-    if (real_n != n)
-        env = add_decl_alias(env, n, mk_constant(real_n));
     level_param_names new_ls;
     if (is_theorem) {
         if (p.num_threads() > 1) {
@@ -285,6 +284,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
         std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value);
         env = module::add(env, check(env, mk_definition(env, real_n, append(ls, new_ls), type, value, modifiers.m_is_opaque)));
     }
+    if (real_n != n)
+        env = add_decl_alias(env, n, mk_constant(real_n));
     if (modifiers.m_is_instance)
         env = add_instance(env, real_n);
     if (modifiers.m_is_coercion)

src/frontends/lean/inductive_cmd.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive/inductive.h"
+#include "kernel/abstract.h"
 #include "kernel/free_vars.h"
 #include "library/scoped_ext.h"
 #include "library/locals.h"
@@ -150,7 +151,7 @@ struct inductive_cmd_fn {
             m_p.parse_binders(ps);
             m_p.check_token_next(g_colon, "invalid inductive declaration, ':' expected");
             type = m_p.parse_scoped_expr(ps);
-            type = m_p.pi_abstract(ps, type);
+            type = Pi(ps, type, m_p);
         } else {
             m_p.next();
             type = m_p.parse_expr();
@@ -263,7 +264,7 @@ struct inductive_cmd_fn {
             }
             m_p.check_token_next(g_colon, "invalid introduction rule, ':' expected");
             expr intro_type = m_p.parse_scoped_expr(params, m_env);
-            intro_type = m_p.pi_abstract(params, intro_type);
+            intro_type = Pi(params, intro_type, m_p);
             intro_type = infer_implicit(intro_type, params.size(), strict);
             intros.push_back(intro_rule(intro_name, intro_type));
         }
@@ -365,7 +366,7 @@ struct inductive_cmd_fn {
         sort_section_params(section_locals, m_p, section_params);
         // First, add section_params to inductive types type.
         for (inductive_decl & d : decls) {
-            d = update_inductive_decl(d, m_p.pi_abstract(section_params, inductive_decl_type(d)));
+            d = update_inductive_decl(d, Pi(section_params, inductive_decl_type(d), m_p));
         }
         // Add section_params to introduction rules type, and also "fix"
         // occurrences of inductive types.
@@ -374,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 = m_p.pi_abstract(section_params, type);
+                type = Pi(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/parser.cpp

@@ -729,7 +729,11 @@ expr parser::parse_notation(parse_table t, expr * left) {
         case notation::action_kind::ScopedExpr: {
             expr r   = parse_scoped_expr(ps, lenv, a.rbp());
             if (is_var(a.get_rec(), 0)) {
-                r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos);
+                if (a.use_lambda_abstraction())
+                    r = Fun(ps, r);
+                else
+                    r = Pi(ps, r);
+                r = rec_save_pos(r, binder_pos);
             } else {
                 expr rec = copy_with_new_pos(a.get_rec(), p);
                 unsigned i = ps.size();
@@ -942,11 +946,6 @@ expr parser::parse_scoped_expr(unsigned num_ps, expr const * ps, local_environme
     return parse_expr(rbp);
 }
 
-expr parser::abstract(unsigned num_ps, expr const * ps, expr const & e, bool lambda, pos_info const & p) {
-    expr r = lambda ? Fun(num_ps, ps, e) : Pi(num_ps, ps, e);
-    return rec_save_pos(r, p);
-}
-
 void parser::parse_command() {
     lean_assert(curr() == scanner::token_kind::CommandKeyword);
     m_last_cmd_pos = pos();

src/frontends/lean/parser.h

@@ -231,12 +231,6 @@ public:
         return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp);
     }
     expr parse_scoped_expr(buffer<expr> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
-    expr abstract(unsigned num_params, expr const * ps, expr const & e, bool lambda, pos_info const & p);
-    expr abstract(buffer<expr> const & ps, expr const & e, bool lambda, pos_info const & p) { return abstract(ps.size(), ps.data(), e, lambda, p); }
-    expr lambda_abstract(buffer<expr> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, true, p); }
-    expr pi_abstract(buffer<expr> const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, false, p); }
-    expr lambda_abstract(buffer<expr> const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); }
-    expr pi_abstract(buffer<expr> const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); }
 
     struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
     void add_local_level(name const & n, level const & l);

src/frontends/lean/parser_bindings.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include <vector>
+#include "kernel/abstract.h"
 #include "frontends/lean/parser_bindings.h"
 
 namespace lean {
@@ -96,9 +97,9 @@ static int lambda_abstract(lua_State * L) {
     expr const & e = to_expr(L, 2);
     expr r;
     if (nargs == 2)
-        r = gparser.abstract(s->second.size(), s->second.data(), e, true, gparser.pos_of(e));
+        r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e), gparser.pos_of(e));
     else
-        r = gparser.abstract(s->second.size(), s->second.data(), e, true, pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4)));
+        r = gparser.rec_save_pos(Fun(s->second.size(), s->second.data(), e), pos_info(lua_tointeger(L, 3), lua_tointeger(L, 4)));
     return push_expr(L, r);
 }
 static int next(lua_State * L) { gparser.next(); return 0; }

src/frontends/lean/util.cpp

@@ -67,4 +67,12 @@ list<expr> locals_to_context(expr const & e, parser const & p) {
     std::reverse(locals.begin(), locals.end());
     return to_list(locals.begin(), locals.end());
 }
+
+expr Fun(buffer<expr> const & locals, expr const & e, parser & p) {
+    return p.rec_save_pos(Fun(locals, e), p.pos_of(e));
+}
+
+expr Pi(buffer<expr> const & locals, expr const & e, parser & p) {
+    return p.rec_save_pos(Pi(locals, e), p.pos_of(e));
+}
 }

src/frontends/lean/util.h

@@ -20,4 +20,8 @@ void collect_section_locals(expr const & type, expr const & value, parser const
 /** \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);
 list<expr> locals_to_context(expr const & e, parser const & p);
+/** \brief Fun(locals, e), but also propagate \c e position to result */
+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);
 }