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

feat(library/vm/vm): add scope_vm_state

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-15 15:10:04 -04:00
parent fd068344a6
commit a30603405c
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1004,6 +1004,15 @@ void vm_state::invoke_builtin(vm_decl const & d) {
LEAN_THREAD_VALUE(vm_state *, g_vm_state, nullptr);
scope_vm_state::scope_vm_state(vm_state & s):
m_prev(g_vm_state) {
g_vm_state = &s;
}
scope_vm_state::~scope_vm_state() {
g_vm_state = m_prev;
}
void vm_state::invoke_cfun(vm_decl const & d) {
flet<vm_state *> Set(g_vm_state, this);
auto & S = m_stack;

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

@ -583,6 +583,14 @@ public:
}
};
/** \brief Helper class for setting thread local vm_state object */
class scope_vm_state {
vm_state * m_prev;
public:
scope_vm_state(vm_state & s);
~scope_vm_state();
};
/** \brief Return reference to thread local VM state object. */
vm_state const & get_vm_state();