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

fix(library/type_context): type_context was not checking if to_revert dependencies were frozen

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-23 11:59:18 -08:00
parent 24e7a5a339
commit 6c3d90e20e
3 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/library/type_context.cpp
View file

@ -278,16 +278,6 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
unsigned num = to_revert.size();
if (num == 0)
return mk_pair(ctx, type);
/* Check whether we are trying to revert a frozen local instance. */
if (optional<local_instances> lis = m_lctx.get_frozen_local_instances()) {
for (expr const & h : to_revert) {
for (local_instance const & li : *lis) {
if (mlocal_name(h) == mlocal_name(li.get_local())) {
throw exception(sstream() << "failed to revert '" << h << "', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)");
}
}
}
}
local_decl d0 = get_local_with_smallest_idx(ctx, to_revert);
bool must_sort = false;
process_to_revert(m_mctx, to_revert, num, d0, preserve_to_revert_order, must_sort);
@ -327,6 +317,16 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
return ctx.get_local_decl(l1).get_idx() < ctx.get_local_decl(l2).get_idx();
});
}
/* Check whether we are trying to revert a frozen local instance. */
if (optional<local_instances> lis = m_lctx.get_frozen_local_instances()) {
for (expr const & h : to_revert) {
for (local_instance const & li : *lis) {
if (mlocal_name(h) == mlocal_name(li.get_local())) {
throw exception(sstream() << "failed to revert '" << h << "', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)");
}
}
}
}
local_context new_ctx = ctx.remove(to_revert);
return mk_pair(new_ctx, mk_pi(ctx, to_revert, type));
}

4
tests/lean/revert_frozen_dep.lean Normal file
View file

@ -0,0 +1,4 @@
lemma ex {α : id Type} [has_add α] : true :=
begin
dsimp at α -- should fail because the frozen instance `[has_add α]` depends on `α`
end

1
tests/lean/revert_frozen_dep.lean.expected.out Normal file
View file

@ -0,0 +1 @@
revert_frozen_dep.lean:4:0: error: failed to revert '_inst_1', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)