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

fix(frontends/lean/elaborator): better position tracking for applications

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-27 18:52:04 -07:00
parent acda62d725
commit ba4abed588
2 changed files with 16 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -720,7 +720,8 @@ expr elaborator::visit_overloaded_app(buffer<expr> const & fns, buffer<expr> con
}
}
expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type) {
expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type,
expr const & ref) {
arg_mask amask = arg_mask::Default;
if (is_explicit(fn)) {
fn = get_explicit_arg(fn);
@ -735,47 +736,47 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
if (is_choice(fn)) {
buffer<expr> fns;
if (amask != arg_mask::Default)
throw elaborator_exception(fn, format("invalid explicit annotation, symbol is overloaded "
"(solution: use fully qualified names)"));
throw elaborator_exception(ref, format("invalid explicit annotation, symbol is overloaded "
"(solution: use fully qualified names)"));
for (unsigned i = 0; i < get_num_choices(fn); i++) {
expr const & fn_i = get_choice(fn, i);
fns.push_back(fn_i);
}
validate_overloads(fns, fn);
validate_overloads(fns, ref);
for (expr & new_fn : fns) {
new_fn = visit_function(new_fn, has_args, fn);
new_fn = visit_function(new_fn, has_args, ref);
}
return visit_overloaded_app(fns, args, expected_type, fn);
return visit_overloaded_app(fns, args, expected_type, ref);
} else {
expr new_fn = visit_function(fn, has_args, fn);
expr new_fn = visit_function(fn, has_args, ref);
/* Check if we should use a custom elaboration procedure for this application. */
if (is_constant(new_fn) && amask == arg_mask::Default) {
if (auto info = use_elim_elab(const_name(new_fn))) {
if (args.size() >= info->m_nexplicit) {
return visit_elim_app(new_fn, *info, args, expected_type, fn);
return visit_elim_app(new_fn, *info, args, expected_type, ref);
} else {
trace_elab(tout() << pos_string_for(fn) << " 'eliminator' elaboration is not used for '" << fn <<
trace_elab(tout() << pos_string_for(ref) << " 'eliminator' elaboration is not used for '" << fn <<
"' because it is not fully applied, #" << info->m_nexplicit <<
" explicit arguments expected\n";);
}
}
}
return visit_default_app(new_fn, amask, args, expected_type, fn);
return visit_default_app(new_fn, amask, args, expected_type, ref);
}
}
expr elaborator::visit_local(expr const & e, optional<expr> const & expected_type) {
return visit_app_core(e, buffer<expr>(), expected_type);
return visit_app_core(e, buffer<expr>(), expected_type, e);
}
expr elaborator::visit_constant(expr const & e, optional<expr> const & expected_type) {
return visit_app_core(e, buffer<expr>(), expected_type);
return visit_app_core(e, buffer<expr>(), expected_type, e);
}
expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type) {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
return visit_app_core(fn, args, expected_type);
return visit_app_core(fn, args, expected_type, e);
}
expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_type) {
@ -786,7 +787,7 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
} else if (is_typed_expr(e)) {
return visit_typed_expr(e);
} else if (is_choice(e) || is_explicit(e) || is_partial_explicit(e)) {
return visit_app_core(e, buffer<expr>(), expected_type);
return visit_app_core(e, buffer<expr>(), expected_type, e);
} else if (is_rec_fn_macro(e)) {
// TODO(Leo)
lean_unreachable();

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

@ -129,7 +129,7 @@ class elaborator {
optional<expr> const & expected_type, expr const & ref);
expr visit_elim_app(expr const & fn, elim_info const & info, buffer<expr> const & args,
optional<expr> const & expected_type, expr const & ref);
expr visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type);
expr visit_app_core(expr fn, buffer<expr> const & args, optional<expr> const & expected_type, expr const & ref);
expr visit_local(expr const & e, optional<expr> const & expected_type);
expr visit_constant(expr const & e, optional<expr> const & expected_type);
expr visit_macro(expr const & e, optional<expr> const & expected_type);