Add frontend object

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

src/frontend/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(frontend frontend.cpp)
+target_link_libraries(frontend ${EXTRA_LIBS})

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 <atomic>
+#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<unsigned> m_num_children;
+    std::shared_ptr<imp>  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<imp> 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<imp> 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); }
+
+}
+

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 <memory>
+#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<imp> m_imp;
+    explicit frontend(imp * new_ptr);
+    explicit frontend(std::shared_ptr<imp> 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;
+
+
+};
+}

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<name> const & get_internal_names() const;
+    
+    fixity get_fixity() const;
+    
+    associativity get_associativity() const;
+
+    unsigned get_precedence() const;
+
+    list<name> 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<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
+};
+
+}

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)

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