From 55eaef1a446872693cb3e2ec4d3e008969815913 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Aug 2013 09:56:07 -0700 Subject: [PATCH] Save position information when parsing expression in the lean default fronted. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_parser.cpp | 127 ++++++++++++++++++++--------- 1 file changed, 89 insertions(+), 38 deletions(-) diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 71ed4c3da..68a06148f 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -15,6 +15,7 @@ Author: Leonardo de Moura #include "printer.h" #include "state.h" #include "option_declarations.h" +#include "expr_maps.h" #include "lean_frontend.h" #include "lean_parser.h" #include "lean_scanner.h" @@ -92,6 +93,8 @@ static name g_unused(name(0u), "parser"); class parser_fn { typedef scoped_map local_decls; typedef std::unordered_map builtins; + typedef std::pair pos_info; + typedef expr_map expr_pos_info; frontend m_frontend; scanner m_scanner; scanner::token m_curr; @@ -101,6 +104,8 @@ class parser_fn { local_decls m_local_decls; unsigned m_num_local_decls; builtins m_builtins; + expr_pos_info m_expr_pos_info; + pos_info m_last_cmd_pos; /** \brief Exception used to track parsing erros, it does not leak outside of this class. */ struct parser_error : public exception { @@ -119,6 +124,21 @@ class parser_fn { ~mk_scope() { m_fn.m_num_local_decls = m_old_num_local_decls; } }; + /** \brief Return the current position information */ + pos_info pos() const { return mk_pair(m_scanner.get_line(), m_scanner.get_pos()); } + + /** \brief Return the position associated with \c e. If there is none, then return \c default_pos. */ + pos_info pos_of(expr const & e, pos_info default_pos) { + auto it = m_expr_pos_info.find(e); + if (it == m_expr_pos_info.end()) + return default_pos; + else + return it->second; + } + + /** \brief Associate position \c p with \c e and return \c e */ + expr save(expr const & e, pos_info p) { m_expr_pos_info[e] = p; return e; } + /** \brief Read the next token. */ void scan() { m_curr = m_scanner.scan(); } /** \brief Return the current token */ @@ -337,31 +357,41 @@ class parser_fn { /** \brief Parse a user defined prefix operator. */ expr parse_prefix(operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); expr arg = parse_expr(op.get_precedence()); - return mk_app(mk_fun(op), arg); + return save(mk_app(f, arg), p); } /** \brief Parse a user defined postfix operator. */ expr parse_postfix(expr const & left, operator_info const & op) { - return mk_app(mk_fun(op), left); + auto p = pos(); + expr f = save(mk_fun(op), p); + return save(mk_app(f, left), p); } /** \brief Parse a user defined infix operator. */ expr parse_infix(expr const & left, operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); expr right = parse_expr(op.get_precedence()+1); - return mk_app(mk_fun(op), left, right); + return save(mk_app(f, left, right), p); } /** \brief Parse a user defined infix-left operator. */ expr parse_infixl(expr const & left, operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); expr right = parse_expr(op.get_precedence()); - return mk_app(mk_fun(op), left, right); + return save(mk_app(f, left, right), p); } /** \brief Parse a user defined infix-right operator. */ expr parse_infixr(expr const & left, operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); expr right = parse_expr(op.get_precedence()-1); - return mk_app(mk_fun(op), left, right); + return save(mk_app(f, left, right), p); } /** @@ -386,26 +416,32 @@ class parser_fn { /** \brief Parse user defined mixfixl operator. It has the form: ID _ ... ID _ */ expr parse_mixfixl(operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); buffer args; - args.push_back(mk_fun(op)); + args.push_back(f); args.push_back(parse_expr(op.get_precedence())); parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); - return mk_app(args.size(), args.data()); + return save(mk_app(args.size(), args.data()), p); } /** \brief Parse user defined mixfixr operator. It has the form: _ ID ... _ ID */ expr parse_mixfixr(expr const & left, operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); buffer args; - args.push_back(mk_fun(op)); + args.push_back(f); args.push_back(left); parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); - return mk_app(args.size(), args.data()); + return save(mk_app(args.size(), args.data()), p); } /** \brief Parse user defined mixfixc operator. It has the form: ID _ ID ... _ ID */ expr parse_mixfixc(operator_info const & op) { + auto p = pos(); + expr f = save(mk_fun(op), p); buffer args; - args.push_back(mk_fun(op)); + args.push_back(f); args.push_back(parse_expr(op.get_precedence())); list const & ops = op.get_op_name_parts(); auto it = ops.begin(); @@ -414,7 +450,7 @@ class parser_fn { check_op_part(*it); ++it; if (it == ops.end()) - return mk_app(args.size(), args.data()); + return save(mk_app(args.size(), args.data()), p); args.push_back(parse_expr(op.get_precedence())); } } @@ -452,11 +488,12 @@ class parser_fn { functions can begin a language construct. */ expr parse_nud_id() { + auto p = pos(); name id = curr_name(); next(); auto it = m_local_decls.find(id); if (it != m_local_decls.end()) { - return mk_var(m_num_local_decls - it->second - 1); + return save(mk_var(m_num_local_decls - it->second - 1), p); } else { operator_info op = m_frontend.find_nud(id); if (op) { @@ -467,7 +504,7 @@ class parser_fn { default: lean_unreachable(); return expr(); } } else { - return get_name_ref(id); + return save(get_name_ref(id), p); } } } @@ -482,11 +519,13 @@ class parser_fn { can appear inside of a construct. */ expr parse_led_id(expr const & left) { + auto p = pos(); + auto p2 = pos_of(left, p); name id = curr_name(); next(); auto it = m_local_decls.find(id); if (it != m_local_decls.end()) { - return mk_app(left, mk_var(m_num_local_decls - it->second - 1)); + return save(mk_app(left, save(mk_var(m_num_local_decls - it->second - 1), p)), p2); } else { operator_info op = m_frontend.find_led(id); if (op) { @@ -498,32 +537,35 @@ class parser_fn { default: lean_unreachable(); return expr(); } } else { - return mk_app(left, get_name_ref(id)); + return save(mk_app(left, save(get_name_ref(id), p)), p2); } } } /** \brief Parse expr '=' expr. */ expr parse_eq(expr const & left) { + auto p = pos(); next(); expr right = parse_expr(g_eq_precedence); - return mk_eq(left, right); + return save(mk_eq(left, right), p); } /** \brief Parse expr '->' expr. */ expr parse_arrow(expr const & left) { + auto p = pos(); next(); mk_scope scope(*this); register_binding(g_unused); // The -1 is a trick to get right associativity in Pratt's parsers expr right = parse_expr(g_arrow_precedence-1); - return mk_arrow(left, right); + return save(mk_arrow(left, right), p); } /** \brief Parse '(' expr ')'. */ expr parse_lparen() { + auto p = pos(); next(); - expr r = parse_expr(); + expr r = save(parse_expr(), p); check_rparen_next("invalid expression, ')' expected"); return r; } @@ -532,9 +574,9 @@ class parser_fn { \brief Parse a sequence of identifiers ID*. Store the result in \c result. */ - void parse_names(buffer & result) { + void parse_names(buffer> & result) { while (curr_is_identifier()) { - result.push_back(curr_name()); + result.push_back(mk_pair(pos(), curr_name())); next(); } } @@ -551,18 +593,18 @@ class parser_fn { \brief Parse ID ... ID ':' expr, where the expression represents the type of the identifiers. */ - void parse_simple_bindings(buffer> & result) { - buffer names; + void parse_simple_bindings(buffer> & result) { + buffer> names; parse_names(names); check_colon_next("invalid binder, ':' expected"); unsigned sz = result.size(); result.resize(sz + names.size()); expr type = parse_expr(); - for (name const & n : names) register_binding(n); + for (std::pair const & n : names) register_binding(n.second); unsigned i = names.size(); while (i > 0) { --i; - result[sz + i] = mk_pair(names[i], lift_free_vars(type, i)); + result[sz + i] = std::make_tuple(names[i].first, names[i].second, lift_free_vars(type, i)); } } @@ -571,7 +613,7 @@ class parser_fn { This is used when parsing lambda, Pi, forall/exists expressions and definitions. */ - void parse_bindings(buffer> & result) { + void parse_bindings(buffer> & result) { if (curr_is_identifier()) { parse_simple_bindings(result); } else { @@ -591,15 +633,16 @@ class parser_fn { \brief Create a lambda/Pi abstraction, using the giving binders and body. */ - expr mk_abstraction(bool is_lambda, buffer> const & bindings, expr const & body) { + expr mk_abstraction(bool is_lambda, buffer> const & bindings, expr const & body) { expr result = body; unsigned i = bindings.size(); while (i > 0) { --i; + pos_info p = std::get<0>(bindings[i]); if (is_lambda) - result = mk_lambda(bindings[i].first, bindings[i].second, result); + result = save(mk_lambda(std::get<1>(bindings[i]), std::get<2>(bindings[i]), result), p); else - result = mk_pi(bindings[i].first, bindings[i].second, result); + result = save(mk_pi(std::get<1>(bindings[i]), std::get<2>(bindings[i]), result), p); } return result; } @@ -608,7 +651,7 @@ class parser_fn { expr parse_abstraction(bool is_lambda) { next(); mk_scope scope(*this); - buffer> bindings; + buffer> bindings; parse_bindings(bindings); check_comma_next("invalid abstraction, ',' expected"); expr result = parse_expr(); @@ -629,17 +672,19 @@ class parser_fn { expr parse_quantifier(bool is_forall) { next(); mk_scope scope(*this); - buffer> bindings; + buffer> bindings; parse_bindings(bindings); check_comma_next("invalid quantifier, ',' expected"); expr result = parse_expr(); unsigned i = bindings.size(); while (i > 0) { --i; + pos_info p = std::get<0>(bindings[i]); + expr lambda = save(mk_lambda(std::get<1>(bindings[i]), std::get<2>(bindings[i]), result), p); if (is_forall) - result = mk_forall(bindings[i].second, mk_lambda(bindings[i].first, bindings[i].second, result)); + result = save(mk_forall(std::get<2>(bindings[i]), lambda), p); else - result = mk_exists(bindings[i].second, mk_lambda(bindings[i].first, bindings[i].second, result)); + result = save(mk_exists(std::get<2>(bindings[i]), lambda), p); } return result; } @@ -658,20 +703,22 @@ class parser_fn { expr parse_let() { next(); mk_scope scope(*this); - buffer> bindings; + buffer> bindings; while (true) { + auto p = pos(); name id = check_identifier_next("invalid let expression, identifier expected"); check_assign_next("invalid let expression, ':=' expected"); expr val = parse_expr(); register_binding(id); - bindings.push_back(mk_pair(id, val)); + bindings.push_back(std::make_tuple(p, id, val)); if (curr_is_in()) { next(); expr r = parse_expr(); unsigned i = bindings.size(); while (i > 0) { --i; - r = mk_let(bindings[i].first, bindings[i].second, r); + auto p = std::get<0>(bindings[i]); + r = save(mk_let(std::get<1>(bindings[i]), std::get<2>(bindings[i]), r), p); } return r; } else { @@ -682,7 +729,8 @@ class parser_fn { /** \brief Parse an integer value. */ expr parse_int() { - expr r = mk_int_value(m_scanner.get_num_val().get_numerator()); + auto p = pos(); + expr r = save(mk_int_value(m_scanner.get_num_val().get_numerator()), p); next(); return r; } @@ -697,9 +745,10 @@ class parser_fn { /** \brief Parse 'Type' and 'Type' level expressions. */ expr parse_type() { + auto p = pos(); next(); if (curr_is_identifier() || curr_is_int()) { - return mk_type(parse_level()); + return save(mk_type(parse_level()), p); } else { return Type(); } @@ -800,7 +849,7 @@ class parser_fn { val = elaborate(parse_expr()); } else { mk_scope scope(*this); - buffer> bindings; + buffer> bindings; parse_bindings(bindings); check_colon_next("invalid definition, ':' expected"); expr type_body = parse_expr(); @@ -1069,6 +1118,8 @@ class parser_fn { /** \brief Parse a Lean command. */ void parse_command() { + m_expr_pos_info.clear(); + m_last_cmd_pos = pos(); name const & cmd_id = curr_name(); if (cmd_id == g_definition_kwd) parse_definition(); else if (cmd_id == g_variable_kwd) parse_variable();