From 9ed700a5a6dfad17c891e68ef490bc9cf0e9511b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 May 2014 08:40:46 -0700
Subject: [PATCH] feat(kernel/environment): add forget method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/environment.cpp      | 4 ++++
 src/kernel/environment.h        | 7 +++++++
 src/library/kernel_bindings.cpp | 2 ++
 tests/lua/env7.lua              | 9 +++++++++
 4 files changed, 22 insertions(+)
 create mode 100644 tests/lua/env7.lua

diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 125dd0050..6339bee74 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -108,6 +108,10 @@ environment environment::replace(certified_definition const & t) const {
     return environment(m_header, m_id, insert(m_definitions, n, t.get_definition()), m_global_levels, m_extensions);
 }
 
+environment environment::forget() const {
+    return environment(m_header, environment_id(), m_definitions, m_global_levels, m_extensions);
+}
+
 class extension_manager {
     std::vector<std::shared_ptr<environment_extension const>> m_exts;
     mutex                                                     m_mutex;
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 6d225e5db..0804877fd 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -181,6 +181,13 @@ public:
 
     /** \brief Update the environment extension with the given id. */
     environment update(unsigned extid, std::shared_ptr<environment_extension const> const & ext) const;
+
+    /**
+        \brief Return a new environment, where its "history" has been truncated/forgotten.
+        That is, <tt>is_descendant(e)</tt> will return false for any environment \c e that
+        is not pointer equal to the result.
+    */
+    environment forget() const;
 };
 
 class name_generator;
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index dcd273a7b..0b3541a42 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -884,6 +884,7 @@ static int mk_empty_environment(lua_State * L) {
     bool impredicative = get_bool_named_param(L, 1, "impredicative", true);
     return push_environment(L, environment(trust_lvl, proof_irrel, eta, impredicative));
 }
+static int environment_forget(lua_State * L) { return push_environment(L, to_environment(L, 1).forget()); }
 
 static const struct luaL_Reg environment_m[] = {
     {"__gc",              environment_gc}, // never throws
@@ -900,6 +901,7 @@ static const struct luaL_Reg environment_m[] = {
     {"get",               safe_function<environment_get>},
     {"add",               safe_function<environment_add>},
     {"replace",           safe_function<environment_replace>},
+    {"forget",            safe_function<environment_forget>},
     {0, 0}
 };
 
diff --git a/tests/lua/env7.lua b/tests/lua/env7.lua
new file mode 100644
index 000000000..b45cf127e
--- /dev/null
+++ b/tests/lua/env7.lua
@@ -0,0 +1,9 @@
+local env1 = empty_environment()
+local env2 = add_decl(env1, mk_var_decl("A", Type))
+assert(env2:is_descendant(env1))
+assert(env2:is_descendant(env2))
+assert(not env1:is_descendant(env2))
+local env3 = env2:forget()
+assert(not env3:is_descendant(env1))
+assert(not env3:is_descendant(env2))
+assert(env3:is_descendant(env3))