feat(kernel/environment): environment as a Lean object

src/frontends/lean/parser_config.cpp

@@ -377,7 +377,7 @@ struct cmd_ext : public environment_extension {
 
 struct cmd_ext_reg {
     unsigned m_ext_id;
-    cmd_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<cmd_ext>()); }
+    cmd_ext_reg() { m_ext_id = environment::register_extension(new cmd_ext()); }
 };
 static cmd_ext_reg * g_ext = nullptr;
 static cmd_ext const & get_extension(environment const & env) {
@@ -391,7 +391,7 @@ environment add_command(environment const & env, name const & n, cmd_info const
     auto env2 = token_ext::register_entry(env, get_dummy_ios(), token_entry(n.to_string()));
     cmd_ext ext = get_extension(env2);
     ext.m_cmds.insert(n, info);
-    return env2.update(g_ext->m_ext_id, std::make_shared<cmd_ext>(ext));
+    return env2.update(g_ext->m_ext_id, new cmd_ext(ext));
 }
 
 void initialize_parser_config() {

src/init/init.cpp

@@ -26,6 +26,15 @@ namespace lean {
 void initialize() {
     save_stack_info();
     initialize_util_module();
+    object * w = initialize_init_default(io_mk_world());
+    w = initialize_init_lean_default(w);
+    if (io_result_is_error(w)) {
+        io_result_show_error(w);
+        dec(w);
+        throw exception("initialization failed");
+    } else {
+        dec(w);
+    }
     initialize_sexpr_module();
     initialize_kernel_module();
     init_default_print_fn();
@@ -36,15 +45,6 @@ void initialize() {
     initialize_constructions_module();
     initialize_equations_compiler_module();
     initialize_frontend_lean_module();
-    object * w = initialize_init_default(io_mk_world());
-    w = initialize_init_lean_default(w);
-    if (io_result_is_error(w)) {
-        io_result_show_error(w);
-        dec(w);
-        throw exception("initialization failed");
-    } else {
-        dec(w);
-    }
 }
 
 void finalize() {

src/kernel/declaration.h

@@ -435,6 +435,8 @@ public:
     constant_info(recursor_val const & v);
     constant_info(constant_info const & other):object_ref(other) {}
     constant_info(constant_info && other):object_ref(other) {}
+    explicit constant_info(b_obj_arg o, bool b):object_ref(o, b) {}
+    explicit constant_info(obj_arg o):object_ref(o) {}
 
     constant_info_kind kind() const { return static_cast<constant_info_kind>(cnstr_tag(raw())); }
 

src/kernel/environment.cpp

@@ -9,24 +9,68 @@ Author: Leonardo de Moura
 #include <limits>
 #include "runtime/sstream.h"
 #include "runtime/thread.h"
+#include "util/map_foreach.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker.h"
 #include "kernel/quot.h"
 
 namespace lean {
-environment_extension::~environment_extension() {}
+object* environment_add_core(object*, object*);
+object* mk_empty_environment_core(uint32, object*);
+object* environment_find_core(object*, object*);
+uint32 environment_trust_level_core(object*);
+object* environment_mark_quot_init_core(object*);
+uint8 environment_quot_init_core(object*);
+object* register_extension_core(object*);
+object* get_extension_core(object*, object*);
+object* set_extension_core(object*, object*, object*);
+object* environment_switch_core(object*);
+
+object* mk_empty_environment(uint32 trust_lvl) {
+    object* r = mk_empty_environment_core(trust_lvl, io_mk_world());
+    if (io_result_is_error(r)) { dec(r); throw exception("error creating empty environment"); }
+    object* env = io_result_get_value(r);
+    inc(env);
+    dec(r);
+    return env;
+}
+
+environment::environment(unsigned trust_lvl):
+    // TODO(Leo): do not eagerly switch
+    object_ref(environment_switch_core(mk_empty_environment(trust_lvl))) {
+}
+
+unsigned environment::trust_lvl() const {
+    return environment_trust_level_core(object_ref::get());
+}
+
+bool environment::is_quot_initialized() const {
+    return environment_quot_init_core(object_ref::get()) != 0;
+}
+
+void environment::mark_quot_initialized() {
+    m_obj = environment_mark_quot_init_core(m_obj);
+}
+
+template<typename T> optional<T> to_optional(obj_arg o) {
+    if (is_scalar(o)) return optional<T>();
+    T r(cnstr_get(o, 0), true);
+    dec(o);
+    return optional<T>(r);
+}
 
 optional<constant_info> environment::find(name const & n) const {
-    constant_info const * r = m_constants.find(n);
-    return r ? some_constant_info(*r) : none_constant_info();
+    return to_optional<constant_info>(environment_find_core(object_ref::get(), n.get()));
 }
 
 constant_info environment::get(name const & n) const {
-    constant_info const * r = m_constants.find(n);
-    if (!r)
+    object * o = environment_find_core(object_ref::get(), n.get());
+    if (is_scalar(o))
         throw unknown_constant_exception(*this, n);
-    return *r;
+    constant_info r(cnstr_get(o, 0), true);
+    dec(o);
+    return r;
 }
 
 static void check_no_metavar(environment const & env, name const & n, expr const & e) {
@@ -82,6 +126,14 @@ static void check_constant_val(environment const & env, constant_val const & v,
     check_constant_val(env, v, checker);
 }
 
+void environment::add_core(constant_info const & info) {
+    m_obj = environment_add_core(m_obj, info.get());
+}
+
+environment environment::add(constant_info const & info) const {
+    return environment(environment_add_core(object_ref::get(), info.get()));
+}
+
 environment environment::add_axiom(declaration const & d, bool check) const {
     axiom_val const & v = d.to_axiom_val();
     if (check)
@@ -188,65 +240,67 @@ environment environment::add(declaration const & d, bool check) const {
     lean_unreachable();
 }
 
-class extension_manager {
-    std::vector<std::shared_ptr<environment_extension const>> m_exts;
-    mutex                                                     m_mutex;
-public:
-    unsigned register_extension(std::shared_ptr<environment_extension const> const & ext) {
-        lock_guard<mutex> lock(m_mutex);
-        unsigned r = m_exts.size();
-        m_exts.push_back(ext);
-        return r;
-    }
-
-    bool has_ext(unsigned extid) const { return extid < m_exts.size(); }
-
-    environment_extension const & get_initial(unsigned extid) {
-        lock_guard<mutex> lock(m_mutex);
-        return *(m_exts[extid].get());
-    }
-};
-
-static extension_manager * g_extension_manager = nullptr;
-static extension_manager & get_extension_manager() {
-    return *g_extension_manager;
+static void env_ext_finalizer(void * ext) {
+    delete static_cast<environment_extension*>(ext);
 }
 
-void initialize_environment() {
-    g_extension_manager = new extension_manager();
+static void env_ext_foreach(void * /* ext */, b_obj_arg /* fn */) {
+    /* The foreach combinator is used by `mark_mt` when marking values as "multi-threaded".
+       Moreover, it is invoked even when we don't use threads because of global
+       IO.Ref is considered to be "multi-threaded".
+
+       So, we just ignore this issue for now.
+       This is not critical since eventually all environment extensions will be implemented in Lean,
+       and we will be able to delete this code.
+    */
 }
 
-void finalize_environment() {
-    delete g_extension_manager;
+static external_object_class * g_env_ext_class = nullptr;
+
+static environment_extension const & to_env_ext(b_obj_arg o) {
+    lean_assert(external_class(o) == g_env_ext_class);
+    return *static_cast<environment_extension *>(external_data(o));
 }
 
-unsigned environment::register_extension(std::shared_ptr<environment_extension const> const & initial) {
-    return get_extension_manager().register_extension(initial);
+static obj_res to_object(environment_extension * ext) {
+    return alloc_external(g_env_ext_class, ext);
 }
 
-[[ noreturn ]] void throw_invalid_extension(environment const & env) {
-    throw kernel_exception(env, "invalid environment extension identifier");
+unsigned environment::register_extension(environment_extension * initial) {
+    object * r = register_extension_core(to_object(initial));
+    if (is_scalar(r)) { throw exception("error creating empty environment"); }
+    unsigned idx = unbox(cnstr_get(r, 0));
+    dec(r);
+    return idx;
 }
 
 environment_extension const & environment::get_extension(unsigned id) const {
-    if (!get_extension_manager().has_ext(id))
-        throw_invalid_extension(*this);
-    if (id >= m_extensions->size() || !(*m_extensions)[id])
-        return get_extension_manager().get_initial(id);
-    return *((*m_extensions)[id].get());
+    object * r = get_extension_core(object_ref::get(), box(id));
+    if (is_scalar(r)) { throw exception("invalid extension id"); }
+    object * ext = cnstr_get(r, 0);
+    dec(r);
+    return to_env_ext(ext);
 }
 
-environment environment::update(unsigned id, std::shared_ptr<environment_extension const> const & ext) const {
-    if (!get_extension_manager().has_ext(id))
-        throw_invalid_extension(*this);
-    auto new_exts = std::make_shared<environment_extensions>(*m_extensions);
-    if (id >= new_exts->size())
-        new_exts->resize(id+1);
-    (*new_exts)[id] = ext;
-    return environment(*this, new_exts);
+environment environment::update(unsigned id, environment_extension * ext) const {
+    object * r = set_extension_core(object_ref::get(), box(id), to_object(ext));
+    if (is_scalar(r)) { throw exception("invalid extension id"); }
+    environment env(cnstr_get(r, 0), true);
+    dec(r);
+    return env;
 }
 
 void environment::for_each_constant(std::function<void(constant_info const & d)> const & f) const {
-    m_constants.for_each([&](name const &, constant_info const & c) { return f(c); });
+    smap_foreach(cnstr_get(raw(), 1), [&](object *, object * v) {
+            constant_info cinfo(v, true);
+            f(cinfo);
+        });
+}
+
+void initialize_environment() {
+    g_env_ext_class = register_external_object_class(env_ext_finalizer, env_ext_foreach);
+}
+
+void finalize_environment() {
 }
 }

src/kernel/environment.h

@@ -24,43 +24,20 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-class environment;
-
 class environment_extension {
 public:
-    virtual ~environment_extension();
+    virtual ~environment_extension() {}
 };
 
-typedef std::vector<std::shared_ptr<environment_extension const>> environment_extensions;
-
-/** \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.
-    2- By attaching additional data as environment::extensions. The additional data can be added
-       at any time. They contain information used by the automation (e.g., rewriting sets, unification hints, etc). */
-class environment {
-    typedef name_map<constant_info>                       constants;
-    typedef std::shared_ptr<environment_extensions const> extensions;
+class environment : public object_ref {
     friend class add_inductive_fn;
 
-    unsigned                  m_trust_lvl;
-    bool                      m_quot_initialized{false};
-    constants                 m_constants;
-    extensions                m_extensions;
-
-    environment(environment const & env, extensions const & exts):
-        m_trust_lvl(env.m_trust_lvl), m_quot_initialized(env.m_quot_initialized),
-        m_constants(env.m_constants), m_extensions(exts) {}
-
-    void check_duplicated_univ_params(names ls) const;
     void check_name(name const & n) const;
+    void check_duplicated_univ_params(names ls) const;
 
-    void add_core(constant_info const & info) { m_constants.insert(info.get_name(), info); }
-    environment add(constant_info const & info) const {
-        environment new_env(*this);
-        new_env.add_core(info);
-        return new_env;
-    }
+    void add_core(constant_info const & info);
+    void mark_quot_initialized();
+    environment add(constant_info const & info) const;
     environment add_axiom(declaration const & d, bool check) const;
     environment add_definition(declaration const & d, bool check) const;
     environment add_theorem(declaration const & d, bool check) const;
@@ -68,17 +45,21 @@ class environment {
     environment add_mutual(declaration const & d, bool check) const;
     environment add_quot() const;
     environment add_inductive(declaration const & d) const;
-
 public:
-    environment(unsigned trust_lvl = 0):
-        m_trust_lvl(trust_lvl),
-        m_extensions(std::make_shared<environment_extensions const>()) {}
+    environment(unsigned trust_lvl = 0);
+    environment(environment const & other):object_ref(other) {}
+    environment(environment && other):object_ref(other) {}
+    explicit environment(b_obj_arg o, bool b):object_ref(o, b) {}
+    explicit environment(obj_arg o):object_ref(o) {}
     ~environment() {}
 
-    /** \brief Return the trust level of this environment. */
-    unsigned trust_lvl() const { return m_trust_lvl; }
+    environment & operator=(environment const & other) { object_ref::operator=(other); return *this; }
+    environment & operator=(environment && other) { object_ref::operator=(other); return *this; }
 
-    bool is_quot_initialized() const { return m_quot_initialized; }
+    /** \brief Return the trust level of this environment. */
+    unsigned trust_lvl() const;
+
+    bool is_quot_initialized() const;
 
     /** \brief Return information for the constant with name \c n (if it is defined in this environment). */
     optional<constant_info> find(name const & n) const;
@@ -98,22 +79,20 @@ public:
         \remark The extension objects are created on demand.
 
         \see get_extension */
-    static unsigned register_extension(std::shared_ptr<environment_extension const> const & initial);
+    static unsigned register_extension(environment_extension * initial);
 
     /** \brief Return the extension with the given id. */
     environment_extension const & get_extension(unsigned extid) const;
 
     /** \brief Update the environment extension with the given id. */
-    environment update(unsigned extid, std::shared_ptr<environment_extension const> const & ext) const;
+    environment update(unsigned extid, environment_extension * ext) const;
 
     /** \brief Apply the function \c f to each constant */
     void for_each_constant(std::function<void(constant_info const & d)> const & f) const;
 
-    /** \brief Return true iff declarations and extensions of e1 and e2 are pointer equal */
+    /** \brief Pointer equality */
     friend bool is_eqp(environment const & e1, environment const & e2) {
-        return
-            is_eqp(e1.m_constants, e2.m_constants) &&
-            e1.m_extensions.get() == e2.m_extensions.get();
+        return e1.raw() == e2.raw();
     }
 };
 

src/kernel/quot.cpp

@@ -45,7 +45,7 @@ static void check_eq_type(environment const & env) {
 }
 
 environment environment::add_quot() const {
-    if (m_quot_initialized)
+    if (is_quot_initialized())
         return *this;
     check_eq_type(*this);
     environment new_env = *this;
@@ -93,7 +93,7 @@ environment environment::add_quot() const {
                    : (∀ a : α, β (@quot.mk.{u} α r a)) → ∀ q : @quot.{u} α r, β q */
     new_env.add_core(constant_info(quot_val(*quot_consts::g_quot_ind, {u_name},
                                             lctx.mk_pi({alpha, r, beta}, mk_arrow(all_quot, lctx.mk_pi(q, beta_q))), quot_kind::Ind)));
-    new_env.m_quot_initialized = true;
+    new_env.mark_quot_initialized();
     return new_env;
 }
 

src/library/aliases.cpp

@@ -122,7 +122,7 @@ struct aliases_ext_reg {
     unsigned m_ext_id;
     aliases_ext_reg() {
         register_scoped_ext(aliases_ext::push_scope, aliases_ext::pop_scope);
-        m_ext_id = environment::register_extension(std::make_shared<aliases_ext>());
+        m_ext_id = environment::register_extension(new aliases_ext());
     }
 };
 static aliases_ext_reg * g_ext = nullptr;
@@ -130,7 +130,7 @@ static aliases_ext const & get_extension(environment const & env) {
     return static_cast<aliases_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, aliases_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<aliases_ext>(ext));
+    return env.update(g_ext->m_ext_id, new aliases_ext(ext));
 }
 
 environment add_expr_alias(environment const & env, name const & a, name const & e, bool overwrite) {

src/library/aux_recursors.cpp

@@ -17,7 +17,7 @@ struct aux_recursor_ext : public environment_extension {
 
 struct aux_recursor_ext_reg {
     unsigned m_ext_id;
-    aux_recursor_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<aux_recursor_ext>()); }
+    aux_recursor_ext_reg() { m_ext_id = environment::register_extension(new aux_recursor_ext()); }
 };
 
 static aux_recursor_ext_reg * g_ext = nullptr;
@@ -25,7 +25,7 @@ static aux_recursor_ext const & get_extension(environment const & env) {
     return static_cast<aux_recursor_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, aux_recursor_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<aux_recursor_ext>(ext));
+    return env.update(g_ext->m_ext_id, new aux_recursor_ext(ext));
 }
 
 struct auxrec_modification : public modification {

src/library/compiler/borrowed_annotation.cpp

@@ -33,7 +33,7 @@ struct borrowed_ext : public environment_extension {
 
 struct borrowed_ext_reg {
     unsigned m_ext_id;
-    borrowed_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<borrowed_ext>()); }
+    borrowed_ext_reg() { m_ext_id = environment::register_extension(new borrowed_ext()); }
 };
 
 static borrowed_ext_reg * g_ext = nullptr;
@@ -41,7 +41,7 @@ static borrowed_ext const & get_extension(environment const & env) {
     return static_cast<borrowed_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, borrowed_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<borrowed_ext>(ext));
+    return env.update(g_ext->m_ext_id, new borrowed_ext(ext));
 }
 
 /* Support for old module manager.

src/library/compiler/closed_term_cache.cpp

@@ -17,7 +17,7 @@ struct closed_term_ext : public environment_extension {
 
 struct closed_term_ext_reg {
     unsigned m_ext_id;
-    closed_term_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<closed_term_ext>()); }
+    closed_term_ext_reg() { m_ext_id = environment::register_extension(new closed_term_ext()); }
 };
 
 static closed_term_ext_reg * g_ext = nullptr;
@@ -25,7 +25,7 @@ static closed_term_ext const & get_extension(environment const & env) {
     return static_cast<closed_term_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, closed_term_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<closed_term_ext>(ext));
+    return env.update(g_ext->m_ext_id, new closed_term_ext(ext));
 }
 
 /* Support for old module manager.

src/library/compiler/llnf_code.cpp

@@ -16,7 +16,7 @@ struct llnf_code_ext : public environment_extension {
 
 struct llnf_code_ext_reg {
     unsigned m_ext_id;
-    llnf_code_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<llnf_code_ext>()); }
+    llnf_code_ext_reg() { m_ext_id = environment::register_extension(new llnf_code_ext()); }
 };
 
 static llnf_code_ext_reg * g_ext = nullptr;
@@ -24,7 +24,7 @@ static llnf_code_ext const & get_extension(environment const & env) {
     return static_cast<llnf_code_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, llnf_code_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<llnf_code_ext>(ext));
+    return env.update(g_ext->m_ext_id, new llnf_code_ext(ext));
 }
 
 environment save_llnf_code(environment const & env, comp_decls const & ds) {

src/library/compiler/specialize.cpp

@@ -128,7 +128,7 @@ struct specialize_ext : public environment_extension {
 
 struct specialize_ext_reg {
     unsigned m_ext_id;
-    specialize_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<specialize_ext>()); }
+    specialize_ext_reg() { m_ext_id = environment::register_extension(new specialize_ext()); }
 };
 
 static specialize_ext_reg * g_ext = nullptr;
@@ -136,7 +136,7 @@ static specialize_ext const & get_extension(environment const & env) {
     return static_cast<specialize_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, specialize_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<specialize_ext>(ext));
+    return env.update(g_ext->m_ext_id, new specialize_ext(ext));
 }
 
 /* Support for old module manager.

src/library/export_decl.cpp

@@ -49,7 +49,7 @@ struct export_decl_env_ext : public environment_extension {
 /** \brief Auxiliary object for registering the environment extension */
 struct export_decl_env_ext_reg {
     unsigned m_ext_id;
-    export_decl_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<export_decl_env_ext>()); }
+    export_decl_env_ext_reg() { m_ext_id = environment::register_extension(new export_decl_env_ext()); }
 };
 
 static export_decl_env_ext_reg * g_ext = nullptr;
@@ -61,7 +61,7 @@ static export_decl_env_ext const & get_export_decl_extension(environment const &
 
 /** \brief Update environment extension */
 static environment update(environment const & env, export_decl_env_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<export_decl_env_ext>(ext));
+    return env.update(g_ext->m_ext_id, new export_decl_env_ext(ext));
 }
 
 static environment add_export_decl_core(environment const & env, name const & in_ns, export_decl const & e) {

src/library/module.cpp

@@ -82,7 +82,7 @@ struct module_ext : public environment_extension {
 
 struct module_ext_reg {
     unsigned m_ext_id;
-    module_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<module_ext>()); }
+    module_ext_reg() { m_ext_id = environment::register_extension(new module_ext()); }
 };
 
 static module_ext_reg * g_ext = nullptr;
@@ -92,7 +92,7 @@ static module_ext const & get_extension(environment const & env) {
 }
 
 static environment update(environment const & env, module_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<module_ext>(ext));
+    return env.update(g_ext->m_ext_id, new module_ext(ext));
 }
 
 static char const * g_olean_end_file = "EndFile";

src/library/private.cpp

@@ -24,7 +24,7 @@ struct private_ext : public environment_extension {
 
 struct private_ext_reg {
     unsigned m_ext_id;
-    private_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<private_ext>()); }
+    private_ext_reg() { m_ext_id = environment::register_extension(new private_ext()); }
 };
 
 static private_ext_reg * g_ext = nullptr;
@@ -32,7 +32,7 @@ static private_ext const & get_extension(environment const & env) {
     return static_cast<private_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, private_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<private_ext>(ext));
+    return env.update(g_ext->m_ext_id, new private_ext(ext));
 }
 
 environment set_main_module_name(environment const & env, name const & mod_name) {

src/library/projection.cpp

@@ -25,7 +25,7 @@ struct projection_ext : public environment_extension {
 struct projection_ext_reg {
     unsigned m_ext_id;
     projection_ext_reg() {
-        m_ext_id = environment::register_extension(std::make_shared<projection_ext>());
+        m_ext_id = environment::register_extension(new projection_ext());
     }
 };
 
@@ -34,7 +34,7 @@ static projection_ext const & get_extension(environment const & env) {
     return static_cast<projection_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, projection_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<projection_ext>(ext));
+    return env.update(g_ext->m_ext_id, new projection_ext(ext));
 }
 
 struct proj_modification : public modification {

src/library/protected.cpp

@@ -17,7 +17,7 @@ struct protected_ext : public environment_extension {
 
 struct protected_ext_reg {
     unsigned m_ext_id;
-    protected_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<protected_ext>()); }
+    protected_ext_reg() { m_ext_id = environment::register_extension(new protected_ext()); }
 };
 
 static protected_ext_reg * g_ext = nullptr;
@@ -25,7 +25,7 @@ static protected_ext const & get_extension(environment const & env) {
     return static_cast<protected_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, protected_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<protected_ext>(ext));
+    return env.update(g_ext->m_ext_id, new protected_ext(ext));
 }
 
 struct protected_modification : public modification {

src/library/scoped_ext.cpp

@@ -30,7 +30,7 @@ struct scope_mng_ext : public environment_extension {
 
 struct scope_mng_ext_reg {
     unsigned m_ext_id;
-    scope_mng_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<scope_mng_ext>()); }
+    scope_mng_ext_reg() { m_ext_id = environment::register_extension(new scope_mng_ext()); }
 };
 
 static scope_mng_ext_reg * g_ext = nullptr;
@@ -38,7 +38,7 @@ static scope_mng_ext const & get_extension(environment const & env) {
     return static_cast<scope_mng_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, scope_mng_ext const & ext) {
-    return env.update(g_ext->m_ext_id, std::make_shared<scope_mng_ext>(ext));
+    return env.update(g_ext->m_ext_id, new scope_mng_ext(ext));
 }
 
 name const & get_namespace(environment const & env) {

src/library/scoped_ext.h

@@ -159,7 +159,7 @@ public:
         reg() {
             register_scoped_ext(push_fn, pop_fn);
             modification::init();
-            m_ext_id = environment::register_extension(std::make_shared<scoped_ext>());
+            m_ext_id = environment::register_extension(new scoped_ext());
         }
         ~reg() {
             modification::finalize();
@@ -174,7 +174,7 @@ public:
         return static_cast<scoped_ext const &>(env.get_extension(g_ext->m_ext_id));
     }
     static environment update(environment const & env, scoped_ext const & ext) {
-        return env.update(g_ext->m_ext_id, std::make_shared<scoped_ext>(ext));
+        return env.update(g_ext->m_ext_id, new scoped_ext(ext));
     }
     static environment push_fn(environment const & env, io_state const &, scope_kind) {
         return update(env, get(env).push());

src/util/object_ref.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 namespace lean {
 /* Smart point for Lean objects. It is useful for writing C++ code that manipulates Lean objects.  */
 class object_ref {
+protected:
     object * m_obj;
 public:
     object_ref():m_obj(box(0)) {}
@@ -34,6 +35,7 @@ public:
     }
     object * raw() const { return m_obj; }
     object * steal() { object * r = m_obj; m_obj = box(0); return r; }
+    object * get() const { inc(m_obj); return m_obj; }
     static void swap(object_ref & a, object_ref & b) { std::swap(a.m_obj, b.m_obj); }
 };