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

test(lua/environment): add missing tests

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

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

@ -50,6 +50,11 @@ static int mk_environment(lua_State * L) {
return push_environment(L, f.get_environment());
}
static int environment_mk_child(lua_State * L) {
rw_environment env(L, 1);
return push_environment(L, env->mk_child());
}
static int environment_has_parent(lua_State * L) {
ro_environment env(L, 1);
lua_pushboolean(L, env->has_parent());
@ -214,6 +219,7 @@ static int environment_tostring(lua_State * L) {
static const struct luaL_Reg environment_m[] = {
{"__gc", environment_gc}, // never throws
{"__tostring", safe_function<environment_tostring>},
{"mk_child", safe_function<environment_mk_child>},
{"has_parent", safe_function<environment_has_parent>},
{"has_children", safe_function<environment_has_children>},
{"parent", safe_function<environment_parent>},

30
tests/lua/env4.lua Normal file
View file

@ -0,0 +1,30 @@
assert(not pcall(function() get_environment() end))
local env = environment()
env:add_uvar("Z", level(level("M"), 1))
assert(env:is_ge(level("Z"), level("M")))
local child = env:mk_child()
assert(env:has_children())
assert(child:has_parent())
child:add_var("x", Const("Int"))
for o in child:local_objects() do
assert(o:get_name() == name("x"))
print(o)
end
local eenv = empty_environment()
assert(eenv:find_object("Int"):is_null())
assert(not pcall(function() env:parent() end))
local p = child:parent()
assert(p:has_children())
assert(not pcall(function() env:add_uvar("Z") end))
child:add_definition("val1", Const("true"), true)
child:add_definition("val2", Const("Bool"), Const("true"), true)
local ok, msg = pcall(function() child:add_definition("val3", Const("Int"), Const("true"), true) end)
assert(not ok)
print(msg)
assert(child:normalize(Const("val2")) == Const("val2"))
child:add_theorem("Th1", Eq(iVal(0), iVal(0)), Const("Trivial"))
child:add_axiom("H1", Eq(Const("x"), iVal(0)))
assert(child:has_object("H1"))
local ctx = context(context(), "x", Const("Int"), iVal(10))
assert(child:normalize(Var(0), ctx) == iVal(10))
assert(child:check_type(Var(0), ctx) == Const("Int"))