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

chore(lua): rename env() to get_env()

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-13 13:58:51 -08:00
parent ba0889265e
commit 8c52d47692
4 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/bindings/lua/environment.cpp
View file

@ -250,6 +250,6 @@ void open_environment(lua_State * L) {
SET_GLOBAL_FUN(mk_environment, "environment"); SET_GLOBAL_FUN(mk_environment, "environment");
SET_GLOBAL_FUN(environment_pred, "is_environment"); SET_GLOBAL_FUN(environment_pred, "is_environment");
SET_GLOBAL_FUN(get_environment, "get_environment"); SET_GLOBAL_FUN(get_environment, "get_environment");
SET_GLOBAL_FUN(get_environment, "env"); SET_GLOBAL_FUN(get_environment, "get_env");
} }
} }

5
tests/lean/lua4.lean
View file

@ -4,9 +4,10 @@ Variable x : Int
-- Add a variable to the environment using Lua -- Add a variable to the environment using Lua
-- The type of the new variable is equal to the type -- The type of the new variable is equal to the type
-- of x -- of x
typeofx = env():check_type(Const("x")) local env = get_environment()
typeofx = env:check_type(Const("x"))
print("type of x is " .. tostring(typeofx)) print("type of x is " .. tostring(typeofx))
env():add_var("y", typeofx) env:add_var("y", typeofx)
**) **)
Check x + y Check x + y

7
tests/lean/lua5.lean
View file

@ -1,11 +1,12 @@
Variable x : Int Variable x : Int
(** (**
local N = 100 local N = 100
local env = get_environment()
-- Create N variables with the same type of x -- Create N variables with the same type of x
typeofx = env():check_type(Const("x")) typeofx = env:check_type(Const("x"))
for i = 1, N do for i = 1, N do
env():add_var("y_" .. i, typeofx) env:add_var("y_" .. i, typeofx)
end end
**) **)

7
tests/lean/lua8.lean
View file

@ -1,13 +1,14 @@
Variable x : Int Variable x : Int
(** (**
ty_x = env():check_type(Const("x")) local env = get_environment()
ty_x = env:check_type(Const("x"))
c = context() c = context()
c = context(c, "x", ty_x) c = context(c, "x", ty_x)
c = context(c, "y", ty_x) c = context(c, "y", ty_x)
print(c) print(c)
o = env():find_object("x") o = env:find_object("x")
print(o) print(o)
o = env():find_object("y") o = env:find_object("y")
print(o) print(o)
**) **)