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

chore(library/aliases, frontends/lean): remove local_ref's

Browse source 
We don't need them since we removed parameters
This commit is contained in:
Leonardo de Moura 2019-05-27 20:59:22 -07:00
parent 9aa40e2491
commit fc0ce5b97e
11 changed files with 12 additions and 231 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/builtin_cmds.cpp
View file

@ -110,16 +110,13 @@ static environment redeclare_aliases(environment env, parser & p,
if (!in_section(old_env))
return env;
list<pair<name, expr>> new_entries = p.get_local_entries();
buffer<pair<name, expr>> to_redeclare;
unsigned new_len = length(new_entries);
unsigned old_len = length(old_entries);
lean_assert(old_len >= new_len);
name_set popped_locals;
while (old_len > new_len) {
pair<name, expr> entry = head(old_entries);
if (is_local_ref(entry.second))
to_redeclare.push_back(entry);
else if (is_local_p(entry.second))
if (is_local_p(entry.second))
popped_locals.insert(local_name_p(entry.second));
old_entries = tail(old_entries);
old_len--;
@ -130,11 +127,6 @@ static environment redeclare_aliases(environment env, parser & p,
if (is_param(l) && !is_placeholder(l) && !level_decls.contains(n))
popped_levels.insert(param_id(l));
});
for (auto const & entry : to_redeclare) {
expr new_ref = update_local_ref(entry.second, popped_levels, popped_locals);
if (!is_constant(new_ref))
env = p.add_local_ref(env, entry.first, new_ref);
}
return env;
}

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

