feat(frontends/lean/parser): add parser_binder(s) and abstract methods

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

src/frontends/lean/parser.cpp

@@ -4,17 +4,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
 #include <string>
 #include <limits>
 #include "util/interrupt.h"
 #include "util/script_exception.h"
 #include "util/sstream.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/abstract.h"
 #include "library/io_state_stream.h"
 #include "library/parser_nested_exception.h"
 #include "library/aliases.h"
 #include "library/private.h"
 #include "library/choice.h"
+#include "library/placeholder.h"
 #include "library/deep_copy.h"
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
@@ -171,13 +174,132 @@ bool parser::curr_is_token(name const & tk) const {
         get_token_info().value() == tk;
 }
 
+void parser::check_token_next(name const & tk, char const * msg) {
+    if (!curr_is_token(tk))
+        throw parser_error(msg, pos());
+    next();
+}
+
 expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
     return save_pos(::lean::mk_app(fn, arg), p);
 }
 
-// expr parser::copy_expr(expr const & e, pos_info const & p) {
+void parser::add_local_entry(name const & n, expr const & e) {
-//     return replace(e, [](
+    m_local_decls.insert(n, local_entry(e, m_local_decls.size()));
-// }
+}
+
+void parser::add_local_decl(expr const & e) {
+    lean_assert(is_local(e));
+    add_local_entry(local_pp_name(e), e);
+}
+
+/** \brief Parse a sequence of identifiers <tt>ID*</tt>. Store the result in \c result. */
+void parser::parse_names(buffer<std::pair<pos_info, name>> & result) {
+    while (curr_is_identifier()) {
+        result.emplace_back(pos(), get_name_val());
+        next();
+    }
+}
+
+static name g_period(".");
+static name g_colon(":");
+static name g_lparen("(");
+static name g_rparen(")");
+static name g_lcurly("{");
+static name g_rcurly("}");
+static name g_lbracket("[");
+static name g_rbracket("]");
+
+/** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
+parameter parser::parse_binder_core(binder_info const & bi) {
+    auto p  = pos();
+    if (!curr_is_identifier())
+        throw parser_error("invalid binder, identifier expected", p);
+    name id = get_name_val();
+    next();
+    expr type;
+    if (curr_is_token(g_colon)) {
+        next();
+        type = parse_expr();
+    } else {
+        type = save_pos(mk_expr_placeholder(), p);
+    }
+    return parameter(p, save_pos(mk_local(id, id, type), p), bi);
+}
+
+parameter parser::parse_binder() {
+    if (curr_is_identifier()) {
+        return parse_binder_core(binder_info());
+    } else if (curr_is_token(g_lparen)) {
+        next();
+        auto p = parse_binder_core(binder_info());
+        check_token_next(g_rparen, "invalid binder, ')' expected");
+        return p;
+    } else if (curr_is_token(g_lcurly)) {
+        next();
+        auto p = parse_binder_core(mk_implicit_binder_info());
+        check_token_next(g_rparen, "invalid binder, '}' expected");
+        return p;
+    } else if (curr_is_token(g_lbracket)) {
+        next();
+        auto p = parse_binder_core(mk_cast_binder_info());
+        check_token_next(g_rparen, "invalid binder, ']' expected");
+        return p;
+    } else {
+        throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
+    }
+}
+
+/**
+   \brief Parse <tt>ID ... ID ':' expr</tt>, where the expression
+   represents the type of the identifiers.
+*/
+void parser::parse_binder_block(buffer<parameter> & r, binder_info const & bi) {
+    buffer<std::pair<pos_info, name>> names;
+    parse_names(names);
+    if (names.empty())
+        throw parser_error("invalid binder, identifier expected", pos());
+    optional<expr> type;
+    if (curr_is_token(g_colon)) {
+        next();
+        type = parse_expr();
+    }
+    for (auto p : names) {
+        expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
+        expr local = mk_local(p.second, p.second, arg_type);
+        add_local_decl(local);
+        r.push_back(parameter(p.first, local, bi));
+    }
+}
+
+void parser::parse_binders_core(buffer<parameter> & r) {
+    if (curr_is_identifier()) {
+        parse_binder_block(r, binder_info());
+    } else if (curr_is_token(g_lparen)) {
+        next();
+        parse_binder_block(r, binder_info());
+        check_token_next(g_rparen, "invalid binder, ')' expected");
+    } else if (curr_is_token(g_lcurly)) {
+        next();
+        parse_binder_block(r, mk_implicit_binder_info());
+        check_token_next(g_rparen, "invalid binder, '}' expected");
+    } else if (curr_is_token(g_lbracket)) {
+        next();
+        parse_binder_block(r, mk_cast_binder_info());
+        check_token_next(g_rparen, "invalid binder, ']' expected");
+    } else {
+        return;
+    }
+    parse_binders_core(r);
+}
+
+void parser::parse_binders(buffer<parameter> & r) {
+    local_decls::mk_scope scope(m_local_decls);
+    unsigned old_sz = r.size();
+    parse_binders_core(r);
+    if (old_sz == r.size())
+        throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
+}
 
 expr parser::parse_nud_keyword() {
     // TODO(Leo)
@@ -267,13 +389,37 @@ expr parser::parse_expr(unsigned rbp) {
 
 expr parser::parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp) {
     local_decls::mk_scope scope(m_local_decls);
-    for (unsigned i = 0; i < num_locals; i++) {
+    for (unsigned i = 0; i < num_locals; i++)
-        lean_assert(is_local(locals[i]));
+        add_local_decl(locals[i]);
-        m_local_decls.insert(local_pp_name(locals[i]), local_entry(locals[i], m_local_decls.size()));
-    }
     return parse_expr(rbp);
 }
 
+expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp) {
+    local_decls::mk_scope scope(m_local_decls);
+    for (unsigned i = 0; i < num_params; i++)
+        add_local_decl(ps[i].m_local);
+    return parse_expr(rbp);
+}
+
+expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda) {
+    buffer<expr> locals;
+    for (unsigned i = 0; i < num_params; i++)
+        locals.push_back(ps[i].m_local);
+    expr r = ::lean::abstract(e, locals.size(), locals.data());
+    unsigned i = num_params;
+    while (i > 0) {
+        --i;
+        expr const & l = ps[i].m_local;
+        name const & n = local_pp_name(l);
+        expr type  = ::lean::abstract(mlocal_type(l), i, locals.data());
+        if (lambda)
+            r = mk_lambda(n, type, r);
+        else
+            r = mk_pi(n, type, r);
+    }
+    return r;
+}
+
 tactic parser::parse_tactic(unsigned /* rbp */) {
     // TODO(Leo):
     return tactic();
@@ -305,7 +451,6 @@ void parser::parse_script(bool as_expr) {
         });
 }
 
