max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): display error when failed to elaborate using expected type

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-29 11:55:05 -07:00
parent ceeebb7e40
commit f2e8b8794c
3 changed files with 35 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
src/frontends/lean/elaborator.cpp
View file

@ -991,41 +991,18 @@ expr elaborator::second_pass(expr const & fn, buffer<expr> const & args,
return mk_app(fn, info.new_args.size(), info.new_args.data());
}
optional<expr> elaborator::visit_app_with_expected(expr const & fn, buffer<expr> 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<expr> const & args,
bool args_already_visited, optional<expr> const & expected_type, expr const & ref) {
expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<expr> const & args,
bool args_already_visited, optional<expr> const & expected_type, expr const & ref) {
expr fn = _fn;
expr fn_type = infer_type(fn);
unsigned i = 0;
buffer<expr> 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<ex
return r;
}
expr elaborator::visit_base_app_core(expr const & fn, arg_mask amask, buffer<expr> const & args,
bool args_already_visited, optional<expr> 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<expr> const & args,
optional<expr> const & expected_type, expr const & ref) {
return visit_base_app_core(fn, amask, args, false, expected_type, ref);

4
src/frontends/lean/elaborator.h
View file

@ -168,8 +168,8 @@ private:
struct first_pass_info;
void first_pass(expr const & fn, buffer<expr> const & args, expr const & expected_type, expr const & ref, first_pass_info & info);
expr second_pass(expr const & fn, buffer<expr> const & args, expr const & ref, first_pass_info & info);
optional<expr> visit_app_with_expected(expr const & fn, buffer<expr> const & args,
expr const & expected_type, expr const & ref);
expr visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<expr> const & args,
bool args_already_visited, optional<expr> const & expected_type, expr const & ref);
expr visit_base_app_core(expr const & fn, arg_mask amask, buffer<expr> const & args,
bool args_already_visited, optional<expr> const & expected_type, expr const & ref);
expr visit_base_app(expr const & fn, arg_mask amask, buffer<expr> const & args,

3
tests/lean/elab12.lean.expected.out
View file

@ -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)