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

feat(library/aliases): add 'exceptions' and support for universes to add_aliases procedure, add for_each_universe method to environment

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-13 08:26:05 -07:00
parent cccec51c1e
commit 5aca452439
24 changed files with 150 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -15,7 +15,7 @@ environment universe_cmd(parser & p) {
// TODO(Leo): take namespace and scopes into account
name n = p.get_name_val();
p.next();
return p.env().add_global_level(n);
return p.env().add_universe(n);
} else {
throw parser_error("invalid universe declaration, identifier expected", p.cmd_pos());
}

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

@ -280,7 +280,7 @@ level parser::parse_level_id() {
auto it = m_local_level_decls.find(id);
if (it != m_local_level_decls.end())
return it->second.first;
if (m_env.is_global_level(id))
if (m_env.is_universe(id))
return mk_global_univ(id);
throw parser_error(sstream() << "unknown level '" << id << "'", p);
}

10
src/kernel/environment.cpp
View file

@ -129,14 +129,14 @@ environment environment::add(certified_declaration const & d) const {
return environment(m_header, m_id, insert(m_declarations, n, d.get_declaration()), m_global_levels, m_extensions);
}
environment environment::add_global_level(name const & n) const {
environment environment::add_universe(name const & n) const {
if (m_global_levels.contains(n))
throw_kernel_exception(*this,
"invalid global universe level declaration, environment already contains a universe level with the given name");
return environment(m_header, m_id, m_declarations, insert(m_global_levels, n), m_extensions);
}
bool environment::is_global_level(name const & n) const {
bool environment::is_universe(name const & n) const {
return m_global_levels.contains(n);
}
@ -213,7 +213,11 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
return environment(m_header, m_id, m_declarations, m_global_levels, new_exts);
}
void environment::for_each(std::function<void(declaration const & d)> const & f) const {
void environment::for_each_declaration(std::function<void(declaration const & d)> const & f) const {
m_declarations.for_each([&](name const &, declaration const & d) { return f(d); });
}
void environment::for_each_universe(std::function<void(name const & n)> const & f) const {
m_global_levels.for_each([&](name const & n) { return f(n); });
}
}

9
src/kernel/environment.h
View file

@ -163,10 +163,10 @@ public:
\brief Add a new global universe level with name \c n
This method throws an exception if the environment already contains a level named \c n.
*/
environment add_global_level(name const & n) const;
environment add_universe(name const & n) const;
/** \brief Return true iff the environment has a universe level named \c n. */
bool is_global_level(name const & n) const;
bool is_universe(name const & n) const;
/**
\brief Extends the current environment with the given (certified) declaration
@ -221,7 +221,10 @@ public:
environment forget() const;
/** \brief Apply the function \c f to each declaration */
void for_each(std::function<void(declaration const & d)> const & f) const;
void for_each_declaration(std::function<void(declaration const & d)> const & f) const;
/** \brief Apply the function \c f to each universe */
void for_each_universe(std::function<void(name const & u)> const & f) const;
};
class name_generator;

2
src/kernel/level.cpp
View file

