From e59fd2927a91e4dbe00c825764632786b6388df2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 25 Apr 2017 17:16:06 -0700 Subject: [PATCH] feat(library): process explicit arguments before implicit Moreover, we process the implicit arguments using at least the Semireducible transparency mode. The idea is to make sure to reduce counterintuitive behavior in rw and simp where the user believes a lemma is applicable but it does not work because the implicit part fails to unify. The modification above fixes the simplifier issues found by @kha when proving the monadic laws. This commit also improves constraints of the form n =?= m where n and m are big distinct numerals. The type_context fails quickly for this kind of constraint even using transparency mode Semireducible. We need this feature otherwise we timeout at @eq char a b =?= @eq unsigned ?x ?y Recall that char := fin char_sz unsigned := fin unsigned_sz --- src/library/tactic/simplify.cpp | 67 +------------ src/library/type_context.cpp | 167 ++++++++++++++++++++++---------- 2 files changed, 118 insertions(+), 116 deletions(-) diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index c1ecc75c29..0081fea806 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -523,73 +523,8 @@ simp_result simplify_core_fn::rewrite(expr const & e) { return simp_result(e); } -struct match_fn { - tmp_type_context & m_ctx; - name const & m_id; - buffer> m_postponed; - - match_fn(tmp_type_context & ctx, name const & id):m_ctx(ctx), m_id(id) {} - - bool match(expr const & p, expr const & t) { - if (m_ctx.ctx().is_mvar(p)) - if (auto v = m_ctx.ctx().get_assignment(p)) - return match(*v, t); - if (is_app(p) && is_app(t)) { - expr const & fn = get_app_fn(p); - if (m_ctx.is_def_eq(fn, get_app_fn(t))) { - buffer p_args; - buffer t_args; - get_app_args(p, p_args); - get_app_args(t, t_args); - fun_info finfo = get_fun_info(m_ctx.ctx(), fn); - if (p_args.size() != t_args.size()) - return false; - auto it = finfo.get_params_info(); - for (unsigned i = 0; i < p_args.size(); i++) { - if (it && head(it).is_inst_implicit()) { - m_postponed.emplace_back(p_args[i], t_args[i], true); - } else if (it && head(it).is_implicit()) { - m_postponed.emplace_back(p_args[i], t_args[i], false); - } else if (!match(p_args[i], t_args[i])) { - return false; - } - if (it) it = tail(it); - } - return true; - } - } - return m_ctx.is_def_eq(p, t); - } - - bool operator()(expr const & p, expr const & t) { - if (!match(p, t)) return false; - - for (unsigned i = 0; i < m_postponed.size(); i++) { - expr p1, t1; bool implicit; - std::tie(p1, t1, implicit) = m_postponed[i]; - p1 = m_ctx.instantiate_mvars(p1); - if (implicit) - p1 = m_ctx.ctx().complete_instance(p1); - { - type_context::transparency_scope _scope(m_ctx.ctx(), transparency_mode::Semireducible); - if (!match(p1, t1)) { - lean_simp_trace_d(m_ctx.ctx(), name({"simplify", "failure"}), - tout() << "fail to match '" << m_id << "':\n"; - tout() << p << "\n=?=\n" << t << "\nbecause the following implicit match\n"; - tout() << p1 << "\n=?=\n" << t1 << "\n";); - return false; - } - } - } - return true; - } -}; - bool simplify_core_fn::match(tmp_type_context & ctx, simp_lemma const & sl, expr const & t) { - if (m_cfg.m_use_matcher) - return match_fn(ctx, sl.get_id())(sl.get_lhs(), t); - else - return ctx.is_def_eq(sl.get_lhs(), t); + return ctx.is_def_eq(sl.get_lhs(), t); } /* If both e and sl.get_lhs() are of the form (f ...), diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 27aa51102a..3f4ab6646a 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2251,6 +2251,16 @@ expr type_context::complete_instance(expr const & e) { return e; } +static transparency_mode ensure_semireducible(transparency_mode m) { + switch (m) { + case transparency_mode::Reducible: + case transparency_mode::None: + return transparency_mode::Semireducible; + default: + return m; + } +} + bool type_context::is_def_eq_args(expr const & e1, expr const & e2) { lean_assert(is_app(e1) && is_app(e2)); buffer args1, args2; @@ -2260,19 +2270,58 @@ bool type_context::is_def_eq_args(expr const & e1, expr const & e2) { return false; fun_info finfo = get_fun_info(*this, fn, args1.size()); unsigned i = 0; + buffer> postponed; + /* First pass: unify explicit arguments, *and* easy cases + + Here, we say a case is easy if it is of the form + + ?m =?= t + or + t =?= ?m + + where ?m is unassigned. + + These easy cases are not just an optimization. When + ?m is a function, by assigning it to t, we make sure + a unification constraint (in the explicit part) + + ?m t =?= f s + + is not higher-order. + */ for (param_info const & pinfo : finfo.get_params_info()) { - if (pinfo.is_inst_implicit()) { - args1[i] = complete_instance(args1[i]); - args2[i] = complete_instance(args2[i]); - } - if (!is_def_eq_core(args1[i], args2[i])) + if (pinfo.is_inst_implicit() || pinfo.is_implicit()) { + if ((is_mvar(args1[i]) && !is_assigned(args1[i])) || + (is_mvar(args2[i]) && !is_assigned(args2[i]))) { + if (!is_def_eq_core(args1[i], args2[i])) { + return false; + } + } else { + postponed.emplace_back(i, pinfo.is_inst_implicit()); + } + } else if (!is_def_eq_core(args1[i], args2[i])) { return false; + } i++; } for (; i < args1.size(); i++) { if (!is_def_eq_core(args1[i], args2[i])) return false; } + /* Second pass: unify implicit arguments. + In the second pass, we make sure we are unfolding at least semireducible (default setting) definitions. */ + { + transparency_scope scope(*this, ensure_semireducible(m_transparency_mode)); + for (pair const & p : postponed) { + unsigned i = p.first; + if (p.second) { + args1[i] = complete_instance(args1[i]); + args2[i] = complete_instance(args2[i]); + } + if (!is_def_eq_core(args1[i], args2[i])) + return false; + } + } return true; } @@ -2732,48 +2781,56 @@ bool type_context::on_is_def_eq_failure(expr const & e1, expr const & e2) { return false; } +/* If e is a numeral, then return it. Otherwise return none. */ +static optional eval_num(expr const & e) { + if (is_constant(e, get_nat_zero_name())) { + return some(mpz(0)); + } else if (is_app_of(e, get_zero_name(), 2)) { + return some(mpz(0)); + } else if (is_app_of(e, get_one_name(), 2)) { + return some(mpz(1)); + } else if (auto a = is_bit0(e)) { + if (auto r1 = eval_num(*a)) + return some(mpz(2) * *r1); + else + return optional(); + } else if (auto a = is_bit1(e)) { + if (auto r1 = eval_num(*a)) + return some(mpz(2) * *r1 + 1); + else + return optional(); + } else if (is_app_of(e, get_nat_succ_name(), 1)) { + if (auto r1 = eval_num(app_arg(e))) + return some(*r1 + 1); + else + return optional(); + } else if (is_app_of(e, get_add_name(), 4)) { + auto r1 = eval_num(app_arg(app_fn(e))); + if (!r1) return optional(); + auto r2 = eval_num(app_arg(e)); + if (!r2) return optional(); + return some(*r1 + *r2); + } else if (is_app_of(e, get_sub_name(), 4)) { + auto r1 = eval_num(app_arg(app_fn(e))); + if (!r1) return optional(); + auto r2 = eval_num(app_arg(e)); + if (!r2) return optional(); + return some(*r2 > *r1 ? mpz(0) : *r1 - *r2); + } else { + return optional(); + } +} + /* If e is a (small) numeral, then return it. Otherwise return none. */ optional type_context::to_small_num(expr const & e) { - unsigned r; - if (is_constant(e, get_nat_zero_name())) { - r = 0; - } else if (is_app_of(e, get_zero_name(), 2)) { - r = 0; - } else if (is_app_of(e, get_one_name(), 2)) { - r = 1; - } else if (auto a = is_bit0(e)) { - if (auto r1 = to_small_num(*a)) - r = 2 * *r1; - else - return optional(); - } else if (auto a = is_bit1(e)) { - if (auto r1 = to_small_num(*a)) - r = 2 * *r1 + 1; - else - return optional(); - } else if (is_app_of(e, get_nat_succ_name(), 1)) { - if (auto r1 = to_small_num(app_arg(e))) - r = *r1 + 1; - else - return optional(); - } else if (is_app_of(e, get_add_name(), 4)) { - auto r1 = to_small_num(app_arg(app_fn(e))); - if (!r1) return optional(); - auto r2 = to_small_num(app_arg(e)); - if (!r2) return optional(); - r = *r1 + *r2; - } else if (is_app_of(e, get_sub_name(), 4)) { - auto r1 = to_small_num(app_arg(app_fn(e))); - if (!r1) return optional(); - auto r2 = to_small_num(app_arg(e)); - if (!r2) return optional(); - r = *r2 > *r1 ? 0 : *r1 - *r2; - } else { - return optional(); + if (optional r = eval_num(e)) { + if (r->is_unsigned_int()) { + unsigned r1 = r->get_unsigned_int(); + if (r1 <= m_cache->m_nat_offset_cnstr_threshold) + return optional(r1); + } } - if (r > m_cache->m_nat_offset_cnstr_threshold) - return optional(); - return optional(r); + return optional(); } /* If \c t is of the form (s + k) where k is a numeral, then return k. Otherwise, return none. */ @@ -2898,15 +2955,25 @@ lbool type_context::try_offset_eq_numeral(expr const & t, expr const & s) { k_1 =?= k_2 - where k_1 and k_2 are numerals, and type is nat */ + where k_1 and k_2 are numerals, and type is nat. + + If t and s are encoding distinct big numerals, we return l_false. + If t and s are encoding the same samll numeral, we return l_true. + Otherwise, we return l_undef. +*/ lbool type_context::try_numeral_eq_numeral(expr const & t, expr const & s) { - optional k1 = to_small_num(t); - if (!k1) return l_undef; - optional k2 = to_small_num(s); - if (!k2) return l_undef; + optional n1 = eval_num(t); + if (!n1) return l_undef; + optional n2 = eval_num(s); + if (!n2) return l_undef; if (!is_nat_type(whnf(infer(t)))) return l_undef; - return to_lbool(*k1 == *k2); + if (*n1 != *n2) + return l_false; + else if (to_small_num(t) && to_small_num(s)) + return l_true; + else + return l_undef; } /* Solve offset constraints. See discussion at issue #1226 */