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

test(lua): coercion serialization

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-25 08:38:50 -07:00
parent 0d02f933cb
commit fc1819aadd
3 changed files with 20 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/coercion.cpp
View file

@ -317,13 +317,13 @@ environment add_coercion(environment const & env, name const & f, io_state const
return add_coercion(env, f, const_name(C), ios); return add_coercion(env, f, const_name(C), ios);
} }
bool is_coercion(environment const & env, expr const & f) { bool is_coercion(environment const & env, name const & f) {
if (is_constant(f)) {
coercion_ext const & ext = get_extension(env); coercion_ext const & ext = get_extension(env);
return ext.m_coercions.contains(const_name(f)); return ext.m_coercions.contains(f);
} else { }
return false;
} bool is_coercion(environment const & env, expr const & f) {
return is_constant(f) && is_coercion(env, const_name(f));
} }
bool has_coercions_from(environment const & env, name const & C) { bool has_coercions_from(environment const & env, name const & C) {
@ -450,7 +450,12 @@ static int add_coercion(lua_State * L) {
else else
return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4))); return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4)));
} }
static int is_coercion(lua_State * L) { return push_boolean(L, is_coercion(to_environment(L, 1), to_expr(L, 2))); } static int is_coercion(lua_State * L) {
if (is_expr(L, 2))
return push_boolean(L, is_coercion(to_environment(L, 1), to_expr(L, 2)));
else
return push_boolean(L, is_coercion(to_environment(L, 1), to_name_ext(L, 2)));
}
static int has_coercions_from(lua_State * L) { static int has_coercions_from(lua_State * L) {
if (is_expr(L, 2)) if (is_expr(L, 2))
return push_boolean(L, has_coercions_from(to_environment(L, 1), to_expr(L, 2))); return push_boolean(L, has_coercions_from(to_environment(L, 1), to_expr(L, 2)));

1
src/library/coercion.h
View file

@ -38,6 +38,7 @@ namespace lean {
*/ */
environment add_coercion(environment const & env, name & f, io_state const & ios); environment add_coercion(environment const & env, name & f, io_state const & ios);
environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios); environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios);
bool is_coercion(environment const & env, name const & f);
bool is_coercion(environment const & env, expr const & f); bool is_coercion(environment const & env, expr const & f);
/** \brief Return true iff the given environment has coercions from a user-class named \c C. */ /** \brief Return true iff the given environment has coercions from a user-class named \c C. */
bool has_coercions_from(environment const & env, name const & C); bool has_coercions_from(environment const & env, name const & C);

7
tests/lua/coe1.lua
View file

@ -48,3 +48,10 @@ print("---------")
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end) for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
print(get_coercion(env, lst_nat, "dlst")) print(get_coercion(env, lst_nat, "dlst"))
assert(env:type_check(get_coercion(env, lst_nat, "dlst"))) assert(env:type_check(get_coercion(env, lst_nat, "dlst")))
env:export("coe1_mod.olean")
local env2 = import_modules("coe1_mod")
print(get_coercion(env2, lst_nat, "dlst"))
assert(env2:type_check(get_coercion(env2, lst_nat, "dlst")))
assert(is_coercion(env2, "vec2mat"))
assert(is_coercion(env2, "lst2vec"))