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

feat(kernel/type_checker): add 'check' procedure that uses 'opaque_hints'

Browse source 
The hints only affect performance. If a declaration type checks assuming
some constants are opaque, it should also type check without this
assumption. Of course, it may be much slower.
This commit is contained in:
Leonardo de Moura 2015-06-30 13:11:32 -07:00
parent 772ed111e5
commit e7c3c887b6
3 changed files with 18 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/kernel/environment.h
View file

@ -230,7 +230,8 @@ class name_generator;
Only the type_checker class can create certified declarations.
*/
class certified_declaration {
friend certified_declaration check(environment const & env, declaration const & d, name_generator && g);
friend certified_declaration check(environment const & env, declaration const & d, name_generator && g,
name_predicate const & opaque_hints);
environment_id m_id;
declaration m_declaration;
certified_declaration(environment_id const & id, declaration const & d):m_id(id), m_declaration(d) {}

22
src/kernel/type_checker.cpp
View file

@ -472,20 +472,18 @@ static void check_duplicated_params(environment const & env, declaration const &
}
}
certified_declaration check(environment const & env, declaration const & d, name_generator && g) {
certified_declaration check(environment const & env, declaration const & d, name_generator && g, name_predicate const & pred) {
if (d.is_definition())
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_duplicated_params(env, d);
bool memoize = true;
type_checker checker1(env, g.mk_child(), std::unique_ptr<converter>(new default_converter(env, memoize)));
expr sort = checker1.check(d.get_type(), d.get_univ_params()).first;
checker1.ensure_sort(sort, d.get_type());
type_checker checker(env, g.mk_child(), std::unique_ptr<converter>(new hint_converter<default_converter>(env, pred)));
expr sort = checker.check(d.get_type(), d.get_univ_params()).first;
checker.ensure_sort(sort, d.get_type());
if (d.is_definition()) {
type_checker checker2(env, g.mk_child(), std::unique_ptr<converter>(new default_converter(env, memoize)));
expr val_type = checker2.check(d.get_value(), d.get_univ_params()).first;
if (!checker2.is_def_eq(val_type, d.get_type()).first) {
expr val_type = checker.check(d.get_value(), d.get_univ_params()).first;
if (!checker.is_def_eq(val_type, d.get_type()).first) {
throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt) {
return pp_def_type_mismatch(fmt, d.get_name(), d.get_type(), val_type, true);
});
@ -494,6 +492,14 @@ certified_declaration check(environment const & env, declaration const & d, name
return certified_declaration(env.get_id(), d);
}
certified_declaration check(environment const & env, declaration const & d, name_generator && g) {
return check(env, d, std::move(g), [](name const &) { return false; });
}
certified_declaration check(environment const & env, declaration const & d, name_predicate const & pred) {
return check(env, d, name_generator(*g_tmp_prefix), pred);
}
certified_declaration check(environment const & env, declaration const & d) {
return check(env, d, name_generator(*g_tmp_prefix));
}

2
src/kernel/type_checker.h
View file

@ -243,6 +243,8 @@ void check_no_metavar(environment const & env, name const & n, expr const & e, b
*/
certified_declaration check(environment const & env, declaration const & d, name_generator && g);
certified_declaration check(environment const & env, declaration const & d);
certified_declaration check(environment const & env, declaration const & d, name_generator && g, name_predicate const & opaque_hints);
certified_declaration check(environment const & env, declaration const & d, name_predicate const & opaque_hints);
/**
\brief Create a justification for an application \c e where the expected type must be \c d_type and