From 203a59b682086f73351d65e618176e63e945059e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 May 2014 12:36:04 -0700 Subject: [PATCH] test(lua): add more tests for the environment Lua API Signed-off-by: Leonardo de Moura --- tests/lua/env11.lua | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tests/lua/env11.lua diff --git a/tests/lua/env11.lua b/tests/lua/env11.lua new file mode 100644 index 000000000..98877ded2 --- /dev/null +++ b/tests/lua/env11.lua @@ -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) +