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

feat(lua): add Consts function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-08 12:09:46 -08:00
parent b7d8391306
commit 5c35a9ad0a
2 changed files with 23 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/bindings/lua/expr.cpp
View file

@ -172,6 +172,18 @@ void open_expr(lua_State * L) {
lua_setfield(L, -2, "__index");
setfuncs(L, expr_m, 0);
dostring(L, R"Lua(
function Consts(s)
r = {}
i = 1
for c in string.gmatch(s, '[^ ,;\t\n]+') do
r[i] = Const(c)
i = i + 1
end
return unpack(r)
end
)Lua");
set_global_function<expr_mk_constant>(L, "mk_constant");
set_global_function<expr_mk_constant>(L, "Const");
set_global_function<expr_mk_var>(L, "mk_var");

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

@ -0,0 +1,11 @@
f = Const("f")
x = Const("x")
y = Const("y")
a = Const("a")
b = Const("b")
print(Let(x, f(a), f(x, x)))
print(Let({{x, f(a)}, {y, f(b)}}, f(x, y)))
x1, x2, x3 = Consts("x1, x2, x3")
assert(tostring(f(x1, x2, x3)) == "f x1 x2 x3")
y1, y2 = Consts("y1 y2")
assert(tostring(f(y1, y2)) == "f y1 y2")