From b2bebbf75d82a177182cb19a29c2e86634512b62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 Jun 2018 08:43:47 -0700 Subject: [PATCH] chore(kernel): check_no_mlocal ==> check_no_metavar_no_fvar --- src/kernel/inductive/inductive.cpp | 2 +- src/kernel/old_type_checker.h | 2 +- src/kernel/type_checker.cpp | 12 ++++++------ src/kernel/type_checker.h | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 0c19b16309..b3d439d0c3 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -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; diff --git a/src/kernel/old_type_checker.h b/src/kernel/old_type_checker.h index 3b405ab787..6e79d41a90 100644 --- a/src/kernel/old_type_checker.h +++ b/src/kernel/old_type_checker.h @@ -130,7 +130,7 @@ public: typedef std::shared_ptr 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); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index a266fe959c..9772d07be3 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -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()); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index e5ac56c6d7..e387f5c048 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -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);