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

feat(library/compiler/vm_compiler): improve local_info collection

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-09 12:18:44 -08:00
parent a3aced1b30
commit b79b76db83
2 changed files with 17 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/library/compiler/vm_compiler.cpp
View file

@ -13,12 +13,14 @@ Author: Leonardo de Moura
#include "library/annotation.h"
#include "library/util.h"
#include "library/quote.h"
#include "library/replace_visitor.h"
#include "library/vm/vm.h"
#include "library/vm/optimize.h"
#include "library/compiler/simp_inductive.h"
#include "library/compiler/erase_irrelevant.h"
#include "library/compiler/nat_value.h"
#include "library/compiler/preprocess.h"
#include "library/compiler/comp_irrelevant.h"
namespace lean {
class vm_compiler_fn {
@ -235,11 +237,21 @@ class vm_compiler_fn {
}
}
class elim_comp_irrelevant_marks_fn : public replace_visitor {
virtual expr visit_macro(expr const & e) override {
if (is_marked_as_comp_irrelevant(e))
return visit(get_annotation_arg(e));
else
return replace_visitor::visit_macro(e);
}
};
optional<expr> to_type_info(expr const & t) {
if (!is_neutral_expr(t) && closed(t))
return some_expr(t);
else
if (!is_neutral_expr(t) && closed(t) && !has_param_univ(t)) {
return some_expr(elim_comp_irrelevant_marks_fn()(t));
} else {
return none_expr();
}
}
void compile_let(expr e, unsigned bpz, name_map<unsigned> const & m) {

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

@ -1758,6 +1758,7 @@ unsigned vm_state::pop_frame() {
void vm_state::invoke_global(vm_decl const & d) {
#if 0
std::cout << d.get_name() << "\n";
for (auto info : d.get_args_info()) {
std::cout << info.first << " : ";
if (info.second)
@ -1766,6 +1767,7 @@ void vm_state::invoke_global(vm_decl const & d) {
std::cout << "none";
std::cout << "\n";
}
std::cout << "----------\n";
#endif
push_frame(d.get_arity(), m_pc+1, d.get_idx());
m_code = d.get_code();