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

fix(library/metavar_context): incorrect assertions

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-25 19:11:01 -07:00
parent c4953cac43
commit b53e50c968
2 changed files with 4 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/metavar_context.cpp
View file

@ -53,26 +53,12 @@ optional<local_decl> metavar_context::get_hypothesis_of(expr const & mvar, name
return mdecl->get_context().get_local_decl(H);
}
void metavar_context::assign_core(level const & u, level const & l) {
void metavar_context::assign(level const & u, level const & l) {
m_uassignment.insert(meta_id(u), l);
}
void metavar_context::assign(level const & u, level const & l) {
lean_assert(!is_assigned(u));
assign_core(u, l);
}
void metavar_context::assign_core(expr const & e, expr const & v) {
m_eassignment.insert(mlocal_name(e), v);
}
void metavar_context::assign(expr const & e, expr const & v) {
// TODO(leo, dhs): confirm that we do not need this assertion
// Note: it triggers an assertion failure from
// https://github.com/leanprover/lean/blob/lean3/src/library/metavar_util.h#L127-L135
// when CTX is a type_context.
// lean_assert(!is_assigned(e));
assign_core(e, v);
m_eassignment.insert(mlocal_name(e), v);
}
optional<level> metavar_context::get_assignment(level const & l) const {
@ -98,12 +84,12 @@ struct metavar_context::interface_impl {
static bool is_mvar(level const & l) { return is_metavar_decl_ref(l); }
bool is_assigned(level const & l) const { return m_ctx.is_assigned(l); }
optional<level> get_assignment(level const & l) const { return m_ctx.get_assignment(l); }
void assign(level const & u, level const & v) { m_ctx.assign_core(u, v); }
void assign(level const & u, level const & v) { m_ctx.assign(u, v); }
static bool is_mvar(expr const & e) { return is_metavar_decl_ref(e); }
bool is_assigned(expr const & e) const { return m_ctx.is_assigned(e); }
optional<expr> get_assignment(expr const & e) const { return m_ctx.get_assignment(e); }
void assign(expr const & m, expr const & v) { m_ctx.assign_core(m, v); }
void assign(expr const & m, expr const & v) { m_ctx.assign(m, v); }
};

2
src/library/metavar_context.h
View file

@ -27,8 +27,6 @@ class metavar_context {
name_map<level> m_uassignment;
name_map<expr> m_eassignment;
struct interface_impl;
void assign_core(level const & u, level const & l);
void assign_core(expr const & e, expr const & v);
friend struct interface_impl;
public:
level mk_univ_metavar_decl();