From 50cf3e42f151966eb0a50311d40c082eea4f0982 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 11 Aug 2013 18:06:37 -0700 Subject: [PATCH] Add operator_info Signed-off-by: Leonardo de Moura --- src/frontend/CMakeLists.txt | 2 +- src/frontend/operator_info.cpp | 140 ++++++++++++++++++++++++++++++++ src/frontend/operator_info.h | 92 +++++++++++++-------- src/tests/frontend/frontend.cpp | 33 +++++++- src/tests/util/list.cpp | 23 ++++++ src/util/list.h | 26 ++++++ 6 files changed, 279 insertions(+), 37 deletions(-) create mode 100644 src/frontend/operator_info.cpp diff --git a/src/frontend/CMakeLists.txt b/src/frontend/CMakeLists.txt index a8769a326..f602416c7 100644 --- a/src/frontend/CMakeLists.txt +++ b/src/frontend/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(frontend frontend.cpp) +add_library(frontend frontend.cpp operator_info) target_link_libraries(frontend ${LEAN_LIBS}) diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp new file mode 100644 index 000000000..57362bd9c --- /dev/null +++ b/src/frontend/operator_info.cpp @@ -0,0 +1,140 @@ + +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "operator_info.h" +#include "rc.h" +#include "options.h" + +namespace lean { + +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(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)) { + 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) { + } +}; + +operator_info::operator_info(imp * p):m_ptr(p) {} + +operator_info::operator_info(operator_info const & info):m_ptr(info.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + +operator_info::operator_info(operator_info && info):m_ptr(info.m_ptr) { info.m_ptr = nullptr; } + +operator_info::~operator_info() { if (m_ptr) m_ptr->dec_ref(); } + +operator_info & operator_info::operator=(operator_info const & s) { LEAN_COPY_REF(operator_info, s); } + +operator_info & operator_info::operator=(operator_info && s) { LEAN_MOVE_REF(operator_info, s); } + +void operator_info::add_internal_name(name const & n) { lean_assert(m_ptr); m_ptr->m_names = cons(n, m_ptr->m_names); } + +bool operator_info::is_overloaded() const { return m_ptr && !is_nil(m_ptr->m_names) && !is_nil(cdr(m_ptr->m_names)); } + +list const & operator_info::get_internal_names() const { lean_assert(m_ptr); return m_ptr->m_names; } + +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); } + +list const & operator_info::get_op_name_parts() const { lean_assert(m_ptr); return m_ptr->m_op_parts; } + +operator_info operator_info::copy() const { return operator_info(new imp(*m_ptr)); } + +operator_info infixr(name const & op, unsigned precedence) { + return operator_info(new operator_info::imp(op, fixity::Infix, associativity::Right, precedence)); +} +operator_info infixl(name const & op, unsigned precedence) { + return operator_info(new operator_info::imp(op, fixity::Infix, associativity::Left, precedence)); +} +operator_info prefix(name const & op, unsigned precedence) { + return operator_info(new operator_info::imp(op, fixity::Prefix, associativity::None, precedence)); +} +operator_info postfix(name const & op, unsigned precedence) { + return operator_info(new operator_info::imp(op, fixity::Postfix, associativity::None, 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)); +} +operator_info mixfixr(unsigned num_parts, name const * parts, unsigned precedence) { + lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixr, precedence)); +} +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)); +} + +static char const * g_arrow = "\u21a6"; + +format pp(operator_info const & o, options const & opt) { + format r; + switch (o.get_fixity()) { + case fixity::Infix: r = format(o.get_associativity() == associativity::Left ? "Infixl" : "Infixr"); break; + case fixity::Prefix: r = format("Prefix"); break; + case fixity::Postfix: r = format("Postfix"); break; + case fixity::Mixfixl: + case fixity::Mixfixr: + case fixity::Mixfixc: r = format("Mixfix"); break; + } + + r += space(); + + if (o.get_precedence() != 0) + r += format{format(o.get_precedence()), space()}; + + switch (o.get_fixity()) { + case fixity::Infix: case fixity::Prefix: case fixity::Postfix: + r += pp(o.get_op_name(), opt); break; + case fixity::Mixfixl: + for (auto p : o.get_op_name_parts()) r += format{pp(p, opt), format(" _")}; + break; + case fixity::Mixfixr: + for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p, opt)}; + break; + case fixity::Mixfixc: { + bool first = true; + for (auto p : o.get_op_name_parts()) { + if (first) first = false; else r += format(" _ "); + r += pp(p, opt); + } + }} + + list const & l = o.get_internal_names(); + if (!is_nil(l)) { + r += format{space(), format(g_arrow)}; + for (auto n : l) r += format{space(), pp(n, opt)}; + } + return r; +} + +format pp(operator_info const & o) { + return pp(o, options()); +} + +std::ostream & operator<<(std::ostream & out, operator_info const & o) { + out << pp(o); + return out; +} + +} diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h index 2e28eebed..f947730d3 100644 --- a/src/frontend/operator_info.h +++ b/src/frontend/operator_info.h @@ -6,22 +6,29 @@ Author: Leonardo de Moura */ #pragma once #include "name.h" +#include "list.h" +#include "format.h" namespace lean { - /** \brief Operator fixity. Prefix: ID _ Infix: _ ID _ (can be left or right associative) Postfix: _ ID - Mixfix_l: ID _ ID _ ... ID _ - Mixfix_r: _ ID _ ID ... _ ID - Mixfix_c: ID _ ID _ ... ID _ 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, Mixfix_l, Mixfix_r, Mixfix_c }; +enum class fixity { Prefix, Infix, Postfix, Mixfixl, Mixfixr, Mixfixc }; -enum class associativity { Left, Right }; +enum class associativity { Left, Right, None }; +/** + \brief Data-structure for storing user defined operator + information. This information is used during parsing and + pretty-printing. + +*/ class operator_info { struct imp; imp * m_ptr; @@ -31,50 +38,65 @@ public: operator_info(operator_info && info); ~operator_info(); - operator_info & operator=(operator const & o); - operator_info & operator=(operator&& o); + operator_info & operator=(operator_info const & o); + operator_info & operator=(operator_info && o); - operator_info infixl(name const & op, unsigned precedence); - operator_info infixr(name const & op, unsigned precedence); - operator_info prefix(name const & op, unsigned precedence); - 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); + friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); } + + friend operator_info infixl(name const & op, unsigned precedence); + friend operator_info infixr(name const & op, unsigned precedence); + friend operator_info prefix(name const & op, unsigned precedence); + friend operator_info postfix(name const & op, unsigned precedence); + 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); /** \brief Associate an internal name for this operator. */ void add_internal_name(name const & n); /** \brief Return true iff the operator is overloaded. */ bool is_overloaded() const; - - /** - \brief Return the list of internal names for this operator. - The list has size greater than 1 iff the operator has been overloaded. - When the operator is overloaded, the first internal name is - the temporary name to be used during parsing (before elaboration). + + /** + \brief Return the list of internal names for this operator. + The list has size greater than 1 iff the operator has been + overloaded. + Internal names are the real names used to identify the operator + in the kernel. */ list const & get_internal_names() const; - + + /** \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; - list const & get_op_parts() const; - + /** \brief Return the operator name. For mixfix operators the result corresponds to the first part. */ + name const & get_op_name() const; + + /** \brief Return the operators parts. */ + list const & get_op_name_parts() const; + + /** \brief Return a copy of the operator. */ operator_info copy() const; - - - -#if 0 - 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. -#endif }; +operator_info infixl(name const & op, unsigned precedence); +operator_info infixr(name const & op, unsigned precedence); +operator_info prefix(name const & op, unsigned precedence); +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); +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); } +class options; +format pp(operator_info const & o, options const &); +format pp(operator_info const & o); +std::ostream & operator<<(std::ostream & out, operator_info const & o); } diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp index 7479e9a4f..417db3c52 100644 --- a/src/tests/frontend/frontend.cpp +++ b/src/tests/frontend/frontend.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "frontend.h" #include "environment.h" +#include "operator_info.h" #include "test.h" using namespace lean; @@ -17,8 +18,38 @@ static void tst1() { lean_assert(f.env().has_children()); } +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); + op1.add_internal_name(name{"Bool","And"}); + operator_info op3 = infixl(name("+"), 10); + op3.add_internal_name(name{"Int", "plus"}); + op3.add_internal_name(name{"Real", "plus"}); + std::cout << op3.get_internal_names() << "\n"; + lean_assert(length(op3.get_internal_names()) == 2); + operator_info op4 = op3.copy(); + op4.add_internal_name(name{"Complex", "plus"}); + 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_op_name() == op3.get_op_name()); + lean_assert(prefix("tst", 20).get_fixity() == fixity::Prefix); + lean_assert(postfix("!", 20).get_fixity() == fixity::Postfix); + lean_assert(length(mixfixl({"if", "then", "else"}, 10).get_op_name_parts()) == 3); + lean_assert(mixfixc({"if", "then", "else", "endif"}, 10).get_fixity() == fixity::Mixfixc); + std::cout << mixfixc({"if", "then", "else", "endif"}, 10).get_op_name_parts() << "\n"; + std::cout << op4 << "\n"; + std::cout << op2 << "\n"; + std::cout << mixfixc({"if", "then", "else", "endif"}, 10) << "\n"; +} + int main() { - continue_on_violation(true); + // continue_on_violation(true); tst1(); + tst2(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp index 987db6e60..89d93eed9 100644 --- a/src/tests/util/list.cpp +++ b/src/tests/util/list.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "list.h" #include "test.h" using namespace lean; @@ -21,8 +22,30 @@ static void tst1() { std::cout << l << "\n"; } +static void tst2() { + std::vector a{10, 20, 30}; + list l = it2list(a.begin(), a.end()); + std::cout << l << "\n"; + lean_assert(head(l) == 10); + lean_assert(head(tail(l)) == 20); + lean_assert(head(tail(tail(l))) == 30); + lean_assert(length(l) == 3); +} + +static void tst3() { + int a[3] = {10, 20, 30}; + list l = it2list(a, a+3); + std::cout << l << "\n"; + lean_assert(head(l) == 10); + lean_assert(head(tail(l)) == 20); + lean_assert(head(tail(tail(l))) == 30); + lean_assert(length(l) == 3); +} + int main() { continue_on_violation(true); tst1(); + tst2(); + tst3(); return has_violations() ? 1 : 0; } diff --git a/src/util/list.h b/src/util/list.h index 990de79fa..1a11d63d1 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -50,6 +50,22 @@ public: friend list const & tail(list const & l) { lean_assert(!is_nil(l)); return l.m_ptr->m_tail; } friend bool operator==(list const & l1, list const & l2) { return l1.m_ptr == l2.m_ptr; } friend bool operator!=(list const & l1, list const & l2) { return l1.m_ptr != l2.m_ptr; } + + class iterator { + friend class list; + cell const * m_it; + iterator(cell const * it):m_it(it) {} + public: + iterator(iterator const & s):m_it(s.m_it) {} + iterator & operator++() { m_it = m_it->m_tail.m_ptr; return *this; } + iterator operator++(int) { iterator tmp(*this); operator++(); return tmp; } + bool operator==(iterator const & s) const { return m_it == s.m_it; } + bool operator!=(iterator const & s) const { return !operator==(s); } + T const & operator*() { lean_assert(m_it); return m_it->m_head; } + }; + + iterator begin() const { return iterator(m_ptr); } + iterator end() const { return iterator(nullptr); } }; template inline list cons(T const & h, list const & t) { return list(h, t); } @@ -81,4 +97,14 @@ template unsigned length(list const & l) { } return r; } + +template list it2list(It const & begin, It const & end) { + list r; + auto it = end; + while (it != begin) { + --it; + r = cons(*it, r); + } + return r; +} }