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

feat(library/type_context): m_update => m_update_left/m_update_right

Browse source
This commit is contained in:
Leonardo de Moura 2018-01-03 13:46:31 -08:00
parent e9650d835d
commit 22270d37cf
5 changed files with 80 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/simplify.cpp
View file

@ -537,7 +537,7 @@ simp_result simplify_core_fn::rewrite(expr const & e) {
}
bool simplify_core_fn::match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t) {
return ctx.is_def_eq(sl.get_lhs(), t);
return ctx.match(sl.get_lhs(), t);
}
/* If both e and sl.get_lhs() are of the form (f ...),

4
src/library/tactic/smt/congruence_closure.h
View file

@ -285,11 +285,11 @@ public:
bool proved(expr const & e) const;
bool is_def_eq(expr const & e1, expr const & e2) const {
return m_ctx.nd_is_def_eq(e1, e2);
return m_ctx.pure_is_def_eq(e1, e2);
}
bool relaxed_is_def_eq(expr const & e1, expr const & e2) const {
return m_ctx.nd_relaxed_is_def_eq(e1, e2);
return m_ctx.pure_relaxed_is_def_eq(e1, e2);
}
expr get_root(expr const & e) const { return m_state.get_root(e); }

2
src/library/tactic/smt/theory_ac.cpp
View file

@ -145,7 +145,7 @@ optional<expr> theory_ac::is_ac(expr const & e) {
return some_expr(*it);
optional<expr> found_op;
m_state.m_op_info.for_each([&](expr const & c_op, expr_pair const &) {
if (!found_op && m_ctx.nd_relaxed_is_def_eq(op, c_op))
if (!found_op && m_ctx.pure_relaxed_is_def_eq(op, c_op))
found_op = c_op;
});
if (found_op) {

48
src/library/type_context.cpp
View file

@ -1567,7 +1567,7 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
if (l1 != new_l1 || l2 != new_l2)
return is_def_eq_core(new_l1, new_l2, partial);
if (m_update && is_mode_mvar(l1)) {
if (m_update_left && is_mode_mvar(l1)) {
lean_assert(!is_assigned(l1));
if (!occurs(l1, l2)) {
assign(l1, l2);
@ -1577,7 +1577,7 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
}
}
if (m_update && is_mode_mvar(l2)) {
if (m_update_right && is_mode_mvar(l2)) {
lean_assert(!is_assigned(l2));
if (!occurs(l2, l1)) {
assign(l2, l1);
@ -1872,7 +1872,7 @@ bool type_context::process_assignment(expr const & m, expr const & v) {
if (is_local_decl_ref(arg) && (is_local(fn) || is_constant(fn))) {
return
is_def_eq_core(mvar, app_fn(v)) &&
is_def_eq_core(app_arg(v), args[0]);
is_def_eq_core(args[0], app_arg(v));
}
}
@ -2265,7 +2265,7 @@ bool type_context::is_def_eq_binding(expr e1, expr e2) {
if (binding_domain(e1) != binding_domain(e2)) {
var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data());
expr var_e2_type = instantiate_rev(binding_domain(e2), subst.size(), subst.data());
if (!is_def_eq_core(var_e2_type, *var_e1_type))
if (!is_def_eq_core(*var_e1_type, var_e2_type))
return false;
}
if (!closed(binding_body(e1)) || !closed(binding_body(e2))) {
@ -2595,11 +2595,11 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
if (is_mode_mvar(f1)) {
lean_assert(!is_assigned(f1));
if (m_update && !is_mode_mvar(f2)) {
if (m_update_left && !is_mode_mvar(f2)) {
return to_lbool(process_assignment(e1, e2));
} else if (m_update && in_tmp_mode()) {
} else if (m_update_left && in_tmp_mode()) {
return to_lbool(process_assignment(e1, e2));
} else if (m_update) {
} else if (m_update_left) {
optional<metavar_decl> m1_decl = m_mctx.find_metavar_decl(f1);
optional<metavar_decl> m2_decl = m_mctx.find_metavar_decl(f2);
if (m1_decl && m2_decl) {
@ -2620,11 +2620,13 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
return to_lbool(process_assignment(e1, e2));
} else if (m1_decl->get_context().is_subset_of(m2_decl->get_context())) {
lean_assert(is_app(e1) || !is_app(e2));
if ((is_app(e1) && !is_app(e2)) || /* ?m2 := ?m1 a_1 ... a_n */
(!mvar_has_user_facing_name(f2) && mvar_has_user_facing_name(f1)) /* ?m2 does not have a user facing name, but ?m1 has */
) {
if (m_update_right &&
((is_app(e1) && !is_app(e2)) || /* ?m2 := ?m1 a_1 ... a_n */
(!mvar_has_user_facing_name(f2) && mvar_has_user_facing_name(f1)))) { /* ?m2 does not have a user facing name, but ?m1 has */
/* Remark: the second case (?m2 has user facing name but ?m1 doesn't) is particularly for
the equation preprocessor. See issue #1801. */
swap_update_flags_scope scope(*this);
/* We need to swap `m_update_left` and `m_update_right` because `process_assignment` uses `is_def_eq` */
return to_lbool(process_assignment(e2, e1));
} else {
return to_lbool(process_assignment(e1, e2));
@ -2636,7 +2638,13 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
}
} else {
lean_assert(!m2_decl->get_context().is_subset_of(m1_decl->get_context()));
return to_lbool(process_assignment(e2, e1));
if (m_update_right) {
swap_update_flags_scope scope(*this);
/* We need to swap `m_update_left` and `m_update_right` because `process_assignment` uses `is_def_eq` */
return to_lbool(process_assignment(e2, e1));
} else {
return l_false;
}
}
} else {
return l_false;
@ -2648,7 +2656,9 @@ lbool type_context::quick_is_def_eq(expr const & e1, expr const & e2) {
if (is_mode_mvar(f2)) {
lean_assert(!is_assigned(f2));
if (m_update) {
if (m_update_right) {
swap_update_flags_scope scope(*this);
/* We need to swap `m_update_left` and `m_update_right` because `process_assignment` uses `is_def_eq` */
return to_lbool(process_assignment(e2, e1));
} else {
return l_false;
@ -3006,8 +3016,11 @@ lbool type_context::try_nat_offset_cnstrs(expr const & t, expr const & s) {
if (r != l_undef) return r;
r = try_offset_eq_numeral(t, s);
if (r != l_undef) return r;
r = try_offset_eq_numeral(s, t);
if (r != l_undef) return r;
{
swap_update_flags_scope scope(*this);
r = try_offset_eq_numeral(s, t);
if (r != l_undef) return r;
}
return try_numeral_eq_numeral(t, s);
}
@ -3807,6 +3820,8 @@ struct instance_synthesizer {
}
optional<expr> operator()(expr const & type) {
flet<bool> scope_left(m_ctx.m_update_left, true);
flet<bool> scope_right(m_ctx.m_update_right, true);
if (is_trace_enabled() && !is_trace_class_enabled("class_instances")) {
scope_trace_silent scope(true);
return main(type);
@ -4058,6 +4073,11 @@ bool tmp_type_context::is_def_eq(expr const & e1, expr const & e2) {
return m_ctx.is_def_eq(e1, e2);
}
bool tmp_type_context::match(expr const & e1, expr const & e2) {
type_context::tmp_mode_scope_with_data tmp_scope(m_ctx, m_tmp_data);
return m_ctx.match(e1, e2);
}
expr tmp_type_context::infer(expr const & e) {
type_context::tmp_mode_scope_with_data tmp_scope(m_ctx, m_tmp_data);
return m_ctx.infer(e);

51
src/library/type_context.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <vector>
#include <unordered_map>
#include <unordered_set>
#include <algorithm>
#include "util/flet.h"
#include "util/lbool.h"
#include "kernel/environment.h"
@ -554,9 +555,24 @@ private:
/* If m_zeta, then use zeta-reduction (i.e., expand let-expressions at whnf) */
bool m_zeta{true};
/* If m_update, then metavariables can be assigned by is_def_eq and similar methods.
This is used to implement nd_is_def_eq (non-destructive is_def_eq predicate. */
bool m_update{true};
/* If m_update_left, then when processing `is_def_eq(t, s)`, metavariables
occurring in `t` can be assigned. */
bool m_update_left{true};
/* If m_update_right, then when processing `is_def_eq(t, s)`, metavariables
occurring in `t` can be assigned. */
bool m_update_right{true};
/* Auxiliary object used to temporarily swap `m_update_left` and `m_update_right`.
We use it before invoking methods where we swap left/right. */
struct swap_update_flags_scope {
type_context & m_ctx;
swap_update_flags_scope(type_context & ctx):m_ctx(ctx) {
std::swap(m_ctx.m_update_left, m_ctx.m_update_right);
}
~swap_update_flags_scope() {
std::swap(m_ctx.m_update_left, m_ctx.m_update_right);
}
};
/* Postponed universe constraints.
We postpone universe constraints containing max/imax. Examples:
@ -674,24 +690,39 @@ public:
virtual expr check(expr const & e) override;
virtual bool is_def_eq(expr const & e1, expr const & e2) override;
bool match(expr const & e1, expr const & e2) {
flet<bool> update_left(m_update_left, true);
flet<bool> no_update_right(m_update_right, false);
return is_def_eq(e1, e2);
}
bool unify(expr const & e1, expr const & e2) {
flet<bool> update_left(m_update_left, true);
flet<bool> update_right(m_update_right, true);
return is_def_eq(e1, e2);
}
virtual expr relaxed_whnf(expr const & e) override;
virtual bool relaxed_is_def_eq(expr const & e1, expr const & e2) override;
/** Non destructive is_def_eq (i.e., metavariables cannot be assigned) */
bool nd_is_def_eq(level const & l1, level const & l2) {
flet<bool> no_update(m_update, false);
bool pure_is_def_eq(level const & l1, level const & l2) {
flet<bool> no_update_left(m_update_left, false);
flet<bool> no_update_right(m_update_right, false);
return is_def_eq(l1, l2);
}
/** Non destructive is_def_eq (i.e., metavariables cannot be assigned) */
bool nd_is_def_eq(expr const & e1, expr const & e2) {
flet<bool> no_update(m_update, false);
bool pure_is_def_eq(expr const & e1, expr const & e2) {
flet<bool> no_update_left(m_update_left, false);
flet<bool> no_update_right(m_update_right, false);
return is_def_eq(e1, e2);
}
/** Non destructive relaxed_is_def_eq (i.e., metavariables cannot be assigned) */
bool nd_relaxed_is_def_eq(expr const & e1, expr const & e2) {
flet<bool> no_update(m_update, false);
bool pure_relaxed_is_def_eq(expr const & e1, expr const & e2) {
flet<bool> no_update_left(m_update_left, false);
flet<bool> no_update_right(m_update_right, false);
return relaxed_is_def_eq(e1, e2);
}
@ -1083,6 +1114,8 @@ public:
virtual expr whnf(expr const & e) override;
virtual bool is_def_eq(expr const & e1, expr const & e2) override;
bool match(expr const & e1, expr const & e2);
expr mk_lambda(buffer<expr> const & locals, expr const & e);
expr mk_pi(buffer<expr> const & locals, expr const & e);
expr mk_lambda(expr const & local, expr const & e);