diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index db5ee3fbb..48f208225 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -24,6 +24,7 @@ Author: Leonardo de Moura #include "library/hop_match.h" #include "library/expr_lt.h" #include "library/simplifier/rewrite_rule_set.h" +#include "library/simplifier/simplifier.h" #ifndef LEAN_SIMPLIFIER_PROOFS #define LEAN_SIMPLIFIER_PROOFS true @@ -137,6 +138,8 @@ class simplifier_fn { congr_thms m_congr_thms; unsigned m_next_idx; // index used to create fresh constants unsigned m_num_steps; // number of steps performed + unsigned m_depth; // recursion depth + std::shared_ptr m_monitor; // Configuration bool m_proofs_enabled; @@ -294,11 +297,16 @@ class simplifier_fn { \brief Create heterogeneous congruence proof. */ optional mk_hcongr_th(expr const & f_type, expr const & new_f_type, expr const & f, expr const & new_f, - expr const & Heq_f, expr const & a, result const & new_a) { + expr const & Heq_f, expr const & a, result const & new_a, + // the following two arguments are used only for invoking the simplifier monitor + expr const & e, unsigned i) { expr const & A = abst_domain(f_type); if (is_TypeU(A)) { - if (!is_definitionally_equal(f, new_f)) + if (!is_definitionally_equal(f, new_f)) { + if (m_monitor) + m_monitor->failed_app_eh(m_depth, e, i, simplifier_monitor::failure_kind::Unsupported); return none_expr(); // can't handle + } // The congruence axiom cannot be used in this case. // Type problem is that we would need provide a proof of (@eq (Type U) a new_a.m_expr), // and (Type U) has type (Type U+1) the congruence axioms expect arguments from @@ -314,8 +322,11 @@ class simplifier_fn { // // @subst (Type i) a a' (fun x : (Type i), (@heq (B a) (B x) (f a) (f x))) (@hrefl (B a) (f a)) H expr a_type = infer_type(a); - if (!is_convertible(a_type, A)) + if (!is_convertible(a_type, A)) { + if (m_monitor) + m_monitor->failed_app_eh(m_depth, e, i, simplifier_monitor::failure_kind::TypeMismatch); return none_expr(); // can't handle + } expr a_prime = new_a.m_expr; expr H = get_proof(new_a); if (new_a.is_heq_proof()) @@ -334,8 +345,11 @@ class simplifier_fn { expr const & new_A = abst_domain(new_f_type); expr a_type = infer_type(a); expr new_a_type = infer_type(new_a.m_expr); - if (!is_convertible(new_a_type, new_A)) + if (!is_convertible(new_a_type, new_A)) { + if (m_monitor) + m_monitor->failed_app_eh(m_depth, e, i, simplifier_monitor::failure_kind::TypeMismatch); return none_expr(); // failed + } expr Heq_a = get_proof(new_a); bool is_heq_proof = new_a.is_heq_proof(); if (!is_definitionally_equal(A, a_type)|| !is_definitionally_equal(new_A, new_a_type)) { @@ -344,6 +358,8 @@ class simplifier_fn { Heq_a = mk_to_eq_th(a_type, a, new_a.m_expr, Heq_a); is_heq_proof = false; } else { + if (m_monitor) + m_monitor->failed_app_eh(m_depth, e, i, simplifier_monitor::failure_kind::Unsupported); return none_expr(); // we don't know how to handle this case } } @@ -691,7 +707,8 @@ class simplifier_fn { expr f = mk_app_prefix(i, new_args); expr pr_i = *proofs[i]; auto new_pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, mk_hrefl_th(f_types[i-1], f), - arg(e, i), result(new_args[i], pr_i, heq_proofs[i])); + arg(e, i), result(new_args[i], pr_i, heq_proofs[i]), + e, i); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -710,7 +727,8 @@ class simplifier_fn { if (!heq_proof) pr = mk_to_heq_th(f_types[i], f, new_f, pr); auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, - arg(e, i), result(new_args[i], pr_i, true)); + arg(e, i), result(new_args[i], pr_i, true), + e, i); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -718,7 +736,8 @@ class simplifier_fn { } else if (heq_proof) { lean_assert(!heq_proofs[i]); auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, - arg(e, i), result(new_args[i], pr_i, false)); + arg(e, i), result(new_args[i], pr_i, false), + e, i); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -727,7 +746,8 @@ class simplifier_fn { } } else if (heq_proof) { auto new_pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, pr, - arg(e, i), result(arg(e, i))); + arg(e, i), result(arg(e, i)), + e, i); if (!new_pr) return rewrite_app(e, result(e)); // failed to create congruence proof pr = *new_pr; @@ -846,6 +866,8 @@ class simplifier_fn { new_proof = rule.get_proof(); } } + if (m_monitor) + m_monitor->rewrite_eh(m_depth, target, new_rhs, rule.get_ceq()); return true; } else { // Conditional rewriting: we try to fill the missing @@ -883,23 +905,34 @@ class simplifier_fn { // The body of ceq depends on this argument, // but proof generation is not enabled. // So, we should fail + if (m_monitor) + m_monitor->failed_rewrite_eh(m_depth, target, rule.get_ceq(), i, simplifier_monitor::failure_kind::Unsupported); return false; } } else { // failed to prove proposition + if (m_monitor) + m_monitor->failed_rewrite_eh(m_depth, target, rule.get_ceq(), i, simplifier_monitor::failure_kind::AssumptionNotProved); return false; } } else { // failed, the argument is not a proposition + if (m_monitor) + m_monitor->failed_rewrite_eh(m_depth, target, rule.get_ceq(), i, simplifier_monitor::failure_kind::MissingArgument); return false; } } } new_proof = mk_app(proof_args); new_rhs = arg(ceq, num_args(ceq) - 1); - if (rule.is_permutation() && !is_lt(new_rhs, target, false)) + if (rule.is_permutation() && !is_lt(new_rhs, target, false)) { + if (m_monitor) + m_monitor->failed_rewrite_eh(m_depth, target, rule.get_ceq(), 0, simplifier_monitor::failure_kind::PermutationGe); return false; - return true; + } + if (m_monitor) + m_monitor->rewrite_eh(m_depth, target, new_rhs, rule.get_ceq()); + return true; } } return false; @@ -1065,6 +1098,8 @@ class simplifier_fn { expr new_bi = res_bi.m_expr; if (occurs(x_old, new_bi)) { // failed, simplifier didn't manage to replace x_old with x_new + if (m_monitor) + m_monitor->failed_abstraction_eh(m_depth, e, simplifier_monitor::failure_kind::AbstractionBody); return rewrite(e, result(e)); } expr new_e = update_lambda(e, new_d, abstract(new_bi, x_new)); @@ -1166,6 +1201,8 @@ class simplifier_fn { } else { expr e_type = infer_type(e); if (is_TypeU(e_type) || !ensure_homogeneous(A, res_A)) { + if (m_monitor) + m_monitor->failed_abstraction_eh(m_depth, e, simplifier_monitor::failure_kind::TypeMismatch); return result(e); // failed, we can't use subst theorem } else { expr H = get_proof(res_A); @@ -1199,6 +1236,8 @@ class simplifier_fn { } else { expr e_type = infer_type(e); if (is_TypeU(e_type) || !ensure_homogeneous(B, res_B)) { + if (m_monitor) + m_monitor->failed_abstraction_eh(m_depth, e, simplifier_monitor::failure_kind::TypeMismatch); return result(e); // failed, we can't use subst theorem } else { expr H = get_proof(res_B); @@ -1278,11 +1317,16 @@ class simplifier_fn { expr new_bi = res_bi.m_expr; if (occurs(x_old, new_bi)) { // failed, simplifier didn't manage to replace x_old with x_new + if (m_monitor) + m_monitor->failed_abstraction_eh(m_depth, e, simplifier_monitor::failure_kind::AbstractionBody); return rewrite(e, result(e)); } expr new_e = update_pi(e, new_d, abstract(new_bi, x_new)); - if (!m_proofs_enabled || is_definitionally_equal(e, new_e)) + if (!m_proofs_enabled || is_definitionally_equal(e, new_e)) { + if (m_monitor) + m_monitor->failed_abstraction_eh(m_depth, e, simplifier_monitor::failure_kind::TypeMismatch); return rewrite(e, result(new_e)); + } ensure_homogeneous(d, res_d); ensure_homogeneous(bi, res_bi); // Remark: the argument with type A = A' in hallext and hpiext is actually @eq TypeM A A', @@ -1319,6 +1363,8 @@ class simplifier_fn { return simplify_forall_body(e); } else { // We currently do simplify (forall x : A, B x) when it is not a proposition. + if (m_monitor) + m_monitor->failed_abstraction_eh(m_depth, e, simplifier_monitor::failure_kind::Unsupported); return result(e); } } @@ -1327,6 +1373,8 @@ class simplifier_fn { if (m_memoize) { result new_r = r.update_expr(m_max_sharing(r.m_expr)); m_cache.insert(mk_pair(e, new_r)); + if (m_monitor) + m_monitor->step_eh(m_depth, e, new_r.m_expr, new_r.m_proof); return new_r; } else { return r; @@ -1336,6 +1384,7 @@ class simplifier_fn { result simplify(expr e) { check_system("simplifier"); m_num_steps++; + flet inc_depth(m_depth, m_depth+1); if (m_num_steps > m_max_steps) throw exception("simplifier failed, maximum number of steps exceeded"); if (m_memoize) { @@ -1345,6 +1394,8 @@ class simplifier_fn { return it->second; } } + if (m_monitor) + m_monitor->pre_eh(m_depth, e); switch (e.kind()) { case expr_kind::Var: return result(e); case expr_kind::Constant: return save(e, simplify_constant(e)); @@ -1394,8 +1445,9 @@ class simplifier_fn { } public: - simplifier_fn(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs): - m_env(env), m_tc(env) { + simplifier_fn(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs, + std::shared_ptr const & monitor): + m_env(env), m_tc(env), m_monitor(monitor) { m_has_heq = m_env->imported("heq"); m_has_cast = m_env->imported("cast"); set_options(o); @@ -1411,22 +1463,25 @@ public: expr_pair operator()(expr const & e, context const & ctx) { set_ctx(ctx); m_num_steps = 0; + m_depth = 0; auto r = simplify(e); return mk_pair(r.m_expr, get_proof(r)); } }; expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, - unsigned num_rs, rewrite_rule_set const * rs) { - return simplifier_fn(env, opts, num_rs, rs)(e, ctx); + unsigned num_rs, rewrite_rule_set const * rs, + std::shared_ptr const & monitor) { + return simplifier_fn(env, opts, num_rs, rs, monitor)(e, ctx); } expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, - unsigned num_ns, name const * ns) { + unsigned num_ns, name const * ns, + std::shared_ptr const & monitor) { buffer rules; for (unsigned i = 0; i < num_ns; i++) rules.push_back(get_rewrite_rule_set(env, ns[i])); - return simplify(e, env, ctx, opts, num_ns, rules.data()); + return simplify(e, env, ctx, opts, num_ns, rules.data(), monitor); } static int simplify_core(lua_State * L, ro_shared_environment const & env) { diff --git a/src/library/simplifier/simplifier.h b/src/library/simplifier/simplifier.h index 1ff032c54..f4813f2f1 100644 --- a/src/library/simplifier/simplifier.h +++ b/src/library/simplifier/simplifier.h @@ -11,9 +11,70 @@ Author: Leonardo de Moura #include "library/simplifier/rewrite_rule_set.h" namespace lean { +/** + \brief Abstract class that specifies the interface for monitoring + the behavior of the simplifier. +*/ +class simplifier_monitor { +public: + /** + \brief This method is invoked to sign that the simplifier is starting to process the expression \c e. + + \remark \c depth is the recursion depth + */ + virtual void pre_eh(unsigned depth, expr const & e) = 0; + + /** + \brief This method is invoked to sign that \c e has be rewritten into \c new_e with proof \c pr. + The proof is none if proof generation is disabled or if \c e and \c new_e are definitionally equal. + + \remark \c depth is the recursion depth + */ + virtual void step_eh(unsigned depth, expr const & e, expr const & new_e, optional const & pr) = 0; + /** + \brief This method is invoked to sign that \c e has be rewritten into \c new_e using the conditional equation \c ceq. + + \remark \c depth is the recursion depth + */ + virtual void rewrite_eh(unsigned depth, expr const & e, expr const & new_e, expr const & ceq) = 0; + + enum class failure_kind { Unsupported, TypeMismatch, AssumptionNotProved, MissingArgument, PermutationGe, AbstractionBody }; + + /** + \brief This method is invoked when the simplifier fails to rewrite an application \c e. + \c i is the argument where the simplifier gave up, and \c k is the reason for failure. + Two possible values are: Unsupported or TypeMismatch (may happen when simplifying terms that use dependent types). + + \remark \c depth is the recursion depth + */ + virtual void failed_app_eh(unsigned depth, expr const & e, unsigned i, failure_kind k) = 0; + + /** + \brief This method is invoked when the simplifier fails to apply a conditional equation \c ceq to \c e. + The \c ceq may have several arguments, the value \c i is the argument where the simplifier gave up, and \c k is the reason for failure. + The possible failure values are: AssumptionNotProved (failed to synthesize a proof for an assumption required by \c ceq), + MissingArgument (failed to infer one of the arguments needed by the conditional equation), PermutationGe + (the conditional equation is a permutation, and the result is not smaller in the term ordering, \c i is irrelevant in this case). + + \remark \c depth is the recursion depth + */ + virtual void failed_rewrite_eh(unsigned depth, expr const & e, expr const & ceq, unsigned i, failure_kind k) = 0; + + /** + \brief This method is invoked when the simplifier fails to simplify an abstraction (Pi or Lambda). + The possible failure values are: Unsupported, TypeMismatch, and AbstractionBody (failed to rewrite the body of the abstraction, + this may happen when we are using dependent types). + + \remark \c depth is the recursion depth + */ + virtual void failed_abstraction_eh(unsigned depth, expr const & e, failure_kind k) = 0; +}; + expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts, - unsigned num_rs, rewrite_rule_set const * rs); + unsigned num_rs, rewrite_rule_set const * rs, + std::shared_ptr const & monitor = std::shared_ptr()); expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts, - unsigned num_ns, name const * ns); + unsigned num_ns, name const * ns, + std::shared_ptr const & monitor = std::shared_ptr()); void open_simplifier(lua_State * L); }