From 03461df55ee9356aaf1735706f5d9ca6dc4c7d7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 Aug 2013 18:00:05 -0700 Subject: [PATCH] Add frontend object Signed-off-by: Leonardo de Moura --- src/frontend/CMakeLists.txt | 2 + src/frontend/frontend.cpp | 83 +++++++++++++++++++++++++++++++ src/frontend/frontend.h | 55 ++++++++++++++++++++ src/frontend/operator_info.h | 80 +++++++++++++++++++++++++++++ src/tests/frontend/CMakeLists.txt | 3 ++ src/tests/frontend/frontend.cpp | 24 +++++++++ 6 files changed, 247 insertions(+) create mode 100644 src/frontend/CMakeLists.txt create mode 100644 src/frontend/frontend.cpp create mode 100644 src/frontend/frontend.h create mode 100644 src/frontend/operator_info.h create mode 100644 src/tests/frontend/CMakeLists.txt create mode 100644 src/tests/frontend/frontend.cpp diff --git a/src/frontend/CMakeLists.txt b/src/frontend/CMakeLists.txt new file mode 100644 index 000000000..c88afc0d4 --- /dev/null +++ b/src/frontend/CMakeLists.txt @@ -0,0 +1,2 @@ +add_library(frontend frontend.cpp) +target_link_libraries(frontend ${EXTRA_LIBS}) diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp new file mode 100644 index 000000000..87d3a4f84 --- /dev/null +++ b/src/frontend/frontend.cpp @@ -0,0 +1,83 @@ +/* +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 +#include "frontend.h" +#include "environment.h" + +namespace lean { + +static name g_overload_prefix(name(0u), "overload"); + +/** \brief Implementation of the Lean frontend */ +struct frontend::imp { + std::atomic m_num_children; + std::shared_ptr m_parent; + environment m_env; + + bool has_children() const { return m_num_children > 0; } + void inc_children() { m_num_children++; } + void dec_children() { m_num_children--; } + + bool has_parent() const { return m_parent != nullptr; } + + imp(): + m_num_children(0) { + } + + explicit imp(std::shared_ptr const & parent): + m_num_children(0), + m_parent(parent), + m_env(m_parent->m_env.mk_child()) { + m_parent->inc_children(); + } + + ~imp() { + if (m_parent) + m_parent->dec_children(); + } +}; + +frontend::frontend(): + m_imp(new imp()) { +} + +frontend::frontend(imp * new_ptr): + m_imp(new_ptr) { +} + +frontend::frontend(std::shared_ptr const & ptr): + m_imp(ptr) { +} + +frontend::~frontend() { +} + +frontend frontend::mk_child() const { + return frontend(new imp(m_imp)); +} + +bool frontend::has_children() const { + return m_imp->has_children(); +} + +bool frontend::has_parent() const { + return m_imp->has_parent(); +} + +frontend frontend::parent() const { + lean_assert(has_parent()); + return frontend(m_imp->m_parent); +} + +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/frontend.h b/src/frontend/frontend.h new file mode 100644 index 000000000..443a73d3d --- /dev/null +++ b/src/frontend/frontend.h @@ -0,0 +1,55 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "level.h" + +namespace lean { +class environment; +/** + \brief Object for managing the environment, parser, pretty printer, + elaborator, etc. +*/ +class frontend { + struct imp; + std::shared_ptr m_imp; + explicit frontend(imp * new_ptr); + explicit frontend(std::shared_ptr const & ptr); +public: + frontend(); + ~frontend(); + + // ======================================= + // Parent/Child frontend management + /** + \brief Create a child environment. This frontend object will + only allow "read-only" operations until all children frontend + objects are deleted. + */ + frontend mk_child() const; + + /** \brief Return true iff this fronted has children frontend. */ + bool has_children() const; + + /** \brief Return true iff this frontend has a parent frontend. */ + bool has_parent() const; + + /** \brief Return parent frontend */ + frontend parent() const; + // ======================================= + + /** \brief Coercion frontend -> environment. */ + environment const & env() const; + operator environment const &() const { return env(); } + + level add_uvar(name const & n, level const & l); + level add_uvar(name const & n); + level get_uvar(name const & n) const; + + +}; +} diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h new file mode 100644 index 000000000..2e28eebed --- /dev/null +++ b/src/frontend/operator_info.h @@ -0,0 +1,80 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "name.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 +*/ +enum class fixity { Prefix, Infix, Postfix, Mixfix_l, Mixfix_r, Mixfix_c }; + +enum class associativity { Left, Right }; + +class operator_info { + struct imp; + imp * m_ptr; + explicit operator_info(imp * p); +public: + operator_info(operator_info const & info); + operator_info(operator_info && info); + ~operator_info(); + + operator_info & operator=(operator const & o); + operator_info & operator=(operator&& 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); + + /** \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). + */ + list const & get_internal_names() const; + + fixity get_fixity() const; + + associativity get_associativity() const; + + unsigned get_precedence() const; + + list const & get_op_parts() const; + + 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 +}; + +} diff --git a/src/tests/frontend/CMakeLists.txt b/src/tests/frontend/CMakeLists.txt new file mode 100644 index 000000000..45fa0bed0 --- /dev/null +++ b/src/tests/frontend/CMakeLists.txt @@ -0,0 +1,3 @@ +add_executable(frontend_tst frontend.cpp) +target_link_libraries(frontend_tst ${EXTRA_LIBS}) +add_test(frontend ${CMAKE_CURRENT_BINARY_DIR}/frontend_tst) diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp new file mode 100644 index 000000000..7479e9a4f --- /dev/null +++ b/src/tests/frontend/frontend.cpp @@ -0,0 +1,24 @@ +/* +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 "frontend.h" +#include "environment.h" +#include "test.h" +using namespace lean; + +static void tst1() { + frontend f; + f.add_uvar("tst"); + frontend c = f.mk_child(); + lean_assert(c.get_uvar("tst") == f.get_uvar("tst")); + lean_assert(f.env().has_children()); +} + +int main() { + continue_on_violation(true); + tst1(); + return has_violations() ? 1 : 0; +}