From edb4d76ecde73e38bc8354419f62cde050385716 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 May 2019 12:41:33 -0700 Subject: [PATCH] feat(kernel/environment): `environment` as a Lean object --- src/frontends/lean/parser_config.cpp | 4 +- src/init/init.cpp | 18 +-- src/kernel/declaration.h | 2 + src/kernel/environment.cpp | 154 +++++++++++++------ src/kernel/environment.h | 63 +++----- src/kernel/quot.cpp | 4 +- src/library/aliases.cpp | 4 +- src/library/aux_recursors.cpp | 4 +- src/library/compiler/borrowed_annotation.cpp | 4 +- src/library/compiler/closed_term_cache.cpp | 4 +- src/library/compiler/llnf_code.cpp | 4 +- src/library/compiler/specialize.cpp | 4 +- src/library/export_decl.cpp | 4 +- src/library/module.cpp | 4 +- src/library/private.cpp | 4 +- src/library/projection.cpp | 4 +- src/library/protected.cpp | 4 +- src/library/scoped_ext.cpp | 4 +- src/library/scoped_ext.h | 4 +- src/util/object_ref.h | 2 + 20 files changed, 168 insertions(+), 131 deletions(-) diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp index 18c6c1275a..34940121cd 100644 --- a/src/frontends/lean/parser_config.cpp +++ b/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_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(ext)); + return env2.update(g_ext->m_ext_id, new cmd_ext(ext)); } void initialize_parser_config() { diff --git a/src/init/init.cpp b/src/init/init.cpp index 4ef0706e25..40f164f49c 100644 --- a/src/init/init.cpp +++ b/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() { diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index f415b93283..ebde315b72 100644 --- a/src/kernel/declaration.h +++ b/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(cnstr_tag(raw())); } diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 712681e91f..dae2b08405 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -9,24 +9,68 @@ Author: Leonardo de Moura #include #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 optional to_optional(obj_arg o) { + if (is_scalar(o)) return optional(); + T r(cnstr_get(o, 0), true); + dec(o); + return optional(r); +} optional 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(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> m_exts; - mutex m_mutex; -public: - unsigned register_extension(std::shared_ptr const & ext) { - lock_guard 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 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(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(external_data(o)); } -unsigned environment::register_extension(std::shared_ptr 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 const & ext) const { - if (!get_extension_manager().has_ext(id)) - throw_invalid_extension(*this); - auto new_exts = std::make_shared(*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 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() { } } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 3e4f721db1..c1f638b4da 100644 --- a/src/kernel/environment.h +++ b/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> 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 constants; - typedef std::shared_ptr 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(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 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 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 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 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(); } }; diff --git a/src/kernel/quot.cpp b/src/kernel/quot.cpp index 988882c714..1b45044807 100644 --- a/src/kernel/quot.cpp +++ b/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; } diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index afb73d8438..2182fcfc77 100644 --- a/src/library/aliases.cpp +++ b/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()); + 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(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(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) { diff --git a/src/library/aux_recursors.cpp b/src/library/aux_recursors.cpp index fad0970e26..c52a7ce9c6 100644 --- a/src/library/aux_recursors.cpp +++ b/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_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(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(ext)); + return env.update(g_ext->m_ext_id, new aux_recursor_ext(ext)); } struct auxrec_modification : public modification { diff --git a/src/library/compiler/borrowed_annotation.cpp b/src/library/compiler/borrowed_annotation.cpp index 43dceea762..4fe064fd04 100644 --- a/src/library/compiler/borrowed_annotation.cpp +++ b/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_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(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(ext)); + return env.update(g_ext->m_ext_id, new borrowed_ext(ext)); } /* Support for old module manager. diff --git a/src/library/compiler/closed_term_cache.cpp b/src/library/compiler/closed_term_cache.cpp index 0faca833d6..8a07f7fb4e 100644 --- a/src/library/compiler/closed_term_cache.cpp +++ b/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_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(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(ext)); + return env.update(g_ext->m_ext_id, new closed_term_ext(ext)); } /* Support for old module manager. diff --git a/src/library/compiler/llnf_code.cpp b/src/library/compiler/llnf_code.cpp index e22294472d..71a8f3ec84 100644 --- a/src/library/compiler/llnf_code.cpp +++ b/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_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(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(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) { diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index c57b718ecc..6391eeb965 100644 --- a/src/library/compiler/specialize.cpp +++ b/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_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(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(ext)); + return env.update(g_ext->m_ext_id, new specialize_ext(ext)); } /* Support for old module manager. diff --git a/src/library/export_decl.cpp b/src/library/export_decl.cpp index 9c21596f04..f08eeb2a3a 100644 --- a/src/library/export_decl.cpp +++ b/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_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(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) { diff --git a/src/library/module.cpp b/src/library/module.cpp index 4491a94e3d..5aa4ac3536 100644 --- a/src/library/module.cpp +++ b/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_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(ext)); + return env.update(g_ext->m_ext_id, new module_ext(ext)); } static char const * g_olean_end_file = "EndFile"; diff --git a/src/library/private.cpp b/src/library/private.cpp index b5f331332d..7d4d5b8667 100644 --- a/src/library/private.cpp +++ b/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_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(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(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) { diff --git a/src/library/projection.cpp b/src/library/projection.cpp index 6885082a55..b1c4bb49fd 100644 --- a/src/library/projection.cpp +++ b/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()); + 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(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(ext)); + return env.update(g_ext->m_ext_id, new projection_ext(ext)); } struct proj_modification : public modification { diff --git a/src/library/protected.cpp b/src/library/protected.cpp index 8b7e58711f..4fe0b932b4 100644 --- a/src/library/protected.cpp +++ b/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_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(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(ext)); + return env.update(g_ext->m_ext_id, new protected_ext(ext)); } struct protected_modification : public modification { diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp index c2224c5e86..311f7c8465 100644 --- a/src/library/scoped_ext.cpp +++ b/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_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(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(ext)); + return env.update(g_ext->m_ext_id, new scope_mng_ext(ext)); } name const & get_namespace(environment const & env) { diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 63afed10ef..3b443e01e1 100644 --- a/src/library/scoped_ext.h +++ b/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()); + m_ext_id = environment::register_extension(new scoped_ext()); } ~reg() { modification::finalize(); @@ -174,7 +174,7 @@ public: return static_cast(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(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()); diff --git a/src/util/object_ref.h b/src/util/object_ref.h index 530011220a..40d4c9c3dc 100644 --- a/src/util/object_ref.h +++ b/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); } };