diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 79eac61ad2..84d0def169 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include #include #include +#include #include "environment.h" #include "exception.h" #include "debug.h" @@ -18,6 +19,14 @@ constexpr unsigned uninit = std::numeric_limits::max(); struct environment::imp { std::vector> m_uvar_distances; std::vector m_uvars; + std::atomic m_num_children; + std::shared_ptr 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 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 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); +} + } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 3072b54621..223e76c985 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -16,7 +16,9 @@ namespace lean { */ class environment { struct imp; - std::unique_ptr m_imp; + std::shared_ptr m_imp; + explicit environment(std::shared_ptr 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; }; } diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt index fe3f17bd50..ce2969fee4 100644 --- a/src/tests/kernel/CMakeLists.txt +++ b/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) diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp new file mode 100644 index 0000000000..feb5474553 --- /dev/null +++ b/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; +}