From 206c7fa20349810e2fd16f090253ebdc2eda5424 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Aug 2013 09:45:00 -0700 Subject: [PATCH] Implement support for notation + implicit arguments. Cleanup pretty printer code for handling implicit arguments. Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_frontend.cpp | 63 +++-- src/frontends/lean/lean_parser.cpp | 88 ++++--- src/frontends/lean/lean_pp.cpp | 344 ++++++++++++++++----------- 3 files changed, 302 insertions(+), 193 deletions(-) diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index b9da61a47b..6ee179d430 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -97,14 +97,6 @@ struct frontend::imp { return operator_info(); } - void diagnostic_msg(char const * msg) { - // TODO - } - - void report_op_redefined(operator_info const & old_op, operator_info const & new_op) { - // TODO - } - /** \brief Remove all internal denotations that are associated with the given operator symbol (aka notation) */ void remove_bindings(operator_info const & op) { for (expr const & d : op.get_exprs()) { @@ -124,6 +116,34 @@ struct frontend::imp { insert(m_expr_to_operator, d, new_op); } + /** + \brief Two operator (aka notation) denotations are compatible + iff one of the following holds: + + 1) Both do not have implicit arguments + + 2) Both have implicit arguments, and the implicit arguments + occur in the same positions. + + */ + bool compatible_denotation(expr const & d1, expr const & d2) { + return get_implicit_arguments(d1) == get_implicit_arguments(d2); + } + + /** + \brief Return true iff the existing denotations (aka + overloads) for an operator op are compatible with the new + denotation d. + + The compatibility is only an issue if implicit arguments are + used. If one of the denotations has implicit arguments, then + all of them should have implicit arguments, and the implicit + arguments should occur in the same positions. + */ + bool compatible_denotations(operator_info const & op, expr const & d) { + return std::all_of(op.get_exprs().begin(), op.get_exprs().end(), [&](expr const & prev_d) { return compatible_denotation(prev_d, d); }); + } + /** \brief Add a new operator and save information as object. @@ -141,17 +161,23 @@ struct frontend::imp { if (!old_op) { register_new_op(new_op, d, led); } else if (old_op == new_op) { - // overload - if (defined_here(old_op, led)) { - old_op.add_expr(d); + if (compatible_denotations(old_op, d)) { + // overload + if (defined_here(old_op, led)) { + old_op.add_expr(d); + } else { + // we must copy the operator because it was defined in + // a parent frontend. + new_op = old_op.copy(); + register_new_op(new_op, d, led); + } } else { - // we must copy the operator because it was defined in - // a parent frontend. - new_op = old_op.copy(); + diagnostic(m_state) << "The denotation(s) for the existing notation:\n " << old_op << "\nhave been replaced with the new denotation:\n " << d << "\nbecause they conflict on how implicit arguments are used.\n"; + remove_bindings(old_op); register_new_op(new_op, d, led); } } else { - report_op_redefined(old_op, new_op); + diagnostic(m_state) << "Notation has been redefined, the existing notation:\n " << old_op << "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n"; remove_bindings(old_op); register_new_op(new_op, d, led); } @@ -214,6 +240,13 @@ struct frontend::imp { } } + std::vector const & get_implicit_arguments(expr const & n) { + if (is_constant(n)) + return get_implicit_arguments(const_name(n)); + else + return g_empty_vector; + } + name const & get_explicit_version(name const & n) { auto it = m_implicit_table.find(n); if (it != m_implicit_table.end()) { diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index f86ed3ce32..198abafe83 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -400,43 +400,72 @@ class parser::imp { return r; } + /** + \brief Create an application for the given operator and + (explicit) arguments. + */ + expr mk_application(operator_info const & op, pos_info const & pos, unsigned num_args, expr const * args) { + buffer new_args; + expr f = save(mk_fun(op), pos); + new_args.push_back(f); + // I'm using the fact that all denotations are compatible. + // See lean_frontend.cpp for the definition of compatible denotations. + expr const & d = head(op.get_exprs()); + if (is_constant(d) && m_frontend.has_implicit_arguments(const_name(d))) { + std::vector const & imp_args = m_frontend.get_implicit_arguments(const_name(d)); + unsigned i = 0; + for (unsigned j = 0; j < imp_args.size(); j++) { + if (imp_args[j]) { + new_args.push_back(save(mk_metavar(), pos)); + } else { + if (i >= num_args) + throw parser_error(sstream() << "unexpected number of arguments for denotation with implicit arguments, it expects " << num_args << " explicit argument(s)", pos); + new_args.push_back(args[i]); + i++; + } + } + } else { + new_args.append(num_args, args); + } + return save(mk_app(new_args.size(), new_args.data()), pos); + } + expr mk_application(operator_info const & op, pos_info const & pos, std::initializer_list const & l) { + return mk_application(op, pos, l.size(), l.begin()); + } + expr mk_application(operator_info const & op, pos_info const & pos, expr const & arg) { + return mk_application(op, pos, 1, &arg); + } + expr mk_application(operator_info const & op, pos_info const & pos, buffer const & args) { + return mk_application(op, pos, args.size(), args.data()); + } + /** \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 save(mk_app(f, arg), p); + return mk_application(op, p, parse_expr(op.get_precedence())); } /** \brief Parse a user defined postfix operator. */ expr parse_postfix(expr const & left, operator_info const & op) { - auto p = pos(); - expr f = save(mk_fun(op), p); - return save(mk_app(f, left), p); + return mk_application(op, pos(), left); } /** \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 save(mk_app(f, left, right), p); + return mk_application(op, p, {left, parse_expr(op.get_precedence()+1)}); } /** \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 save(mk_app(f, left, right), p); + return mk_application(op, p, {left, parse_expr(op.get_precedence())}); } /** \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 save(mk_app(f, left, right), p); + return mk_application(op, p, {left, parse_expr(op.get_precedence()-1)}); } /** @@ -462,31 +491,25 @@ class parser::imp { /** \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(f); args.push_back(parse_expr(op.get_precedence())); parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); - return save(mk_app(args.size(), args.data()), p); + return mk_application(op, p, args); } /** \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(f); args.push_back(left); parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); - return save(mk_app(args.size(), args.data()), p); + return mk_application(op, p, args); } /** \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(f); args.push_back(parse_expr(op.get_precedence())); list const & ops = op.get_op_name_parts(); auto it = ops.begin(); @@ -495,22 +518,11 @@ class parser::imp { check_op_part(*it); ++it; if (it == ops.end()) - return save(mk_app(args.size(), args.data()), p); + return mk_application(op, p, args); args.push_back(parse_expr(op.get_precedence())); } } - /** \brief Return true iff all implicit arguments occur in the beginning. */ - bool is_imp_arg_prefix(std::vector const & imp_args) { - for (unsigned i = 0; i < imp_args.size(); i++) { - // Remark: I'm using the fact that the implicit argument - // positions are sorted. - if (imp_args[i] != i) - return false; - } - return true; - } - /** \brief Try to find an object (Definition or Postulate) named \c id in the frontend/environment. If there isn't one, then tries @@ -1146,7 +1158,8 @@ class parser::imp { unsigned prec = parse_precedence(); name op_id = parse_op_id(); check_colon_next("invalid operator definition, ':' expected"); - expr d = parse_expr(); + name name_id = check_identifier_next("invalid operator definition, identifier expected"); + expr d = mk_constant(name_id); switch (fx) { case fixity::Prefix: m_frontend.add_prefix(op_id, prec, d); break; case fixity::Postfix: m_frontend.add_postfix(op_id, prec, d); break; @@ -1174,7 +1187,8 @@ class parser::imp { } lean_assert(curr_is_colon()); next(); - expr d = parse_expr(); + name name_id = check_identifier_next("invalid operator definition, identifier expected"); + expr d = mk_constant(name_id); switch (fx) { case fixity::Mixfixl: m_frontend.add_mixfixl(parts.size(), parts.data(), prec, d); break; case fixity::Mixfixr: m_frontend.add_mixfixr(parts.size(), parts.data(), prec, d); break; diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 785bdd31be..424e21fd52 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -200,59 +200,6 @@ class pp_fn { } } - /** - \brief Return the operator associated with \c e. - Return the null operator if there is none. - - We say \c e has an operator associated with it, if: - - 1) \c e is associated with an operator. - - 2) It is an application, and the function is associated with an - operator. - */ - operator_info get_operator(expr const & e) { - operator_info op = m_frontend.find_op_for(e); - if (op) - return op; - else if (is_app(e)) - return m_frontend.find_op_for(arg(e, 0)); - else - return operator_info(); - } - - /** - \brief Return the precedence of the given expression - */ - unsigned get_operator_precedence(expr const & e) { - if (is_constant(e)) { - operator_info op = get_operator(e); - return op ? op.get_precedence() : 0; - } else if (is_eq(e)) { - return g_eq_precedence; - } else if (is_arrow(e)) { - return g_arrow_precedence; - } else { - return 0; - } - } - - /** \brief Return true if the application \c e has the number of arguments expected by the operator \c op. */ - bool has_expected_num_args(expr const & e, operator_info const & op) { - switch (op.get_fixity()) { - case fixity::Infix: case fixity::Infixl: case fixity::Infixr: - return num_args(e) == 3; - case fixity::Prefix: case fixity::Postfix: - return num_args(e) == 2; - case fixity::Mixfixl: case fixity::Mixfixr: - return num_args(e) == length(op.get_op_name_parts()) + 1; - case fixity::Mixfixc: - return num_args(e) == length(op.get_op_name_parts()); - } - lean_unreachable(); - return false; - } - /** \brief Pretty print given expression and put parenthesis around it IF the pp of the expression is not a simple name. @@ -280,42 +227,6 @@ class pp_fn { return pp_child_with_paren(e, depth); } - /** - \brief Pretty print the child of an infix, prefix, postfix or - mixfix operator. It will add parethesis when needed. - */ - result pp_mixfix_child(operator_info const & op, expr const & e, unsigned depth) { - if (is_atomic(e)) { - return pp(e, depth + 1); - } else { - if (op.get_precedence() < get_operator_precedence(e)) - return pp(e, depth + 1); - else - return pp_child_with_paren(e, depth); - } - } - - /** - \brief Pretty print the child of an associative infix - operator. It will add parethesis when needed. - */ - result pp_infix_child(operator_info const & op, expr const & e, unsigned depth) { - if (is_atomic(e)) { - return pp(e, depth + 1); - } else { - if (op.get_precedence() < get_operator_precedence(e) || op == get_operator(e)) - return pp(e, depth + 1); - else - return pp_child_with_paren(e, depth); - } - } - - result mk_infix(operator_info const & op, result const & lhs, result const & rhs) { - unsigned r_weight = lhs.second + rhs.second + 1; - format r_format = group(format{lhs.first, space(), format(op.get_op_name()), line(), rhs.first}); - return mk_result(r_format, r_weight); - } - bool is_forall_expr(expr const & e) { return is_app(e) && arg(e, 0) == mk_forall_fn() && num_args(e) == 3; } @@ -359,6 +270,8 @@ class pp_fn { } } + /** \brief Auxiliary function for pretty printing exists and + forall formulas */ result pp_quantifier(expr const & e, unsigned depth, bool is_forall) { buffer> nested; expr b = collect_nested_quantifiers(e, is_forall, nested); @@ -416,38 +329,214 @@ class pp_fn { return pp_quantifier(e, depth, false); } + /** + \brief Return the operator associated with \c e. + Return the null operator if there is none. + + We say \c e has an operator associated with it, if: + + 1) \c e is associated with an operator. + + 2) It is an application, and the function is associated with an + operator. + */ + operator_info get_operator(expr const & e) { + operator_info op = m_frontend.find_op_for(e); + if (op) + return op; + else if (is_app(e)) + return m_frontend.find_op_for(arg(e, 0)); + else + return operator_info(); + } + + /** + \brief Return the precedence of the given expression + */ + unsigned get_operator_precedence(expr const & e) { + if (is_constant(e)) { + operator_info op = get_operator(e); + return op ? op.get_precedence() : 0; + } else if (is_eq(e)) { + return g_eq_precedence; + } else if (is_arrow(e)) { + return g_arrow_precedence; + } else { + return 0; + } + } + + /** + \brief Pretty print the child of an infix, prefix, postfix or + mixfix operator. It will add parethesis when needed. + */ + result pp_mixfix_child(operator_info const & op, expr const & e, unsigned depth) { + if (is_atomic(e)) { + return pp(e, depth + 1); + } else { + if (op.get_precedence() < get_operator_precedence(e)) + return pp(e, depth + 1); + else + return pp_child_with_paren(e, depth); + } + } + + /** + \brief Pretty print the child of an associative infix + operator. It will add parethesis when needed. + */ + result pp_infix_child(operator_info const & op, expr const & e, unsigned depth) { + if (is_atomic(e)) { + return pp(e, depth + 1); + } else { + if (op.get_precedence() < get_operator_precedence(e) || op == get_operator(e)) + return pp(e, depth + 1); + else + return pp_child_with_paren(e, depth); + } + } + + result mk_infix(operator_info const & op, result const & lhs, result const & rhs) { + unsigned r_weight = lhs.second + rhs.second + 1; + format r_format = group(format{lhs.first, space(), format(op.get_op_name()), line(), rhs.first}); + return mk_result(r_format, r_weight); + } + + /** + \brief Wrapper for accessing the explicit arguments of an + application and its function. + + \remark If show_implicit is true, then we show the explicit + arguments even if the function has implicit arguments. + + \remark We also show the implicit arguments, if the + application does not have the necessary number of + arguments. + + \remark When we expose the implicit arguments, we use the + explicit version of the function. So, the user can + understand the pretty printed term. + */ + struct application { + expr const & m_app; + expr m_f; + std::vector const * m_implicit_args; + bool m_notation_enabled; + + application(expr const & e, frontend const & fe, bool show_implicit):m_app(e) { + expr const & f = arg(e,0); + if (is_constant(f) && fe.has_implicit_arguments(const_name(f))) { + m_implicit_args = &(fe.get_implicit_arguments(const_name(f))); + if (show_implicit || num_args(e) - 1 < m_implicit_args->size()) { + // we are showing implicit arguments, thus we do + // not need the bit-mask for implicit arguments + m_implicit_args = nullptr; + // we use the explicit name of f, to make it clear + // that we are exposing implicit arguments + m_f = mk_constant(fe.get_explicit_version(const_name(f))); + m_notation_enabled = false; + } else { + m_f = f; + m_notation_enabled = true; + } + } else { + m_f = f; + m_implicit_args = nullptr; + m_notation_enabled = true; + } + } + + unsigned get_num_args() const { + if (m_implicit_args) { + unsigned r = 0; + for (unsigned i = 0; i < num_args(m_app) - 1; i++) { + if (!(*m_implicit_args)[i]) + r++; + } + return r; + } else { + return num_args(m_app) - 1; + } + } + + expr const & get_arg(unsigned i) const { + lean_assert(i < get_num_args()); + if (m_implicit_args) { + unsigned n = num_args(m_app); + for (unsigned j = 1; j < n; j++) { + if (!(*m_implicit_args)[j-1]) { + // explicit argument found + if (i == 0) + return arg(m_app, j); + --i; + } + } + lean_unreachable(); + return arg(m_app, n - 1); + } else { + return arg(m_app, i + 1); + } + } + + expr const & get_function() const { + return m_f; + } + + bool notation_enabled() const { + return m_notation_enabled; + } + }; + + /** \brief Return true if the application \c app has the number of arguments expected by the operator \c op. */ + bool has_expected_num_args(application const & app, operator_info const & op) { + switch (op.get_fixity()) { + case fixity::Infix: case fixity::Infixl: case fixity::Infixr: + return app.get_num_args() == 2; + case fixity::Prefix: case fixity::Postfix: + return app.get_num_args() == 1; + case fixity::Mixfixl: case fixity::Mixfixr: + return app.get_num_args() == length(op.get_op_name_parts()) + 1; + case fixity::Mixfixc: + return app.get_num_args() == length(op.get_op_name_parts()); + } + lean_unreachable(); + return false; + } + /** \brief Pretty print an application. */ result pp_app(expr const & e, unsigned depth) { + application app(e, m_frontend, m_implict); operator_info op; - if (m_notation && (op = get_operator(e)) && has_expected_num_args(e, op)) { + if (m_notation && app.notation_enabled() && (op = get_operator(e)) && has_expected_num_args(app, op)) { result p_arg; format r_format; unsigned sz; unsigned r_weight = 1; switch (op.get_fixity()) { case fixity::Infix: - return mk_infix(op, pp_mixfix_child(op, arg(e, 1), depth), pp_mixfix_child(op, arg(e, 2), depth)); + return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_mixfix_child(op, app.get_arg(1), depth)); case fixity::Infixr: - return mk_infix(op, pp_mixfix_child(op, arg(e, 1), depth), pp_infix_child(op, arg(e, 2), depth)); + return mk_infix(op, pp_mixfix_child(op, app.get_arg(0), depth), pp_infix_child(op, app.get_arg(1), depth)); case fixity::Infixl: - return mk_infix(op, pp_infix_child(op, arg(e, 1), depth), pp_mixfix_child(op, arg(e, 2), depth)); + return mk_infix(op, pp_infix_child(op, app.get_arg(0), depth), pp_mixfix_child(op, app.get_arg(1), depth)); case fixity::Prefix: - p_arg = pp_infix_child(op, arg(e, 1), depth); + p_arg = pp_infix_child(op, app.get_arg(0), depth); sz = op.get_op_name().size(); return mk_result(group(format{format(op.get_op_name()), nest(sz+1, format{line(), p_arg.first})}), p_arg.second + 1); case fixity::Postfix: - p_arg = pp_mixfix_child(op, arg(e, 1), depth); + p_arg = pp_mixfix_child(op, app.get_arg(0), depth); return mk_result(group(format{p_arg.first, space(), format(op.get_op_name())}), p_arg.second + 1); case fixity::Mixfixr: { // _ ID ... _ ID list parts = op.get_op_name_parts(); auto it = parts.begin(); - for (unsigned i = 1; i < num_args(e); i++) { - result p_arg = pp_mixfix_child(op, arg(e, i), depth); + unsigned num = app.get_num_args(); + for (unsigned i = 0; i < num; i++) { + result p_arg = pp_mixfix_child(op, app.get_arg(i), depth); r_format += format{p_arg.first, space(), format(*it), line()}; r_weight += p_arg.second; ++it; @@ -459,8 +548,9 @@ class pp_fn { // ID _ ... _ ID list parts = op.get_op_name_parts(); auto it = parts.begin(); - for (unsigned i = 1; i < num_args(e); i++) { - result p_arg = pp_mixfix_child(op, arg(e, i), depth); + unsigned num = app.get_num_args(); + for (unsigned i = 0; i < num; i++) { + result p_arg = pp_mixfix_child(op, app.get_arg(i), depth); unsigned sz = it->size(); if (i > 1) r_format += space(); r_format += format{format(*it), nest(sz+1, format{line(), p_arg.first})}; @@ -481,47 +571,17 @@ class pp_fn { return pp_exists(e, depth); } else { // standard function application - expr f = arg(e, 0); - std::vector const * implicit_args = nullptr; - format r_format; - unsigned r_weight; - bool simple = false; - unsigned indent = m_indent; - if (is_constant(f)) { - name const & n = const_name(f); - simple = const_name(f).size() <= m_indent + 4; - indent = simple ? const_name(f).size()+1 : m_indent; - if (m_frontend.has_implicit_arguments(n)) { - implicit_args = &(m_frontend.get_implicit_arguments(n)); - lean_assert(implicit_args->size() != 0); - if (m_implict || num_args(e) - 1 < implicit_args->size()) { - // If implicit arguments should be displayed, or - // If we do not have enough arguments, then - // we use the explicit representation - implicit_args = nullptr; - // we should use the explicit version of the - // definition, since we are not hiding implicit arguments - r_format = format(m_frontend.get_explicit_version(n)); - simple = false; - indent = m_indent; - } else { - r_format = format(n); - } - } else { - r_format = format(n); - } - r_weight = 1; - } else { - result p = pp_child(f, depth); - r_format = p.first; - r_weight = p.second; - } - for (unsigned i = 1; i < num_args(e); i++) { - if (!is_implicit(implicit_args, i-1)) { - result p_arg = pp_child(arg(e, i), depth); - r_format += format{i == 1 && simple ? space() : line(), p_arg.first}; - r_weight += p_arg.second; - } + expr const & f = app.get_function(); + result p = is_constant(f) ? mk_result(format(const_name(f)),1) : pp_child(f, depth); + bool simple = is_constant(f) && const_name(f).size() <= m_indent + 4; + unsigned indent = simple ? const_name(f).size()+1 : m_indent; + format r_format = p.first; + unsigned r_weight = p.second; + unsigned num = app.get_num_args(); + for (unsigned i = 0; i < num; i++) { + result p_arg = pp_child(app.get_arg(i), depth); + r_format += format{i == 0 && simple ? space() : line(), p_arg.first}; + r_weight += p_arg.second; } return mk_result(group(nest(indent, r_format)), r_weight); } @@ -970,7 +1030,9 @@ class pp_formatter_cell : public formatter_cell { format pp_notation_decl(object const & obj, options const & opts) { notation_declaration const & n = *(static_cast(obj.cell())); - return format{::lean::pp(n.get_op()), space(), colon(), space(), pp(n.get_expr(), opts)}; + expr const & d = n.get_expr(); + format d_fmt = is_constant(d) ? format(const_name(d)) : pp(d, opts); + return format{::lean::pp(n.get_op()), space(), colon(), space(), d_fmt}; } public: