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

feat(library/vm): add get_vm_decl

Browse source
This commit is contained in:
Leonardo de Moura 2016-05-11 17:42:14 -07:00
parent 61471df3eb
commit 7a4ed85fee
2 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/vm.cpp
View file

@ -491,6 +491,14 @@ environment optimize_vm_decls(environment const & env) {
}
}
optional<vm_decl> get_vm_decl(environment const & env, name const & n) {
vm_decls const & ext = get_extension(env);
if (auto idx = ext.m_name2idx.find(n))
return optional<vm_decl>(ext.m_decls[*idx]);
else
return optional<vm_decl>();
}
vm_state::vm_state(environment const & env):
m_env(optimize_vm_decls(env)),
m_decls(get_extension(m_env).m_decls.as_vector_if_compressed()),

2
src/library/vm.h
View file

@ -424,6 +424,8 @@ bool is_vm_function(environment const & env, name const & fn);
/** \brief Return true iff \c fn is implemented in C++. */
bool is_vm_builtin_function(name const & fn);
optional<vm_decl> get_vm_decl(environment const & env, name const & n);
void display_vm_code(std::ostream & out, environment const & env, unsigned code_sz, vm_instr const * code);
void initialize_vm();