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

test(lua): add tests for improving kernel_bindings coverage

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-20 12:16:12 -07:00
parent c5e8c10c9d
commit 11fc917102
4 changed files with 40 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/kernel_bindings.cpp
View file

@ -846,11 +846,11 @@ static int declaration_get_type(lua_State * L) { return push_expr(L, to_declarat
static int declaration_get_value(lua_State * L) {
if (to_declaration(L, 1).is_definition())
return push_expr(L, to_declaration(L, 1).get_value());
throw exception("arg #1 must be a declaration");
throw exception("arg #1 must be a definition");
}
static int declaration_get_weight(lua_State * L) { return push_integer(L, to_declaration(L, 1).get_weight()); }
static list<name> to_level_param_names(lua_State * L, int _idx) {
return table_to_list<name>(L, _idx, [](lua_State * L, int idx) -> name {
return table_to_list<name>(L, _idx, [=](lua_State * L, int idx) -> name {
if (is_level(L, idx)) {
level const & l = to_level(L, idx);
if (is_param(l))
@ -858,7 +858,7 @@ static list<name> to_level_param_names(lua_State * L, int _idx) {
else if (is_global(l))
return global_id(l);
else
throw exception(sstream() << "arg #" << idx << " contain a level expression that is not a parameter/global");
throw exception(sstream() << "arg #" << _idx << " contain a level expression that is not a parameter/global");
} else {
return to_name_ext(L, idx);
}
@ -896,10 +896,10 @@ static int mk_definition(lua_State * L) {
int nargs = lua_gettop(L);
bool opaque = true; unsigned weight = 0; module_idx mod_idx = 0; bool use_conv_opt = true;
if (nargs < 3) {
throw exception("mk_declaration must have at least 3 arguments");
throw exception("mk_definition must have at least 3 arguments");
} else if (is_environment(L, 1)) {
if (nargs < 4) {
throw exception("mk_declaration must have at least 4 arguments, when the first argument is an environment");
throw exception("mk_definition must have at least 4 arguments, when the first argument is an environment");
} else if (is_expr(L, 3)) {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_declaration(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), level_param_names(),

9
tests/lua/def1.lua
View file

@ -14,6 +14,7 @@ local ax = mk_axiom("ax", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)))
assert(ax:is_var_decl())
assert(ax:is_axiom())
assert(ax:name() == name("ax"))
assert(not pcall(function() print(ax:value()) end))
local th = mk_theorem("t1", {"l1", "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0)))
assert(th:is_theorem())
assert(th:is_definition())
@ -65,3 +66,11 @@ assert(d7:univ_params():head() == name("l1"))
assert(d7:univ_params():tail():head() == name("l2"))
assert(d7:opaque())
print("done")
assert(not pcall(function() mk_theorem("t1", {max_univ("l1", "l2")}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0))) end))
local l1 = global_univ("l1")
mk_theorem("t1", {l1, "l2"}, mk_arrow(mk_sort(l1), mk_sort(l2)), mk_lambda("x", mk_sort(l1), Var(0)))
assert(not pcall(function() mk_definition("bit", Type) end))
local env = environment(10)
assert(not pcall(function() mk_definition(env, "bit", Type) end))

11
tests/lua/expr11.lua Normal file
View file

@ -0,0 +1,11 @@
local a = Const("a")
local f = Const("f")
local x = Var(0)
assert(not f(a):has_free_var(0))
assert(f(a, x):has_free_var(0))
assert(not f(a, x):has_free_var(1, 3))
assert(f(a, Var(1)):has_free_var(1, 3))
assert(f(a, Var(2)):has_free_var(1, 3))
assert(not f(a, Var(3)):has_free_var(1, 3))
assert(not f(a, Var(4)):has_free_var(1, 3))
assert(f(a, Var(2)):lower_free_vars(2) == f(a, Var(0)))

15
tests/lua/res1.lua
View file

@ -94,6 +94,12 @@ assert(Pr1:is_macro())
assert(Pr1:macro_num_args() == 3)
assert(Pr1:macro_arg(0) == l6)
assert(Pr1:macro_def() == Pr2:macro_def())
assert(Pr1:data() == Pr1:macro_def())
assert(Pr1 == mk_macro(Pr1:macro_def(), {Pr1:macro_arg(0), Pr1:macro_arg(1), Pr1:macro_arg(2)}))
assert(Pr1:macro_def():name() == name("resolve"))
assert(Pr1:macro_def():trust_level() >= 0)
print(Pr1:macro_def():hash())
print(Pr1:macro_def())
print("-----------")
print(tc:check(H2))
print(tc:check(H1))
@ -118,3 +124,12 @@ local tc = type_checker(env)
print(tc:whnf(Pr1))
print(tc:check(Pr1))
print(tc:check(Pr4))
print(env:normalize(Pr4))
local a = Const("a")
assert(not pcall(function() a:macro_num_args() end))
assert(not pcall(function() a:let_name() end))
assert(not pcall(function() mk_arrow(a) end))