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

feat(kernel/type_checker): improve 'declaration still has metavars' error message

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 08:51:33 -07:00
parent 3e7dfa6212
commit c427c5bdc9
3 changed files with 25 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/error_msgs.cpp
View file

@ -41,4 +41,18 @@ format pp_def_type_mismatch(formatter const & fmt, environment const & env, opti
r += pp_indent_expr(fmt, env, opts, given_type); r += pp_indent_expr(fmt, env, opts, given_type);
return r; return r;
} }
format pp_decl_has_metavars(formatter const & fmt, environment const & env, options const & opts, name const & n,
expr const & e, bool is_type) {
format r("failed to add declaration '");
r += format(n);
r += format("' to environment, ");
if (is_type)
r += format("type");
else
r += format("value");
r += format(" has metavariables");
r += pp_indent_expr(fmt, env, opts, e);
return r;
}
} }

2
src/kernel/error_msgs.h
View file

@ -15,4 +15,6 @@ format pp_app_type_mismatch(formatter const & fmt, environment const & env, opti
expr const & expected_type, expr const & given_type); expr const & expected_type, expr const & given_type);
format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n, format pp_def_type_mismatch(formatter const & fmt, environment const & env, options const & opts, name const & n,
expr const & expected_type, expr const & given_type); expr const & expected_type, expr const & given_type);
format pp_decl_has_metavars(formatter const & fmt, environment const & env, options const & opts, name const & n,
expr const & e, bool is_type);
} }

15
src/kernel/type_checker.cpp
View file

@ -433,9 +433,12 @@ type_checker::type_checker(environment const & env):
type_checker::~type_checker() {} type_checker::~type_checker() {}
static void check_no_metavar(environment const & env, expr const & e) { static void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type) {
if (has_metavar(e)) if (has_metavar(e))
throw_kernel_exception(env, "failed to add declaration to environment, it contains metavariables", e); throw_kernel_exception(env, e,
[=](formatter const & fmt, options const & o) {
return pp_decl_has_metavars(fmt, env, o, n, e, is_type);
});
} }
static void check_no_local(environment const & env, expr const & e) { static void check_no_local(environment const & env, expr const & e) {
@ -443,8 +446,8 @@ static void check_no_local(environment const & env, expr const & e) {
throw_kernel_exception(env, "failed to add declaration to environment, it contains local constants", e); throw_kernel_exception(env, "failed to add declaration to environment, it contains local constants", e);
} }
static void check_no_mlocal(environment const & env, expr const & e) { static void check_no_mlocal(environment const & env, name const & n, expr const & e, bool is_type) {
check_no_metavar(env, e); check_no_metavar(env, n, e, is_type);
check_no_local(env, e); check_no_local(env, e);
} }
@ -466,9 +469,9 @@ static void check_duplicated_params(environment const & env, declaration const &
} }
certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) { certified_declaration check(environment const & env, declaration const & d, name_generator const & g, name_set const & extra_opaque, bool memoize) {
check_no_mlocal(env, d.get_type());
if (d.is_definition()) if (d.is_definition())
check_no_mlocal(env, d.get_value()); check_no_mlocal(env, d.get_name(), d.get_value(), false);
check_no_mlocal(env, d.get_name(), d.get_type(), true);
check_name(env, d.get_name()); check_name(env, d.get_name());
check_duplicated_params(env, d); check_duplicated_params(env, d);
type_checker checker1(env, g, mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque)); type_checker checker1(env, g, mk_default_converter(env, optional<module_idx>(), memoize, extra_opaque));