diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index 1218e8cf4..64ae4e408 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -24,8 +24,23 @@ public: static char const * g_keyword; virtual char const * keyword() const { return g_keyword; } virtual format pp(environment const &) const { - // TODO - return format(); + char const * cmd; + switch (m_op.get_fixity()) { + case fixity::Infixl: cmd = "Infixl"; break; + case fixity::Infixr: cmd = "Infixr"; break; + case fixity::Prefix: cmd = "Prefix"; break; + case fixity::Postfix: cmd = "Postfix"; break; + case fixity::Mixfixl: cmd = "Mixfixl"; break; + case fixity::Mixfixr: cmd = "Mixfixr"; break; + case fixity::Mixfixc: cmd = "Mixfixc"; break; + } + format r = highlight_command(format(cmd)); + if (m_op.get_precedence() != 0) + r += format{space(), format(m_op.get_precedence())}; + for (auto p : m_op.get_op_name_parts()) + r += format{space(), format(p)}; + r += format{space(), format(m_name)}; + return r; } }; char const * notation_declaration::g_keyword = "Notation"; @@ -167,6 +182,22 @@ struct frontend::imp { m_env.add_anonymous_object(new notation_declaration(new_op, n)); } + void add_infixl(name const & opn, unsigned precedence, name const & n) { + add_op(infixl(opn, precedence), n, true); + } + + void add_infixr(name const & opn, unsigned precedence, name const & n) { + add_op(infixr(opn, precedence), n, true); + } + + void add_prefix(name const & opn, unsigned precedence, name const & n) { + add_op(prefix(opn, precedence), n, false); + } + + void add_postfix(name const & opn, unsigned precedence, name const & n) { + add_op(postfix(opn, precedence), n, true); + } + imp(): m_num_children(0) { } @@ -221,5 +252,12 @@ environment const & frontend::env() const { return m_imp->m_env; } level frontend::add_uvar(name const & n, level const & l) { return m_imp->m_env.add_uvar(n, l); } level frontend::add_uvar(name const & n) { return m_imp->m_env.add_uvar(n); } level frontend::get_uvar(name const & n) const { return m_imp->m_env.get_uvar(n); } + +void frontend::add_infixl(name const & opn, unsigned p, name const & n) { m_imp->add_infixl(opn, p, n); } +void frontend::add_infixr(name const & opn, unsigned p, name const & n) { m_imp->add_infixr(opn, p, n); } +void frontend::add_prefix(name const & opn, unsigned p, name const & n) { m_imp->add_prefix(opn, p, n); } +void frontend::add_postfix(name const & opn, unsigned p, name const & n) { m_imp->add_postfix(opn, p, n); } + +void frontend::display(std::ostream & out) const { m_imp->m_env.display(out); } } diff --git a/src/frontend/frontend.h b/src/frontend/frontend.h index 443a73d3d..6479e66ab 100644 --- a/src/frontend/frontend.h +++ b/src/frontend/frontend.h @@ -50,6 +50,16 @@ public: level add_uvar(name const & n); level get_uvar(name const & n) const; + // ======================================= + // Notation + void add_infixl(name const & opn, unsigned precedence, name const & n); + void add_infixr(name const & opn, unsigned precedence, name const & n); + void add_prefix(name const & opn, unsigned precedence, name const & n); + void add_postfix(name const & opn, unsigned precedence, name const & n); + // ======================================= + /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ + void display(std::ostream & out) const; }; +inline std::ostream & operator<<(std::ostream & out, frontend const & f) { f.display(out); return out; } } diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp index 128dfdd61..a2c481a5e 100644 --- a/src/frontend/operator_info.cpp +++ b/src/frontend/operator_info.cpp @@ -14,27 +14,25 @@ struct operator_info::imp { void dealloc() { delete this; } MK_LEAN_RC(); fixity m_fixity; - associativity m_assoc; // Relevant only for infix operators. unsigned m_precedence; list m_op_parts; // operator parts, > 1 only if the operator is mixfix. list m_names; // internal names, > 1 only if the operator is overloaded. - imp(name const & op, fixity f, associativity a, unsigned p): - m_rc(1), m_fixity(f), m_assoc(a), m_precedence(p), m_op_parts(cons(op, list())) {} + imp(name const & op, fixity f, unsigned p): + m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(cons(op, list())) {} imp(unsigned num_parts, name const * parts, fixity f, unsigned p): - m_rc(1), m_fixity(f), m_assoc(associativity::None), m_precedence(p), m_op_parts(it2list(parts, parts + num_parts)) { + m_rc(1), m_fixity(f), m_precedence(p), m_op_parts(it2list(parts, parts + num_parts)) { lean_assert(num_parts > 0); } imp(imp const & s): - m_rc(1), m_fixity(s.m_fixity), m_assoc(s.m_assoc), m_precedence(s.m_precedence), m_op_parts(s.m_op_parts), m_names(s.m_names) { + m_rc(1), m_fixity(s.m_fixity), m_precedence(s.m_precedence), m_op_parts(s.m_op_parts), m_names(s.m_names) { } bool is_eq(imp const & other) const { return m_fixity == other.m_fixity && - m_assoc == other.m_assoc && m_precedence == other.m_precedence && m_op_parts == other.m_op_parts; } @@ -61,8 +59,6 @@ list const & operator_info::get_internal_names() const { lean_assert(m_ptr fixity operator_info::get_fixity() const { lean_assert(m_ptr); return m_ptr->m_fixity; } -associativity operator_info::get_associativity() const { lean_assert(m_ptr); return m_ptr->m_assoc; } - unsigned operator_info::get_precedence() const { lean_assert(m_ptr); return m_ptr->m_precedence; } name const & operator_info::get_op_name() const { lean_assert(m_ptr); return car(m_ptr->m_op_parts); } @@ -81,16 +77,16 @@ bool operator==(operator_info const & op1, operator_info const & op2) { } operator_info infixr(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Infix, associativity::Right, precedence)); + return operator_info(new operator_info::imp(op, fixity::Infixr, precedence)); } operator_info infixl(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Infix, associativity::Left, precedence)); + return operator_info(new operator_info::imp(op, fixity::Infixl, precedence)); } operator_info prefix(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Prefix, associativity::None, precedence)); + return operator_info(new operator_info::imp(op, fixity::Prefix, precedence)); } operator_info postfix(name const & op, unsigned precedence) { - return operator_info(new operator_info::imp(op, fixity::Postfix, associativity::None, precedence)); + return operator_info(new operator_info::imp(op, fixity::Postfix, precedence)); } operator_info mixfixl(unsigned num_parts, name const * parts, unsigned precedence) { lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixl, precedence)); @@ -107,7 +103,8 @@ static char const * g_arrow = "\u21a6"; format pp(operator_info const & o) { format r; switch (o.get_fixity()) { - case fixity::Infix: r = format(o.get_associativity() == associativity::Left ? "Infixl" : "Infixr"); break; + case fixity::Infixl: r = format("Infixl"); break; + case fixity::Infixr: r = format("Infixr"); break; case fixity::Prefix: r = format("Prefix"); break; case fixity::Postfix: r = format("Postfix"); break; case fixity::Mixfixl: @@ -121,7 +118,7 @@ format pp(operator_info const & o) { r += format{format(o.get_precedence()), space()}; switch (o.get_fixity()) { - case fixity::Infix: case fixity::Prefix: case fixity::Postfix: + case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix: r += pp(o.get_op_name()); break; case fixity::Mixfixl: for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")}; diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h index 2a83d26ef..60d26ab48 100644 --- a/src/frontend/operator_info.h +++ b/src/frontend/operator_info.h @@ -13,15 +13,14 @@ namespace lean { /** \brief Operator fixity. Prefix: ID _ - Infix: _ ID _ (can be left or right associative) + Infixl: _ ID _ (left associative) + Infixr: _ ID _ (right associative) Postfix: _ ID 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) */ -enum class fixity { Prefix, Infix, Postfix, Mixfixl, Mixfixr, Mixfixc }; - -enum class associativity { Left, Right, None }; +enum class fixity { Prefix, Infixl, Infixr, Postfix, Mixfixl, Mixfixr, Mixfixc }; /** \brief Data-structure for storing user defined operator @@ -72,9 +71,6 @@ public: /** \brief Return the operator fixity. */ fixity get_fixity() const; - /** \brief Return the operator associativity. */ - associativity get_associativity() const; - /** \brief Return the operator precedence. */ unsigned get_precedence() const; diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 2703afd38..5d6e113ee 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -341,17 +341,13 @@ struct environment::imp { } } - void display_objects(std::ostream & out, environment const & env) const { - for (object const * obj : m_objects) { - out << obj->pp(env) << "\n"; - } - } - /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ void display(std::ostream & out, environment const & env) const { if (has_parent()) m_parent->display(out, env); - display_objects(out, env); + for (object const * obj : m_objects) { + out << obj->pp(env) << "\n"; + } } imp(): @@ -480,10 +476,6 @@ object const & environment::get_object(unsigned i) const { return *(m_imp->m_objects[i]); } -void environment::display_objects(std::ostream & out) const { - m_imp->display_objects(out, *this); -} - void environment::display(std::ostream & out) const { m_imp->display(out, *this); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index a90147a3b..c9d6e59e0 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -158,14 +158,8 @@ public: object_iterator end_objects() const { return object_iterator(*this, get_num_objects()); } // ======================================= - // ======================================= - // Pretty printing - /** \brief Display all objects stored in the environment */ - void display_objects(std::ostream & out) const; - /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ void display(std::ostream & out) const; - // ======================================= }; inline std::ostream & operator<<(std::ostream & out, environment const & env) { env.display(out); return out; } } diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp index ab8dd29db..2f5e7abc1 100644 --- a/src/tests/frontend/frontend.cpp +++ b/src/tests/frontend/frontend.cpp @@ -22,8 +22,7 @@ static void tst2() { operator_info op1 = infixl(name("and"), 10); operator_info op2 = infixr(name("implies"), 20); lean_assert(op1.get_precedence() == 10); - lean_assert(op1.get_associativity() == associativity::Left); - lean_assert(op1.get_fixity() == fixity::Infix); + lean_assert(op1.get_fixity() == fixity::Infixl); op1.add_internal_name(name{"Bool","And"}); operator_info op3 = infixl(name("+"), 10); op3.add_internal_name(name{"Int", "plus"}); @@ -35,7 +34,7 @@ static void tst2() { std::cout << op4.get_internal_names() << "\n"; lean_assert(length(op3.get_internal_names()) == 2); lean_assert(length(op4.get_internal_names()) == 3); - lean_assert(op4.get_fixity() == fixity::Infix); + lean_assert(op4.get_fixity() == fixity::Infixl); lean_assert(op4.get_op_name() == op3.get_op_name()); lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix); lean_assert(postfix("!", 20).get_fixity() == fixity::Postfix); @@ -47,8 +46,16 @@ static void tst2() { std::cout << mixfixc({"if", "then", "else", "endif"}, 10) << "\n"; } +static void tst3() { + frontend f; + f.add_infixl("+", 10, name{"Int", "add"}); + f.add_infixl("-", 10, name{"Int", "sub"}); + std::cout << f; +} + int main() { tst1(); tst2(); + tst3(); return has_violations() ? 1 : 0; }