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

perf(library/compiler/nat_value): replace all numerals with nat_value_macro

Browse source 
Reason: Later we try to type check the compiler intermediate results.
If only some of the numerals are converted, we may spend a lot of time
making sure the two different representations are equivalent.
This commit is contained in:
Leonardo de Moura 2016-09-04 16:42:40 -07:00
parent f7df7dc9a7
commit 0b2c3659cf
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/compiler/nat_value.cpp
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/num.h"
#include "library/kernel_serializer.h"
#include "library/compiler/compiler_step_visitor.h"
#include "library/replace_visitor_with_tc.h"
namespace lean {
static expr * g_nat = nullptr;
@ -92,18 +92,19 @@ optional<expr> to_nat_value(type_context & ctx, expr const & e) {
return none_expr();
}
class find_nat_values_fn : public compiler_step_visitor {
class find_nat_values_fn : public replace_visitor_with_tc {
expr visit_app(expr const & e) override {
if (auto v = to_nat_value(ctx(), e))
if (auto v = to_nat_value(m_ctx, e))
return *v;
return compiler_step_visitor::visit_app(e);
return replace_visitor_with_tc::visit_app(e);
}
public:
find_nat_values_fn(environment const & env):compiler_step_visitor(env) {}
find_nat_values_fn(type_context & ctx):replace_visitor_with_tc(ctx) {}
};
expr find_nat_values(environment const & env, expr const & e) {
return find_nat_values_fn(env)(e);
type_context ctx(env, transparency_mode::All);
return find_nat_values_fn(ctx)(e);
}
void initialize_nat_value() {