From 0450e81392bd693b580e3a74c1ae933b5fed1799 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Aug 2014 16:09:28 -0700 Subject: [PATCH] feat(library/unifier): allow computation when solving flex-rigid constraints Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 9 ++++++++- src/library/unifier.h | 8 +++++--- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 54b8fc91f..2e624192d 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1635,6 +1635,13 @@ struct unifier_fn { return modified ? mk_app(m, margs) : lhs; } + /** \brief Return true if all arguments of lhs are local constants */ + bool all_local(expr const & lhs) { + buffer margs; + get_app_args(lhs, margs); + return std::all_of(margs.begin(), margs.end(), [&](expr const & e) { return is_local(e); }); + } + /** \brief Process a flex rigid constraint */ bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j, bool relax) { lean_assert(is_meta(lhs)); @@ -1656,7 +1663,7 @@ struct unifier_fn { buffer alts; process_flex_rigid_core(lhs, rhs, j, relax, alts); append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end())); - if (m_expensive) { + if (!all_local(lhs)) { expr rhs_whnf = whnf(rhs, j, relax, aux); if (rhs_whnf != rhs) { buffer alts2; diff --git a/src/library/unifier.h b/src/library/unifier.h index 9a6894ac5..dd87862fd 100644 --- a/src/library/unifier.h +++ b/src/library/unifier.h @@ -16,7 +16,7 @@ Author: Leonardo de Moura #include "kernel/metavar.h" #ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS -#define LEAN_DEFAULT_UNIFIER_MAX_STEPS 10000 +#define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000 #endif #ifndef LEAN_DEFAULT_UNIFIER_EXPENSIVE @@ -41,11 +41,13 @@ unify_status unify_simple(substitution & s, level const & lhs, level const & rhs unify_status unify_simple(substitution & s, constraint const & c); lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, - bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool expensive = LEAN_DEFAULT_UNIFIER_EXPENSIVE); + bool use_exception = true, unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, + bool expensive = LEAN_DEFAULT_UNIFIER_EXPENSIVE); lazy_list unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen, bool use_exception, options const & o); lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque, - substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, bool expensive = LEAN_DEFAULT_UNIFIER_MAX_STEPS); + substitution const & s = substitution(), unsigned max_steps = LEAN_DEFAULT_UNIFIER_MAX_STEPS, + bool expensive = LEAN_DEFAULT_UNIFIER_MAX_STEPS); lazy_list unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen, bool relax_main_opaque, substitution const & s, options const & o);