From 33bbcd95262544d8fb93ab335b0eca96c68afd99 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 16:20:34 -0700 Subject: [PATCH] chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 2 +- src/kernel/declaration.cpp | 2 +- src/kernel/declaration.h | 2 +- src/kernel/type_checker.cpp | 8 ++++---- src/library/aliases.cpp | 2 +- src/library/coercion.cpp | 4 ++-- src/library/kernel_bindings.cpp | 2 +- src/library/kernel_serializer.cpp | 2 +- src/library/level_names.cpp | 2 +- src/library/module.cpp | 2 +- src/library/scope.cpp | 6 +++--- src/library/update_declaration.cpp | 6 +++--- 12 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 589648807..8b880bb71 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -179,7 +179,7 @@ struct default_converter : public converter { if (is_constant(e)) { if (auto d = m_env.find(const_name(e))) { if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w) - return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_levels(e)), w); + return unfold_name_core(instantiate_params(d->get_value(), d->get_univ_params(), const_levels(e)), w); } } return e; diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 4142137d1..19af64aac 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -55,7 +55,7 @@ bool declaration::is_axiom() const { return is_var_decl() && m_ptr->m_theor bool declaration::is_theorem() const { return is_definition() && m_ptr->m_theorem; } name declaration::get_name() const { return m_ptr->m_name; } -level_param_names const & declaration::get_params() const { return m_ptr->m_params; } +level_param_names const & declaration::get_univ_params() const { return m_ptr->m_params; } expr declaration::get_type() const { return m_ptr->m_type; } bool declaration::is_opaque() const { return m_ptr->m_opaque; } diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 8bff7ce7b..8feff1e15 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -58,7 +58,7 @@ public: bool is_var_decl() const; name get_name() const; - level_param_names const & get_params() const; + level_param_names const & get_univ_params() const; expr get_type() const; expr get_value() const; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 95f5045bd..5558ac92d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -308,7 +308,7 @@ struct type_checker::imp { break; case expr_kind::Constant: { declaration d = m_env.get(const_name(e)); - auto const & ps = d.get_params(); + auto const & ps = d.get_univ_params(); auto const & ls = const_levels(e); if (length(ps) != length(ls)) throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '" << const_name(e) << "', #" @@ -446,7 +446,7 @@ static void check_name(environment const & env, name const & n) { } static void check_duplicated_params(environment const & env, declaration const & d) { - level_param_names ls = d.get_params(); + level_param_names ls = d.get_univ_params(); while (!is_nil(ls)) { auto const & p = head(ls); ls = tail(ls); @@ -464,13 +464,13 @@ certified_declaration check(environment const & env, declaration const & d, name check_name(env, d.get_name()); check_duplicated_params(env, d); type_checker checker1(env, g, mk_default_converter(env, optional(), memoize, extra_opaque)); - checker1.check(d.get_type(), d.get_params()); + checker1.check(d.get_type(), d.get_univ_params()); if (d.is_definition()) { optional midx; if (d.is_opaque()) midx = optional(d.get_module_idx()); type_checker checker2(env, g, mk_default_converter(env, midx, memoize, extra_opaque)); - expr val_type = checker2.check(d.get_value(), d.get_params()); + expr val_type = checker2.check(d.get_value(), d.get_univ_params()); if (!checker2.is_def_eq(val_type, d.get_type())) { throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt, options const & o) { diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index d6cb9bacb..eec0de709 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -69,7 +69,7 @@ environment add_aliases(environment const & env, name const & prefix, name const if (is_prefix_of(prefix, d.get_name())) { name a = d.get_name().replace_prefix(prefix, new_prefix); check_name(env, a, ios); - levels ls = map2(d.get_params(), [](name const &) { return mk_level_placeholder(); }); + levels ls = map2(d.get_univ_params(), [](name const &) { return mk_level_placeholder(); }); expr c = mk_constant(d.get_name(), ls); if (num_fix_params > 0) { expr t = d.get_type(); diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 3c91c7107..c463132d2 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -306,14 +306,14 @@ environment add_coercion(environment const & env, name const & f, name const & C const_name(C_fn) == C && num == args.size() && check_var_args(args) && - check_levels(const_levels(C_fn), d.get_params())) { + check_levels(const_levels(C_fn), d.get_univ_params())) { expr fn = mk_constant(f, const_levels(C_fn)); optional cls = type_to_coercion_class(binding_body(t)); if (!cls) throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'"); else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C) throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself"); - return add_coercion_fn(env, ios)(C, fn, d.get_type(), d.get_params(), num, *cls); + return add_coercion_fn(env, ios)(C, fn, d.get_type(), d.get_univ_params(), num, *cls); } t = binding_body(t); num++; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 6607c60b9..ed5dcf59f 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -851,7 +851,7 @@ DECLARATION_PRED(is_var_decl) DECLARATION_PRED(is_opaque) DECLARATION_PRED(use_conv_opt) static int declaration_get_name(lua_State * L) { return push_name(L, to_declaration(L, 1).get_name()); } -static int declaration_get_params(lua_State * L) { return push_list_name(L, to_declaration(L, 1).get_params()); } +static int declaration_get_params(lua_State * L) { return push_list_name(L, to_declaration(L, 1).get_univ_params()); } static int declaration_get_type(lua_State * L) { return push_expr(L, to_declaration(L, 1).get_type()); } static int declaration_get_value(lua_State * L) { if (to_declaration(L, 1).is_definition()) diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index af5227c8a..4fa9ee405 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -268,7 +268,7 @@ serializer & operator<<(serializer & s, declaration const & d) { } if (d.is_theorem() || d.is_axiom()) k |= 8; - s << k << d.get_name() << d.get_params() << d.get_type(); + s << k << d.get_name() << d.get_univ_params() << d.get_type(); if (d.is_definition()) { s << d.get_value(); if (!d.is_theorem()) diff --git a/src/library/level_names.cpp b/src/library/level_names.cpp index cba6d55b9..05452dbb1 100644 --- a/src/library/level_names.cpp +++ b/src/library/level_names.cpp @@ -96,7 +96,7 @@ declaration sanitize_level_params(declaration const & d) { if (globals.empty()) return d; name_map param_name_map; - level_param_names new_ls = sanitize_level_params(d.get_params(), globals, param_name_map); + level_param_names new_ls = sanitize_level_params(d.get_univ_params(), globals, param_name_map); if (param_name_map.empty()) return d; expr new_type = rename_param_levels(d.get_type(), param_name_map); diff --git a/src/library/module.cpp b/src/library/module.cpp index ace3655e1..670a8bdb3 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -255,7 +255,7 @@ struct import_modules_fn { declaration theorem2axiom(declaration const & decl) { lean_assert(decl.is_theorem()); - return mk_axiom(decl.get_name(), decl.get_params(), decl.get_type()); + return mk_axiom(decl.get_name(), decl.get_univ_params(), decl.get_type()); } void import_decl(deserializer & d, module_idx midx) { diff --git a/src/library/scope.cpp b/src/library/scope.cpp index 204d134e1..174eb16de 100644 --- a/src/library/scope.cpp +++ b/src/library/scope.cpp @@ -164,7 +164,7 @@ public: void add_local_decl(declaration const & d, binder_info const & bi) { lean_assert(d.is_var_decl()); - lean_assert(is_nil(d.get_params())); + lean_assert(is_nil(d.get_univ_params())); expr new_type = convert(d.get_type()); dependencies var_deps = mk_var_deps(); var_deps.push_back(mk_constant(d.get_name())); @@ -179,7 +179,7 @@ public: expr new_type = convert(d.get_type()); expr new_value = convert(d.get_value()); level_param_names level_deps = mk_level_deps(); - level_param_names new_ls = append(level_deps, d.get_params()); + level_param_names new_ls = append(level_deps, d.get_univ_params()); dependencies var_deps = mk_var_deps(); new_type = Pi(new_type, var_deps); new_value = Fun(new_value, var_deps); @@ -239,7 +239,7 @@ environment add_global_level(environment const & env, name const & l) { static environment save_section_declaration(environment const & env, declaration const & d, binder_info const & bi) { if (d.is_var_decl()) { - if (!is_nil(d.get_params())) + if (!is_nil(d.get_univ_params())) throw exception("section parameters and axiom cannot contain universe level parameter"); return add(env, [=](abstraction_context & ctx) { static_cast(ctx).add_local_decl(d, bi); diff --git a/src/library/update_declaration.cpp b/src/library/update_declaration.cpp index 00f5ebfb8..fa997f4f2 100644 --- a/src/library/update_declaration.cpp +++ b/src/library/update_declaration.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura namespace lean { static declaration update_declaration(declaration d, optional const & ps, optional const & type, optional const & value) { - level_param_names _ps = ps ? *ps : d.get_params(); + level_param_names _ps = ps ? *ps : d.get_univ_params(); expr _type = type ? *type : d.get_type(); expr _value; if (d.is_definition()) { @@ -18,14 +18,14 @@ static declaration update_declaration(declaration d, optional lean_assert(!value); } if (d.is_var_decl()) { - if (is_eqp(d.get_type(), _type) && is_eqp(d.get_params(), _ps)) + if (is_eqp(d.get_type(), _type) && is_eqp(d.get_univ_params(), _ps)) return d; if (d.is_axiom()) return mk_axiom(d.get_name(), _ps, _type); else return mk_var_decl(d.get_name(), _ps, _type); } else { - if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_params(), _ps)) + if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_univ_params(), _ps)) return d; if (d.is_theorem()) return mk_theorem(d.get_name(), _ps, _type, _value);