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

fix(library/kernel_bindings): bug in mk_app, add expr_lt tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-09 19:54:52 -07:00
parent 6493ff5388
commit a650a4f9b5
2 changed files with 46 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/library/kernel_bindings.cpp
View file

@ -234,13 +234,19 @@ static int expr_tostring(lua_State * L) {
static int expr_eq(lua_State * L) { return push_boolean(L, to_expr(L, 1) == to_expr(L, 2)); }
static int expr_lt(lua_State * L) { return push_boolean(L, to_expr(L, 1) < to_expr(L, 2)); }
static int expr_mk_constant(lua_State * L) { return push_expr(L, mk_constant(to_name_ext(L, 1))); }
static int expr_mk_constant(lua_State * L) {
int nargs = lua_gettop(L);
if (nargs == 1)
return push_expr(L, mk_constant(to_name_ext(L, 1)));
else
return push_expr(L, mk_constant(to_name_ext(L, 1), to_list_level_ext(L, 2)));
}
static int expr_mk_var(lua_State * L) { return push_expr(L, mk_var(luaL_checkinteger(L, 1))); }
static int expr_mk_app(lua_State * L) {
int nargs = lua_gettop(L);
expr r;
r = mk_app(to_expr(L, 1), to_expr(L, 2));
for (int i = 3; i < nargs; i++)
for (int i = 3; i <= nargs; i++)
r = mk_app(r, to_expr(L, i));
return push_expr(L, r);
}
@ -458,8 +464,10 @@ static int expr_occurs(lua_State * L) { return push_boolean(L, occurs(to_expr(L,
static int expr_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); }
static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); }
static int expr_depth(lua_State * L) { return push_integer(L, get_depth(to_expr(L, 1))); }
static int expr_is_lt(lua_State * L) { return push_boolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), false)); }
static int expr_is_lt(lua_State * L) {
int nargs = lua_gettop(L);
return push_boolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), nargs == 3 && lua_toboolean(L, 3)));
}
static int expr_mk_macro(lua_State * L) {
buffer<expr> args;
copy_lua_array(L, 2, args);
@ -655,18 +663,23 @@ static int mk_definition(lua_State * L) {
if (is_environment(L, 1)) {
if (nargs <= 5) {
get_definition_args(L, 5, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(), level_cnstrs(), to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), param_names(), level_cnstrs(),
to_expr(L, 3), to_expr(L, 4), opaque, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 7, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_list_name_ext(L, 3), to_list_pair_level_ext(L, 4), to_expr(L, 5), to_expr(L, 6), opaque, mod_idx, use_conv_opt));
return push_definition(L, mk_definition(to_environment(L, 1), to_name_ext(L, 2), to_list_name_ext(L, 3),
to_list_pair_level_ext(L, 4), to_expr(L, 5), to_expr(L, 6),
opaque, mod_idx, use_conv_opt));
}
} else {
if (nargs <= 4) {
get_definition_args(L, 4, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2), to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
return push_definition(L, mk_definition(to_name_ext(L, 1), param_names(), level_cnstrs(), to_expr(L, 2),
to_expr(L, 3), opaque, weight, mod_idx, use_conv_opt));
} else {
get_definition_args(L, 6, opaque, weight, mod_idx, use_conv_opt);
return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3), to_expr(L, 4), to_expr(L, 5), opaque, weight, mod_idx, use_conv_opt));
return push_definition(L, mk_definition(to_name_ext(L, 1), to_list_name_ext(L, 2), to_list_pair_level_ext(L, 3),
to_expr(L, 4), to_expr(L, 5), opaque, weight, mod_idx, use_conv_opt));
}
}
}

25
tests/lua/expr2.lua Normal file
View file

@ -0,0 +1,25 @@
local f = Const("f")
local a = Const("a")
local b = Const("b")
local x = Var(0)
assert(f(a, a):is_lt(f(a, b)))
assert(Const("a"):is_lt(Const("b")))
assert(Var(0):is_lt(Const("b")))
assert(name("a") < name("b"))
assert(not (Bool:is_lt(Bool)))
assert(not (Bool < Bool))
assert(mk_metavar("a", Bool):is_lt(mk_metavar("b", Bool)))
assert(not mk_metavar("a", Bool):is_lt(mk_metavar("a", Bool)))
assert(mk_metavar("a", Bool):is_lt(mk_metavar("a", Type)))
assert(mk_local("a", Bool):is_lt(mk_local("b", Bool)))
assert(not mk_local("a", Bool):is_lt(mk_local("a", Bool)))
assert(Bool:is_lt(Const("a")))
assert(Fun(a, Bool, a):is_lt(Fun(a, Type, a)))
assert(Fun(a, Bool, a):is_lt(Fun(a, Bool, Var(2))))
assert(Pi(a, Bool, a):is_lt(Pi(a, Type, a)))
assert(Pi(a, Bool, a):is_lt(Pi(a, Bool, Var(2))))
assert(Var(0) < Var(1))
print(Const("a", {mk_level_one(), mk_level_zero()}))
assert(Const("a", {mk_level_one()}):is_lt(Const("a", {mk_level_one(), mk_level_zero()})))
assert(Const("a", {mk_level_zero(), mk_level_one()}):is_lt(Const("a", {mk_level_one()})))
assert(not Const("a", {mk_level_zero(), mk_level_one()}):is_lt(Const("a", {mk_level_zero(), mk_level_one()})))