michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontend/lean): minor modification to be able to execute lean frontend while refactoring elaborator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-01 17:41:03 -07:00
parent 7cf83800c0
commit 61ccaf741c
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/elaborator.cpp
View file

@ -59,8 +59,10 @@ expr elaborator::operator()(expr const & e, expr const & /* expected_type */) {
expr const & elaborator::get_original(expr const & e) const { return e; }
void elaborator::set_interrupt(bool ) {}
void elaborator::clear() {}
environment g_env;
environment const & elaborator::get_environment() const { return g_env; }
environment const & elaborator::get_environment() const {
static thread_local environment g_env;
return g_env;
}
void elaborator::display(std::ostream & ) const {}
format elaborator::pp(formatter &, options const &) const { return format(); }
void elaborator::print(imp * ptr) { lean_assert(ptr); }

2
src/kernel/level.cpp
View file

@ -57,7 +57,7 @@ void level_cell::dealloc() {
}
}
static name g_bot_name("bot");
level::level(): m_ptr(new level_uvar(g_bot_name)) { lean_assert(uvar_name(*this) == name("bot")); }
level::level(): m_ptr(new level_uvar(g_bot_name)) { lean_assert_eq(uvar_name(*this), name("bot")); }
level::level(name const & n): m_ptr(new level_uvar(n)) {}
level::level(level const & l, unsigned k):m_ptr(new level_lift(l, k)) { lean_assert(is_uvar(l)); }
level::level(level_cell * ptr): m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); }