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

feat(kernel,library,frontends/lean,api): remove global universe levels from kernel and APIs

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-08 17:41:44 -08:00
parent 32e6442d0a
commit 3d603ec28e
26 changed files with 39 additions and 252 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
doc/export_format.md
View file

@ -57,14 +57,13 @@ The following commands are used to create universe terms in the export file.
<uidx'> #UM <uidx_1> <uidx_2>
<uidx'> #UIM <uidx_1> <uidx_2>
<uidx'> #UP <nidx>
<uidx'> #UG <nidx>
```
In the commands above, `uidx`, `uidx_1` and `uidx_2` denote the unique identifier of existing universe terms,
`nidx` the unique identifier of existing hierarchical names, and `nidx'` is the identifier for the universe
term being defined. The command `#US` defines the _successor_ universe for `uidx`, the `#UM` the maximum universe for `uidx_1` and `uidx_2`,
and `#UIM` is the "impredicative" maximum. It is defined as zero if `uidx_2` evaluates to zero, and `#UM` otherwise.
The command `#UP` defines the universe parameter with name `nidx`, and `#UG` the global universe with name `nidx`.
The command `#UP` defines the universe parameter with name `nidx`.
Here is the sequence of commands for creating the universe term `imax (max 2 l1) l2`.
```
1 #NS 0 l1
@ -141,15 +140,6 @@ We annotate some commands with comments of the form `-- ...` to make the example
9 #EA 8 5 -- vector.{1} nat (nat.succ (nat.succ (nat.succ nat.zero)))
```
Global universe level declaration
---------------------------------
The command
```
#UNI <nidx>
```
declares a global universe with name `nidx`.
Definitions and Axioms
----------------------

1
library/init/meta/level.lean
View file

@ -13,7 +13,6 @@ inductive level
| max : level → level → level
| imax : level → level → level
| param : name → level
| global : name → level
| mvar : name → level
instance : inhabited level :=

22
src/api/env.cpp
View file

@ -19,14 +19,6 @@ lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex) {
LEAN_CATCH;
}
lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(e);
check_nonnull(u);
*r = of_env(new environment(module::add_universe(to_env_ref(e), to_name_ref(u))));
LEAN_CATCH;
}
lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex) {
LEAN_TRY;
check_nonnull(e);
@ -51,10 +43,6 @@ unsigned lean_env_trust_level(lean_env e) {
return e ? to_env_ref(e).trust_lvl() : 0;
}
lean_bool lean_env_contains_univ(lean_env e, lean_name n) {
return e && n && to_env_ref(e).is_universe(to_name_ref(n));
}
lean_bool lean_env_contains_decl(lean_env e, lean_name n) {
return e && n && to_env_ref(e).find(to_name_ref(n));
}
@ -87,13 +75,3 @@ lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exceptio
return lean_true;
LEAN_CATCH;
}
lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex) {
LEAN_TRY;
check_nonnull(e);
to_env_ref(e).for_each_universe([&](name const & u) {
f(of_name(new name(u)));
});
return lean_true;
LEAN_CATCH;
}

8
src/api/lean_env.h
View file

@ -28,9 +28,6 @@ lean_bool lean_env_mk_std(unsigned t, lean_env * r, lean_exception * ex);
/** Trust all macros implemented in Lean, and do no retype-check imported modules */
#define LEAN_TRUST_HIGH 100000
/** \brief Add a new global universe with name \c u.
\remark exceptions: LEAN_KERNEL_EXCEPTION */
lean_bool lean_env_add_univ(lean_env e, lean_name u, lean_env * r, lean_exception * ex);
/** \brief Create a new environment by adding the given certified declaration \c d to the environment \c e.
\remark exceptions: LEAN_KERNEL_EXCEPTION */
lean_bool lean_env_add(lean_env e, lean_cert_decl d, lean_env * r, lean_exception * ex);
@ -47,8 +44,6 @@ void lean_env_del(lean_env e);
/** \brief Return the trust level of the given environment */
unsigned lean_env_trust_level(lean_env e);
/** \brief Return true iff \c e contains a global universe with name \c n. */
lean_bool lean_env_contains_univ(lean_env e, lean_name n);
/** \brief Return true iff \c e contains a declaration with name \c n. */
lean_bool lean_env_contains_decl(lean_env e, lean_name n);
/** \brief Store in \c d the declaration with name \c n in \c e.
@ -65,9 +60,6 @@ lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex);
/** \brief Execute \c f for each declaration in \c env.
\remark Every declaration passed to \c f must be disposed using \c lean_decl_del. */
lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex);
/** \brief Execute \c f for each global universe in \c env.
\remark Every name passed to \c f must be disposed using \c lean_name_del. */
lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex);
/*@}*/
/*@}*/

