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

refactor(library/aliases): it is bad design to instantiate parameter using the parameter name, the parameter names have no semantic value

Browse source 
Moreover, we could create type incorrect aliases by "accident".

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-03 15:19:29 -07:00
parent 1f6cfce05c
commit 45a3ab5141
3 changed files with 4 additions and 95 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

73
src/library/aliases.cpp
View file

@ -49,21 +49,6 @@ environment add_alias(environment const & env, name const & a, expr const & e, i
}
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, io_state const & ios) {
return add_aliases(env, prefix, new_prefix, 0, nullptr, ios);
}
static optional<expr> get_fix_param(unsigned num_fix_params, std::pair<name, expr> const * fix_params, name const & n) {
for (unsigned i = 0; i < num_fix_params; i++) {
if (fix_params[i].first == n)
return some_expr(fix_params[i].second);
}
return none_expr();
}
static name g_local_name = name::mk_internal_unique_name();
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_fix_params, std::pair<name, expr> const * fix_params, io_state const & ios) {
aliases_ext ext = get_extension(env);
env.for_each([&](declaration const & d) {
if (is_prefix_of(prefix, d.get_name())) {
@ -71,45 +56,6 @@ environment add_aliases(environment const & env, name const & prefix, name const
check_name(env, a, ios);
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();
buffer<expr> locals;
buffer<binder_info> infos;
buffer<expr> args;
name_generator ngen(g_local_name);
bool found_free = false;
bool found_fix = false;
bool easy = true;
while (is_pi(t)) {
if (auto p = get_fix_param(num_fix_params, fix_params, binding_name(t))) {
args.push_back(*p);
if (found_free)
easy = false;
found_fix = true;
t = instantiate(binding_body(t), *p);
} else {
found_free = true;
expr l = mk_local(ngen.next(), binding_name(t), binding_domain(t));
infos.push_back(binding_info(t));
locals.push_back(l);
args.push_back(l);
t = instantiate(binding_body(t), l);
}
}
if (found_fix) {
if (easy) {
args.shrink(args.size() - locals.size());
c = mk_app(c, args);
} else {
c = mk_app(c, args);
unsigned i = locals.size();
while (i > 0) {
--i;
c = Fun(locals[i], c, infos[i]);
}
}
}
}
ext.m_aliases.insert(a, c);
ext.m_inv_aliases.insert(c, a);
}
@ -137,25 +83,8 @@ static int add_aliases(lua_State * L) {
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), name(), get_io_state(L)));
} else if (nargs == 3) {
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), get_io_state(L)));
} else if (nargs == 4 && is_io_state(L, 4)) {
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4)));
} else {
buffer<std::pair<name, expr>> fix_params;
luaL_checktype(L, 4, LUA_TTABLE);
int sz = objlen(L, 4);
for (int i = 1; i <= sz; i++) {
lua_rawgeti(L, 4, i);
luaL_checktype(L, -1, LUA_TTABLE);
lua_rawgeti(L, -1, 1);
name n = to_name_ext(L, -1);
lua_pop(L, 1);
lua_rawgeti(L, -1, 2);
expr e = to_expr(L, -1);
lua_pop(L, 2);
fix_params.emplace_back(n, e);
}
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3),
fix_params.size(), fix_params.data(), to_io_state_ext(L, 5)));
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4)));
}
}

8
src/library/aliases.h
View file

@ -25,14 +25,6 @@ environment add_alias(environment const & env, name const & a, expr const & e, i
\remark \c new_prefix may be the anonymous name.
*/
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix, io_state const & ios);
/**
\brief Create an alias for each declaration named <tt>prefix.rest</tt>, the alias will also fix the value of parameters
in \c fix_params. The argument \c fix_params is a sequence of pairs <tt>(name, expr)</tt>, where the \c name is the
name of the parameter to be fixed.
Warning messages are generated if the new aliases shadow existing aliases and/or declarations.
*/
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_fix_params, std::pair<name, expr> const * fix_params, io_state const & ios);
/** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */
optional<name> is_aliased(environment const & env, expr const & t);

18
tests/lua/alias1.lua
View file

@ -35,27 +35,15 @@ print(get_alias(env, "list_rec"))
assert(get_alias(env, "list_rec"))
assert(get_alias(env, {"lst", "list_rec"}))
env = add_aliases(env, "list", "lnat", {{"A", nat}})
print(get_alias(env, {"lnat", "list"}))
print(get_alias(env, {"lnat", "cons"}))
assert(get_alias(env, {"lnat", "cons"}) == Const({"list", "cons"}, { mk_level_placeholder() })(nat))
env = add_aliases(env, "list", "l")
print(get_alias(env, {"l", "list"}))
print(get_alias(env, {"l", "cons"}))
local A = Local("A", mk_sort(1))
local R = Local("R", mk_arrow(A, A, Bool))
local a = Local("a", A)
local b = Local("b", A)
env = add_decl(env, mk_var_decl({"foo", "pred"}, Pi({A, R, a, b}, Bool)))
env = add_aliases(env, "foo", nil, {{"A", nat}, {"a", zero}})
local Rn = Local("R", mk_arrow(nat, nat, Bool))
local bn = Local("b", nat)
local a1 = get_alias(env, "pred")
local a2 = Fun({Rn, bn}, Const({"foo", "pred"})(nat, Rn, zero, bn))
print(a1)
print(a2)
assert(a1 == a2)
env = add_aliases(env, "foo", nil, {{"A", nat}, {"a", zero}, {"b", one}})
print(get_alias(env, "pred"))
env = add_alias(env, "z", zero)
assert(get_alias(env, "z") == zero)
assert(not get_alias(env, "zz"))