-static name g_period(".");
 bool parser::parse_commands() {
     // We disable hash-consing while parsing to make sure the pos-info are correct.
     scoped_expr_caching disable(false);

src/frontends/lean/parser.h

@@ -23,11 +23,10 @@ Author: Leonardo de Moura
 namespace lean {
 struct parameter {
     pos_info    m_pos;
-    name        m_name;
+    expr        m_local;
-    expr        m_type;
     binder_info m_bi;
-    parameter(pos_info const & p, name const & n, expr const & t, binder_info const & bi):
+    parameter(pos_info const & p, expr const & l, binder_info const & bi):
-        m_pos(p), m_name(n), m_type(t), m_bi(bi) {}
+        m_pos(p), m_local(l), m_bi(bi) {}
     parameter():m_pos(0, 0) {}
 };
 
@@ -95,6 +94,9 @@ class parser {
     parse_table const & nud() const { return cfg().m_nud; }
     parse_table const & led() const { return cfg().m_led; }
 
+    void add_local_entry(name const & n, expr const & e);
+    void add_local_decl(expr const & t);
+
     void parse_command();
     void parse_script(bool as_expr = false);
     bool parse_commands();
@@ -107,6 +109,9 @@ class parser {
     expr parse_numeral_expr();
     expr parse_decimal_expr();
     expr parse_string_expr();
+    parameter parse_binder_core(binder_info const & bi);
+    void parse_binder_block(buffer<parameter> & r, binder_info const & bi);
+    void parse_binders_core(buffer<parameter> & r);
     expr mk_app(expr fn, expr arg, pos_info const & p);
 
 public:
@@ -118,11 +123,17 @@ public:
     io_state const & ios() const { return m_ios; }
     script_state * ss() const { return m_ss; }
 
+    void parse_names(buffer<std::pair<pos_info, name>> & result);
+
     parameter parse_binder();
     void parse_binders(buffer<parameter> & r);
 
     expr parse_expr(unsigned rbp = 0);
     expr parse_scoped_expr(unsigned num_locals, expr const * locals, unsigned rbp = 0);
+    expr parse_scoped_expr(unsigned num_params, parameter const * ps, unsigned rbp = 0);
+    expr parse_scoped_expr(buffer<parameter> & ps, unsigned rbp = 0) { return parse_scoped_expr(ps.size(), ps.data(), rbp); }
+    expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda = true);
+    expr abstract(buffer<parameter> const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); }
 
     tactic parse_tactic(unsigned rbp = 0);
 
@@ -137,10 +148,14 @@ public:
     void scan() { m_curr = m_scanner.scan(m_env); }
     /** \brief Return the current token */
     scanner::token_kind curr() const { return m_curr; }
+    /** \brief Return true iff the current token is an identifier */
+    bool curr_is_identifier() const { return curr() == scanner::token_kind::Identifier; }
     /** \brief Read the next token if the current one is not End-of-file. */
     void next() { if (m_curr != scanner::token_kind::Eof) scan(); }
     /** \brief Return true iff the current token is equal to \c tk */
     bool curr_is_token(name const & tk) const;
+    /** \brief Check current token, and move to next characther, throw exception if current token is not \c tk. */
+    void check_token_next(name const & tk, char const * msg);
 
     mpq const & get_num_val() const { return m_scanner.get_num_val(); }
     name const & get_name_val() const { return m_scanner.get_name_val(); }

src/kernel/expr.h

@@ -252,6 +252,9 @@ public:
     bool is_contextual() const { return m_contextual; }
 };
 
+inline binder_info mk_implicit_binder_info() { return binder_info(true); }
+inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
+
 bool operator==(binder_info const & i1, binder_info const & i2);
 inline bool operator!=(binder_info const & i1, binder_info const & i2) { return !(i1 == i2); }