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

feat(frontends/lean/server): unifier maximum number of steps error in FINDG, closes #155

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-09 10:36:41 -07:00
parent 53292d8297
commit 0505be2aca
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/frontends/lean/server.cpp
View file

@ -34,6 +34,7 @@ Author: Leonardo de Moura
#define LEAN_FUZZY_MAX_ERRORS 3 #define LEAN_FUZZY_MAX_ERRORS 3
#define LEAN_FUZZY_MAX_ERRORS_FACTOR 3 #define LEAN_FUZZY_MAX_ERRORS_FACTOR 3
#define LEAN_FIND_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments when printing the type of declarations in FINDP and FINDG #define LEAN_FIND_CONSUME_IMPLICIT true // lean will add metavariables for implicit arguments when printing the type of declarations in FINDP and FINDG
#define LEAN_FINDG_MAX_STEPS 128 // maximum number of steps per unification problem
namespace lean { namespace lean {
server::file::file(std::istream & in, std::string const & fname):m_fname(fname) { server::file::file(std::istream & in, std::string const & fname):m_fname(fname) {
@ -717,8 +718,14 @@ bool match_type(type_checker & tc, expr const & meta, expr const & expected_type
// just ingore them. // just ingore them.
if (is_meta(dt)) if (is_meta(dt))
return false; // matches anything return false; // matches anything
auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), true); try {
return static_cast<bool>(r.pull()); unifier_config cfg;
cfg.m_max_steps = LEAN_FINDG_MAX_STEPS;
auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), true, substitution(), cfg);
return static_cast<bool>(r.pull());
} catch (exception&) {
return false;
}
} }
static name g_tmp_prefix = name::mk_internal_unique_name(); static name g_tmp_prefix = name::mk_internal_unique_name();