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

fix(library/type_context): allow assigned regular meta-variables to be "read" in tmp-mode

Browse source 
This commit also removes a "hack" that tried to fix this problem for
universe meta-variables only. Moreover, the hack was incomplete, since
it would not consider nested metavars.
This commit is contained in:
Leonardo de Moura 2016-10-21 13:32:27 -07:00
parent a9fe684f26
commit fa3475fa66
5 changed files with 26 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/metavar_context.cpp
View file

@ -98,12 +98,12 @@ struct metavar_context::interface_impl {
metavar_context & m_ctx;
interface_impl(metavar_context const & ctx):m_ctx(const_cast<metavar_context&>(ctx)) {}
static bool is_mvar(level const & l) { return is_metavar_decl_ref(l); }
static bool is_mvar_core(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(u, v); }
static bool is_mvar(expr const & e) { return is_metavar_decl_ref(e); }
static bool is_mvar_core(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(m, v); }

14
src/library/metavar_util.h
View file

@ -14,12 +14,12 @@ Helper functions for metavariable assignments.
The template parameter CTX must be an object that
provides the following API:
bool is_mvar(level const & l) const;
bool is_mvar_core(level const & l) const;
bool is_assigned(level const & l) const;
optional<level> get_assignment(level const & l) const;
void assign(level const & u, level const & v);
bool is_mvar(expr const & e) const;
bool is_mvar_core(expr const & e) const;
bool is_assigned(expr const & e) const;
optional<expr> get_assignment(expr const & e) const;
void assign(expr const & m, expr const & v);
@ -35,7 +35,7 @@ bool has_assigned(CTX const & ctx, level const & l) {
return false; // stop search
if (found)
return false; // stop search
if (ctx.is_mvar(l) && ctx.is_assigned(l)) {
if (ctx.is_mvar_core(l) && ctx.is_assigned(l)) {
found = true;
return false; // stop search
}
@ -63,7 +63,7 @@ bool has_assigned(CTX const & ctx, expr const & e) {
return false; // stop search
if (found)
return false; // stop search
if ((ctx.is_mvar(e) && ctx.is_assigned(e)) ||
if ((ctx.is_mvar_core(e) && ctx.is_assigned(e)) ||
(is_constant(e) && has_assigned(ctx, const_levels(e))) ||
(is_sort(e) && has_assigned(ctx, sort_level(e)))) {
found = true;
@ -83,7 +83,7 @@ level instantiate_mvars(CTX & ctx, level const & l) {
return replace(l, [&](level const & l) {
if (!has_meta(l)) {
return some_level(l);
} else if (ctx.is_mvar(l)) {
} else if (ctx.is_mvar_core(l)) {
if (auto v1 = ctx.get_assignment(l)) {
level v2 = instantiate_mvars(ctx, *v1);
if (*v1 != v2) {
@ -125,7 +125,7 @@ class instantiate_mvars_fn : public replace_visitor {
}
virtual expr visit_meta(expr const & m) override {
if (m_ctx.is_mvar(m)) {
if (m_ctx.is_mvar_core(m)) {
if (auto v1 = m_ctx.get_assignment(m)) {
if (!has_metavar(*v1)) {
return *v1;
@ -146,7 +146,7 @@ class instantiate_mvars_fn : public replace_visitor {
virtual expr visit_app(expr const & e) override {
buffer<expr> args;
expr const & f = get_app_rev_args(e, args);
if (m_ctx.is_mvar(f)) {
if (m_ctx.is_mvar_core(f)) {
if (auto v = m_ctx.get_assignment(f)) {
expr new_app = apply_beta(*v, args.size(), args.data());
if (has_metavar(new_app))

35
src/library/type_context.cpp
View file

@ -1114,6 +1114,13 @@ void type_context::clear_tmp_eassignment() {
/* -----------------------------------
Uniform interface to temporary & regular metavariables
----------------------------------- */
bool type_context::is_mvar_core(level const & l) const {
return (in_tmp_mode() && is_idx_metauniv(l)) || is_metavar_decl_ref(l);
}
bool type_context::is_mvar_core(expr const & e) const {
return (in_tmp_mode() && is_idx_metavar(e)) || is_metavar_decl_ref(e);
}
bool type_context::is_mvar(level const & l) const {
if (in_tmp_mode())
@ -1131,7 +1138,7 @@ bool type_context::is_mvar(expr const & e) const {
bool type_context::is_assigned(level const & l) const {
const_cast<type_context*>(this)->m_used_assignment = true;
if (in_tmp_mode())
if (in_tmp_mode() && is_idx_metauniv(l))
return static_cast<bool>(get_tmp_assignment(l));
else
return m_mctx.is_assigned(l);
@ -1139,7 +1146,7 @@ bool type_context::is_assigned(level const & l) const {
bool type_context::is_assigned(expr const & e) const {
const_cast<type_context*>(this)->m_used_assignment = true;
if (in_tmp_mode())
if (in_tmp_mode() && is_idx_metavar(e))
return static_cast<bool>(get_tmp_assignment(e));
else
return m_mctx.is_assigned(e);
@ -1147,7 +1154,7 @@ bool type_context::is_assigned(expr const & e) const {
optional<level> type_context::get_assignment(level const & l) const {
const_cast<type_context*>(this)->m_used_assignment = true;
if (in_tmp_mode())
if (in_tmp_mode() && is_idx_metauniv(l))
return get_tmp_assignment(l);
else
return m_mctx.get_assignment(l);
@ -1155,7 +1162,7 @@ optional<level> type_context::get_assignment(level const & l) const {
optional<expr> type_context::get_assignment(expr const & e) const {
const_cast<type_context*>(this)->m_used_assignment = true;
if (in_tmp_mode())
if (in_tmp_mode() && is_idx_metavar(e))
return get_tmp_assignment(e);
else
return m_mctx.get_assignment(e);
@ -1163,7 +1170,7 @@ optional<expr> type_context::get_assignment(expr const & e) const {
void type_context::assign(level const & u, level const & l) {
m_used_assignment = true;
if (in_tmp_mode())
if (in_tmp_mode() && is_idx_metauniv(u))
assign_tmp(u, l);
else
m_mctx.assign(u, l);
@ -1171,7 +1178,7 @@ void type_context::assign(level const & u, level const & l) {
void type_context::assign(expr const & m, expr const & v) {
m_used_assignment = true;
if (in_tmp_mode())
if (in_tmp_mode() && is_idx_metavar(m))
assign_tmp(m, v);
else
m_mctx.assign(m, v);
@ -1243,22 +1250,6 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
flet<unsigned> inc_depth(m_is_def_eq_depth, m_is_def_eq_depth+1);
if (in_tmp_mode()) {
/* TODO(Leo): we should instantiate any assigned regular metavariable
when we are in tmp_mode. */
if (is_metavar_decl_ref(l1)) {
/* Check if l1 is regular metavar that is already assigned */
if (auto v1 = m_mctx.get_assignment(l1))
return is_def_eq_core(*v1, l2, partial);
}
if (is_metavar_decl_ref(l2)) {
/* Check if l2 is regular metavar that is already assigned */
if (auto v2 = m_mctx.get_assignment(l2))
return is_def_eq_core(l1, *v2, partial);
}
}
level new_l1 = instantiate_mvars(l1);
level new_l2 = instantiate_mvars(l2);

2
src/library/type_context.h
View file

@ -476,6 +476,8 @@ private:
and in regular mode they access m_mctx.
------------ */
public:
bool is_mvar_core(level const & l) const;
bool is_mvar_core(expr const & e) const;
bool is_mvar(level const & l) const;
bool is_mvar(expr const & e) const;
bool is_assigned(level const & l) const;

2
tests/lean/run/mixed_tmp_non_tmp_universe_bug.lean Normal file
View file

@ -0,0 +1,2 @@
eval default (bool × unit × nat)
eval default (bool × bool × bool × bool)