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

fix: don't try to interpret [builtinInit] constants

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-21 10:30:23 +02:00
parent 64fc4897c3
commit 86fe95898d
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/compiler/ir_interpreter.cpp
View file

@ -207,6 +207,16 @@ static bool type_is_scalar(type t) {
return t != type::Object && t != type::TObject && t != type::Irrelevant;
}
extern "C" object* lean_get_regular_init_fn_name_for(object* env, object* fn);
optional<name> get_regular_init_fn_name_for(environment const & env, name const & n) {
return to_optional<name>(lean_get_regular_init_fn_name_for(env.to_obj_arg(), n.to_obj_arg()));
}
extern "C" object* lean_get_builtin_init_fn_name_for(object* env, object* fn);
optional<name> get_builtin_init_fn_name_for(environment const & env, name const & n) {
return to_optional<name>(lean_get_builtin_init_fn_name_for(env.to_obj_arg(), n.to_obj_arg()));
}
/** \brief Value stored in an interpreter variable slot */
union value {
// NOTE: the IR type system guarantees that we always access the active union member
@ -695,7 +705,7 @@ class interpreter {
return *e;
} else {
symbol_cache_entry e_new { get_decl(fn), nullptr, false };
if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern) {
if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || get_builtin_init_fn_name_for(m_env, fn)) {
string_ref mangled = name_mangle(fn, *g_mangle_prefix);
string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
// check for boxed version first