Implement support for notation + implicit arguments. Cleanup pretty printer code for handling implicit arguments.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
76c968a5b8
commit
206c7fa203
3 changed files with 302 additions and 193 deletions
|
|
@ -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<bool> 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()) {
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<bool> 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<expr> 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<expr> 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<expr> 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<expr> 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<expr> args;
|
||||
args.push_back(f);
|
||||
args.push_back(parse_expr(op.get_precedence()));
|
||||
list<name> 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<unsigned> 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;
|
||||
|
|
|
|||
|
|
@ -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<std::pair<name, expr>> 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<bool> 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<name> 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<name> 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<bool> 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<notation_declaration const *>(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:
|
||||
|
|
|
|||
Loading…
Reference in a new issue