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

refactor(kernel/level): naming consistency

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-22 09:39:48 -07:00
parent c30f40e4ac
commit bc57c66ae3
30 changed files with 124 additions and 130 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/decl_cmds.cpp
View file

@ -38,11 +38,11 @@ void update_univ_parameters(parser & p, buffer<name> & lp_names, name_set const
static environment declare_universe(parser & p, environment env, name const & n, bool local) {
if (local) {
p.add_local_level(n, mk_param_univ(n), local);
p.add_local_level(n, mk_univ_param(n), local);
} else if (in_section(env)) {
p.add_local_level(n, mk_param_univ(n), false);
p.add_local_level(n, mk_univ_param(n), false);
} else {
p.add_local_level(n, mk_param_univ(n), true);
p.add_local_level(n, mk_univ_param(n), true);
}
return env;
}
@ -147,7 +147,7 @@ static environment declare_var(parser & p, environment env,
/** \brief If we are in a section, then add the new local levels to it. */
static void update_local_levels(parser & p, level_param_names const & new_ls, bool is_variable) {
for (auto const & l : new_ls)
p.add_local_level(l, mk_param_univ(l), is_variable);
p.add_local_level(l, mk_univ_param(l), is_variable);
}
optional<binder_info> parse_binder_info(parser & p, variable_kind k) {

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

@ -35,7 +35,7 @@ bool parse_univ_params(parser & p, buffer<name> & lp_names) {
auto pos0 = p.pos();
name l = p.check_atomic_id_next("invalid declaration, identifier expected");
lp_names.push_back(l);
p.add_local_level(l, mk_param_univ(l));
p.add_local_level(l, mk_univ_param(l));
if (p.pos() == pos0) break;
}
p.next();

6
src/frontends/lean/elaborator.cpp
View file

@ -2060,7 +2060,7 @@ expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type)
static level ground_uvars(level const & l) {
return replace(l, [] (level const & l) {
if (is_meta(l)) {
if (is_mvar(l)) {
return some_level(mk_level_zero());
} else {
return none_level();
@ -3943,7 +3943,7 @@ struct sanitize_param_names_fn : public replace_visitor {
m_idx++;
if (!m_L.contains(new_n)) {
m_new_param_names.push_back(new_n);
return mk_param_univ(new_n);
return mk_univ_param(new_n);
}
}
}
@ -3951,7 +3951,7 @@ struct sanitize_param_names_fn : public replace_visitor {
level sanitize(level const & l) {
name p("u");
return replace(l, [&](level const & l) -> optional<level> {
if (is_meta(l)) {
if (is_mvar(l)) {
if (is_metavar_decl_ref(l) && m_ctx.is_assigned(l)) {
return some_level(sanitize(*m_ctx.get_assignment(l)));
} else {

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

@ -447,7 +447,7 @@ class inductive_cmd_fn {
new_ind_type = elab.elaborate(replace_locals(new_ind_type, params_no_inds, new_params));
new_ind_type = normalize(new_ind_type);
level l = get_datatype_result_level(new_ind_type);
if (is_meta(l)) {
if (is_mvar(l)) {
if (m_explicit_levels)
throw_error("resultant universe must be provided, when using explicit universe levels");
new_ind_type = update_result_sort(new_ind_type, m_u_meta);
@ -457,7 +457,7 @@ class inductive_cmd_fn {
result_level = l;
first = false;
} else {
if (!is_meta(l) && result_level != l) {
if (!is_mvar(l) && result_level != l) {
throw_error("mutually inductive types must live in the same universe");
}
}

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

@ -252,15 +252,15 @@ name pretty_fn::mk_local_name(name const & n, name const & suggested) {
}
level pretty_fn::purify(level const & l) {
if (!m_universes || !m_purify_metavars || !has_meta(l))
if (!m_universes || !m_purify_metavars || !has_mvar(l))
return l;
return replace(l, [&](level const & l) {
if (!has_meta(l))
if (!has_mvar(l))
return some_level(l);
if (is_metavar_decl_ref(l))
return some_level(mk_meta_univ(mk_metavar_name(meta_id(l), "l")));
if (is_meta(l) && !is_idx_metauniv(l))
return some_level(mk_meta_univ(mk_metavar_name(meta_id(l))));
return some_level(mk_univ_mvar(mk_metavar_name(mvar_id(l), "l")));
if (is_mvar(l) && !is_idx_metauniv(l))
return some_level(mk_univ_mvar(mk_metavar_name(mvar_id(l))));
return none_level();
});
}
@ -358,7 +358,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)) {
if (is_explicit(l) || is_param(l) || is_mvar(l)) {
return pp_level(l);
} else {
return paren(pp_level(l));
@ -388,7 +388,7 @@ format pretty_fn::pp_meta(level const & l) {
} else if (is_metavar_decl_ref(l)) {
return format((sstream() << "?l_" << get_metavar_decl_ref_suffix(l)).str());
} else {
return compose(format("?"), format(meta_id(l)));
return compose(format("?"), format(mvar_id(l)));
}
} else {
return format("?");
@ -405,7 +405,7 @@ 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::Meta:
case level_kind::MVar:
return pp_meta(l);
case level_kind::Succ: {
auto p = to_offset(l);

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

@ -779,7 +779,7 @@ struct structure_cmd_fn {
void add_locals() {
if (m_explicit_universe_params) {
for (name const & l : m_level_names)
m_p.add_local_level(l, mk_param_univ(l));
m_p.add_local_level(l, mk_univ_param(l));
}
for (expr const & param : m_params)
m_p.add_local(param);

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

@ -97,7 +97,7 @@ levels collect_local_nonvar_levels(parser & p, level_param_names const & ls) {
buffer<level> section_ls_buffer;
for (name const & l : ls) {
if (p.is_local_level(l) && !p.is_local_level_variable(l))
section_ls_buffer.push_back(mk_param_univ(l));
section_ls_buffer.push_back(mk_univ_param(l));
else
break;
}

4
src/kernel/expr.cpp
View file

@ -367,7 +367,7 @@ expr mk_fvar(name const & n) {
expr mk_const(name const & n, levels const & ls) {
inc(n.raw()); inc(ls.raw());
expr r(mk_cnstr(static_cast<unsigned>(expr_kind::Const), n.raw(), ls.raw(), expr_scalar_size(expr_kind::Const)));
set_scalar<expr_kind::Const>(r, hash(n.hash(), hash(ls)), false, has_meta(ls), false, has_param(ls));
set_scalar<expr_kind::Const>(r, hash(n.hash(), hash(ls)), false, has_mvar(ls), false, has_param(ls));
return r;
}
@ -389,7 +389,7 @@ expr mk_app(expr const & f, expr const & a) {
expr mk_sort(level const & l) {
inc(l.raw());
expr r(mk_cnstr(static_cast<unsigned>(expr_kind::Sort), l.raw(), expr_scalar_size(expr_kind::Sort)));
set_scalar<expr_kind::Sort>(r, hash(l), false, has_meta(l), false, has_param(l));
set_scalar<expr_kind::Sort>(r, hash(l), false, has_mvar(l), false, has_param(l));
return r;
}

2
src/kernel/inductive.cpp
View file

@ -204,7 +204,7 @@ public:
u = name("u").append_after(i);
i++;
}
m_elim_level = mk_param_univ(u);
m_elim_level = mk_univ_param(u);
}
std::cout << ">> elim_level: " << m_elim_level << "\n";
}

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

@ -512,7 +512,7 @@ struct add_inductive_fn {
l = name("l").append_after(i);
i++;
}
m_elim_level = mk_param_univ(l);
m_elim_level = mk_univ_param(l);
}
}

60
src/kernel/level.cpp
View file

@ -31,12 +31,12 @@ inline static void set_level_scalar_fields(object * lvl, unsigned num_objs, unsi
inline static unsigned get_hash(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned>(lvl, num_objs*sizeof(object*)); }
inline static unsigned get_depth(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned>(lvl, num_objs*sizeof(object*) + sizeof(unsigned)); }
inline static bool get_has_param(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned)); }
inline static bool get_has_meta(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned) + sizeof(unsigned char)); }
inline static bool get_has_mvar(object * lvl, unsigned num_objs) { return cnstr_scalar<unsigned char>(lvl, num_objs*sizeof(object*) + 2*sizeof(unsigned) + sizeof(unsigned char)); }
level mk_succ(level const & l) {
inc(l.raw());
level r(mk_cnstr(static_cast<unsigned>(level_kind::Succ), l.raw(), g_level_num_scalars));
set_level_scalar_fields(r.raw(), 1, hash(hash(l), 17u), get_depth(l)+1, has_param(l), has_meta(l));
set_level_scalar_fields(r.raw(), 1, hash(hash(l), 17u), get_depth(l)+1, has_param(l), has_mvar(l));
return r;
}
@ -47,25 +47,25 @@ level mk_max_imax(level_kind k, level const & l1, level const & l2) {
hash(hash(l1), hash(l2)),
std::max(get_depth(l1), get_depth(l2)) + 1,
has_param(l1) || has_param(l2),
has_meta(l1) || has_meta(l2));
has_mvar(l1) || has_mvar(l2));
return level(r);
}
level mk_param_univ(name const & n) {
level mk_univ_param(name const & n) {
inc(n.raw());
return level(mk_cnstr(static_cast<unsigned>(level_kind::Param), n.raw()));
}
level mk_meta_univ(name const & n) {
level mk_univ_mvar(name const & n) {
inc(n.raw());
return level(mk_cnstr(static_cast<unsigned>(level_kind::Meta), n.raw()));
return level(mk_cnstr(static_cast<unsigned>(level_kind::MVar), n.raw()));
}
unsigned level::hash() const {
switch (kind()) {
case level_kind::Zero:
return 31;
case level_kind::Param: case level_kind::Meta:
case level_kind::Param: case level_kind::MVar:
return level_id(*this).hash();
case level_kind::Succ:
return get_hash(raw(), 1);
@ -77,7 +77,7 @@ unsigned level::hash() const {
unsigned get_depth(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
return 1;
case level_kind::Succ:
return get_depth(l.raw(), 1);
@ -89,7 +89,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::Zero: case level_kind::MVar:
return false;
case level_kind::Param:
return true;
@ -101,16 +101,16 @@ bool has_param(level const & l) {
lean_unreachable(); // LCOV_EXCL_LINE
}
bool has_meta(level const & l) {
bool has_mvar(level const & l) {
switch (kind(l)) {
case level_kind::Zero: case level_kind::Param:
return false;
case level_kind::Meta:
case level_kind::MVar:
return true;
case level_kind::Succ:
return get_has_meta(l.raw(), 1);
return get_has_mvar(l.raw(), 1);
case level_kind::Max: case level_kind::IMax:
return get_has_meta(l.raw(), 2);
return get_has_mvar(l.raw(), 2);
}
lean_unreachable(); // LCOV_EXCL_LINE
}
@ -120,7 +120,7 @@ bool is_explicit(level const & l) {
switch (kind(l)) {
case level_kind::Zero:
return true;
case level_kind::Param: case level_kind::Meta: case level_kind::Max: case level_kind::IMax:
case level_kind::Param: case level_kind::MVar: case level_kind::Max: case level_kind::IMax:
return false;
case level_kind::Succ:
return is_explicit(succ_of(l));
@ -194,7 +194,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::Meta:
case level_kind::Param: case level_kind::MVar:
return level_id(l1) == level_id(l2);
case level_kind::Max: case level_kind::IMax: case level_kind::Succ:
if (get_depth(l1) != get_depth(l2))
@ -202,7 +202,7 @@ bool operator==(level const & l1, level const & l2) {
break;
}
switch (kind(l1)) {
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Max: case level_kind::IMax:
return
@ -216,7 +216,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::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
return false;
case level_kind::Succ:
return true;
@ -243,7 +243,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::Meta:
case level_kind::Param: case level_kind::MVar:
return level_id(a) < level_id(b);
case level_kind::Max: case level_kind::IMax:
if (level_lhs(a) != level_lhs(b))
@ -268,7 +268,7 @@ 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_meta(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_meta(l); }); }
bool has_mvar(levels const & ls) { return std::any_of(ls.begin(), ls.end(), [](level const & l) { return has_mvar(l); }); }
void for_each_level_fn::apply(level const & l) {
if (!m_f(l))
@ -279,7 +279,7 @@ void for_each_level_fn::apply(level const & l) {
case level_kind::Max: case level_kind::IMax:
apply(level_lhs(l)); apply(level_rhs(l)); break;
case level_kind::Zero: case level_kind::Param:
case level_kind::Meta:
case level_kind::MVar:
break;
}
}
@ -296,7 +296,7 @@ level replace_level_fn::apply(level const & l) {
level l2 = apply(level_rhs(l));
return update_max(l, l1, l2);
}
case level_kind::Zero: case level_kind::Param: case level_kind::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
return l;
}
lean_unreachable(); // LCOV_EXCL_LINE
@ -365,7 +365,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)) {
if (is_explicit(l) || is_param(l) || is_mvar(l)) {
print(out, l);
} else {
out << "(";
@ -384,8 +384,8 @@ static void print(std::ostream & out, level l) {
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
out << param_id(l); break;
case level_kind::Meta:
out << "?" << meta_id(l); break;
case level_kind::MVar:
out << "?" << mvar_id(l); break;
case level_kind::Succ:
out << "succ "; print_child(out, succ_of(l)); break;
case level_kind::Max: case level_kind::IMax:
@ -415,7 +415,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)) {
if (is_explicit(l) || is_param(l) || is_mvar(l)) {
return pp(l, unicode, indent);
} else {
return paren(pp(l, unicode, indent));
@ -432,8 +432,8 @@ format pp(level l, bool unicode, unsigned indent) {
lean_unreachable(); // LCOV_EXCL_LINE
case level_kind::Param:
return format(param_id(l));
case level_kind::Meta:
return format("?") + format(meta_id(l));
case level_kind::MVar:
return format("?") + format(mvar_id(l));
case level_kind::Succ: {
auto p = to_offset(l);
auto fmt1 = pp_child(p.first, unicode, indent);
@ -482,7 +482,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::Meta:
case level_kind::Param: case level_kind::MVar:
return level_id(l1) < level_id(l2);
case level_kind::Max: case level_kind::IMax:
if (level_lhs(l1) != level_lhs(l2))
@ -537,7 +537,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::Meta:
case level_kind::MVar:
return l;
case level_kind::IMax: {
auto l1 = normalize(imax_lhs(r));
@ -627,7 +627,7 @@ bool is_geq(level const & l1, level const & l2) {
levels param_names_to_levels(level_param_names const & ps) {
buffer<level> ls;
for (auto const & p : ps)
ls.push_back(mk_param_univ(p));
ls.push_back(mk_univ_param(p));
return levels(ls);
}

44
src/kernel/level.h
View file

@ -18,30 +18,24 @@ namespace lean {
class environment;
struct level_cell;
/**
\brief Universe level kinds.
inductive level
| zero : level
| succ : level → level
| max : level → level → level
| imax : level → level → level
| param : name → level
| mvar : name → level
- Zero : It is also Prop level if env.impredicative() is true
- Succ(l) : successor level
- Max(l1, l2) : maximum of two levels
- IMax(l1, l2) : IMax(x, zero) = zero for all x
IMax(x, succ(y)) = Max(x, succ(y)) for all x, y
We use IMax to handle Pi-types, and Max for Sigma-types.
Their definitions "mirror" the typing rules for Pi and Sigma.
- Param(n) : A parameter. In Lean, we have universe polymorphic definitions.
- 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.
We level.imax to handle Pi-types.
*/
enum class level_kind { Zero, Succ, Max, IMax, Param, Meta };
enum class level_kind { Zero, Succ, Max, IMax, Param, MVar };
/** \brief Universe level. */
class level : public object_ref {
friend level mk_succ(level const & l);
friend level mk_max_imax(level_kind k, level const & l1, level const & l2);
friend level mk_param_univ(name const & n);
friend level mk_meta_univ(name const & n);
friend level mk_univ_param(name const & n);
friend level mk_univ_mvar(name const & n);
explicit level(object * o):object_ref(o) { inc(o); }
explicit level(object_ref && o):object_ref(o) {}
public:
@ -64,7 +58,7 @@ public:
bool is_max() const { return kind() == level_kind::Max; }
bool is_imax() const { return kind() == level_kind::IMax; }
bool is_param() const { return kind() == level_kind::Param; }
bool is_meta() const { return kind() == level_kind::Meta; }
bool is_mvar() const { return kind() == level_kind::MVar; }
friend inline level const & max_lhs(level const & l) { lean_assert(l.is_max()); return static_cast<level const &>(cnstr_obj_ref(l, 0)); }
friend inline level const & max_rhs(level const & l) { lean_assert(l.is_max()); return static_cast<level const &>(cnstr_obj_ref(l, 1)); }
@ -74,8 +68,8 @@ public:
friend inline level const & level_rhs(level const & l) { lean_assert(l.is_max() || l.is_imax()); return static_cast<level const &>(cnstr_obj_ref(l, 1)); }
friend inline level const & succ_of(level const & l) { lean_assert(l.is_succ()); return static_cast<level const &>(cnstr_obj_ref(l, 0)); }
friend inline name const & param_id(level const & l) { lean_assert(l.is_param()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
friend inline name const & meta_id(level const & l) { lean_assert(l.is_meta()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
friend inline name const & level_id(level const & l) { lean_assert(l.is_param() || l.is_meta()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
friend inline name const & mvar_id(level const & l) { lean_assert(l.is_mvar()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
friend inline name const & level_id(level const & l) { lean_assert(l.is_param() || l.is_mvar()); return static_cast<name const &>(cnstr_obj_ref(l, 0)); }
};
typedef list_ref<level> levels;
@ -103,8 +97,8 @@ inline level mk_imax_core(level const & l1, level const & l2) { return mk_max_im
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_meta_univ(name const & n);
level mk_univ_param(name const & n);
level mk_univ_mvar(name const & n);
/** \brief Convert (succ^k l) into (l, k). If l is not a succ, then return (l, 0) */
pair<level, unsigned> to_offset(level l);
@ -113,7 +107,7 @@ 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 l.is_zero(); }
inline bool is_param(level const & l) { return l.is_param(); }
inline bool is_meta(level const & l) { return l.is_meta(); }
inline bool is_mvar(level const & l) { return l.is_mvar(); }
inline bool is_succ(level const & l) { return l.is_succ(); }
inline bool is_max(level const & l) { return l.is_max(); }
inline bool is_imax(level const & l) { return l.is_imax(); }
@ -130,7 +124,7 @@ bool is_explicit(level const & l);
\pre is_explicit(l) */
unsigned to_explicit(level const & l);
/** \brief Return true iff \c l contains placeholder (aka meta parameters). */
bool has_meta(level const & l);
bool has_mvar(level const & l);
/** \brief Return true iff \c l contains parameters */
bool has_param(level const & l);
@ -158,7 +152,7 @@ bool is_geq_core(level l1, level l2);
bool is_geq(level const & l1, level const & l2);
bool has_meta(levels const & ls);
bool has_mvar(levels const & ls);
bool has_param(levels const & ls);
/** \brief An arbitrary (monotonic) total order on universe level terms. */

6
src/kernel/quot.cpp
View file

@ -30,7 +30,7 @@ static void check_eq_type(environment const & env) {
throw exception("failed to initialize quot module, unexpected number of universe params at 'eq' type");
local_ctx lctx;
name_generator g;
level u = mk_param_univ(head(decl->m_level_params));
level u = mk_univ_param(head(decl->m_level_params));
expr alpha = lctx.mk_local_decl(g, "α", mk_sort(u), mk_implicit_binder_info());
expr expected_eq_type = lctx.mk_pi(alpha, mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
if (decl->m_type != expected_eq_type)
@ -50,7 +50,7 @@ environment quot_declare(environment const & env) {
name u_name("u");
local_ctx lctx;
name_generator g;
level u = mk_param_univ(u_name);
level u = mk_univ_param(u_name);
expr Sort_u = mk_sort(u);
expr alpha = lctx.mk_local_decl(g, "α", Sort_u, mk_implicit_binder_info());
expr r = lctx.mk_local_decl(g, "r", mk_arrow(alpha, mk_arrow(alpha, mk_Prop())));
@ -68,7 +68,7 @@ environment quot_declare(environment const & env) {
quot_r = mk_app(mk_constant(*quot_consts::g_quot, {u}), alpha, r);
a = lctx.mk_local_decl(g, "a", alpha);
name v_name("v");
level v = mk_param_univ(v_name);
level v = mk_univ_param(v_name);
expr Sort_v = mk_sort(v);
expr beta = lctx.mk_local_decl(g, "β", Sort_v, mk_implicit_binder_info());
expr f = lctx.mk_local_decl(g, "f", mk_arrow(alpha, beta));

8
src/library/aux_definition.cpp
View file

@ -18,14 +18,14 @@ namespace lean {
level closure_helper::collect(level const & l) {
lean_assert(!m_finalized_collection);
return replace(l, [&](level const & l) {
if (is_meta(l)) {
name const & id = meta_id(l);
if (is_mvar(l)) {
name const & id = mvar_id(l);
if (auto r = m_univ_meta_to_param.find(id)) {
return some_level(*r);
} else {
name n = m_prefix.append_after(m_next_idx);
m_next_idx++;
level new_r = mk_param_univ(n);
level new_r = mk_univ_param(n);
m_univ_meta_to_param.insert(id, new_r);
m_univ_meta_to_param_inv.insert(n, l);
m_level_params.push_back(n);
@ -129,7 +129,7 @@ void closure_helper::get_level_closure(buffer<level> & ls) {
if (level const * l = m_univ_meta_to_param_inv.find(n))
ls.push_back(*l);
else
ls.push_back(mk_param_univ(n));
ls.push_back(mk_univ_param(n));
}
}

4
src/library/constructions/brec_on.cpp
View file

@ -53,7 +53,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
unsigned ntypeformers = 1;
level_param_names lps = rec_decl.get_univ_params();
bool is_reflexive = is_reflexive_datatype(tc, n);
level lvl = mk_param_univ(head(lps));
level lvl = mk_univ_param(head(lps));
levels lvls = param_names_to_levels(tail(lps));
level_param_names blvls; // universe level parameters of ibelow/below
level rlvl; // universe level of the resultant type
@ -179,7 +179,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
unsigned ntypeformers = 1;
level_param_names lps = rec_decl.get_univ_params();
bool is_reflexive = is_reflexive_datatype(tc, n);
level lvl = mk_param_univ(head(lps));
level lvl = mk_univ_param(head(lps));
levels lvls = param_names_to_levels(tail(lps));
level rlvl;
level_param_names blps;

2
src/library/constructions/injective.cpp
View file

@ -212,7 +212,7 @@ environment mk_injective_arrow(environment const & env, name const & ir_name) {
type_context_old tctx(env);
name P_lp_name = mk_fresh_lp_name(d.get_univ_params());
expr P = tctx.push_local(name("P"), mk_sort(mk_param_univ(P_lp_name)), mk_strict_implicit_binder_info());
expr P = tctx.push_local(name("P"), mk_sort(mk_univ_param(P_lp_name)), mk_strict_implicit_binder_info());
expr ty = d.get_type();
buffer<expr> args;

2
src/library/constructions/no_confusion.cpp
View file

@ -36,7 +36,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
declaration ind_decl = env.get(n);
declaration cases_decl = env.get(name(n, "cases_on"));
level_param_names lps = cases_decl.get_univ_params();
level plvl = mk_param_univ(head(lps));
level plvl = mk_univ_param(head(lps));
levels ilvls = param_names_to_levels(tail(lps));
level rlvl = plvl;
expr ind_type = instantiate_type_univ_params(ind_decl, ilvls);

4
src/library/expr_lt.cpp
View file

@ -89,8 +89,8 @@ 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::Meta:
return meta_id(a) < meta_id(b);
case level_kind::MVar:
return mvar_id(a) < mvar_id(b);
case level_kind::Max:
if (is_lt_no_level_params(max_lhs(a), max_lhs(b)))
return true;

20
src/library/idx_metavar.cpp
View file

@ -26,7 +26,7 @@ void finalize_idx_metavar() {
}
level mk_idx_metauniv(unsigned i) {
return mk_meta_univ(name(*g_tmp_prefix, i));
return mk_univ_mvar(name(*g_tmp_prefix, i));
}
expr mk_idx_metavar(unsigned i, expr const & type) {
@ -34,15 +34,15 @@ expr mk_idx_metavar(unsigned i, expr const & type) {
}
bool is_idx_metauniv(level const & l) {
if (!is_meta(l))
if (!is_mvar(l))
return false;
name const & n = meta_id(l);
name const & n = mvar_id(l);
return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
}
unsigned to_meta_idx(level const & l) {
lean_assert(is_idx_metauniv(l));
return meta_id(l).get_numeral().get_small_value();
return mvar_id(l).get_numeral().get_small_value();
}
bool is_idx_metavar(expr const & e) {
@ -58,12 +58,12 @@ unsigned to_meta_idx(expr const & e) {
}
bool has_idx_metauniv(level const & l) {
if (!has_meta(l))
if (!has_mvar(l))
return false;
bool found = false;
for_each(l, [&](level const & l) {
if (found) return false;
if (!has_meta(l)) return false;
if (!has_mvar(l)) return false;
if (is_idx_metauniv(l))
found = true;
return true;
@ -111,13 +111,13 @@ struct to_idx_metavars_fn : public replace_visitor {
m_mctx(mctx), m_new_us(new_us), m_new_ms(new_ms) {}
level visit(level const & l) {
if (!has_meta(l)) return l;
if (!has_mvar(l)) return l;
return replace(l, [&](level const & l) {
if (is_meta(l) && !is_idx_metauniv(l)) {
if (auto it = m_lvl_cache.find(meta_id(l)))
if (is_mvar(l) && !is_idx_metauniv(l)) {
if (auto it = m_lvl_cache.find(mvar_id(l)))
return some_level(*it);
level new_l = mk_idx_metauniv(m_new_us.size());
m_lvl_cache.insert(meta_id(l), new_l);
m_lvl_cache.insert(mvar_id(l), new_l);
m_new_us.push_back(new_l);
return some_level(new_l);
}

2
src/library/inductive_compiler/mutual.cpp
View file

@ -721,7 +721,7 @@ class add_mutual_inductive_decl_fn {
level_param_names rec_lp_names = rec_decl.get_univ_params();
bool elim_to_prop = rec_decl.get_num_univ_params() == m_basic_decl.get_lp_names().size();
m_elim_level = elim_to_prop ? mk_level_zero() : mk_param_univ(head(rec_lp_names));
m_elim_level = elim_to_prop ? mk_level_zero() : mk_univ_param(head(rec_lp_names));
levels rec_levels = param_names_to_levels(rec_lp_names);
expr rec_const = mk_constant(rec_name, rec_levels);

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::Meta:
case level_kind::MVar:
res = l;
break;
case level_kind::Succ:

10
src/library/metavar_context.cpp
View file

@ -19,7 +19,7 @@ static expr mk_meta_ref(name const & n) {
}
bool is_metavar_decl_ref(level const & u) {
return is_meta(u) && is_prefix_of(*g_meta_prefix, meta_id(u));
return is_mvar(u) && is_prefix_of(*g_meta_prefix, mvar_id(u));
}
bool is_metavar_decl_ref(expr const & e) {
@ -28,7 +28,7 @@ bool is_metavar_decl_ref(expr const & e) {
name get_metavar_decl_ref_suffix(level const & u) {
lean_assert(is_metavar_decl_ref(u));
return meta_id(u).replace_prefix(*g_meta_prefix, name());
return mvar_id(u).replace_prefix(*g_meta_prefix, name());
}
name get_metavar_decl_ref_suffix(expr const & e) {
@ -43,7 +43,7 @@ static name mk_meta_decl_name() {
level metavar_context::mk_univ_metavar_decl() {
// TODO(Leo): should use name_generator
return mk_meta_univ(mk_meta_decl_name());
return mk_univ_mvar(mk_meta_decl_name());
}
expr metavar_context::mk_metavar_decl(name const & user_name, local_context const & lctx, expr const & type) {
@ -83,7 +83,7 @@ expr metavar_context::get_local(expr const & mvar, name const & n) const {
}
void metavar_context::assign(level const & u, level const & l) {
m_uassignment.insert(meta_id(u), l);
m_uassignment.insert(mvar_id(u), l);
}
void metavar_context::assign(expr const & e, expr const & v) {
@ -97,7 +97,7 @@ void metavar_context::assign(expr const & e, local_context const & lctx, list<ex
optional<level> metavar_context::get_assignment(level const & l) const {
lean_assert(is_metavar_decl_ref(l));
if (auto v = m_uassignment.find(meta_id(l)))
if (auto v = m_uassignment.find(mvar_id(l)))
return some_level(*v);
else
return none_level();

2
src/library/metavar_context.h
View file

@ -75,7 +75,7 @@ public:
bool is_assigned(level const & l) const {
lean_assert(is_metavar_decl_ref(l));
return m_uassignment.contains(meta_id(l));
return m_uassignment.contains(mvar_id(l));
}
bool is_assigned(expr const & m) const {

6
src/library/metavar_util.h
View file

@ -28,11 +28,11 @@ bool in_tmp_mode() const;
template<typename CTX>
bool has_assigned(CTX const & ctx, level const & l) {
if (!has_meta(l))
if (!has_mvar(l))
return false;
bool found = false;
for_each(l, [&](level const & l) {
if (!has_meta(l))
if (!has_mvar(l))
return false; // stop search
if (found)
return false; // stop search
@ -82,7 +82,7 @@ level instantiate_mvars(CTX & ctx, level const & l) {
if (!has_assigned(ctx, l))
return l;
return replace(l, [&](level const & l) {
if (!has_meta(l)) {
if (!has_mvar(l)) {
return some_level(l);
} else if (ctx.is_mvar(l)) {
if (auto v1 = ctx.get_assignment(l)) {

4
src/library/placeholder.cpp
View file

@ -36,8 +36,8 @@ static unsigned next_placeholder_id() {
g_placeholder_id++;
return r;
}
level mk_level_placeholder() { return mk_param_univ(name(*g_placeholder_name, next_placeholder_id())); }
level mk_level_one_placeholder() { return mk_param_univ(*g_placeholder_one_name); }
level mk_level_placeholder() { return mk_univ_param(name(*g_placeholder_name, next_placeholder_id())); }
level mk_level_one_placeholder() { return mk_univ_param(*g_placeholder_one_name); }
static name const & to_prefix(expr_placeholder_kind k) {
switch (k) {
case expr_placeholder_kind::Implicit: return *g_implicit_placeholder_name;

2
src/library/tactic/tactic_state.cpp
View file

@ -655,7 +655,7 @@ vm_obj tactic_mk_meta_var(vm_obj const & t, vm_obj const & s0) {
vm_obj tactic_get_univ_assignment(vm_obj const & u, vm_obj const & s0) {
tactic_state const & s = tactic::to_state(s0);
metavar_context mctx = s.mctx();
if (!is_meta(to_level(u))) {
if (!is_mvar(to_level(u))) {
return tactic::mk_exception("get_univ_assignment tactic failed, argument is not an universe metavariable", s);
} else if (auto r = mctx.get_assignment(to_level(u))) {
return tactic::mk_success(to_obj(*r), s);

8
src/library/type_context.cpp
View file

@ -1452,7 +1452,7 @@ static bool is_max_like(level const & l) {
such that l_i's do not contain m.
If the result is true, then all l_i's are stored in rest. */
static bool generalized_check_meta(level const & m, level const & rhs, bool & found_m, buffer<level> & rest) {
lean_assert(is_meta(m));
lean_assert(is_mvar(m));
if (is_max(rhs)) {
return
generalized_check_meta(m, max_lhs(rhs), found_m, rest) &&
@ -1475,7 +1475,7 @@ static bool generalized_check_meta(level const & m, level const & rhs, bool & fo
?u := max v ?w
*/
bool type_context_old::solve_u_eq_max_u_v(level const & lhs, level const & rhs) {
lean_assert(is_meta(lhs));
lean_assert(is_mvar(lhs));
lean_assert(occurs(lhs, rhs));
buffer<level> rest;
bool found_lhs = false;
@ -1559,7 +1559,7 @@ lbool type_context_old::is_def_eq_core(level const & l1, level const & l2, bool
case level_kind::Succ:
return is_def_eq_core(succ_of(l1), succ_of(l2), partial);
case level_kind::Param:
case level_kind::Meta:
case level_kind::MVar:
/* This can happen, for example, when we are in tmp_mode, but l1 and l2 are not tmp universe metavariables. */
return l_false;
case level_kind::Zero:
@ -3885,7 +3885,7 @@ expr type_context_old::preprocess_class(expr const & type,
return type;
buffer<level> C_levels;
for (level const & l : const_levels(C)) {
if (has_meta(l)) {
if (has_mvar(l)) {
level new_uvar = mk_tmp_univ_mvar();
u_replacements.emplace_back(l, new_uvar);
C_levels.push_back(new_uvar);

2
src/library/util.cpp
View file

@ -133,7 +133,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::Meta:
case level_kind::Zero: case level_kind::Param: case level_kind::MVar:
return none_level();
case level_kind::Succ:
return some_level(succ_of(l));

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

@ -53,11 +53,11 @@ vm_obj level_imax(vm_obj const & o1, vm_obj const & o2) {
}
vm_obj level_param(vm_obj const & n) {
return to_obj(mk_param_univ(to_name(n)));
return to_obj(mk_univ_param(to_name(n)));
}
vm_obj level_mvar(vm_obj const & n) {
return to_obj(mk_meta_univ(to_name(n)));
return to_obj(mk_univ_mvar(to_name(n)));
}
unsigned level_cases_on(vm_obj const & o, buffer<vm_obj> & data) {
@ -79,8 +79,8 @@ 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::Meta:
data.push_back(to_obj(meta_id(l)));
case level_kind::MVar:
data.push_back(to_obj(mvar_id(l)));
break;
}
return static_cast<unsigned>(l.kind());

10
src/tests/kernel/level.cpp
View file

@ -36,7 +36,7 @@ static void tst1() {
lean_assert(mk_imax(two, zero) == zero);
check_serializer(two);
check_serializer(one);
level p = mk_param_univ("p");
level p = mk_univ_param("p");
lean_assert(mk_imax(p, zero) == zero);
lean_assert(mk_max(zero, p) == p);
lean_assert(mk_max(p, zero) == p);
@ -45,16 +45,16 @@ static void tst1() {
check_serializer(mk_imax(p, one));
check_serializer(mk_imax(one, p));
check_serializer(mk_imax(mk_succ(p), p));
std::cout << pp(mk_max(p, mk_max(mk_succ(mk_param_univ("a")), one))) << "\n";
std::cout << pp(mk_max(p, mk_max(mk_succ(mk_univ_param("a")), one))) << "\n";
}
static void tst2() {
level zero;
level one = mk_succ(zero);
level two = mk_succ(one);
level p1 = mk_param_univ("p1");
level p2 = mk_param_univ("p2");
level m1 = mk_meta_univ("m1");
level p1 = mk_univ_param("p1");
level p2 = mk_univ_param("p2");
level m1 = mk_univ_mvar("m1");
lean_assert(is_equivalent(mk_succ(p2), mk_max(p2, mk_succ(p2))));
lean_assert(is_equivalent(mk_max(p1, p2), mk_max(p2, p1)));
lean_assert(!is_equivalent(mk_imax(p1, p2), mk_imax(p2, p1)));