From f2e8b8794c073149fe605ef96a85580eb61a9ff7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Sep 2016 11:55:05 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): display error when failed to elaborate using expected type --- src/frontends/lean/elaborator.cpp | 55 ++++++++++++++++------------- src/frontends/lean/elaborator.h | 4 +-- tests/lean/elab12.lean.expected.out | 3 ++ 3 files changed, 35 insertions(+), 27 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 2c3f76d4d6..fd96719af1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -991,41 +991,18 @@ expr elaborator::second_pass(expr const & fn, buffer const & args, return mk_app(fn, info.new_args.size(), info.new_args.data()); } -optional elaborator::visit_app_with_expected(expr const & fn, buffer const & args, - expr const & expected_type, expr const & ref) { - snapshot C(*this); - first_pass_info info; - try { - first_pass(fn, args, expected_type, ref, info); - } catch (elaborator_exception &) { - C.restore(*this); - return none_expr(); - } - return some_expr(second_pass(fn, args, ref, info)); -} - bool elaborator::is_with_expected_candidate(expr const & fn) { if (!is_constant(fn)) return false; return get_elaborator_strategy(m_env, const_name(fn)) == elaborator_strategy::WithExpectedType; } -expr elaborator::visit_base_app_core(expr const & _fn, arg_mask amask, buffer const & args, - bool args_already_visited, optional const & expected_type, expr const & ref) { +expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer const & args, + bool args_already_visited, optional const & expected_type, expr const & ref) { expr fn = _fn; expr fn_type = infer_type(fn); unsigned i = 0; buffer new_args; - /** Check if this application is a candidate for propagating the expected type to arguments */ - if (!args_already_visited && /* if the arguments have already been visited, then there is no point. */ - expected_type && /* the expected type must be known */ - amask == arg_mask::Default && /* we do not propagate information when @ and @@ are used */ - is_with_expected_candidate(fn)) { - if (auto r = visit_app_with_expected(fn, args, *expected_type, ref)) { - return *r; - } - } - /* We manually track the type before whnf. We do that because after the loop we check whether the application type is definitionally equal to expected_type. Suppose, the result type is (tactic expr) and the expected type is (?M1 ?M2). @@ -1110,6 +1087,34 @@ expr elaborator::visit_base_app_core(expr const & _fn, arg_mask amask, buffer const & args, + bool args_already_visited, optional const & expected_type, expr const & ref) { + /** Check if this application is a candidate for propagating the expected type to arguments */ + if (args_already_visited || /* if the arguments have already been visited, then there is no point. */ + amask != arg_mask::Default || /* we do not propagate expected type info when @ and @@ are used */ + !is_with_expected_candidate(fn) || + !expected_type) { + return visit_base_app_simple(fn, amask, args, args_already_visited, expected_type, ref); + } + + snapshot C(*this); + first_pass_info info; + try { + first_pass(fn, args, *expected_type, ref, info); + } catch (elaborator_exception & ex1) { + C.restore(*this); + try { + return visit_base_app_simple(fn, amask, args, args_already_visited, expected_type, ref); + } catch (elaborator_exception & ex2) { + throw nested_elaborator_exception(ref, ex2, + format("switched to simple application elaboration procedure because " + "failed to use expected type to elaborate it, " + "error message") + nest(get_pp_indent(m_opts), line() + ex1.pp())); + } + } + return second_pass(fn, args, ref, info); +} + expr elaborator::visit_base_app(expr const & fn, arg_mask amask, buffer const & args, optional const & expected_type, expr const & ref) { return visit_base_app_core(fn, amask, args, false, expected_type, ref); diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index f0ff86a37c..5009406930 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -168,8 +168,8 @@ private: struct first_pass_info; void first_pass(expr const & fn, buffer const & args, expr const & expected_type, expr const & ref, first_pass_info & info); expr second_pass(expr const & fn, buffer const & args, expr const & ref, first_pass_info & info); - optional visit_app_with_expected(expr const & fn, buffer const & args, - expr const & expected_type, expr const & ref); + expr visit_base_app_simple(expr const & _fn, arg_mask amask, buffer const & args, + bool args_already_visited, optional const & expected_type, expr const & ref); expr visit_base_app_core(expr const & fn, arg_mask amask, buffer const & args, bool args_already_visited, optional const & expected_type, expr const & ref); expr visit_base_app(expr const & fn, arg_mask amask, buffer const & args, diff --git a/tests/lean/elab12.lean.expected.out b/tests/lean/elab12.lean.expected.out index f11932311c..d3ff171c7a 100644 --- a/tests/lean/elab12.lean.expected.out +++ b/tests/lean/elab12.lean.expected.out @@ -2,6 +2,9 @@ elab12.lean:1:30: error: type expected at 0 elab12.lean:4:42: error: function expected at rfl +Additional information: +elab12.lean:4:42: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message + too many arguments elab12.lean:7:44: error: failed to synthesize type class instance for a : ℕ ⊢ has_add (a = a)