From f70b1b028a11a6d75c9a94cf7594064b7770ac88 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 12:28:58 -0700 Subject: [PATCH] feat(frontends/lean): provide position to parse_fn external function, add 'by' expression Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 36 +++++++++++++--------- src/frontends/lean/builtin_tactic_cmds.cpp | 9 +++++- src/frontends/lean/parse_table.h | 3 +- src/frontends/lean/parser.cpp | 33 +++++++++++++++----- src/frontends/lean/parser.h | 6 ++++ tests/lean/run/t8.lean | 1 + 6 files changed, 65 insertions(+), 23 deletions(-) create mode 100644 tests/lean/run/t8.lean diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 5c3b3b5a1..a89892690 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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_body(parser & p) { +static expr parse_let(parser & p, pos_info const & pos); +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); - return mk_let(id, type, value, body); + expr body = abstract(parse_let_body(p, pos), l); + return p.save_pos(mk_let(id, type, value, body), pos); } } -static expr parse_let_expr(parser & p, unsigned, expr const *) { - return parse_let(p); +static expr parse_let_expr(parser & p, unsigned, expr const *, pos_info const & pos) { + return parse_let(p, pos); } -static expr parse_placeholder(parser &, unsigned, expr const *) { - return mk_expr_placeholder(); +static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const & pos) { + 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); diff --git a/src/frontends/lean/builtin_tactic_cmds.cpp b/src/frontends/lean/builtin_tactic_cmds.cpp index 763b2e5a4..e16d3753d 100644 --- a/src/frontends/lean/builtin_tactic_cmds.cpp +++ b/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; } } diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h index 54a422840..f2482483b 100644 --- a/src/frontends/lean/parse_table.h +++ b/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 parse_fn; +typedef std::function parse_fn; enum class action_kind { Skip, Expr, Exprs, Binder, Binders, ScopedExpr, Ext }; struct action_cell; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 955dfb3be..b2b22f9f0 100644 --- a/src/frontends/lean/parser.cpp +++ b/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()); - if (!p) + auto r = t.find(get_token_info().value()); + 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 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): - return tactic(); + if (curr_is_token(g_lparen)) { + 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() { diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 2fc4f50b9..e68967237 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -44,6 +44,7 @@ struct interrupt_parser {}; typedef local_decls local_expr_decls; typedef local_decls local_level_decls; typedef environment local_environment; +typedef std::unordered_map 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 elaborate(expr const & t, expr const & v, level_param_names const &); diff --git a/tests/lean/run/t8.lean b/tests/lean/run/t8.lean new file mode 100644 index 000000000..e7c750fae --- /dev/null +++ b/tests/lean/run/t8.lean @@ -0,0 +1 @@ +print raw (by skip) \ No newline at end of file