diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index fddf4ad130..c08e8b19c0 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -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 ...), diff --git a/src/library/tactic/smt/congruence_closure.h b/src/library/tactic/smt/congruence_closure.h index c08d89fd2d..3a4a7eef59 100644 --- a/src/library/tactic/smt/congruence_closure.h +++ b/src/library/tactic/smt/congruence_closure.h @@ -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); } diff --git a/src/library/tactic/smt/theory_ac.cpp b/src/library/tactic/smt/theory_ac.cpp index d178fd9d23..95e181d396 100644 --- a/src/library/tactic/smt/theory_ac.cpp +++ b/src/library/tactic/smt/theory_ac.cpp @@ -145,7 +145,7 @@ optional theory_ac::is_ac(expr const & e) { return some_expr(*it); optional 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) { diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 59049cc065..7aefae8604 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -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 m1_decl = m_mctx.find_metavar_decl(f1); optional 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 operator()(expr const & type) { + flet scope_left(m_ctx.m_update_left, true); + flet 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); diff --git a/src/library/type_context.h b/src/library/type_context.h index f40818a936..06bd0874fe 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include #include +#include #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 update_left(m_update_left, true); + flet no_update_right(m_update_right, false); + return is_def_eq(e1, e2); + } + + bool unify(expr const & e1, expr const & e2) { + flet update_left(m_update_left, true); + flet 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 no_update(m_update, false); + bool pure_is_def_eq(level const & l1, level const & l2) { + flet no_update_left(m_update_left, false); + flet 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 no_update(m_update, false); + bool pure_is_def_eq(expr const & e1, expr const & e2) { + flet no_update_left(m_update_left, false); + flet 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 no_update(m_update, false); + bool pure_relaxed_is_def_eq(expr const & e1, expr const & e2) { + flet no_update_left(m_update_left, false); + flet 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 const & locals, expr const & e); expr mk_pi(buffer const & locals, expr const & e); expr mk_lambda(expr const & local, expr const & e);