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

test(lua): add more tests for the environment Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-21 12:36:04 -07:00
parent e39feabb72
commit 203a59b682
1 changed files with 37 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
tests/lua/env11.lua Normal file
View file

@ -0,0 +1,37 @@
local A = Const("A")
local B = Const("B")
local env = environment()
local env1 = add_decl(env, mk_var_decl("A", Bool))
env1 = add_decl(env1, mk_var_decl("B", Bool))
env1 = add_decl(env1, mk_axiom("H", B))
local c1 = check(env1, mk_axiom("H1", A))
local c2 = check(env1, mk_axiom("H2", A))
local env1b = env1:add(c1)
local env2 = env1b:add(c2)
local c3 = check(env2, mk_theorem("H3", A, Const("H1")))
function expected_error(f)
ok, ex = pcall(f)
assert(not ok)
print("expected error: " .. ex:what())
end
expected_error(function() env1:add(c3) end)
expected_error(function() env2:add(c1) end)
env3 = env2:add_global_level("u")
expected_error(function() env3:add_global_level("u") end)
expected_error(function() check(env2, mk_theorem("H1", A, Const("H1"))) end)
local c4 = check(env1b, mk_theorem("H2", A, Const("H1")))
expected_error(function() env3:add(c4) end)
env3 = env3:replace(c4)
assert(env2:find("H2"):is_axiom())
assert(not env3:find("H2"):is_axiom())
assert(env3:find("H2"):is_theorem())
local c5 = check(env1b, mk_theorem("H5", A, Const("H1")))
expected_error(function() env3:replace(c5) end)
local c6 = check(env, mk_definition("A", Type, Bool))
expected_error(function() env3:replace(c6) end)
local c7 = check(env1b, mk_definition("H2", A, Const("H1")))
expected_error(function() env2:replace(c7) end)
local c8 = check(env1b, mk_theorem("H2", B, Const("H")))
expected_error(function() env2:replace(c8) end)