lean2/tests/lua/threads/st2.lua
Leonardo de Moura 2ac594a159 test(lua): add a new example showing how to create nested State objects and threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-11 18:27:09 -08:00

58 lines
1.4 KiB
Lua

-- Create a nested lua_State object
S = State()
-- Remarks:
-- '[[ ... ]]' is a multi-line string in Lua
-- obj:method(args) is the syntax for invoking a method
-- it is actually syntax sugar for
-- obj.method(obj, args)
S:dostring([[
x = 10
]])
-- Variable x is not visible in the main State object
print(x) -- it will print nil
S:dostring([[
print(x)
]])
-- Remark: '...' is a reference to varargs in Lua
-- We can pass arguments to/from a nested state
-- The following statement passes 10 and 20 as arguments
-- to the nested lua_State object S.
-- The values returned by the script are stored in r1 and r2
r1, r2 = S:dostring([[
-- extract arguments passed to dostring
a1, a2 = ...
return a1 + a2, a1 - a2
]], 10, 20)
print("r1:", r1)
print("r2:", r2)
-- We can communicate integers, strings and Lean objects
f = Const("f")
a = Const("a")
T = S:dostring([[
t = ...
g = Const("g")
return g(g(g(t)))
]], f(a))
print(T)
-- We can also execute commands in a separate thread.
-- The following command creates a thread for running
-- the given script in the state S.
-- It does not wait the thread to finish.
T = thread(S, [[
t = ...
g = Const("g")
b = Const("b")
return g(b, t)
]], f(a))
-- The method wait makes us wait for the thread T.
-- It return the values returned by the script.
r = T:wait()
-- It will print the Lean expression g(b, f(a))
print(r)