Add notation support to frontend object

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

src/frontend/frontend.cpp

@@ -5,22 +5,43 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <atomic>
-#include <unordered_map>
+#include "map.h"
 #include "frontend.h"
 #include "environment.h"
 #include "operator_info.h"
 
 namespace lean {
+/**
+    \brief Create object for tracking notation/operator declarations.
+    This object is mainly used for pretty printing.
+*/
+class notation_declaration : public anonymous_object {
+    operator_info m_op;
+    name          m_name;
+public:
+    notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {}
+    virtual ~notation_declaration() {}
+    static char const * g_keyword;
+    virtual char const * keyword() const { return g_keyword; }
+    virtual format pp(environment const &) const {
+        // TODO
+        return format();
+    }
+};
+char const * notation_declaration::g_keyword = "Notation";
+
 /** \brief Implementation of the Lean frontend */
 struct frontend::imp {
     // Remark: only named objects are stored in the dictionary.
     typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
+    typedef std::unordered_map<name, unsigned, name_hash, name_eq> implicit_table;
     std::atomic<unsigned> m_num_children;
     std::shared_ptr<imp>  m_parent;
     environment           m_env;
     operator_table        m_nud; // nud table for Pratt's parser
     operator_table        m_led; // led table for Pratt's parser
     operator_table        m_name_to_operator; // map internal names to operators (this is used for pretty printing)
+    implicit_table        m_implicit_table; // track the number of implicit arguments for a symbol.
 
     bool has_children() const { return m_num_children > 0; }
     void inc_children() { m_num_children++; }
@@ -28,6 +49,124 @@ struct frontend::imp {
 
     bool has_parent() const { return m_parent != nullptr; }
 
+    /** \brief Return the nud operator for the given symbol. */
+    operator_info find_nud(name const & n) const {
+        auto it = m_nud.find(n);
+        if (it != m_nud.end())
+            return it->second;
+        else if (has_parent())
+            return m_parent->find_nud(n);
+        else
+            return operator_info();
+    }
+
+    /** \brief Return the led operator for the given symbol. */
+    operator_info find_led(name const & n) const {
+        auto it = m_led.find(n);
+        if (it != m_led.end())
+            return it->second;
+        else if (has_parent())
+            return m_parent->find_led(n);
+        else
+            return operator_info();
+    }
+
+    /**
+        \brief Return true if the given operator is defined in this
+        frontend object (parent frontends are ignored).
+    */
+    bool defined_here(operator_info const & n, bool led) const {
+        if (led)
+            return m_led.find(n.get_op_name()) != m_led.end();
+        else
+            return m_nud.find(n.get_op_name()) != m_nud.end();
+    }
+
+    /** \brief Return the led/nud operator for the given symbol. */
+    operator_info find_op(name const & n, bool led) const {
+        return led ? find_led(n) : find_nud(n);
+    }
+
+    /** \brief Insert a new led/nud operator. */
+    void insert_op(operator_info const & op, bool led) {
+        if (led)
+            insert(m_led, op.get_op_name(), op);
+        else
+            insert(m_nud, op.get_op_name(), op);
+    }
+
+    /** \brief Find the operator that is used as notation for the given internal symbol. */
+    operator_info find_op_for(name const & n) const {
+        auto it = m_name_to_operator.find(n);
+        if (it != m_name_to_operator.end())
+            return it->second;
+        else if (has_parent())
+            return m_parent->find_op_for(n);
+        else
+            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 operators that are associated with the given operator symbol (aka notation) */
+    void remove_bindings(operator_info const & op) {
+        for (name const & n : op.get_internal_names()) {
+            if (has_parent() && !is_nil(m_parent->find_op_for(n))) {
+                // parent has a binding for n... we must hide it.
+                insert(m_name_to_operator, n, operator_info());
+            } else {
+                m_name_to_operator.erase(n);
+            }
+        }
+    }
+
+    /** \brief Register the new operator in the tables for parsing and pretty printing. */
+    void register_new_op(operator_info new_op, name const & n, bool led) {
+        new_op.add_internal_name(n);
+        insert_op(new_op, led);
+        insert(m_name_to_operator, n, new_op);
+    }
+
+    /**
+        \brief Add a new operator and save information as object.
+
+        If the new operator does not conflict with existing operators,
+        then we just register it.
+        If it conflicts, there are two options:
+        1) It is an overload (we just add the internal name \c n as
+        new option.
+        2) It is a real conflict, and report the issue in the
+        diagnostic channel, and override the existing operator (aka notation).
+    */
+    void add_op(operator_info new_op, name const & n, bool led) {
+        name const & opn = new_op.get_op_name();
+        operator_info old_op = find_op(opn, led);
+        if (is_nil(old_op)) {
+            register_new_op(new_op, n, led);
+        } else if (old_op == new_op) {
+            // overload
+            if (defined_here(old_op, led)) {
+                old_op.add_internal_name(n);
+            } else {
+                // we must copy the operator because it was defined in
+                // a parent frontend.
+                new_op = old_op.copy();
+                register_new_op(new_op, n, led);
+            }
+        } else {
+            report_op_redefined(old_op, new_op);
+            remove_bindings(old_op);
+            register_new_op(new_op, n, led);
+        }
+        m_env.add_anonymous_object(new notation_declaration(new_op, n));
+    }
+
     imp():
         m_num_children(0) {
     }
@@ -82,6 +221,5 @@ 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); }
-
 }
 

src/frontend/operator_info.h

@@ -34,6 +34,7 @@ class operator_info {
     imp * m_ptr;
     explicit operator_info(imp * p);
 public:
+    operator_info():m_ptr(nullptr) {}
     operator_info(operator_info const & info);
     operator_info(operator_info && info);
     ~operator_info();
@@ -43,6 +44,8 @@ public:
 
     friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); }
 
+    friend bool is_nil(operator_info const & o) { return o.m_ptr == nullptr; }
+
     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);

src/frontend/scanner.h

@@ -55,6 +55,7 @@ public:
 
     /** \brief Register a new command keyword. */
     void add_command_keyword(name const & n);
+    void set_command_keywords(list<name> const & l) { m_commands = l; }
 
     int get_line() const { return m_line; }
     int get_pos() const { return m_pos; }

src/kernel/environment.cpp

@@ -460,6 +460,10 @@ void environment::add_var(name const & n, expr const & t) {
     m_imp->add_var(n, t, *this);
 }
 
+void environment::add_anonymous_object(anonymous_object * o) {
+    m_imp->m_objects.push_back(o);
+}
+
 named_object const & environment::get_object(name const & n) const {
     return m_imp->get_object(n);
 }

src/kernel/environment.h

@@ -115,6 +115,12 @@ public:
     void add_axiom(name const & n, expr const & t);
     void add_var(name const & n, expr const & t);
 
+    /**
+       \brief Register the given unanymous object in this environment.
+       The environment assume the object ownership.
+    */
+    void add_anonymous_object(anonymous_object * o);
+
     /**
        \brief Return the object with the given name.
        It throws an exception if the environment does not have an object with the given name.
@@ -127,6 +133,9 @@ public:
     */
     named_object const * get_object_ptr(name const & n) const;
 
+    /** \brief Return true iff the environment has an object with the given name */
+    bool has_object(name const & n) const { return get_object_ptr(n) != nullptr; }
+
     /** \brief Iterator for Lean environment objects. */
     class object_iterator {
         environment const & m_env;