From 46c292be7188367a5aca81c5e33b2cfb99f58db6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 May 2014 11:26:28 -0700 Subject: [PATCH] test(lua): add simple module export/import test Signed-off-by: Leonardo de Moura --- tests/lua/mod1.lua | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/lua/mod1.lua diff --git a/tests/lua/mod1.lua b/tests/lua/mod1.lua new file mode 100644 index 000000000..f7ad7ef5b --- /dev/null +++ b/tests/lua/mod1.lua @@ -0,0 +1,21 @@ +local env = environment() +env = add_decl(env, mk_var_decl("A", Bool)) +local A = Const("A") +env = add_decl(env, mk_axiom("H1", A)) +local H1 = Const("H1") +env = add_decl(env, mk_theorem("H2", A, H1)) +assert(env:get("H2"):is_theorem()) +env = add_decl(env, mk_definition("B", Bool, A)) +env:export("mod1_mod.olean") + +local env2 = import_modules("mod1_mod.olean") +assert(env2:get("A"):type() == Bool) +assert(env2:get("A"):is_var_decl()) +assert(env2:get("H1"):type() == A) +assert(env2:get("H1"):is_axiom()) +assert(env2:get("H2"):type() == A) +assert(env2:get("H2"):is_theorem()) +assert(env2:get("H2"):value() == H1) +assert(env2:get("B"):type() == Bool) +assert(env2:get("B"):value() == A) +assert(env2:get("B"):is_definition())