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

perf(library/vm/vm): make sure builtin cases_on recursors are assigned ids first

Browse source 
This will minimize the size of the m_builtin_cases_vector.
It also indirectly prevents the crash decribed at 144d9096e2.
However, the fix used there is more robust.
This commit is contained in:
Leonardo de Moura 2016-12-22 18:46:51 -08:00
parent 144d9096e2
commit 94e6fbcbbf
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/vm/vm.cpp
View file

@ -900,16 +900,16 @@ struct vm_decls : public environment_extension {
name m_monitor;
vm_decls() {
g_vm_cases_builtins->for_each([&](name const & n, std::tuple<char const *, vm_cases_function> const & p) {
unsigned idx = get_vm_index(n);
m_cases.insert(idx, std::get<1>(p));
});
g_vm_builtins->for_each([&](name const & n, std::tuple<unsigned, char const *, vm_function> const & p) {
add_core(vm_decl(n, get_vm_index(n), std::get<0>(p), std::get<2>(p)));
});
g_vm_cbuiltins->for_each([&](name const & n, std::tuple<unsigned, char const *, vm_cfunction> const & p) {
add_core(vm_decl(n, get_vm_index(n), std::get<0>(p), std::get<2>(p)));
});
g_vm_cases_builtins->for_each([&](name const & n, std::tuple<char const *, vm_cases_function> const & p) {
unsigned idx = get_vm_index(n);
m_cases.insert(idx, std::get<1>(p));
});
}
void add_core(vm_decl const & d) {