@ -405,7 +405,7 @@ optional<name> get_undef_global(level const & l, environment const & env) {
for_each(l, [&](level const & l) {
if (!has_global(l) || r)
return false;
if (is_global(l) && !env.is_global_level(global_id(l)))
if (is_global(l) && !env.is_universe(global_id(l)))
r = global_id(l);
return true;
});

72
src/library/aliases.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <algorithm>
#include "util/rb_map.h"
#include "util/name_generator.h"
#include "util/sstream.h"
@ -57,19 +58,6 @@ environment add_alias(environment const & env, name const & a, expr const & e) {
return update(env, ext);
}
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix) {
aliases_ext ext = get_extension(env);
env.for_each([&](declaration const & d) {
if (is_prefix_of(prefix, d.get_name())) {
name a = d.get_name().replace_prefix(prefix, new_prefix);
levels ls = map2<level>(d.get_univ_params(), [](name const &) { return mk_level_placeholder(); });
expr c = mk_constant(d.get_name(), ls);
ext.add_alias(a, c);
}
});
return update(env, ext);
}
optional<name> is_aliased(environment const & env, expr const & t) {
auto it = get_extension(env).m_inv_aliases.find(t);
return it ? optional<name>(*it) : optional<name>();
@ -81,7 +69,7 @@ list<expr> get_alias_exprs(environment const & env, name const & n) {
}
environment add_alias(environment const & env, name const & a, level const & l) {
if (env.is_global_level(a))
if (env.is_universe(a))
throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
aliases_ext ext = get_extension(env);
ext.add_alias(a, l);
@ -98,6 +86,33 @@ optional<level> get_alias_level(environment const & env, name const & n) {
return it ? some_level(*it) : optional<level>();
}
// Return true iff \c n is (prefix + ex) for some ex in exceptions
static 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; });
}
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_exceptions, name const * exceptions) {
aliases_ext ext = get_extension(env);
env.for_each_declaration([&](declaration const & d) {
if (is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
name a = d.get_name().replace_prefix(prefix, new_prefix);
levels ls = map2<level>(d.get_univ_params(), [](name const &) { return mk_level_placeholder(); });
expr c = mk_constant(d.get_name(), ls);
ext.add_alias(a, c);
}
});
env.for_each_universe([&](name const & u) {
if (is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
name a = u.replace_prefix(prefix, new_prefix);
if (env.is_universe(a))
throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
ext.add_alias(a, mk_global_univ(u));
}
});
return update(env, ext);
}
static int add_alias(lua_State * L) {
if (is_expr(L, 3))
return push_environment(L, add_alias(to_environment(L, 1), to_name_ext(L, 2), to_expr(L, 3)));
@ -105,15 +120,6 @@ static int add_alias(lua_State * L) {
return push_environment(L, add_alias(to_environment(L, 1), to_name_ext(L, 2), to_level(L, 3)));
}
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), name()));
} else {
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
}
}
static int is_aliased(lua_State * L) {
if (is_expr(L, 2))
return push_optional_name(L, is_aliased(to_environment(L, 1), to_expr(L, 2)));
@ -129,6 +135,26 @@ static int get_alias_level(lua_State * L) {
return push_optional_level(L, get_alias_level(to_environment(L, 1), to_name_ext(L, 2)));
}
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), name()));
} else if (nargs == 3) {
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3)));
} else {
buffer<name> exs;
luaL_checktype(L, 4, LUA_TTABLE);
int n = objlen(L, 4);
for (int i = 1; i <= n; i++) {
lua_rawgeti(L, 4, i);
exs.push_back(to_name_ext(L, -1));
lua_pop(L, 1);
}
return push_environment(L, add_aliases(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3),
exs.size(), exs.data()));
}
}
void open_aliases(lua_State * L) {
SET_GLOBAL_FUN(add_alias, "add_alias");
SET_GLOBAL_FUN(add_aliases, "add_aliases");

21
src/library/aliases.h
View file

@ -12,14 +12,6 @@ Author: Leonardo de Moura
namespace lean {
/** \brief Add the alias \c a for expression \c e. \c e must not have free variables. */
environment add_alias(environment const & env, name const & a, expr const & e);
/**
\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, name const & new_prefix);
/** \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);
@ -40,5 +32,18 @@ optional<name> is_aliased(environment const & env, level const & l);
/** \brief Return the level associated with the given alias. */
optional<level> get_alias_level(environment const & env, name const & n);
/**
\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>.
The command will also create aliases for universe level declarations.
However, an error is thrown if the universe level shadows existing aliases and/or declarations.
We don't have "choice" construct for universe levels.
\remark \c new_prefix may be the anonymous name.
*/
environment add_aliases(environment const & env, name const & prefix, name const & new_prefix,
unsigned num_exceptions = 0, name const * exceptions = nullptr);
void open_aliases(lua_State * L);
}

29
src/library/kernel_bindings.cpp
View file

@ -1152,10 +1152,10 @@ static int environment_prop_proof_irrel(lua_State * L) { return push_boolean(L,
static int environment_cls_proof_irrel(lua_State * L) { return push_list_name(L, to_environment(L, 1).cls_proof_irrel()); }
static int environment_eta(lua_State * L) { return push_boolean(L, to_environment(L, 1).eta()); }
static int environment_impredicative(lua_State * L) { return push_boolean(L, to_environment(L, 1).impredicative()); }
static int environment_add_global_level(lua_State * L) {
return push_environment(L, module::add_global_level(to_environment(L, 1), to_name_ext(L, 2)));
static int environment_add_universe(lua_State * L) {
return push_environment(L, module::add_universe(to_environment(L, 1), to_name_ext(L, 2)));
}
static int environment_is_global_level(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_global_level(to_name_ext(L, 2))); }
static int environment_is_universe(lua_State * L) { return push_boolean(L, to_environment(L, 1).is_universe(to_name_ext(L, 2))); }
static int environment_find(lua_State * L) { return push_optional_declaration(L, to_environment(L, 1).find(to_name_ext(L, 2))); }
static int environment_get(lua_State * L) { return push_declaration(L, to_environment(L, 1).get(to_name_ext(L, 2))); }
static int environment_add(lua_State * L) {
@ -1188,16 +1188,26 @@ static int environment_whnf(lua_State * L) { return push_expr(L, type_checker(to
static int environment_normalize(lua_State * L) { return push_expr(L, normalize(to_environment(L, 1), to_expr(L, 2))); }
static int environment_infer_type(lua_State * L) { return push_expr(L, type_checker(to_environment(L, 1)).infer(to_expr(L, 2))); }
static int environment_type_check(lua_State * L) { return push_expr(L, type_checker(to_environment(L, 1)).check(to_expr(L, 2))); }
static int environment_for_each(lua_State * L) {
static int environment_for_each_decl(lua_State * L) {
environment const & env = to_environment(L, 1);
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
env.for_each([&](declaration const & d) {
env.for_each_declaration([&](declaration const & d) {
lua_pushvalue(L, 2); // push user-fun
push_declaration(L, d);
pcall(L, 1, 0, 0);
});
return 0;
}
static int environment_for_each_universe(lua_State * L) {
environment const & env = to_environment(L, 1);
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
env.for_each_universe([&](name const & u) {
lua_pushvalue(L, 2); // push user-fun
push_name(L, u);
pcall(L, 1, 0, 0);
});
return 0;
}
static void to_string_buffer(lua_State * L, int i, buffer<std::string> & r) {
if (lua_isstring(L, i)) {
@ -1256,8 +1266,8 @@ static const struct luaL_Reg environment_m[] = {
{"cls_proof_irrel", safe_function<environment_cls_proof_irrel>},
{"eta", safe_function<environment_eta>},
{"impredicative", safe_function<environment_impredicative>},
{"add_global_level", safe_function<environment_add_global_level>},
{"is_global_level", safe_function<environment_is_global_level>},
{"add_universe", safe_function<environment_add_universe>},
{"is_universe", safe_function<environment_is_universe>},
{"find", safe_function<environment_find>},
{"get", safe_function<environment_get>},
{"add", safe_function<environment_add>},
@ -1267,7 +1277,10 @@ static const struct luaL_Reg environment_m[] = {
{"normalize", safe_function<environment_normalize>},
{"infer_type", safe_function<environment_infer_type>},
{"type_check", safe_function<environment_type_check>},
{"for_each", safe_function<environment_for_each>},
{"for_each_declaration", safe_function<environment_for_each_decl>},
{"for_each_decl", safe_function<environment_for_each_decl>},
{"for_each_universe", safe_function<environment_for_each_universe>},
{"for_each_univ", safe_function<environment_for_each_universe>},
{"export", safe_function<export_module>},
{0, 0}
};

10
src/library/module.cpp
View file

@ -109,8 +109,8 @@ environment add(environment const & env, std::string const & k, std::function<vo
return update(env, ext);
}
environment add_global_level(environment const & env, name const & l) {
environment new_env = env.add_global_level(l);
environment add_universe(environment const & env, name const & l) {
environment new_env = env.add_universe(l);
return add(new_env, g_glvl_key, [=](serializer & s) { s << l; });
}
@ -293,9 +293,9 @@ struct import_modules_fn {
}
}
void import_global_level(deserializer & d) {
void import_universe(deserializer & d) {
name const l = read_name(d);
m_senv.update([=](environment const & env) { return env.add_global_level(l); });
m_senv.update([=](environment const & env) { return env.add_universe(l); });
}
void import_module(module_info_ptr const & r) {
@ -319,7 +319,7 @@ struct import_modules_fn {
} else if (k == g_decl_key) {
import_decl(d, r->m_module_idx);
} else if (k == g_glvl_key) {
import_global_level(d);
import_universe(d);
} else {
object_readers & readers = get_object_readers();
auto it = readers.find(k);

4
src/library/module.h
View file

@ -75,8 +75,8 @@ namespace module {
*/
environment add(environment const & env, std::string const & k, std::function<void(serializer &)> const & writer);
/** \brief Add the global level declaration to the environment, and mark it to be exported. */
environment add_global_level(environment const & env, name const & l);
/** \brief Add the global universe declaration to the environment, and mark it to be exported. */
environment add_universe(environment const & env, name const & l);
/** \brief Add the given declaration to the environment, and mark it to be exported. */
environment add(environment const & env, certified_declaration const & d);

4
tests/lua/acc.lua
View file

@ -16,8 +16,8 @@ env = add_inductive(env,
"Acc", {l}, 2, Pi({A, R, x}, mk_sort(l+1)),
"Acc_intro", Pi({A, R, x}, mk_arrow(Pi(y, mk_arrow(R(y, x), Acc(A, R, y))), Acc(A, R, x))))
env = env:add_global_level("u")
env = env:add_global_level("v")
env = env:add_universe("u")
env = env:add_universe("v")
local u = global_univ("u")
local v = global_univ("v")
display_type(env, Const("Acc_rec", {v, u}))

2
tests/lua/alias1.lua
View file

@ -17,7 +17,7 @@ env = add_inductive(env,
name("nat", "zero"), nat,
name("nat", "succ"), mk_arrow(nat, nat))
env:for_each(function(d) print(d:name()) end)
env:for_each_decl(function(d) print(d:name()) end)
env = add_aliases(env, "nat", "natural")
assert(get_alias_exprs(env, {"natural", "zero"}):head() == zero)
assert(get_alias_exprs(env, {"natural", "nat"}):head() == nat)

13
tests/lua/alias3.lua Normal file
View file

@ -0,0 +1,13 @@
local env = environment()
env = add_decl(env, mk_var_decl(name("foo", "x"), Bool))
env = add_decl(env, mk_var_decl(name("foo", "y"), Bool))
env = add_decl(env, mk_var_decl(name("foo", "z"), Bool))
env = env:add_universe(name("foo", "u"))
env = env:add_universe(name("foo", "v"))
env = add_aliases(env, "foo", "bla", {"z", "v"})
assert(not get_alias_exprs(env, {"bla", "x"}):is_nil())
assert(not get_alias_exprs(env, {"bla", "y"}):is_nil())
assert(get_alias_exprs(env, {"bla", "z"}):is_nil())
assert(get_alias_level(env, {"bla", "u"}))
assert(not get_alias_level(env, {"bla", "v"}))

8
tests/lua/env1.lua
View file

@ -1,9 +1,9 @@
local env = bare_environment()
assert(is_environment(env))
assert(not env:is_global_level("U"))
local env2 = env:add_global_level("U")
assert(not env:is_global_level("U"))
assert(env2:is_global_level("U"))
assert(not env:is_universe("U"))
local env2 = env:add_universe("U")
assert(not env:is_universe("U"))
assert(env2:is_universe("U"))
assert(env:eta())
assert(env:prop_proof_irrel())
assert(env:impredicative())

6
tests/lua/env10.lua
View file

@ -36,7 +36,7 @@ env = add_inductive(env,
"inl", Pi({A, B, a}, coproduct_l1l2(A, B)),
"inr", Pi({A, B, b}, coproduct_l1l2(A, B)))
env:for_each(function(d)
print(tostring(d:name()) .. " : " .. tostring(d:type()))
end
env:for_each_decl(function(d)
print(tostring(d:name()) .. " : " .. tostring(d:type()))
end
)

4
tests/lua/env11.lua
View file

@ -17,8 +17,8 @@ end
expected_error(function() env1:add(c3) end)
expected_error(function() env2:add(c1) end)
env3 = env2:add_global_level("u")
expected_error(function() env3:add_global_level("u") end)
env3 = env2:add_universe("u")
expected_error(function() env3:add_universe("u") end)
expected_error(function() check(env2, mk_theorem("H1", A, Const("H1"))) end)
local c4 = check(env1b, mk_theorem("H2", A, Const("H1")))
expected_error(function() env3:add(c4) end)

2
tests/lua/env5.lua
View file

@ -34,7 +34,7 @@ assert(not pcall(function()
print(tc:check(id_1_1))
end
))
local env2 = env:add_global_level("u")
local env2 = env:add_universe("u")
assert(env2:is_descendant(env))
assert(not env:is_descendant(env2))
local tc2 = type_checker(env2)

6
tests/lua/env8.lua
View file

@ -7,7 +7,7 @@ env = add_inductive(env,
"succ", mk_arrow(nat, nat))
-- Display all declarations in the environment
env:for_each(function(d)
print(tostring(d:name()) .. " : " .. tostring(d:type()))
end
env:for_each_decl(function(d)
print(tostring(d:name()) .. " : " .. tostring(d:type()))
end
)

10
tests/lua/glvl1.lua
View file

@ -1,9 +1,9 @@
local env = environment()
env = env:add_global_level("u")
env = env:add_global_level("v")
assert(env:is_global_level("u"))
env = env:add_universe("u")
env = env:add_universe("v")
assert(env:is_universe("u"))
env:export("glvl1_mod.olean")
local env2 = import_modules("glvl1_mod")
assert(env2:is_global_level("u"))
assert(env2:is_global_level("v"))
assert(env2:is_universe("u"))
assert(env2:is_universe("v"))

8
tests/lua/ind1.lua
View file

@ -12,8 +12,8 @@ local forest_l = Const("forest", {l})
local tree_l = Const("tree", {l})
local n = Const("n")
env = env:add_global_level("u")
env = env:add_global_level("v")
env = env:add_universe("u")
env = env:add_universe("v")
local u = global_univ("u")
local v = global_univ("v")
@ -138,8 +138,8 @@ assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(z
-- Martin-Lof style identity type
local env = hott_environment()
local Id_l = Const("Id", {l})
env = env:add_global_level("u")
env = env:add_global_level("v")
env = env:add_universe("u")
env = env:add_universe("v")
env = add_inductive(env,
"Id", {l}, 1, Pi({{A, U_l}, {a, A}, {b, A}}, U_l),
"Id_refl", Pi({{A, U_l, true}, {b, A}}, Id_l(A, b, b)))

2
tests/lua/ind5.lua
View file

@ -11,7 +11,7 @@ env = add_inductive(env,
"inj", Pi(A, retraction))
local u = global_univ("u")
env = env:add_global_level("u")
env = env:add_universe("u")
local a = Local("a", Bool)
local r = Local("r", retraction)

2
tests/lua/ind_tricky.lua
View file

@ -11,7 +11,7 @@ function display_type(env, t)
print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
end
env = env:add_global_level("u")
env = env:add_universe("u")
local tricky_rec = Const("tricky_rec", {0})
display_type(env, tricky_rec)

6
tests/lua/mod5.lua
View file

@ -47,9 +47,9 @@ end
mk_modules()
local env = import_modules(mod_name(NumMods))
env:for_each(function(d)
print(d:name())
end
env:for_each_decl(function(d)
print(d:name())
end
)
for i = 1, NumMods do
assert(env:get(const_name(i)):is_definition())

2
tests/lua/tc2.lua
View file

@ -33,7 +33,7 @@ env = add_decl(env, mk_theorem("trans", {l},
local symm_l = Const("symm", {l})
local trans_l = Const("trans", {l})
print(env:get("trans"):value())
env = env:add_global_level("u")
env = env:add_universe("u")
local u = mk_global_univ("u")
local tc = type_checker(env)
print(tc:check(Const("trans", {u})))