michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/unifier): allow computation when solving flex-rigid constraints

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-20 16:09:28 -07:00
parent be5d034b6e
commit 0450e81392
2 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/unifier.cpp
View file

@ -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<expr> 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<constraints> 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<constraints> alts2;

8
src/library/unifier.h
View file

@ -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<substitution> 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<substitution> unify(environment const & env, unsigned num_cs, constraint const * cs, name_generator const & ngen,
bool use_exception, options const & o);
lazy_list<substitution> 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<substitution> unify(environment const & env, expr const & lhs, expr const & rhs, name_generator const & ngen,
bool relax_main_opaque, substitution const & s, options const & o);