feat(frontends/lean): provide position to parse_fn external function, add 'by' expression

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

src/frontends/lean/builtin_exprs.cpp

@@ -19,22 +19,22 @@ static name g_colon(":");
 static name g_assign(":=");
 static name g_comma(",");
 
-static expr parse_Type(parser & p, unsigned, expr const *) {
+static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
     if (p.curr_is_token(g_llevel_curly)) {
         p.next();
         level l = p.parse_level();
         p.check_token_next(g_rcurly, "invalid Type expression, '}' expected");
-        return mk_sort(l);
+        return p.save_pos(mk_sort(l), pos);
     } else {
-        return p.mk_Type();
+        return p.save_pos(p.mk_Type(), pos);
     }
 }
 
-static expr parse_let(parser & p);
+static expr parse_let(parser & p, pos_info const & pos);
-static expr parse_let_body(parser & p) {
+static expr parse_let_body(parser & p, pos_info const & pos) {
     if (p.curr_is_token(g_comma)) {
         p.next();
-        return parse_let(p);
+        return parse_let(p, pos);
     } else if (p.curr_is_token(g_in)) {
         p.next();
         return p.parse_expr();
@@ -43,10 +43,10 @@ static expr parse_let_body(parser & p) {
     }
 }
 
-static expr parse_let(parser & p) {
+static expr parse_let(parser & p, pos_info const & pos) {
     parser::local_scope scope1(p);
     if (p.parse_local_notation_decl()) {
-        return parse_let_body(p);
+        return parse_let_body(p, pos);
     } else {
         name id = p.check_id_next("invalid let declaration, identifier expected");
         expr type, value;
@@ -76,17 +76,24 @@ static expr parse_let(parser & p) {
         }
         expr l = mk_local(id, id, type);
         p.add_local(l);
-        expr body = abstract(parse_let_body(p), l);
+        expr body = abstract(parse_let_body(p, pos), l);
-        return mk_let(id, type, value, body);
+        return p.save_pos(mk_let(id, type, value, body), pos);
     }
 }
 
-static expr parse_let_expr(parser & p, unsigned, expr const *) {
+static expr parse_let_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return parse_let(p);
+    return parse_let(p, pos);
 }
 
-static expr parse_placeholder(parser &, unsigned, expr const *) {
+static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return mk_expr_placeholder();
+    return p.save_pos(mk_expr_placeholder(), pos);
+}
+
+static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) {
+    tactic t = p.parse_tactic();
+    expr r = p.save_pos(mk_expr_placeholder(), pos);
+    p.save_hint(r, t);
+    return r;
 }
 
 parse_table init_nud_table() {
@@ -96,6 +103,7 @@ parse_table init_nud_table() {
     expr x0 = mk_var(0);
     parse_table r;
     r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0);
+    r = r.add({transition("by", mk_ext_action(parse_by))}, x0);
     r = r.add({transition("(", Expr), transition(")", Skip)}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);

src/frontends/lean/builtin_tactic_cmds.cpp

@@ -7,7 +7,14 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser.h"
 
 namespace lean {
+tactic parse_skip_tactic(parser &) {
+    // TODO(Leo): this is just for testing
+    return tactic();
+}
+
 tactic_cmd_table get_builtin_tactic_cmds() {
-    return tactic_cmd_table();
+    tactic_cmd_table t;
+    t.insert("skip", tactic_cmd_info("skip", "dummy tactic", parse_skip_tactic));
+    return t;
 }
 }

src/frontends/lean/parse_table.h

@@ -10,11 +10,12 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "kernel/expr.h"
 #include "frontends/lean/token_table.h"
+#include "frontends/lean/parser_pos_provider.h"
 
 namespace lean {
 class parser;
 namespace notation {
-typedef std::function<expr(parser &, unsigned, expr const *)> parse_fn;
+typedef std::function<expr(parser &, unsigned, expr const *, pos_info const &)> parse_fn;
 
 enum class action_kind { Skip, Expr, Exprs, Binder, Binders, ScopedExpr, Ext };
 struct action_cell;

src/frontends/lean/parser.cpp

@@ -609,11 +609,11 @@ expr parser::parse_notation(parse_table t, expr * left) {
     while (true) {
         if (curr() != scanner::token_kind::Keyword)
             break;
-        auto p = t.find(get_token_info().value());
+        auto r = t.find(get_token_info().value());
-        if (!p)
+        if (!r)
             break;
         next();
-        notation::action const & a = p->first;
+        notation::action const & a = r->first;
         switch (a.kind()) {
         case notation::action_kind::Skip:
             break;
@@ -676,10 +676,10 @@ expr parser::parse_notation(parse_table t, expr * left) {
             break;
         }
         case notation::action_kind::Ext:
-            args.push_back(a.get_parse_fn()(*this, args.size(), args.data()));
+            args.push_back(a.get_parse_fn()(*this, args.size(), args.data(), p));
             break;
         }
-        t = p->second;
+        t = r->second;
     }
     list<expr> const & as = t.is_accepting();
     if (is_nil(as)) {
@@ -836,8 +836,27 @@ expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e,
 }
 
 tactic parser::parse_tactic(unsigned /* rbp */) {
-    // TODO(Leo):
+    if (curr_is_token(g_lparen)) {
-    return tactic();
+        next();
+        auto r = parse_tactic();
+        check_token_next(g_rparen, "invalid tactic, ')' expected");
+        return r;
+    } else if (curr_is_identifier()) {
+        auto p  = pos();
+        name id = get_name_val();
+        next();
+        if (auto it = tactic_cmds().find(id)) {
+            return it->get_fn()(*this);
+        } else {
+            throw parser_error(sstream() << "unknown tactic '" << id << "'", p);
+        }
+    } else {
+        throw parser_error("invalid tactic, '(' or tactic name expected", pos());
+    }
+}
+
+void parser::save_hint(expr const & e, tactic const & t) {
+    m_hints.insert(mk_pair(get_tag(e), t));
 }
 
 void parser::parse_command() {

src/frontends/lean/parser.h

@@ -44,6 +44,7 @@ struct interrupt_parser {};
 typedef local_decls<parameter> local_expr_decls;
 typedef local_decls<level>     local_level_decls;
 typedef environment            local_environment;
+typedef std::unordered_map<unsigned, tactic> hint_table;
 
 class parser {
     environment             m_env;
@@ -62,6 +63,7 @@ class parser {
     unsigned                m_next_tag_idx;
     bool                    m_found_errors;
     pos_info_table_ptr      m_pos_table;
+    hint_table              m_hints;
     // If m_type_use_placeholder is true, then the token Type is parsed as Type.{_}.
     // if it is false, then it is parsed as Type.{l} where l is a fresh parameter,
     // and is automatically inserted into m_local_level_decls.
@@ -95,6 +97,7 @@ class parser {
     cmd_table const & cmds() const { return get_cmd_table(env()); }
     parse_table const & nud() const { return get_nud_table(env()); }
     parse_table const & led() const { return get_led_table(env()); }
+    tactic_cmd_table const & tactic_cmds() const { return get_tactic_cmd_table(env()); }
 
     unsigned curr_level_lbp() const;
     level parse_max_imax(bool is_max);
@@ -230,6 +233,9 @@ public:
     struct param_universe_scope { parser & m_p; bool m_old; param_universe_scope(parser &); ~param_universe_scope(); };
     expr mk_Type();
 
+    /** \brief Use tactic \c t for "synthesizing" the placeholder \c e. */
+    void save_hint(expr const & e, tactic const & t);
+
     expr elaborate(expr const & e, level_param_names const &);
     std::pair<expr, expr> elaborate(expr const & t, expr const & v, level_param_names const &);
 

tests/lean/run/t8.lean

@@ -0,0 +1 @@
+print raw (by skip)