@ -333,56 +333,6 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
}
}
environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name, buffer<name> const & lp_names, buffer<expr> const & var_params) {
buffer<expr> params;
buffer<name> lps;
for (name const & u : lp_names) {
if (!p.is_local_level(u)) {
/* Stop, it is a definition parameter */
break;
} else if (p.is_local_level_variable(u)) {
/* Stop, it is a parser universe variable (i.e., it has been declared using the `universe variable` command */
break;
} else {
lps.push_back(u);
}
}
for (expr const & e : var_params) {
if (!p.is_local_decl(e)) {
/* Stop, it is a definition parameter */
break;
} else if (p.is_local_variable(e)) {
/* Stop, it is a parser variable (i.e., it has been declared using the `variable` command */
break;
} else {
/* It is a parser parameter (i.e., it has been declared with the `parameter` command */
params.push_back(e);
}
}
if (lps.empty() && params.empty()) return env;
/*
Procedures such as `collect_implicit_locals` wrap parameter types with the `as_is` annotation.
So, we remove these annotations before creating the local reference using `mk_local_ref`.
Remark: the resulting object is wrapped with the macro `as_atomic`.
Remark: The local constants created here and `collect_implicit_locals` are not structurally
equal. That is, `l : ty` is not structurally equal to `l : as_is ty`, but they are definitionally
equal, and moreover the collection method relies on the fact that they have the same internal
id.
*/
buffer<expr> new_params;
for (unsigned i = 0; i < params.size(); i++) {
expr & param = params[i];
expr type = local_type_p(param);
if (is_as_is(type))
type = get_as_is_arg(type);
expr new_type = replace_locals_preserving_pos_info(type, i, params.data(), new_params.data());
new_params.push_back(copy_pos(param, update_local_p(param, new_type)));
}
expr ref = mk_local_ref(c_real_name, lparams_to_levels(names(lps)), new_params);
return p.add_local_ref(env, c_name, ref);
}
environment add_alias(environment const & env, bool is_protected, name const & c_name, name const & c_real_name) {
if (c_name != c_real_name) {
if (is_protected)

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

@ -173,8 +173,6 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
/** \brief Create an alias c_name --> (c_real_name.{level_params} params)
level_params and params are subsets of lp_names and var_params that were
declared using the parameter command. */
environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name,
buffer<name> const & lp_names, buffer<expr> const & var_params);
/** \brief Add alias for new declaration. */
environment add_alias(environment const & env, bool is_protected, name const & c_name, name const & c_real_name);

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

@ -259,7 +259,6 @@ static environment elab_defs_core(parser & p, decl_cmd_kind kind, cmd_meta const
name c_real_name;
std::tie(env, c_real_name) = declare_definition(env, kind, lp_names, c_name, prv_names[i],
curr_type, some_expr(curr), meta);
env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
new_d_names.push_back(c_real_name);
elab.set_env(env);
}
@ -566,7 +565,6 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), c_name);
environment new_env = env_n.first;
name c_real_name = env_n.second;
new_env = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
if (!meta.m_modifiers.m_is_unsafe && !meta.m_modifiers.m_is_partial &&
(kind == decl_cmd_kind::Definition || kind == decl_cmd_kind::Instance)) {
new_env = mk_smart_unfolding_definition(new_env, p.get_options(), c_real_name);

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

@ -385,25 +385,6 @@ void parser::add_local_expr(name const & n, expr const & p, bool is_variable) {
}
}
environment parser::add_local_ref(environment const & env, name const & n, expr const & ref) {
add_local_expr(n, ref, false);
if (is_as_atomic(ref)) {
buffer<expr> args;
expr f = get_app_args(get_as_atomic_arg(ref), args);
if (is_explicit(f))
f = get_explicit_arg(f);
if (is_constant(f)) {
return ::lean::add_local_ref(env, const_name(f), ref);
} else {
return env;
}
} else if (is_constant(ref) && const_levels(ref)) {
return ::lean::add_local_ref(env, const_name(ref), ref);
} else {
return env;
}
}
static void check_no_metavars(name const & n, expr const & e) {
lean_assert(is_local_p(e));
if (has_metavar(e)) {
@ -1750,11 +1731,6 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only,
return save_pos(mk_local(id, save_pos(mk_expr_placeholder(), p)), p);
}
if (auto ref = get_local_ref(m_env, id)) {
check_no_levels(ls, p);
return copy_with_new_pos(*ref, p);
}
for (name const & ns : get_namespaces(m_env)) {
auto new_id = ns + id;
if (!ns.is_anonymous() && m_env.find(new_id) &&

1
src/frontends/lean/parser.h
View file

@ -461,7 +461,6 @@ public:
bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); }
void add_local_level(name const & n, level const & l, bool is_variable = false);
void add_local_expr(name const & n, expr const & p, bool is_variable = false);
environment add_local_ref(environment const & env, name const & n, expr const & ref);
void add_variable(name const & n, expr const & p);
void add_parameter(name const & n, expr const & p);
void add_local(expr const & p) { return add_local_expr(local_pp_name_p(p), p); }

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

@ -490,94 +490,6 @@ static expr consume_ref_annotations(expr const & e) {
return e;
}
enum local_ref_kind { LocalRef, OverridenLocalRef, NotLocalRef };
static local_ref_kind check_local_ref(environment const & env, expr const & e, unsigned & num_ref_univ_params) {
expr const & rfn = get_app_fn(e);
if (!is_constant(rfn))
return NotLocalRef;
auto ref = get_local_ref(env, const_name(rfn));
if (!ref)
return NotLocalRef;
if (is_as_atomic(*ref))
ref = get_as_atomic_arg(*ref);
buffer<expr> ref_args, e_args;
expr ref_fn = consume_ref_annotations(get_app_args(*ref, ref_args));
get_app_args(e, e_args);
if (!is_constant(ref_fn) || e_args.size() != ref_args.size()) {
return NotLocalRef;
}
for (unsigned i = 0; i < e_args.size(); i++) {
expr e_arg = e_args[i];
expr ref_arg = consume_ref_annotations(ref_args[i]);
if (!is_local(e_arg) || !is_local(ref_arg) || local_pp_name(e_arg) != local_pp_name(ref_arg))
return OverridenLocalRef;
}
num_ref_univ_params = length(const_levels(ref_fn));
buffer<level> lvls;
to_buffer(const_levels(rfn), lvls);
if (lvls.size() < num_ref_univ_params) {
return NotLocalRef;
}
for (unsigned i = 0; i < num_ref_univ_params; i++) {
level const & l = lvls[i];
if (!is_param(l)) {
return OverridenLocalRef;
}
for (unsigned j = 0; j < i; j++)
if (lvls[i] == lvls[j]) {
return OverridenLocalRef;
}
}
return LocalRef;
}
static bool is_local_ref(environment const & env, expr const & e) {
unsigned num_ref_univ_params;
return check_local_ref(env, e, num_ref_univ_params) == LocalRef;
}
auto pretty_fn::pp_overriden_local_ref(expr const & e) -> result {
buffer<expr> args;
expr const & fn = get_app_args(e, args);
result res_fn;
{
flet<bool> set1(m_full_names, true);
res_fn = pp_const(fn, some(0u));
}
format fn_fmt = res_fn.fmt();
if (const_name(fn).is_atomic())
fn_fmt = compose(format("_root_."), fn_fmt);
if (m_implict && has_implicit_args(fn))
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
format r_fmt = fn_fmt;
expr curr_fn = fn;
for (unsigned i = 0; i < args.size(); i++) {
expr const & arg = args[i];
if (m_implict || !is_implicit(curr_fn)) {
result res_arg = pp_child(arg, max_bp());
r_fmt = group(compose(r_fmt, nest(m_indent, compose(line(), res_arg.fmt()))));
}
curr_fn = mk_app(curr_fn, arg);
}
return result(max_bp()-1, r_fmt);
}
// Return some result if \c e is of the form (c p_1 ... p_n) where
// c is a constant, and p_i's are parameters fixed in a section.
auto pretty_fn::pp_local_ref(expr const & e) -> optional<result> {
unsigned num_ref_univ_params;
switch (check_local_ref(m_env, e, num_ref_univ_params)) {
case NotLocalRef:
return optional<result>();
case LocalRef:
return some(pp_const(get_app_fn(e), optional<unsigned>(num_ref_univ_params)));
case OverridenLocalRef:
return some(pp_overriden_local_ref(e));
}
lean_unreachable();
}
static bool is_coercion(expr const & e) {
return is_app_of(e, get_coe_name()) && get_app_num_args(e) >= 4;
}
@ -612,8 +524,6 @@ auto pretty_fn::pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hid
auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
if (is_app(e)) {
if (auto r = pp_local_ref(e))
return add_paren_if_needed(*r, bp);
if (m_numerals) {
if (auto n = to_num(e)) return pp_num(*n, bp);
}
@ -681,10 +591,6 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
name n = const_name(e);
if (m_notation && n == get_unit_unit_name())
return format("()");
if (!num_ref_univ_params) {
if (auto r = pp_local_ref(e))
return *r;
}
// Remark: if num_ref_univ_params is "some", then it contains the number of
// universe levels that are fixed in a section. That is, \c e corresponds to
// a constant in a section which has fixed levels.
@ -869,8 +775,6 @@ auto pretty_fn::pp_field_notation(expr const & e) -> result {
}
auto pretty_fn::pp_app(expr const & e) -> result {
if (auto r = pp_local_ref(e))
return *r;
if (is_default_arg_app(e))
return pp_child(app_fn(e), max_bp());
expr const & fn = app_fn(e);
@ -885,7 +789,7 @@ auto pretty_fn::pp_app(expr const & e) -> result {
bool ignore_hide = true;
result res_fn = pp_child(fn, max_bp()-1, ignore_hide);
format fn_fmt = res_fn.fmt();
if (m_implict && (!is_app(fn) || (is_local_ref(m_env, fn))) && has_implicit_args(fn))
if (m_implict && !is_app(fn) && has_implicit_args(fn))
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
result res_arg = pp_child(app_arg(e), max_bp());
return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));

3
src/frontends/lean/pp.h
View file

@ -123,9 +123,6 @@ private:
result add_paren_if_needed(result const & r, unsigned bp);
std::pair<bool, token_table const *> needs_space_sep(token_table const * t, std::string const &s1, std::string const &s2) const;
result pp_overriden_local_ref(expr const & e);
optional<result> pp_local_ref(expr const & e);
result pp_hide_coercion(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hide = false);
result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);

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

@ -13,10 +13,10 @@ Author: Leonardo de Moura
namespace lean {
environment add_alias(parser & p, environment env, name const & id, name const & full_id,
levels const & ctx_levels, buffer<expr> const & ctx_params) {
if (!empty(ctx_levels) || !ctx_params.empty()) {
expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
env = p.add_local_ref(env, id, r);
}
// if (!empty(ctx_levels) || !ctx_params.empty()) {
// expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
// env = p.add_local_ref(env, id, r);
// }
if (full_id != id)
env = add_expr_alias_rec(env, id, full_id);
return env;

39
src/library/aliases.cpp
View file

@ -27,24 +27,15 @@ struct aliases_ext : public environment_extension {
bool m_in_section;
name_map<names> m_aliases;
name_map<name> m_inv_aliases;
name_map<expr> m_local_refs;
state():m_in_section(false) {}
void add_local_ref(name const & a, expr const & ref) {
m_local_refs.insert(a, ref);
}
void add_expr_alias(name const & a, name const & e, bool overwrite) {
if (auto ref = m_local_refs.find(e)) {
add_local_ref(a, *ref);
} else {
auto it = m_aliases.find(a);
if (it && !overwrite)
m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
else
m_aliases.insert(a, names(e));
m_inv_aliases.insert(e, a);
}
auto it = m_aliases.find(a);
if (it && !overwrite)
m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
else
m_aliases.insert(a, names(e));
m_inv_aliases.insert(e, a);
}
};
@ -76,10 +67,6 @@ struct aliases_ext : public environment_extension {
add_expr_alias(a, e, overwrite);
}
void add_local_ref(name const & a, expr const & ref) {
m_state.add_local_ref(a, ref);
}
void push(bool in_section) {
m_scopes = cons(m_state, m_scopes);
m_state.m_in_section = in_section;
@ -150,20 +137,6 @@ environment erase_expr_aliases(environment const & env, name const & n) {
return update(env, ext);
}
environment add_local_ref(environment const & env, name const & a, expr const & ref) {
aliases_ext ext = get_extension(env);
ext.add_local_ref(a, ref);
return update(env, ext);
}
optional<expr> get_local_ref(environment const & env, name const & n) {
aliases_ext const & ext = get_extension(env);
if (auto r = ext.m_state.m_local_refs.find(n))
return some_expr(*r);
else
return none_expr();
}
// Return true iff \c n is (prefix + ex) for some ex in exceptions
bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions) {
return std::any_of(exceptions, exceptions + num_exceptions, [&](name const & ex) { return (prefix + ex) == n; });

6
src/library/aliases.h
View file

@ -42,12 +42,6 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
void for_each_expr_alias(environment const & env, std::function<void(name const &, names const &)> const & fn);
/* When we declare a definition in a section, we create an alias for it that fixes the parameters in
universe parameters. */
environment add_local_ref(environment const & env, name const & a, expr const & ref);
optional<expr> get_local_ref(environment const & env, name const & n);
void initialize_aliases();
void finalize_aliases();
}