From aa138fe68684aa6b7f700e56d34705a9995f296b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 16 May 2019 14:42:02 -0700 Subject: [PATCH] chore(*): `get_obj_arg` => `to_obj_arg` --- src/frontends/lean/lean_elaborator.cpp | 2 +- src/kernel/environment.cpp | 18 +++++++++--------- src/library/compiler/closed_term_cache.cpp | 4 ++-- src/library/module.cpp | 4 ++-- src/library/protected.cpp | 4 ++-- src/shell/lean.cpp | 2 +- src/util/object_ref.h | 2 +- src/util/options.h | 2 ++ 8 files changed, 20 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index c631248a7b..1344194c9b 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -511,7 +511,7 @@ extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_ } object * args[] = { - p.env().get_obj_arg(), + p.env().to_obj_arg(), to_obj(s->m_ngen).steal(), vm_lds.steal(), vm_eds.steal(), diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 0eedf88459..86d8b7822c 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -42,11 +42,11 @@ environment::environment(unsigned trust_lvl): } unsigned environment::trust_lvl() const { - return environment_trust_level_core(get_obj_arg()); + return environment_trust_level_core(to_obj_arg()); } bool environment::is_quot_initialized() const { - return environment_quot_init_core(get_obj_arg()) != 0; + return environment_quot_init_core(to_obj_arg()) != 0; } void environment::mark_quot_initialized() { @@ -54,11 +54,11 @@ void environment::mark_quot_initialized() { } optional environment::find(name const & n) const { - return to_optional(environment_find_core(get_obj_arg(), n.get_obj_arg())); + return to_optional(environment_find_core(to_obj_arg(), n.to_obj_arg())); } constant_info environment::get(name const & n) const { - object * o = environment_find_core(get_obj_arg(), n.get_obj_arg()); + object * o = environment_find_core(to_obj_arg(), n.to_obj_arg()); if (is_scalar(o)) throw unknown_constant_exception(*this, n); constant_info r(cnstr_get(o, 0), true); @@ -120,11 +120,11 @@ static void check_constant_val(environment const & env, constant_val const & v, } void environment::add_core(constant_info const & info) { - m_obj = environment_add_core(m_obj, info.get_obj_arg()); + m_obj = environment_add_core(m_obj, info.to_obj_arg()); } environment environment::add(constant_info const & info) const { - return environment(environment_add_core(get_obj_arg(), info.get_obj_arg())); + return environment(environment_add_core(to_obj_arg(), info.to_obj_arg())); } environment environment::add_axiom(declaration const & d, bool check) const { @@ -268,7 +268,7 @@ unsigned environment::register_extension(environment_extension * initial) { } environment_extension const & environment::get_extension(unsigned id) const { - object * r = get_extension_core(get_obj_arg(), box(id)); + object * r = get_extension_core(to_obj_arg(), box(id)); if (is_scalar(r)) { throw exception("invalid extension id"); } object * ext = cnstr_get(r, 0); dec(r); @@ -276,7 +276,7 @@ environment_extension const & environment::get_extension(unsigned id) const { } environment environment::update(unsigned id, environment_extension * ext) const { - object * r = set_extension_core(get_obj_arg(), box(id), to_object(ext)); + object * r = set_extension_core(to_obj_arg(), box(id), to_object(ext)); if (is_scalar(r)) { throw exception("invalid extension id"); } environment env(cnstr_get(r, 0), true); dec(r); @@ -293,7 +293,7 @@ void environment::for_each_constant(std::function obj_res display_stats_core(obj_arg env, obj_arg w); void environment::display_stats() const { - dec_ref(display_stats_core(get_obj_arg(), io_mk_world())); + dec_ref(display_stats_core(to_obj_arg(), io_mk_world())); } void initialize_environment() { diff --git a/src/library/compiler/closed_term_cache.cpp b/src/library/compiler/closed_term_cache.cpp index 06fa51ce2a..b6381d8b23 100644 --- a/src/library/compiler/closed_term_cache.cpp +++ b/src/library/compiler/closed_term_cache.cpp @@ -19,10 +19,10 @@ object * cache_closed_term_name_core(object * env, object * e, object * n); object * get_closed_term_name_core(object * env, object * e); optional get_closed_term_name(environment const & env, expr const & e) { - return to_optional(get_closed_term_name_core(env.get_obj_arg(), e.get_obj_arg())); + return to_optional(get_closed_term_name_core(env.to_obj_arg(), e.to_obj_arg())); } environment cache_closed_term_name(environment const & env, expr const & e, name const & n) { - return environment(cache_closed_term_name_core(env.get_obj_arg(), e.get_obj_arg(), n.get_obj_arg())); + return environment(cache_closed_term_name_core(env.to_obj_arg(), e.to_obj_arg(), n.to_obj_arg())); } } diff --git a/src/library/module.cpp b/src/library/module.cpp index 5e252c445a..66a65feb07 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -204,7 +204,7 @@ def writeModule (env : Environment) (fname : String) : IO Unit := */ object * write_module_core(object * env, object * fname, object * w); void write_module(environment const & env, std::string const & olean_fn) { - object * r = write_module_core(env.get_obj_arg(), mk_string(olean_fn), io_mk_world()); + object * r = write_module_core(env.to_obj_arg(), mk_string(olean_fn), io_mk_world()); if (io_result_is_error(r)) { dec_ref(r); throw exception(sstream() << "failed to write module '" << olean_fn << "'"); @@ -237,7 +237,7 @@ object * environment_add_modification_core(object * env, object * mod); namespace module { environment add(environment const & env, modification* modf) { - return environment(environment_add_modification_core(env.get_obj_arg(), to_object(modf))); + return environment(environment_add_modification_core(env.to_obj_arg(), to_object(modf))); } environment add_and_perform(environment const & env, modification * modf) { diff --git a/src/library/protected.cpp b/src/library/protected.cpp index cc913778e8..53758f782e 100644 --- a/src/library/protected.cpp +++ b/src/library/protected.cpp @@ -15,11 +15,11 @@ object * add_protected_core(object * env, object * n); uint8 is_protected_core(object * env, object * n); environment add_protected(environment const & env, name const & n) { - return environment(add_protected_core(env.get_obj_arg(), n.get_obj_arg())); + return environment(add_protected_core(env.to_obj_arg(), n.to_obj_arg())); } bool is_protected(environment const & env, name const & n) { - return is_protected_core(env.get_obj_arg(), n.get_obj_arg()); + return is_protected_core(env.to_obj_arg(), n.to_obj_arg()); } name get_protected_shortest_name(name const & n) { diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 3db2573c7b..01312fa34a 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -512,7 +512,7 @@ int main(int argc, char ** argv) { scope_message_log scope_log(l); // res : estate.result io.error io.world (prod (list syntax) environment) object_ref res { lean_process_file(mk_string(mod_fn), mk_string(contents), static_cast(json_output), - env.get_obj_arg(), io_mk_world()) }; + env.to_obj_arg(), io_mk_world()) }; if (io_result_is_error(res.raw())) { // estate.result.error _ ok = false; diff --git a/src/util/object_ref.h b/src/util/object_ref.h index 2afa125aa5..8916cccdd6 100644 --- a/src/util/object_ref.h +++ b/src/util/object_ref.h @@ -36,7 +36,7 @@ public: } object * raw() const { return m_obj; } object * steal() { object * r = m_obj; m_obj = box(0); return r; } - object * get_obj_arg() const { inc(m_obj); return m_obj; } + object * to_obj_arg() const { inc(m_obj); return m_obj; } static void swap(object_ref & a, object_ref & b) { std::swap(a.m_obj, b.m_obj); } }; diff --git a/src/util/options.h b/src/util/options.h index 2718748c3d..5ae29b34b7 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -66,6 +66,8 @@ public: opts2 overrides the ones in opts1. */ friend options join(options const & opts1, options const & opts2); + + object * to_obj_arg() const { return m_value.to_obj_arg(); } }; bool get_verbose(options const & opts);