From 0505be2aca154e6522231137d5e00a970fb9b1a2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Sep 2014 10:36:41 -0700 Subject: [PATCH] feat(frontends/lean/server): unifier maximum number of steps error in FINDG, closes #155 Signed-off-by: Leonardo de Moura --- src/frontends/lean/server.cpp | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 567d355cd..c6c676bd3 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #define LEAN_FUZZY_MAX_ERRORS 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_FINDG_MAX_STEPS 128 // maximum number of steps per unification problem namespace lean { 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. if (is_meta(dt)) return false; // matches anything - auto r = unify(tc.env(), dt, expected_type, tc.mk_ngen(), true); - return static_cast(r.pull()); + try { + 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(r.pull()); + } catch (exception&) { + return false; + } } static name g_tmp_prefix = name::mk_internal_unique_name();