Add operator_info

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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<name>    m_op_parts;  // operator parts, > 1 only if the operator is mixfix.
+    list<name>    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<name>())) {}
+
+    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<name, name const *>(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<name> 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<name> 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<name> 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;
+}
+
+}

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<name> 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<name> 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<name> 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<name>    m_op_parts;  // operator parts, > 1 only if the operator is mixfix.
-    list<name>    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<name> const & l, unsigned precedence) { return mixfixl(l.size(), l.begin(), precedence); }
+inline operator_info mixfixr(std::initializer_list<name> const & l, unsigned precedence) { return mixfixr(l.size(), l.begin(), precedence); }
+inline operator_info mixfixc(std::initializer_list<name> 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);
 }

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;
 }

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 <vector>
 #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<int> a{10, 20, 30};
+    list<int> l = it2list<int>(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<int> l = it2list<int, int*>(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;
 }

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<typename T> inline list<T>         cons(T const & h, list<T> const & t) { return list<T>(h, t); }
@@ -81,4 +97,14 @@ template<typename T> unsigned length(list<T> const & l) {
     }
     return r;
 }
+
+template<typename T, typename It> list<T> it2list(It const & begin, It const & end) {
+    list<T> r;
+    auto it = end;
+    while (it != begin) {
+        --it;
+        r = cons(*it, r);
+    }
+    return r;
+}
 }