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

chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 16:20:34 -07:00
parent 82e1f87e08
commit 33bbcd9526
12 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/converter.cpp
View file

@ -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;

2
src/kernel/declaration.cpp
View file

@ -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; }

2
src/kernel/declaration.h
View file

@ -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;

8
src/kernel/type_checker.cpp
View file

@ -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<module_idx>(), 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<module_idx> midx;
if (d.is_opaque())
midx = optional<module_idx>(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) {

2
src/library/aliases.cpp
View file

@ -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<level>(d.get_params(), [](name const &) { return mk_level_placeholder(); });
levels ls = map2<level>(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();

4
src/library/coercion.cpp
View file

@ -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<coercion_class> 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++;

2
src/library/kernel_bindings.cpp
View file

@ -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())

2
src/library/kernel_serializer.cpp
View file

@ -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())

2
src/library/level_names.cpp
View file

@ -96,7 +96,7 @@ declaration sanitize_level_params(declaration const & d) {
if (globals.empty())
return d;
name_map<name> 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);

2
src/library/module.cpp
View file

@ -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) {

6
src/library/scope.cpp
View file

@ -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<abstraction_context_imp&>(ctx).add_local_decl(d, bi);

6
src/library/update_declaration.cpp
View file

@ -9,7 +9,7 @@ Author: Leonardo de Moura
namespace lean {
static declaration update_declaration(declaration d, optional<level_param_names> const & ps,
optional<expr> const & type, optional<expr> 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<level_param_names>
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);