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

feat(library/vm/interaction_state): capture tactic profile data if enabled

Browse source
This commit is contained in:
Sebastian Ullrich 2017-04-11 13:31:48 +02:00 • committed by Leonardo de Moura
parent 4483e53de0
commit 17204f9629
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/vm/interaction_state.h
View file

@ -26,6 +26,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
#include "library/scoped_ext.h"
#include "library/aux_definition.h"
#include "library/unfold_macros.h"
#include "library/message_builder.h"
#include "library/vm/vm.h"
#include "library/vm/vm_environment.h"
#include "library/vm/vm_exceptional.h"
@ -235,7 +236,17 @@ struct interaction_monad {
name interaction_name("_interaction");
environment new_env = compile(interaction_name, interaction);
vm_state S(new_env, m_opts);
vm_state::profiler prof(S, m_opts);
vm_obj r = invoke(S, interaction_name, {to_obj(s)});
if (prof.enabled()) {
auto out = message_builder(environment(), get_global_ios(),
get_pos_info_provider()->get_file_name(),
get_pos_info_provider()->get_pos_info_or_some(interaction),
INFORMATION);
out.set_caption("tactic profile data");
prof.get_snapshots().display(out.get_text_stream().get_stream());
out.report();
}
if (!is_success(r))
process_failure(S, r);