From 45a3ab5141ae0d98451873c23ea73566d3f95369 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Jun 2014 15:19:29 -0700 Subject: [PATCH] refactor(library/aliases): it is bad design to instantiate parameter using the parameter name, the parameter names have no semantic value Moreover, we could create type incorrect aliases by "accident". Signed-off-by: Leonardo de Moura --- src/library/aliases.cpp | 73 +---------------------------------------- src/library/aliases.h | 8 ----- tests/lua/alias1.lua | 18 ++-------- 3 files changed, 4 insertions(+), 95 deletions(-) diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp index eec0de709..8a52197eb 100644 --- a/src/library/aliases.cpp +++ b/src/library/aliases.cpp @@ -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 get_fix_param(unsigned num_fix_params, std::pair 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 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(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 locals; - buffer infos; - buffer 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> 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))); } } diff --git a/src/library/aliases.h b/src/library/aliases.h index 53713d1de..1237f21d3 100644 --- a/src/library/aliases.h +++ b/src/library/aliases.h @@ -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 prefix.rest, the alias will also fix the value of parameters - in \c fix_params. The argument \c fix_params is a sequence of pairs (name, expr), 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 const * fix_params, io_state const & ios); /** \brief If \c t is aliased in \c env, then return its name. Otherwise, return none. */ optional is_aliased(environment const & env, expr const & t); diff --git a/tests/lua/alias1.lua b/tests/lua/alias1.lua index eced6897c..f4092abb3 100644 --- a/tests/lua/alias1.lua +++ b/tests/lua/alias1.lua @@ -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"))