max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(*): get_obj_arg => to_obj_arg

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-16 14:42:02 -07:00
parent 9d9f546ad8
commit aa138fe686
8 changed files with 20 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/lean_elaborator.cpp
View file

@ -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(),

18
src/kernel/environment.cpp
View file

@ -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<constant_info> environment::find(name const & n) const {
return to_optional<constant_info>(environment_find_core(get_obj_arg(), n.get_obj_arg()));
return to_optional<constant_info>(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<void(constant_info const & d)>
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() {

4
src/library/compiler/closed_term_cache.cpp
View file

@ -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<name> get_closed_term_name(environment const & env, expr const & e) {
return to_optional<name>(get_closed_term_name_core(env.get_obj_arg(), e.get_obj_arg()));
return to_optional<name>(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()));
}
}

4
src/library/module.cpp
View file

@ -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) {

4
src/library/protected.cpp
View file

@ -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) {

2
src/shell/lean.cpp
View file

@ -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<uint8>(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;

2
src/util/object_ref.h
View file

@ -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); }
};

2
src/util/options.h
View file

@ -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);