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

feat(library/tactic/tactic_state): add get_tactic_vm_state

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-24 15:56:19 -07:00
parent d604cb8b4e
commit 72606479ec
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/tactic/tactic_state.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "library/pp_options.h"
#include "library/trace.h"
#include "library/util.h"
#include "library/cache_helper.h"
#include "library/vm/vm_environment.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_format.h"
@ -460,6 +461,13 @@ vm_obj tactic_mk_fresh_name(vm_obj const & s) {
return mk_tactic_success(to_obj(mk_fresh_name()), to_tactic_state(s));
}
typedef transparencyless_cache_compatibility_helper<vm_state> vm_state_cache_helper;
MK_THREAD_LOCAL_GET_DEF(vm_state_cache_helper, get_vmsc);
vm_state & get_tactic_vm_state(environment const & env) {
return get_vmsc().get_cache_for(env);
}
void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic_state", "env"}), tactic_state_env);
DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);

2
src/library/tactic/tactic_state.h
View file

@ -138,6 +138,8 @@ struct type_context_scope {
#define LEAN_TACTIC_TRY try {
#define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); }
vm_state & get_tactic_vm_state(environment const & env);
void initialize_tactic_state();
void finalize_tactic_state();
}