From f1e3449aae569948ed22a8f9617287c9562dc47b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 13:00:35 -0700 Subject: [PATCH] fix(frontends/lean): propagate position information Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_cmds.cpp | 8 +++++++- src/frontends/lean/builtin_exprs.cpp | 9 +++++---- src/frontends/lean/parser.cpp | 14 +++++++++----- src/frontends/lean/parser.h | 10 ++++++---- src/frontends/lean/token_table.cpp | 2 +- 5 files changed, 28 insertions(+), 15 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index b95d7cb44b..5223692529 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -74,6 +74,7 @@ static void update_parameters(buffer & ls_buffer, name_set const & found, } environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) { + auto pos = p.pos(); name n = p.check_id_next("invalid declaration, identifier expected"); check_atomic(n); buffer ls_buffer; @@ -104,7 +105,7 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) } type = p.elaborate(type, ls); if (in_section(p.env())) { - p.add_local_expr(n, mk_local(n, n, type), bi); + p.add_local_expr(n, p.save_pos(mk_local(n, n, type), pos), bi); return p.env(); } else { environment env = p.env(); @@ -313,8 +314,13 @@ environment set_line_cmd(parser & p) { return p.env(); } +environment exit_cmd(parser &) { + throw interrupt_parser(); +} + cmd_table init_cmd_table() { cmd_table r; + add_cmd(r, cmd_info("exit", "exit", exit_cmd)); add_cmd(r, cmd_info("print", "print a string", print_cmd)); add_cmd(r, cmd_info("universe", "declare a global universe level", universe_cmd)); add_cmd(r, cmd_info("section", "open a new section", section_cmd)); diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index a89892690d..fbc31f1d5d 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -48,11 +48,12 @@ static expr parse_let(parser & p, pos_info const & pos) { if (p.parse_local_notation_decl()) { return parse_let_body(p, pos); } else { - name id = p.check_id_next("invalid let declaration, identifier expected"); + auto pos = p.pos(); + name id = p.check_id_next("invalid let declaration, identifier expected"); expr type, value; if (p.curr_is_token(g_assign)) { p.next(); - type = mk_expr_placeholder(); + type = p.save_pos(mk_expr_placeholder(), pos); value = p.parse_expr(); } else if (p.curr_is_token(g_colon)) { p.next(); @@ -67,14 +68,14 @@ static expr parse_let(parser & p, pos_info const & pos) { p.next(); type = p.parse_scoped_expr(ps, lenv); } else { - type = mk_expr_placeholder(); + type = p.save_pos(mk_expr_placeholder(), pos); } p.check_token_next(g_assign, "invalid let declaration, ':=' expected"); value = p.parse_scoped_expr(ps, lenv); type = p.pi_abstract(ps, type); value = p.lambda_abstract(ps, value); } - expr l = mk_local(id, id, type); + expr l = p.save_pos(mk_local(id, id, type), pos); p.add_local(l); expr body = abstract(parse_let_body(p, pos), l); return p.save_pos(mk_let(id, type, value, body), pos); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b2b22f9f0a..18469de7da 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -538,7 +538,7 @@ void parser::parse_binder_block(buffer & r, binder_info const & bi) { } 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); + expr local = save_pos(mk_local(p.second, p.second, arg_type), p.first); add_local(local); r.push_back(parameter(p.first, local, bi)); } @@ -604,6 +604,7 @@ expr parser::parse_notation(parse_table t, expr * left) { buffer args; buffer ps; local_environment lenv(m_env); + pos_info binder_pos; if (left) args.push_back(*left); while (true) { @@ -649,24 +650,26 @@ expr parser::parse_notation(parse_table t, expr * left) { break; } case notation::action_kind::Binder: + binder_pos = pos(); ps.push_back(parse_binder()); break; case notation::action_kind::Binders: + binder_pos = pos(); lenv = parse_binders(ps); break; 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()); + r = abstract(ps, r, a.use_lambda_abstraction(), binder_pos); } else { unsigned i = ps.size(); while (i > 0) { --i; expr const & l = ps[i].m_local; if (a.use_lambda_abstraction()) - r = Fun(l, r, ps[i].m_bi); + r = save_pos(Fun(l, r, ps[i].m_bi), binder_pos); else - r = Pi(l, r, ps[i].m_bi); + r = save_pos(Pi(l, r, ps[i].m_bi), binder_pos); args.push_back(r); r = instantiate_rev(a.get_rec(), args.size(), args.data()); args.pop_back(); @@ -816,7 +819,7 @@ expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_ } } -expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda) { +expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p) { buffer locals; for (unsigned i = 0; i < num_params; i++) locals.push_back(ps[i].m_local); @@ -831,6 +834,7 @@ expr parser::abstract(unsigned num_params, parameter const * ps, expr const & e, r = mk_lambda(n, type, r, ps[i].m_bi); else r = mk_pi(n, type, r, ps[i].m_bi); + r = save_pos(r, p); } return r; } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index e689672370..e62e16b904 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -206,10 +206,12 @@ public: return parse_scoped_expr(num_params, ps, local_environment(m_env), rbp); } expr parse_scoped_expr(buffer & 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 const & ps, expr const & e, bool lambda = true) { return abstract(ps.size(), ps.data(), e, lambda); } - expr lambda_abstract(buffer const & ps, expr const & e) { return abstract(ps, e, true); } - expr pi_abstract(buffer const & ps, expr const & e) { return abstract(ps, e, false); } + expr abstract(unsigned num_params, parameter const * ps, expr const & e, bool lambda, pos_info const & p); + expr abstract(buffer const & ps, expr const & e, bool lambda, pos_info const & p) { return abstract(ps.size(), ps.data(), e, lambda, p); } + expr lambda_abstract(buffer const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, true, p); } + expr pi_abstract(buffer const & ps, expr const & e, pos_info const & p) { return abstract(ps, e, false, p); } + expr lambda_abstract(buffer const & ps, expr const & e) { return lambda_abstract(ps, e, pos_of(e)); } + expr pi_abstract(buffer const & ps, expr const & e) { return pi_abstract(ps, e, pos_of(e)); } tactic parse_tactic(unsigned rbp = 0); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 37ef1deb4a..4c12c523b2 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -65,7 +65,7 @@ token_table init_token_table() { "variables", "{variables}", "[variables]", "[private]", "[inline]", "abbreviation", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "inductive", "record", "structure", "module", "universe", - "precedence", "infixl", "infixr", "infix", "postfix", "notation", "#setline", nullptr}; + "precedence", "infixl", "infixr", "infix", "postfix", "notation", "exit", "#setline", nullptr}; std::pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},