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

feat(library/kernel_bindings): expose expression tags in the Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-12 16:50:43 -07:00
parent 3bc83fae56
commit c883c638d6
2 changed files with 25 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/kernel_bindings.cpp
View file

@ -481,6 +481,12 @@ static int macro_def(lua_State * L) { return push_macro_definition(L, macro_def(
static int macro_num_args(lua_State * L) { return push_integer(L, macro_num_args(to_macro_app(L, 1))); }
static int macro_arg(lua_State * L) { return push_expr(L, macro_arg(to_macro_app(L, 1), luaL_checkinteger(L, 2))); }
static int expr_set_tag(lua_State * L) { to_expr(L, 1).set_tag(luaL_checkinteger(L, 2)); return 0; }
static int expr_tag(lua_State * L) {
auto t = to_expr(L, 1).get_tag();
return (t == nulltag) ? push_nil(L) : push_integer(L, t);
}
static const struct luaL_Reg expr_m[] = {
{"__gc", expr_gc}, // never throws
{"__tostring", safe_function<expr_tostring>},
@ -527,6 +533,8 @@ static const struct luaL_Reg expr_m[] = {
{"is_eqp", safe_function<expr_is_eqp>},
{"is_lt", safe_function<expr_is_lt>},
{"hash", safe_function<expr_hash>},
{"tag", safe_function<expr_tag>},
{"set_tag", safe_function<expr_set_tag>},
{0, 0}
};

17
tests/lua/tag1.lua Normal file
View file

@ -0,0 +1,17 @@
local f = Const("f")
local x = Const("x")
local a = Const("a")
local t1 = f(x, a, Var(1))
local t2 = Fun(x, Bool, t1)
assert(not t2:tag())
assert(not t2:binder_body():tag())
t2:set_tag(2)
t2:binder_body():set_tag(1)
assert(t2:tag() == 2)
assert(t2:binder_body():tag() == 1)
print(t2)
local new_t2 = t2:instantiate(Const("b"))
assert(new_t2:tag() == 2)
assert(new_t2:binder_body():tag() == 1)
assert(not (t2 == new_t2))