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

refactor(library/aliases): move replace_prefix to util/name

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-31 15:11:22 -07:00
parent f7b3061a66
commit 3145cee51f
5 changed files with 57 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/library/aliases.cpp
View file

@ -48,20 +48,10 @@ environment add_alias(environment const & env, name const & a, expr const & e, i
return update(env, ext);
}
environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix, io_state const & ios) {
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 name replace_prefix(name const & n, name const & prefix, optional<name> const & new_prefix) {
if (n == prefix)
return new_prefix ? *new_prefix : name();
name p = replace_prefix(n.get_prefix(), prefix, new_prefix);
if (n.is_string())
return name(p, n.get_string());
else
return name(p, n.get_numeral());
}
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)
@ -72,12 +62,12 @@ static optional<expr> get_fix_param(unsigned num_fix_params, std::pair<name, exp
static name g_local_name = name::mk_internal_unique_name();
environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix,
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())) {
name a = replace_prefix(d.get_name(), prefix, new_prefix);
name a = d.get_name().replace_prefix(prefix, new_prefix);
check_name(env, a, ios);
levels ls = map2<level>(d.get_params(), [](name const &) { return mk_level_placeholder(); });
expr c = mk_constant(d.get_name(), ls);
@ -144,11 +134,11 @@ static int add_alias(lua_State * L) {
static int add_aliases(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 2) {
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), optional<name>(), get_io_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_optional_name(L, 3), get_io_state(L)));
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_optional_name(L, 3), to_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);
@ -164,7 +154,7 @@ static int add_aliases(lua_State * L) {
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_optional_name(L, 3),
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)));
}
}

10
src/library/aliases.h
View file

@ -18,18 +18,20 @@ namespace lean {
*/
environment add_alias(environment const & env, name const & a, expr const & e, io_state const & ios);
/**
\brief Create an alias for each declaration named <tt>prefix.rest</tt>. If \c new_prefix is not none,
then the alias for <tt>prefix.rest</tt> is <tt>new_prefix.rest</tt>. Otherwise, it is just \c rest.
\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>.
Warning messages are generated if the new aliases shadow existing aliases and/or declarations.
\remark \c new_prefix may be the anonymous name.
*/
environment add_aliases(environment const & env, name const & prefix, optional<name> const & new_prefix, io_state const & ios);
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, optional<name> const & new_prefix,
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. */

45
src/util/name.cpp
View file

@ -387,6 +387,18 @@ name name::append_after(unsigned i) const {
return append_after(s.str().c_str());
}
name name::replace_prefix(name const & prefix, name const & new_prefix) const {
if (*this == prefix)
return new_prefix;
if (is_anonymous())
return *this;
name p = get_prefix().replace_prefix(prefix, new_prefix);
if (is_string())
return name(p, get_string());
else
return name(p, get_numeral());
}
enum name_ll_kind { LL_ANON = 0, LL_STRING = 1, LL_INT = 2, LL_STRING_PREFIX = 3, LL_INT_PREFIX = 4 };
name_ll_kind ll_kind(name const & n) {
if (n.is_anonymous())
@ -478,6 +490,8 @@ static int mk_name(lua_State * L) {
name to_name_ext(lua_State * L, int idx) {
if (lua_isstring(L, idx)) {
return luaL_checkstring(L, idx);
} else if (lua_isnil(L, idx)) {
return name();
} else if (lua_istable(L, idx)) {
name r;
int n = objlen(L, idx);
@ -548,21 +562,24 @@ static int name_append_after(lua_State * L) {
return push_name(L, to_name(L, 1).append_after(lua_tostring(L, 2)));
}
static int name_replace_prefix(lua_State * L) { return push_name(L, to_name(L, 1).replace_prefix(to_name_ext(L, 2), to_name_ext(L, 3))); }
static const struct luaL_Reg name_m[] = {
{"__gc", name_gc}, // never throws
{"__tostring", safe_function<name_tostring>},
{"__eq", safe_function<name_eq>},
{"__lt", safe_function<name_lt>},
{"is_atomic", safe_function<name_is_atomic>},
{"is_anonymous", safe_function<name_is_anonymous>},
{"is_numeral", safe_function<name_is_numeral>},
{"is_string", safe_function<name_is_string>},
{"get_prefix", safe_function<name_get_prefix>},
{"get_numeral", safe_function<name_get_numeral>},
{"get_string", safe_function<name_get_string>},
{"hash", safe_function<name_hash>},
{"append_before", safe_function<name_append_before>},
{"append_after", safe_function<name_append_after>},
{"__gc", name_gc}, // never throws
{"__tostring", safe_function<name_tostring>},
{"__eq", safe_function<name_eq>},
{"__lt", safe_function<name_lt>},
{"is_atomic", safe_function<name_is_atomic>},
{"is_anonymous", safe_function<name_is_anonymous>},
{"is_numeral", safe_function<name_is_numeral>},
{"is_string", safe_function<name_is_string>},
{"get_prefix", safe_function<name_get_prefix>},
{"get_numeral", safe_function<name_get_numeral>},
{"get_string", safe_function<name_get_string>},
{"hash", safe_function<name_hash>},
{"append_before", safe_function<name_append_before>},
{"append_after", safe_function<name_append_after>},
{"replace_prefix", safe_function<name_replace_prefix>},
{0, 0}
};

6
src/util/name.h
View file

@ -121,6 +121,12 @@ public:
*/
name append_after(unsigned i) const;
/**
\brief If prefix is a prefix of this name, then return a new name where the prefix is replaced with new_prefix.
Otherwise, return this name.
*/
name replace_prefix(name const & prefix, name const & new_prefix) const;
friend void swap(name & a, name & b) {
std::swap(a.m_ptr, b.m_ptr);
}

7
tests/lua/n7.lua Normal file
View file

@ -0,0 +1,7 @@
local n1 = name("foo", "bar", 1)
assert(n1:replace_prefix("foo", {"hello", "world"}) == name("hello", "world", "bar", 1))
assert(n1:replace_prefix("foo2", {"hello", "world"}) == name("foo", "bar", 1))
assert(n1:replace_prefix("foo", nil) == name("bar", 1))
assert(n1:replace_prefix("foo", name()) == name("bar", 1))
assert(n1:replace_prefix({"foo", "bar"}, {"hello", "world"}) == name("hello", "world", 1))
assert(n1:replace_prefix({"foo", "bar"}, "tst") == name("tst", 1))