From b0f2ee6de0fd77c7898b08470fdee1585e09e78f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 Aug 2013 18:16:11 -0700 Subject: [PATCH] Add notation support to frontend object Signed-off-by: Leonardo de Moura --- src/frontend/frontend.cpp | 142 ++++++++++++++++++++++++++++++++++- src/frontend/operator_info.h | 3 + src/frontend/scanner.h | 1 + src/kernel/environment.cpp | 4 + src/kernel/environment.h | 9 +++ 5 files changed, 157 insertions(+), 2 deletions(-) diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index c0c50fe82..1218e8cf4 100644 --- a/src/frontend/frontend.cpp +++ b/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 -#include +#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 operator_table; + typedef std::unordered_map implicit_table; std::atomic m_num_children; std::shared_ptr 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); } - } diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h index cf8ceebc7..2a83d26ef 100644 --- a/src/frontend/operator_info.h +++ b/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); diff --git a/src/frontend/scanner.h b/src/frontend/scanner.h index 43cdbb567..70a06957f 100644 --- a/src/frontend/scanner.h +++ b/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 const & l) { m_commands = l; } int get_line() const { return m_line; } int get_pos() const { return m_pos; } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 44a6b5823..2703afd38 100644 --- a/src/kernel/environment.cpp +++ b/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); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index f73228ded..a90147a3b 100644 --- a/src/kernel/environment.h +++ b/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;