1
src/api/univ.cpp
View file

@ -97,7 +97,6 @@ lean_univ_kind lean_univ_get_kind(lean_univ u) {
case level_kind::IMax: return LEAN_UNIV_IMAX;
case level_kind::Param: return LEAN_UNIV_PARAM;
case level_kind::Meta: return LEAN_UNIV_META;
case level_kind::Global: break; // TODO(Leo): delete
}
lean_unreachable();
}

1
src/checker/simple_pp.cpp
View file

@ -82,7 +82,6 @@ struct simple_pp_fn {
pp_level(imax_lhs(l)).maybe_paren(1),
pp_level(imax_rhs(l)).maybe_paren(1)}), 0);
case level_kind::Param: return pp_name(param_id(l));
case level_kind::Global: return pp_name(global_id(l));
case level_kind::Meta: return pp_meta(meta_id(l));
}
lean_unreachable();

3
src/checker/text_import.cpp
View file

@ -154,9 +154,6 @@ struct text_importer {
} else if (kind == "#UP") {
unsigned i1; in >> i1;
m_level[idx] = mk_param_univ(m_name.at(i1));
} else if (kind == "#UG") {
unsigned i1; in >> i1;
m_level[idx] = mk_global_univ(m_name.at(i1));
} else if (kind == "#EV") {
unsigned v; in >> v;
m_expr[idx] = mk_var(v);

2
src/frontends/lean/parser.cpp
View file

@ -520,8 +520,6 @@ void parser::clear_expr_locals() {
}
void parser::add_local_level(name const & n, level const & l, bool is_variable) {
if (m_env.is_universe(n))
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
if (m_local_level_decls.contains(n))
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
m_local_level_decls.insert(n, l);

2
src/frontends/lean/parser_state.cpp
View file

@ -355,8 +355,6 @@ void parser_state::clear_expr_locals() {
void parser_state::add_local_level(name const & n, level const & l, bool is_variable) {
ensure_exclusive_context();
if (env().is_universe(n))
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a global universe");
if (m_context->m_local_level_decls.contains(n))
throw exception(sstream() << "invalid universe declaration, '" << n << "' shadows a local universe");
m_context->m_local_level_decls.insert(n, l);

4
src/frontends/lean/pp.cpp
View file

@ -341,7 +341,7 @@ void pretty_fn::set_options(options const & o) {
}
format pretty_fn::pp_child(level const & l) {
if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
if (is_explicit(l) || is_param(l) || is_meta(l)) {
return pp_level(l);
} else {
return paren(pp_level(l));
@ -388,8 +388,6 @@ format pretty_fn::pp_level(level const & l) {
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
return format(param_id(l));
case level_kind::Global:
return format(global_id(l));
case level_kind::Meta:
return pp_meta(l);
case level_kind::Succ: {

33
src/kernel/environment.cpp
View file

@ -68,8 +68,8 @@ bool environment_id::is_descendant(environment_id const & id) const {
return false;
}
environment::environment(header const & h, environment_id const & ancestor, declarations const & d, name_set const & g, extensions const & exts):
m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {}
environment::environment(header const & h, environment_id const & ancestor, declarations const & d, extensions const & exts):
m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_extensions(exts) {}
environment::environment(unsigned trust_lvl):
environment(trust_lvl, mk_id_normalizer_extension())
@ -104,24 +104,7 @@ environment environment::add(certified_declaration const & d) const {
name const & n = d.get_declaration().get_name();
if (find(n))
throw_already_declared(*this, n);
return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_global_levels, m_extensions);
}
environment environment::add_universe(name const & n) const {
if (m_global_levels.contains(n))
throw_kernel_exception(*this,
"invalid global universe level declaration, environment already contains a universe level with the given name");
return environment(m_header, m_id, m_declarations, insert(m_global_levels, n), m_extensions);
}
environment environment::remove_universe(name const & n) const {
if (!m_global_levels.contains(n))
throw_kernel_exception(*this, "no universe of the given name");
return environment(m_header, m_id, m_declarations, erase(m_global_levels, n), m_extensions);
}
bool environment::is_universe(name const & n) const {
return m_global_levels.contains(n);
return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_extensions);
}
environment environment::replace(certified_declaration const & t) const {
@ -139,11 +122,11 @@ environment environment::replace(certified_declaration const & t) const {
throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same type");
if (ax->get_univ_params() != t.get_declaration().get_univ_params())
throw_kernel_exception(*this, "invalid replacement of axiom with theorem, the 'replace' operation can only be used when the axiom and theorem have the same universe parameters");
return environment(m_header, m_id, insert(m_declarations, n, t.get_declaration()), m_global_levels, m_extensions);
return environment(m_header, m_id, insert(m_declarations, n, t.get_declaration()), m_extensions);
}
environment environment::forget() const {
return environment(m_header, environment_id(), m_declarations, m_global_levels, m_extensions);
return environment(m_header, environment_id(), m_declarations, m_extensions);
}
class extension_manager {
@ -201,17 +184,13 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
if (id >= new_exts->size())
new_exts->resize(id+1);
(*new_exts)[id] = ext;
return environment(m_header, m_id, m_declarations, m_global_levels, new_exts);
return environment(m_header, m_id, m_declarations, new_exts);
}
void environment::for_each_declaration(std::function<void(declaration const & d)> const & f) const {
m_declarations.for_each([&](name const &, declaration const & d) { return f(d); });
}
void environment::for_each_universe(std::function<void(name const & n)> const & f) const {
m_global_levels.for_each([&](name const & n) { return f(n); });
}
class environment_check_task : public task<bool> {
environment m_env;
public:

22
src/kernel/environment.h
View file

@ -102,10 +102,9 @@ class environment {
header m_header;
environment_id m_id;
declarations m_declarations;
name_set m_global_levels;
extensions m_extensions;
environment(header const & h, environment_id const & id, declarations const & d, name_set const & global_levels, extensions const & ext);
environment(header const & h, environment_id const & id, declarations const & d, extensions const & ext);
public:
environment(unsigned trust_lvl = 0);
@ -134,21 +133,6 @@ public:
/** \brief Return declaration with name \c n. Throws and exception if declaration does not exist in this environment. */
declaration get(name const & n) const;
/**
\brief Add a new global universe level with name \c n
This method throws an exception if the environment already contains a level named \c n.
*/
environment add_universe(name const & n) const;
/**
\brief Remove global universe level with name \c n
This method throws an exception if the environment does not contain a level named \c n.
*/
environment remove_universe(name const & n) const;
/** \brief Return true iff the environment has a universe level named \c n. */
bool is_universe(name const & n) const;
/**
\brief Extends the current environment with the given (certified) declaration
This method throws an exception if:
@ -194,14 +178,10 @@ public:
/** \brief Apply the function \c f to each declaration */
void for_each_declaration(std::function<void(declaration const & d)> const & f) const;
/** \brief Apply the function \c f to each universe */
void for_each_universe(std::function<void(name const & u)> const & f) const;
/** \brief Return true iff declarations and extensions of e1 and e2 are pointer equal */
friend bool is_eqp(environment const & e1, environment const & e2) {
return
is_eqp(e1.m_declarations, e2.m_declarations) &&
is_eqp(e1.m_global_levels, e2.m_global_levels) &&
e1.m_extensions.get() == e2.m_extensions.get();
}

78
src/kernel/level.cpp
View file

@ -37,17 +37,16 @@ struct level_cell {
struct level_composite : public level_cell {
unsigned m_depth;
unsigned m_has_param:1;
unsigned m_has_global:1;
unsigned m_has_meta:1;
level_composite(level_kind k, unsigned h, unsigned d, bool has_param, bool has_global, bool has_meta):
level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_global(has_global), m_has_meta(has_meta) {}
level_composite(level_kind k, unsigned h, unsigned d, bool has_param, bool has_meta):
level_cell(k, h), m_depth(d), m_has_param(has_param), m_has_meta(has_meta) {}
};
bool is_composite(level const & l) {
switch (kind(l)) {
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return true;
case level_kind::Param: case level_kind::Global: case level_kind::Meta: case level_kind::Zero:
case level_kind::Param: case level_kind::Meta: case level_kind::Zero:
return false;
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -62,7 +61,7 @@ struct level_succ : public level_composite {
level m_l;
bool m_explicit;
level_succ(level const & l):
level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_global(l), has_meta(l)),
level_composite(level_kind::Succ, hash(hash(l), 17u), get_depth(l) + 1, has_param(l), has_meta(l)),
m_l(l),
m_explicit(is_explicit(l)) {}
};
@ -78,7 +77,6 @@ struct level_max_core : public level_composite {
hash(hash(l1), hash(l2)),
std::max(get_depth(l1), get_depth(l2)) + 1,
has_param(l1) || has_param(l2),
has_global(l1) || has_global(l2),
has_meta(l1) || has_meta(l2)),
m_lhs(l1), m_rhs(l2) {
lean_assert(!is_explicit(l1) || !is_explicit(l2));
@ -100,11 +98,11 @@ struct level_param_core : public level_cell {
level_param_core(level_kind k, name const & id):
level_cell(k, hash(id.hash(), static_cast<unsigned>(k))),
m_id(id) {
lean_assert(k == level_kind::Meta || k == level_kind::Param || k == level_kind::Global);
lean_assert(k == level_kind::Meta || k == level_kind::Param);
}
};
bool is_param_core(level const & l) { return is_param(l) || is_global(l) || is_meta(l); }
bool is_param_core(level const & l) { return is_param(l) || is_meta(l); }
static level_param_core const & to_param_core(level const & l) {
lean_assert(is_param_core(l));
@ -112,10 +110,9 @@ static level_param_core const & to_param_core(level const & l) {
}
name const & param_id(level const & l) { lean_assert(is_param(l)); return to_param_core(l).m_id; }
name const & global_id(level const & l) { lean_assert(is_global(l)); return to_param_core(l).m_id; }
name const & meta_id(level const & l) { lean_assert(is_meta(l)); return to_param_core(l).m_id; }
name const & level_id(level const & l) {
lean_assert(is_param(l) || is_global(l) || is_meta(l));
lean_assert(is_param(l) || is_meta(l));
return to_param_core(l).m_id;
}
@ -127,7 +124,7 @@ void level_cell::dealloc() {
case level_kind::Max: case level_kind::IMax:
delete static_cast<level_max_core*>(this);
break;
case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Param: case level_kind::Meta:
delete static_cast<level_param_core*>(this);
break;
case level_kind::Zero:
@ -138,7 +135,7 @@ void level_cell::dealloc() {
unsigned get_depth(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
return 1;
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return to_composite(l).m_depth;
@ -148,7 +145,7 @@ unsigned get_depth(level const & l) {
bool has_param(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Meta: case level_kind::Global:
case level_kind::Zero: case level_kind::Meta:
return false;
case level_kind::Param:
return true;
@ -158,21 +155,9 @@ bool has_param(level const & l) {
lean_unreachable(); // LCOV_EXCL_LINE
}
bool has_global(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
return false;
case level_kind::Global:
return true;
case level_kind::Succ: case level_kind::Max: case level_kind::IMax:
return to_composite(l).m_has_param;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
bool has_meta(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global:
case level_kind::Zero: case level_kind::Param:
return false;
case level_kind::Meta:
return true;
@ -186,7 +171,7 @@ bool is_explicit(level const & l) {
switch (kind(l)) {
case level_kind::Zero:
return true;
case level_kind::Param: case level_kind::Global: case level_kind::Meta: case level_kind::Max: case level_kind::IMax:
case level_kind::Param: case level_kind::Meta: case level_kind::Max: case level_kind::IMax:
return false;
case level_kind::Succ:
return to_level_succ(l).m_explicit;
@ -252,7 +237,6 @@ level mk_imax(level const & l1, level const & l2) {
}
level mk_param_univ(name const & n) { return cache(level(new level_param_core(level_kind::Param, n))); }
level mk_global_univ(name const & n) { return cache(level(new level_param_core(level_kind::Global, n))); }
level mk_meta_univ(name const & n) { return cache(level(new level_param_core(level_kind::Meta, n))); }
static level * g_level_zero = nullptr;
@ -308,7 +292,7 @@ bool operator==(level const & l1, level const & l2) {
switch (kind(l1)) {
case level_kind::Zero:
return true;
case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Param: case level_kind::Meta:
return to_param_core(l1).m_id == to_param_core(l2).m_id;
case level_kind::Max: case level_kind::IMax: case level_kind::Succ:
if (to_composite(l1).m_depth != to_composite(l2).m_depth)
@ -316,7 +300,7 @@ bool operator==(level const & l1, level const & l2) {
break;
}
switch (kind(l1)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Max: case level_kind::IMax:
return
@ -338,7 +322,7 @@ bool operator==(level const & l1, level const & l2) {
bool is_not_zero(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
return false;
case level_kind::Succ:
return true;
@ -366,7 +350,7 @@ bool is_lt(level const & a, level const & b, bool use_hash) {
switch (kind(a)) {
case level_kind::Zero:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Param: case level_kind::Meta:
return to_param_core(a).m_id < to_param_core(b).m_id;
case level_kind::Max: case level_kind::IMax:
if (to_max_core(a).m_lhs != to_max_core(b).m_lhs)
@ -391,7 +375,6 @@ bool is_lt(levels const & as, levels const & bs, bool use_hash) {
}
bool has_param(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_param(l); }); }
bool has_global(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_global(l); }); }
bool has_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
void for_each_level_fn::apply(level const & l) {
@ -401,7 +384,8 @@ void for_each_level_fn::apply(level const & l) {
case level_kind::Succ: apply(succ_of(l)); break;
case level_kind::Max: case level_kind::IMax: apply(to_max_core(l).m_lhs); apply(to_max_core(l).m_rhs); break;
case level_kind::Zero: case level_kind::Param:
case level_kind::Meta: case level_kind::Global: break;
case level_kind::Meta:
break;
}
}
@ -414,7 +398,7 @@ level replace_level_fn::apply(level const & l) {
return update_succ(l, apply(succ_of(l)));
case level_kind::Max: case level_kind::IMax:
return update_max(l, apply(to_max_core(l).m_lhs), apply(to_max_core(l).m_rhs));
case level_kind::Zero: case level_kind::Param: case level_kind::Meta: case level_kind::Global:
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
return l;
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -442,18 +426,6 @@ optional<name> get_undef_param(level const & l, level_param_names const & ps) {
return r;
}
optional<name> get_undef_global(level const & l, environment const & env) {
optional<name> r;
for_each(l, [&](level const & l) {
if (!has_global(l) || r)
return false;
if (is_global(l) && !env.is_universe(global_id(l)))
r = global_id(l);
return true;
});
return r;
}
level update_succ(level const & l, level const & new_arg) {
if (is_eqp(succ_of(l), new_arg))
return l;
@ -495,7 +467,7 @@ level instantiate(level const & l, level_param_names const & ps, levels const &
static void print(std::ostream & out, level l);
static void print_child(std::ostream & out, level const & l) {
if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
if (is_explicit(l) || is_param(l) || is_meta(l)) {
print(out, l);
} else {
out << "(";
@ -512,7 +484,7 @@ static void print(std::ostream & out, level l) {
switch (kind(l)) {
case level_kind::Zero:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param: case level_kind::Global:
case level_kind::Param:
out << to_param_core(l).m_id; break;
case level_kind::Meta:
out << "?" << meta_id(l); break;
@ -545,7 +517,7 @@ std::ostream & operator<<(std::ostream & out, level const & l) {
format pp(level l, bool unicode, unsigned indent);
static format pp_child(level const & l, bool unicode, unsigned indent) {
if (is_explicit(l) || is_param(l) || is_meta(l) || is_global(l)) {
if (is_explicit(l) || is_param(l) || is_meta(l)) {
return pp(l, unicode, indent);
} else {
return paren(pp(l, unicode, indent));
@ -560,7 +532,7 @@ format pp(level l, bool unicode, unsigned indent) {
switch (kind(l)) {
case level_kind::Zero:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param: case level_kind::Global:
case level_kind::Param:
return format(to_param_core(l).m_id);
case level_kind::Meta:
return format("?") + format(meta_id(l));
@ -611,7 +583,7 @@ static bool is_norm_lt(level const & a, level const & b) {
switch (kind(l1)) {
case level_kind::Zero: case level_kind::Succ:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Param: case level_kind::Meta:
return to_param_core(l1).m_id < to_param_core(l2).m_id;
case level_kind::Max: case level_kind::IMax:
if (to_max_core(l1).m_lhs != to_max_core(l2).m_lhs)
@ -666,7 +638,7 @@ level normalize(level const & l) {
case level_kind::Succ:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Zero: case level_kind::Param:
case level_kind::Global: case level_kind::Meta:
case level_kind::Meta:
return l;
case level_kind::IMax: {
auto l1 = normalize(imax_lhs(r));

16
src/kernel/level.h
View file

@ -30,12 +30,11 @@ struct level_cell;
Their definitions "mirror" the typing rules for Pi and Sigma.
- Param(n) : A parameter. In Lean, we have universe polymorphic definitions.
- Global(n) : A global level.
- Meta(n) : Placeholder. It is the equivalent of a metavariable for universe levels.
The elaborator is responsible for replacing Meta with level expressions
that do not contain Meta.
*/
enum class level_kind { Zero, Succ, Max, IMax, Param, Global, Meta };
enum class level_kind { Zero, Succ, Max, IMax, Param, Meta };
/**
\brief Universe level.
@ -90,7 +89,6 @@ level mk_max(level const & l1, level const & l2);
level mk_imax(level const & l1, level const & l2);
level mk_succ(level const & l);
level mk_param_univ(name const & n);
level mk_global_univ(name const & n);
level mk_meta_univ(name const & n);
/** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
@ -100,7 +98,6 @@ inline unsigned hash(level const & l) { return l.hash(); }
inline level_kind kind(level const & l) { return l.kind(); }
inline bool is_zero(level const & l) { return kind(l) == level_kind::Zero; }
inline bool is_param(level const & l) { return kind(l) == level_kind::Param; }
inline bool is_global(level const & l) { return kind(l) == level_kind::Global; }
inline bool is_meta(level const & l) { return kind(l) == level_kind::Meta; }
inline bool is_succ(level const & l) { return kind(l) == level_kind::Succ; }
inline bool is_max(level const & l) { return kind(l) == level_kind::Max; }
@ -115,7 +112,6 @@ level const & imax_lhs(level const & l);
level const & imax_rhs(level const & l);
level const & succ_of(level const & l);
name const & param_id(level const & l);
name const & global_id(level const & l);
name const & meta_id(level const & l);
name const & level_id(level const & l);
/**
@ -131,8 +127,6 @@ bool is_explicit(level const & l);
unsigned to_explicit(level const & l);
/** \brief Return true iff \c l contains placeholder (aka meta parameters). */
bool has_meta(level const & l);
/** \brief Return true iff \c l contains globals */
bool has_global(level const & l);
/** \brief Return true iff \c l contains parameters */
bool has_param(level const & l);
@ -160,7 +154,7 @@ bool is_equivalent(level const & lhs, level const & rhs);
level normalize(level const & l);
/**
\brief If the result is true, then forall assignments \c A that assigns all parameters, globals and metavariables occuring
\brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring
in \c l1 and \l2, we have that the universe level l1[A] is bigger or equal to l2[A].
\remark This function assumes l1 and l2 are normalized
@ -173,7 +167,6 @@ bool is_geq(level const & l1, level const & l2);
typedef list<level> levels;
bool has_meta(levels const & ls);
bool has_global(levels const & ls);
bool has_param(levels const & ls);
/** \brief An arbitrary (monotonic) total order on universe level terms. */
@ -206,9 +199,6 @@ bool occurs(level const & u, level const & l);
typedef list<name> level_param_names;
/** \brief If \c l contains a global that is not in \c env, then return it. Otherwise, return none. */
optional<name> get_undef_global(level const & l, environment const & env);
/** \brief If \c l contains a parameter that is not in \c ps, then return it. Otherwise, return none. */
optional<name> get_undef_param(level const & l, level_param_names const & ps);
@ -222,7 +212,7 @@ level instantiate(level const & l, level_param_names const & ps, levels const &
std::ostream & operator<<(std::ostream & out, level const & l);
/**
\brief If the result is true, then forall assignments \c A that assigns all parameters, globals and metavariables occuring
\brief If the result is true, then forall assignments \c A that assigns all parameters and metavariables occuring
in \c l, l[A] != zero.
*/
bool is_not_zero(level const & l);

2
src/kernel/type_checker.cpp
View file

@ -66,8 +66,6 @@ expr type_checker::ensure_pi_core(expr e, expr const & s) {
}
void type_checker::check_level(level const & l, expr const & s) {
if (auto n1 = get_undef_global(l, m_env))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined global universe level '" << *n1 << "'", s);
if (m_params) {
if (auto n2 = get_undef_param(l, *m_params))
throw_kernel_exception(m_env, sstream() << "invalid reference to undefined universe level parameter '"

16
src/library/aliases.cpp
View file

@ -168,13 +168,7 @@ optional<expr> get_local_ref(environment const & env, name const & n) {
return none_expr();
}
static void check_no_shadow(environment const & env, name const & a) {
if (env.is_universe(a))
throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
}
environment add_level_alias(environment const & env, name const & a, name const & l) {
check_no_shadow(env, a);
aliases_ext ext = get_extension(env);
ext.add_level_alias(a, l);
return update(env, ext);
@ -206,16 +200,6 @@ environment add_aliases(environment const & env, name const & prefix, name const
ext.add_expr_alias(a, d.get_name(), overwrite);
}
});
env.for_each_universe([&](name const & u) {
if (is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
name a = u.replace_prefix(prefix, new_prefix);
if (env.is_universe(a))
throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
if (!(is_protected(env, u) && a.is_atomic()) &&
!a.is_anonymous())
ext.add_level_alias(a, u);
}
});
return update(env, ext);
}

4
src/library/aliases.h
View file

@ -40,10 +40,6 @@ optional<name> get_level_alias(environment const & env, name const & n);
\brief Create an alias for each declaration named <tt>prefix.rest</tt>.
The alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>.
The command will also create aliases for universe level declarations.
However, an error is thrown if the universe level shadows existing aliases and/or declarations.
We don't have "choice" construct for universe levels.
\remark \c new_prefix may be the anonymous name.
*/
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,

13
src/library/export.cpp
View file

@ -83,11 +83,6 @@ class exporter {
i = static_cast<unsigned>(m_level2idx.size());
m_out << i << " #UP " << n << "\n";
break;
case level_kind::Global:
n = export_name(global_id(l));
i = static_cast<unsigned>(m_level2idx.size());
m_out << i << " #UG " << n << "\n";
break;
case level_kind::Meta:
throw exception("invalid 'export', universe meta-variables cannot be exported");
}
@ -288,13 +283,6 @@ class exporter {
});
}
void export_global_universes() {
m_env.for_each_universe([&](name const & u) {
unsigned n = export_name(u);
m_out << "#UNI " << n << "\n";
});
}
void export_quotient() {
if (m_quotient_exported) return;
m_quotient_exported = true;
@ -344,7 +332,6 @@ public:
void operator()() {
m_name2idx[{}] = 0;
m_level2idx[{}] = 0;
export_global_universes();
if (has_quotient(m_env))
export_quotient();
export_declarations();

2
src/library/expr_lt.cpp
View file

@ -78,8 +78,6 @@ bool is_lt_no_level_params(level const & a, level const & b) {
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
return false;
case level_kind::Global:
return global_id(a) < global_id(b);
case level_kind::Meta:
return meta_id(a) < meta_id(b);
case level_kind::Max:

3
src/library/kernel_serializer.cpp
View file

@ -24,7 +24,6 @@ public:
switch (k) {
case level_kind::Zero: break;
case level_kind::Param: s << param_id(l); break;
case level_kind::Global: s << global_id(l); break;
case level_kind::Meta: s << meta_id(l); break;
case level_kind::Max: write(max_lhs(l)); write(max_rhs(l)); break;
case level_kind::IMax: write(imax_lhs(l)); write(imax_rhs(l)); break;
@ -46,8 +45,6 @@ public:
return mk_level_zero();
case level_kind::Param:
return mk_param_univ(read_name(d));
case level_kind::Global:
return mk_global_univ(read_name(d));
case level_kind::Meta:
return mk_meta_univ(read_name(d));
case level_kind::Max: {

2
src/library/max_sharing.cpp
View file

@ -29,7 +29,7 @@ struct max_sharing_fn::imp {
level res;
switch (l.kind()) {
case level_kind::Zero: case level_kind::Param:
case level_kind::Global: case level_kind::Meta:
case level_kind::Meta:
res = l;
break;
case level_kind::Succ:

29
src/library/module.cpp
View file

@ -296,27 +296,6 @@ struct import_helper {
}
};
struct glvl_modification : public modification {
LEAN_MODIFICATION("glvl")
name m_name;
glvl_modification() {}
glvl_modification(name const & name) : m_name(name) {}
void perform(environment & env) const override {
env = env.add_universe(m_name);
}
void serialize(serializer & s) const override {
s << m_name;
}
static std::shared_ptr<modification const> deserialize(deserializer & d) {
return std::make_shared<glvl_modification>(read_name(d));
}
};
struct decl_modification : public modification {
LEAN_MODIFICATION("decl")
@ -425,12 +404,6 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
return update(new_env, ext);
}
environment add_universe(environment const & env, name const & l) {
module_ext ext = get_extension(env);
ext.m_module_univs = cons(l, ext.m_module_univs);
return add_and_perform(update(env, ext), std::make_shared<glvl_modification>(l));
}
environment update_module_defs(environment const & env, declaration const & d) {
if (d.is_definition() && !d.is_theorem()) {
module_ext ext = get_extension(env);
@ -725,7 +698,6 @@ module_loader mk_dummy_loader() {
void initialize_module() {
g_ext = new module_ext_reg();
g_object_readers = new object_readers();
glvl_modification::init();
decl_modification::init();
inductive_modification::init();
quot_modification::init();
@ -737,7 +709,6 @@ void finalize_module() {
pos_info_mod::finalize();
inductive_modification::finalize();
decl_modification::finalize();
glvl_modification::finalize();
delete g_object_readers;
delete g_ext;
}

3
src/library/module.h
View file

@ -132,9 +132,6 @@ namespace module {
environment add(environment const & env, std::shared_ptr<modification const> const & modif);
environment add_and_perform(environment const & env, std::shared_ptr<modification const> const & modif);
/** \brief Add the global universe declaration to the environment, and mark it to be exported. */
environment add_universe(environment const & env, name const & l);
/** \brief Add the given declaration to the environment, and mark it to be exported. */
environment add(environment const & env, certified_declaration const & d);

2
src/library/type_context.cpp
View file

@ -1455,8 +1455,6 @@ lbool type_context::is_def_eq_core(level const & l1, level const & l2, bool part
case level_kind::Succ:
return is_def_eq_core(succ_of(l1), succ_of(l2), partial);
case level_kind::Param:
case level_kind::Global:
return l_false;
case level_kind::Meta:
/* This can happen, for example, when we are in tmp_mode, but l1 and l2 are not tmp universe metavariables. */
return l_false;

2
src/library/util.cpp
View file

@ -99,7 +99,7 @@ optional<expr> unfold_app(environment const & env, expr const & e) {
optional<level> dec_level(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Global: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
return none_level();
case level_kind::Succ:
return some_level(succ_of(l));

8
src/library/vm/vm_level.cpp
View file

@ -58,10 +58,6 @@ vm_obj level_param(vm_obj const & n) {
return to_obj(mk_param_univ(to_name(n)));
}
vm_obj level_global(vm_obj const & n) {
return to_obj(mk_global_univ(to_name(n)));
}
vm_obj level_mvar(vm_obj const & n) {
return to_obj(mk_meta_univ(to_name(n)));
}
@ -85,9 +81,6 @@ unsigned level_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
case level_kind::Param:
data.push_back(to_obj(param_id(l)));
break;
case level_kind::Global:
data.push_back(to_obj(global_id(l)));
break;
case level_kind::Meta:
data.push_back(to_obj(meta_id(l)));
break;
@ -159,7 +152,6 @@ void initialize_vm_level() {
DECLARE_VM_BUILTIN(name({"level", "max"}), level_max);
DECLARE_VM_BUILTIN(name({"level", "imax"}), level_imax);
DECLARE_VM_BUILTIN(name({"level", "param"}), level_param);
DECLARE_VM_BUILTIN(name({"level", "global"}), level_global);
DECLARE_VM_BUILTIN(name({"level", "mvar"}), level_mvar);
DECLARE_VM_BUILTIN(name({"level", "has_decidable_eq"}), level_has_decidable_eq);
DECLARE_VM_BUILTIN(name({"level", "lt"}), level_lt);