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

chore(kernel): check_no_mlocal ==> check_no_metavar_no_fvar

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-12 08:43:47 -07:00
parent 42d58580e6
commit b2bebbf75d
4 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/inductive/inductive.cpp
View file

@ -390,7 +390,7 @@ struct add_inductive_fn {
expr t = intro_rule_type(ir);
name n = intro_rule_name(ir);
/* make sure intro rule type does not contain locals nor metavariables. */
check_no_mlocal(m_env, n, t);
check_no_metavar_no_fvar(m_env, n, t);
tc().check(t, m_decl.m_level_params);
unsigned i = 0;
bool found_rec = false;

2
src/kernel/old_type_checker.h
View file

@ -130,7 +130,7 @@ public:
typedef std::shared_ptr<old_type_checker> old_type_checker_ref;
void check_no_metavar(environment const & env, name const & n, expr const & e);
void check_no_mlocal(environment const & env, name const & n, expr const & e);
void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e);
void check_decl_type(environment const & env, declaration const & d);
void check_decl_value(environment const & env, declaration const & d);

12
src/kernel/type_checker.cpp
View file

@ -734,14 +734,14 @@ void check_no_metavar(environment const & env, name const & n, expr const & e) {
throw declaration_has_metavars_exception(env, n, e);
}
static void check_no_local(environment const & env, name const & n, expr const & e) {
if (has_local(e))
static void check_no_fvar(environment const & env, name const & n, expr const & e) {
if (has_fvar(e))
throw declaration_has_free_vars_exception(env, n, e);
}
void check_no_mlocal(environment const & env, name const & n, expr const & e) {
void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e) {
check_no_metavar(env, n, e);
check_no_local(env, n, e);
check_no_fvar(env, n, e);
}
static void check_name(environment const & env, name const & n) {
@ -763,7 +763,7 @@ static void check_duplicated_params(environment const & env, declaration const &
}
static void check_definition(environment const & env, declaration const & d, type_checker & checker) {
check_no_mlocal(env, d.get_name(), d.get_value());
check_no_metavar_no_fvar(env, d.get_name(), d.get_value());
expr val_type = checker.check(d.get_value(), d.get_univ_params());
if (!checker.is_def_eq(val_type, d.get_type())) {
throw definition_type_mismatch_exception(env, d, val_type);
@ -771,7 +771,7 @@ static void check_definition(environment const & env, declaration const & d, typ
}
static void check_decl_type(environment const & env, declaration const & d, type_checker & checker) {
check_no_mlocal(env, d.get_name(), d.get_type());
check_no_metavar_no_fvar(env, d.get_name(), d.get_type());
check_name(env, d.get_name());
check_duplicated_params(env, d);
expr sort = checker.check(d.get_type(), d.get_univ_params());

2
src/kernel/type_checker.h
View file

@ -134,7 +134,7 @@ public:
};
void check_no_metavar(environment const & env, name const & n, expr const & e);
void check_no_mlocal(environment const & env, name const & n, expr const & e);
void check_no_metavar_no_fvar(environment const & env, name const & n, expr const & e);
void check_decl_type(environment const & env, declaration const & d);
void check_decl_value(environment const & env, declaration const & d);