From e4f09335cecc8e0dabfae80e65bffda4abdd761e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 May 2014 14:54:20 -0700
Subject: [PATCH] test(lua): new module system test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lua/mod2.lua | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 tests/lua/mod2.lua

diff --git a/tests/lua/mod2.lua b/tests/lua/mod2.lua
new file mode 100644
index 000000000..2e2062071
--- /dev/null
+++ b/tests/lua/mod2.lua
@@ -0,0 +1,46 @@
+function mk_env(prefix, sz)
+   prefix    = name(prefix)
+   local env = environment()
+   local A   = Local("A", mk_sort(0))
+   local x   = Local("x", A)
+   env = add_decl(env, mk_definition(name(prefix, "id"), Pi(A, mk_arrow(A, A)), Fun({A, x}, x), {opaque=false}))
+   env = add_decl(env, mk_var_decl(name(prefix, "P"), Bool))
+   local P   = Const(name(prefix, "P"))
+   local id  = Const(name(prefix, "id"))
+   env = add_decl(env, mk_axiom(name(prefix, "Ax"), P))
+   local Ax  = Const(name(prefix, "Ax"))
+   for i = 1, sz do
+      local pr = id(P, Ax)
+      for j = 1, i do
+         pr = id(P, pr)
+      end
+      local pr2 = id(P, pr)
+      env = add_decl(env, mk_theorem(name(prefix, "T", i), P, pr))
+   end
+   return env
+end
+
+local mod_names = {}
+
+function export_env(i, sz)
+   local prefix = "mod" .. tostring(i)
+   local mname  = "mod2_" .. prefix
+   mod_names[#mod_names + 1] = mname
+   mk_env(prefix, sz):export(mname .. ".olean")
+end
+
+local NumMods=40
+local NumThs=200
+for i = 1, NumMods do
+   export_env(i, NumThs)
+end
+
+print("importing...")
+local initt = os.clock()
+local env2  = import_modules(mod_names, 4)
+print(string.format("elapsed time: %.2f\n", os.clock() - initt))
+for i = 1, NumMods do
+   for j = 1, NumThs do
+      assert(env2:get({"mod" .. tostring(i), "T", j}):is_theorem())
+   end
+end