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

feat(library/type_context): add set_env

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-23 18:31:30 -07:00
parent a93eada058
commit 55bd3e223e
3 changed files with 15 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1312,6 +1312,7 @@ expr elaborator::visit_equations(expr const & e) {
new_e = instantiate_mvars(new_e);
metavar_context mctx = m_ctx.mctx();
expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e);
m_ctx.set_env(m_env);
m_ctx.set_mctx(mctx);
return r;
}
@ -1658,6 +1659,7 @@ void elaborator::invoke_tactic(expr const & mvar, expr const & tactic) {
}
mctx.assign(mvar, val);
m_env = new_s->env();
m_ctx.set_env(m_env);
m_ctx.set_mctx(mctx);
} else if (optional<pair<format, tactic_state>> ex = is_tactic_exception(S, m_opts, r)) {
throw_unsolved_tactic_state(ex->second, ex->first, ref);

10
src/library/type_context.cpp
View file

@ -217,6 +217,16 @@ type_context::~type_context() {
m_cache_manager->recycle(m_cache);
}
void type_context::set_env(environment const & env) {
options o = m_cache->m_options;
if (m_cache_manager) {
m_cache_manager->recycle(m_cache);
m_cache = m_cache_manager->mk(env, o);
} else {
m_cache = mk_cache(env, o, false);
}
}
expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {
return m_lctx.mk_local_decl(pp_name, type, bi);
}

4
src/library/type_context.h
View file

@ -235,8 +235,10 @@ public:
expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); }
/* note: mctx must be a descendent of m_mctx */
/* note: mctx must be a descendant of m_mctx */
void set_mctx(metavar_context const & mctx) { m_mctx = mctx; }
/* note: env must be a descendant of m_env */
void set_env(environment const & env);
bool is_def_eq_core(level const & l1, level const & l2);
bool is_def_eq(level const & l1, level const & l2);