From 5aae838e1c336a7ed3b47980019fdf4790f7e7b8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Aug 2013 10:09:46 -0700 Subject: [PATCH] Add missing mixfix notation Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_frontend.cpp | 2 ++ src/frontends/lean/lean_frontend.h | 1 + src/frontends/lean/lean_operator_info.cpp | 4 ++++ src/frontends/lean/lean_operator_info.h | 6 +++++- src/frontends/lean/lean_parser.cpp | 16 +++++++++++++++- src/frontends/lean/lean_pp.cpp | 18 ++++++++++++++---- 6 files changed, 41 insertions(+), 6 deletions(-) diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index 3a5151a8b..1493c9eff 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -192,6 +192,7 @@ struct frontend::imp { void add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixl(sz, opns, p), d, false); } void add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixr(sz, opns, p), d, true); } void add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixc(sz, opns, p), d, false); } + void add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { add_op(mixfixo(sz, opns, p), d, false); } void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) { if (has_children()) @@ -326,6 +327,7 @@ void frontend::add_postfix(name const & opn, unsigned p, expr const & d) { m_imp void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixl(sz, opns, p, d); } void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixr(sz, opns, p, d); } void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixc(sz, opns, p, d); } +void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) { m_imp->add_mixfixo(sz, opns, p, d); } operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_op_for(n); } operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); } operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); } diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index c4f638239..0b028db72 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -84,6 +84,7 @@ public: void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, expr const & d); void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, expr const & d); void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, expr const & d); + void add_mixfixo(unsigned sz, name const * opns, unsigned precedence, expr const & d); /** \brief Return the operator (if one exists) associated with the given expression. diff --git a/src/frontends/lean/lean_operator_info.cpp b/src/frontends/lean/lean_operator_info.cpp index fed8a50c8..aabb5fbb2 100644 --- a/src/frontends/lean/lean_operator_info.cpp +++ b/src/frontends/lean/lean_operator_info.cpp @@ -100,6 +100,9 @@ operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedenc operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence) { lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixc, precedence)); } +operator_info mixfixo(unsigned num_parts, name const * parts, unsigned precedence) { + lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixo, precedence)); +} char const * to_string(fixity f) { switch (f) { @@ -111,6 +114,7 @@ char const * to_string(fixity f) { case fixity::Mixfixl: return "Mixfixl"; case fixity::Mixfixr: return "Mixfixr"; case fixity::Mixfixc: return "Mixfixc"; + case fixity::Mixfixo: return "Mixfixo"; } lean_unreachable(); return 0; diff --git a/src/frontends/lean/lean_operator_info.h b/src/frontends/lean/lean_operator_info.h index 039f4fe8e..b21c68900 100644 --- a/src/frontends/lean/lean_operator_info.h +++ b/src/frontends/lean/lean_operator_info.h @@ -21,8 +21,9 @@ namespace lean { Mixfixl: ID _ ID _ ... ID _ (has at least two parts) Mixfixr: _ ID _ ID ... _ ID (has at least two parts) Mixfixc: ID _ ID _ ... ID _ ID (has at least two parts) + Mixfixo: _ ID _ ... ID _ (has at least two parts) */ -enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc }; +enum class fixity { Prefix, Infix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc, Mixfixo }; /** \brief Data-structure for storing user defined operator @@ -54,6 +55,7 @@ public: friend operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence); friend operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence); friend operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence); + friend operator_info mixfixo(unsigned num_parts, name const * parts, unsigned precedence); /** \brief Associate a denotation (expression) with this operator. */ void add_expr(expr const & n); @@ -95,9 +97,11 @@ operator_info postfix(name const & op, unsigned precedence); operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence); operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence); operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedence); +operator_info mixfixo(unsigned num_parts, name const * parts, unsigned precedence); inline operator_info mixfixl(std::initializer_list const & l, unsigned precedence) { return mixfixl(l.size(), l.begin(), precedence); } inline operator_info mixfixr(std::initializer_list const & l, unsigned precedence) { return mixfixr(l.size(), l.begin(), precedence); } inline operator_info mixfixc(std::initializer_list const & l, unsigned precedence) { return mixfixc(l.size(), l.begin(), precedence); } +inline operator_info mixfixo(std::initializer_list const & l, unsigned precedence) { return mixfixo(l.size(), l.begin(), precedence); } format pp(operator_info const & o); std::ostream & operator<<(std::ostream & out, operator_info const & o); diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index 96c413185..de28d0a19 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -477,7 +477,11 @@ class parser::imp { check_name_next(op_part, "invalid mixfix operator application, identifier expected"); } - /** \brief Auxiliary function for #parse_mixfixl and #parse_mixfixr */ + /** + \brief Auxiliary function for #parse_mixfixl and #parse_mixfixr + + It parses (ID _)* + */ void parse_mixfix_args(list const & ops, unsigned prec, buffer & args) { auto it = ops.begin(); ++it; @@ -506,6 +510,15 @@ class parser::imp { return mk_application(op, p, args); } + /** \brief Parse user defined mixfixr operator. It has the form: _ ID ... _ ID _ */ + expr parse_mixfixo(expr const & left, operator_info const & op) { + auto p = pos(); + buffer args; + args.push_back(left); + parse_mixfix_args(op.get_op_name_parts(), op.get_precedence(), args); + 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(); @@ -619,6 +632,7 @@ class parser::imp { case fixity::Infixl: return parse_infixl(left, op); case fixity::Infixr: return parse_infixr(left, op); case fixity::Mixfixr: return parse_mixfixr(left, op); + case fixity::Mixfixo: return parse_mixfixo(left, op); default: lean_unreachable(); return expr(); } } else { diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp index 424e21fd5..eaec2922c 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -495,9 +495,11 @@ class pp_fn { 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()); + case fixity::Mixfixc: + return app.get_num_args() == length(op.get_op_name_parts()) - 1; + case fixity::Mixfixo: + return app.get_num_args() == length(op.get_op_name_parts()) + 1; } lean_unreachable(); return false; @@ -530,14 +532,22 @@ class pp_fn { 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: { + case fixity::Mixfixr: case fixity::Mixfixo: { // _ ID ... _ ID + // _ ID ... _ ID _ list parts = op.get_op_name_parts(); auto it = parts.begin(); 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()}; + if (i == num - 1) { + if (op.get_fixity() == fixity::Mixfixo) + r_format += p_arg.first; + else + r_format += format{p_arg.first, space(), format(*it)}; + } else { + r_format += format{p_arg.first, space(), format(*it), line()}; + } r_weight += p_arg.second; ++it; }