Add children environments

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

src/kernel/environment.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <vector>
 #include <limits>
+#include <atomic>
 #include "environment.h"
 #include "exception.h"
 #include "debug.h"
@@ -18,6 +19,14 @@ constexpr unsigned uninit = std::numeric_limits<int>::max();
 struct environment::imp {
     std::vector<std::vector<unsigned>> m_uvar_distances;
     std::vector<level>                 m_uvars;
+    std::atomic<unsigned>              m_num_children;
+    std::shared_ptr<imp>               m_parent;
+
+    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; }
 
     /** \brief Return v - k. It throws an exception if there is a underflow. */
     static int sub(int v, unsigned k) {
@@ -63,7 +72,10 @@ struct environment::imp {
     }
 
     bool is_ge(level const & l1, level const & l2) {
-        return is_ge(l1, l2, 0);
+        if (!has_parent())
+            return is_ge(l1, l2, 0);
+        else
+            return m_parent->is_ge(l1, l2);
     }
 
     level add_var(name const & n) {
@@ -111,6 +123,10 @@ struct environment::imp {
     }
 
     level define_uvar(name const & n, level const & l) {
+        if (has_parent())
+            throw exception("invalid universe declaration, universe variables can only be declared in top-level environments");
+        if (has_children())
+            throw exception("invalid universe declaration, environment has children environments");
         level r = add_var(n);
         add_constraints(uvar_idx(r), l, 0);
         return r;
@@ -139,13 +155,33 @@ struct environment::imp {
                       });
     }
 
-    imp() {
+    imp():
+        m_num_children(0) {
         init_uvars();
     }
+
+    explicit imp(std::shared_ptr<imp> const & parent):
+        m_num_children(0),
+        m_parent(parent) {
+        m_parent->inc_children();
+    }
+
+    ~imp() {
+        if (m_parent)
+            m_parent->dec_children();
+    }
 };
 
 environment::environment():
-    m_imp(new imp) {
+    m_imp(new imp()) {
+}
+
+environment::environment(imp * new_ptr):
+    m_imp(new_ptr) {
+}
+
+environment::environment(std::shared_ptr<imp> const & ptr):
+    m_imp(ptr) {
 }
 
 environment::~environment() {
@@ -162,4 +198,22 @@ bool environment::is_ge(level const & l1, level const & l2) const {
 void environment::display_uvars(std::ostream & out) const {
     m_imp->display_uvars(out);
 }
+
+environment environment::mk_child() const {
+    return environment(new imp(m_imp));
+}
+
+bool environment::has_children() const {
+    return m_imp->has_children();
+}
+
+bool environment::has_parent() const {
+    return m_imp->has_parent();
+}
+
+environment environment::parent() const {
+    lean_assert(has_parent());
+    return environment(m_imp->m_parent);
+}
+
 }

src/kernel/environment.h

@@ -16,7 +16,9 @@ namespace lean {
 */
 class environment {
     struct imp;
-    std::unique_ptr<imp> m_imp;
+    std::shared_ptr<imp> m_imp;
+    explicit environment(std::shared_ptr<imp> const & ptr);
+    explicit environment(imp * new_ptr);
 public:
     environment();
     ~environment();
@@ -40,5 +42,29 @@ public:
 
     /** \brief Display universal variables, and their constraints */
     void display_uvars(std::ostream & out) const;
+
+    /**
+       \brief Return universal variable with the given name.
+       Throw an exception if variable is not defined in this environment.
+    */
+    level get_uvar(name const & n) const;
+
+    /**
+       \brief Create a child environment. This environment will only allow "read-only" operations until
+       all children environments are deleted.
+    */
+    environment mk_child() const;
+
+    /** \brief Return true iff this environment has children environments. */
+    bool has_children() const;
+
+    /** \brief Return true iff this environment has a parent environment. */
+    bool has_parent() const;
+
+    /**
+        \brief Return parent environment of this environment.
+        \pre has_parent()
+    */
+    environment parent() const;
 };
 }

src/tests/kernel/CMakeLists.txt

@@ -22,3 +22,6 @@ add_test(type_check ${CMAKE_CURRENT_BINARY_DIR}/type_check)
 add_executable(arith arith.cpp)
 target_link_libraries(arith ${EXTRA_LIBS})
 add_test(arith ${CMAKE_CURRENT_BINARY_DIR}/arith)
+add_executable(environment environment.cpp)
+target_link_libraries(environment ${EXTRA_LIBS})
+add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)

src/tests/kernel/environment.cpp

@@ -0,0 +1,65 @@
+/*
+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 "environment.h"
+#include "type_check.h"
+#include "builtin.h"
+#include "arith.h"
+#include "normalize.h"
+#include "abstract.h"
+#include "exception.h"
+#include "test.h"
+using namespace lean;
+
+static void tst1() {
+    environment env;
+    level u = env.define_uvar("u", level() + 1);
+    level w = env.define_uvar("w", u + 1);
+    lean_assert(!env.has_children());
+    lean_assert(!env.has_parent());
+    {
+        environment child = env.mk_child();
+        lean_assert(child.is_ge(w, u));
+        lean_assert(child.is_ge(w, level() + 2));
+        lean_assert(env.is_ge(w, level() + 2));
+        lean_assert(env.has_children());
+        lean_assert(child.has_parent());
+        lean_assert(!env.has_parent());
+        try {
+            level o = env.define_uvar("o", w + 1);
+            lean_unreachable();
+        }
+        catch (exception const & ex) {
+            std::cout << "expected error: " << ex.what() << "\n";
+        }
+    }
+    std::cout << "tst1 checkpoint" << std::endl;
+    level o = env.define_uvar("o", w + 1);
+    lean_assert(!env.has_children());
+    env.display_uvars(std::cout);
+}
+
+static environment mk_child() {
+    environment env;
+    level u = env.define_uvar("u", level() + 1);
+    return env.mk_child();
+}
+
+static void tst2() {
+    environment child = mk_child();
+    lean_assert(child.has_parent());
+    lean_assert(!child.has_children());
+    environment parent = child.parent();
+    parent.display_uvars(std::cout);
+    lean_assert(parent.has_children());
+}
+
+int main() {
+    continue_on_violation(true);
+    tst1();
+    tst2();
+    return has_violations() ? 1 : 0;
+}