diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 80074d77b2..a44b3cef54 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -20,57 +20,6 @@ environment_header::environment_header(unsigned trust_lvl, std::unique_ptrinc_ref(); - } - ~path() { if (m_prev) m_prev->dec_ref(); } -}; - -environment_id::environment_id():m_ptr(new path()), m_depth(0) {} -environment_id::environment_id(environment_id const & ancestor, bool) { - if (ancestor.m_depth == std::numeric_limits::max()) - throw exception("maximal depth in is_descendant tree has been reached, use 'forget' method to workaround this limitation"); - lock_guard lock(ancestor.m_ptr->m_mutex); - if (ancestor.m_ptr->m_next_depth == ancestor.m_depth + 1) { - m_ptr = ancestor.m_ptr; - m_depth = ancestor.m_depth + 1; - m_ptr->m_next_depth++; - m_ptr->inc_ref(); - } else { - m_ptr = new path(ancestor.m_depth+1, ancestor.m_ptr); - m_depth = ancestor.m_depth + 1; - } - lean_assert(m_depth == ancestor.m_depth+1); - lean_assert(m_ptr->m_next_depth == m_depth+1); -} -environment_id::environment_id(environment_id const & id):m_ptr(id.m_ptr), m_depth(id.m_depth) { if (m_ptr) m_ptr->inc_ref(); } -environment_id::environment_id(environment_id && id):m_ptr(id.m_ptr), m_depth(id.m_depth) { id.m_ptr = nullptr; } -environment_id::~environment_id() { if (m_ptr) m_ptr->dec_ref(); } -environment_id & environment_id::operator=(environment_id const & s) { m_depth = s.m_depth; LEAN_COPY_REF(s); } -environment_id & environment_id::operator=(environment_id && s) { m_depth = s.m_depth; LEAN_MOVE_REF(s); } -bool environment_id::is_descendant(environment_id const & id) const { - if (m_depth < id.m_depth) - return false; - path * p = m_ptr; - while (p != nullptr) { - if (p == id.m_ptr) - return true; - if (p->m_start_depth <= id.m_depth) - return false; - p = p->m_prev; - } - return false; -} - environment::environment(unsigned trust_lvl): environment(trust_lvl, mk_id_normalizer_extension()) {} @@ -115,8 +64,6 @@ environment environment::add_quot() const { } environment environment::add(certified_declaration const & d) const { - if (!m_id.is_descendant(d.get_id())) - throw_incompatible_environment(*this); name const & n = d.get_declaration().get_name(); if (find(n)) throw already_declared_exception(*this, n); @@ -142,12 +89,6 @@ environment environment::add_meta(buffer const & ds, bool check) co return new_env; } -environment environment::forget() const { - environment new_env = *this; - new_env.m_id = environment_id(); - return new_env; -} - class extension_manager { std::vector> m_exts; mutex m_mutex; diff --git a/src/kernel/environment.h b/src/kernel/environment.h index dfffd6faac..1966a387eb 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -57,49 +57,6 @@ public: typedef std::vector> environment_extensions; -/** \brief environment identifier for tracking descendants of a given environment. - - It is used in the following places: - 1) `environment::add`: to check whether the certified declaration has been type checked - in an "ancestor" of the `this` environment. - - 2) `environment::replace`: (similar to previous case) to check whether the new declaration - has been type checked in an "ancestor" of the `this` environment. - - 3) `tactic.set_env`: to check whether the new environment is a descendant of the environment - in the current `tactic_state` object. - - 4) `vm::update_env`: similar to case 3. - - 5) To check whether user_attribute and simp_lemmas thread local caches needs to be reset or not. - - Cases 1 and 2 are needed for soundness. Cases 3 and 4 are necessary to enforce invariants that - we assume in the frontend, otherwise user defined tactics may break the system. Case 5 can - be avoided after we stop using thread local caches. */ -class environment_id { - friend class environment_id_tester; - friend class environment; // Only the environment class can create object of this type. - struct path; - path * m_ptr; - unsigned m_depth; - /** \brief Create an identifier for an environment that is a direct descendant of the given one. - The bool field is just to make sure this constructor is not confused with a copy constructor */ - environment_id(environment_id const & ancestor, bool); - /** \brief Create an identifier for an environment without ancestors (e.g., empty environment) */ - environment_id(); - /** Create an identifier for an environment that is a direct descendant of the given one. */ - static environment_id mk_descendant(environment_id const & ancestor) { return environment_id(ancestor, true); } -public: - environment_id(environment_id const & id); - environment_id(environment_id && id); - ~environment_id(); - environment_id & operator=(environment_id const & s); - environment_id & operator=(environment_id && s); - - /** \brief Return true iff this object is a descendant of the given one. */ - bool is_descendant(environment_id const & id) const; -}; - /** \brief Lean core environment. An environment object can be extended/customized in different ways: 1- By providing a normalizer_extension when creating an empty environment. @@ -112,26 +69,19 @@ class environment { friend class add_inductive_fn; header m_header; - environment_id m_id; bool m_quot_initialized{false}; declarations m_declarations; extensions m_extensions; environment(environment const & env, declarations const & ds): - m_header(env.m_header), m_id(environment_id::mk_descendant(env.m_id)), m_quot_initialized(env.m_quot_initialized), m_declarations(ds), m_extensions(env.m_extensions) {} + m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_declarations(ds), m_extensions(env.m_extensions) {} environment(environment const & env, extensions const & exts): - m_header(env.m_header), m_id(environment_id::mk_descendant(env.m_id)), m_quot_initialized(env.m_quot_initialized), m_declarations(env.m_declarations), m_extensions(exts) {} + m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_declarations(env.m_declarations), m_extensions(exts) {} public: environment(unsigned trust_lvl = 0); environment(unsigned trust_lvl, std::unique_ptr ext); ~environment(); - /** \brief Return the environment unique identifier. */ - environment_id const & get_id() const { return m_id; } - - /** \brief Return true iff this environment is a descendant of \c env. */ - bool is_descendant(environment const & env) const { return m_id.is_descendant(env.m_id); } - /** \brief Return the trust level of this environment. */ unsigned trust_lvl() const { return m_header->trust_lvl(); } @@ -187,11 +137,6 @@ public: /** \brief Update the environment extension with the given id. */ environment update(unsigned extid, std::shared_ptr const & ext) const; - /** \brief Return a new environment, where its "history" has been truncated/forgotten. - That is, is_descendant(e) will return false for any environment \c e that - is not pointer equal to the result. */ - environment forget() const; - /** \brief Apply the function \c f to each declaration */ void for_each_declaration(std::function const & f) const; @@ -217,12 +162,10 @@ class name_generator; class certified_declaration { friend class certify_unchecked; friend certified_declaration check(environment const & env, declaration const & d); - environment_id m_id; declaration m_declaration; - certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {} + certified_declaration(declaration const & d):m_declaration(d) {} public: /** \brief Return the id of the environment that was used to type check this declaration. */ - environment_id const & get_id() const { return m_id; } declaration const & get_declaration() const { return m_declaration; } /** \brief Certifies a declaration without type-checking. diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index a53cb7b463..4b41fc3e64 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -873,13 +873,13 @@ certified_declaration check(environment const & env, declaration const & d) { if (d.has_value()) { check_definition(env, d, checker); } - return certified_declaration(env.get_id(), d); + return certified_declaration(d); } certified_declaration certified_declaration::certify(environment const & env, declaration const & d) { if (env.trust_lvl() == 0) throw kernel_exception(env, "environment trust level does not allow users to add declarations that were not type checked"); - return certified_declaration(env.get_id(), d); + return certified_declaration(d); } certified_declaration certified_declaration::certify_or_check(environment const & env, declaration const & d) { diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index e908026d72..acf6e389eb 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -1164,8 +1164,8 @@ public: } bool is_compatible(entry const & C, environment const & env, simp_lemmas_token tk) { - if (!env.is_descendant(C.m_env)) - return false; + // if (!env.is_descendant(C.m_env)) + // return false; auto & cfg = get_simp_lemmas_config(tk); unsigned i = 0; for (name const & attr_name : cfg.m_simp_attrs) { diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index f35a7a2e72..baa4e42aa7 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -724,10 +724,7 @@ vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) { vm_obj tactic_set_env(vm_obj const & _env, vm_obj const & _s) { tactic_state const & s = tactic::to_state(_s); environment const & new_env = to_env(_env); - if (new_env.is_descendant(s.env())) - return tactic::mk_success(set_env(s, new_env)); - else - return tactic::mk_exception(sstream() << "new environment is not a descendent from old environment.", s); + return tactic::mk_success(set_env(s, new_env)); } vm_obj tactic_open_namespaces(vm_obj const & s) {