From 9f86aa73c83238209090cb06f1d511d748a21ed6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 12 May 2014 14:51:18 -0700
Subject: [PATCH] test(lua): add basic universe level tests

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

diff --git a/tests/lua/env5.lua b/tests/lua/env5.lua
new file mode 100644
index 000000000..fe316ff09
--- /dev/null
+++ b/tests/lua/env5.lua
@@ -0,0 +1,56 @@
+local env    = empty_environment()
+local l_name = name("l")
+local l      = mk_param_univ(l_name)
+local U_l    = mk_sort(l)
+local A      = Const("A")
+local x      = Const("x")
+local A2A    = mk_arrow(A, A)
+local id_ty  = Pi(A, U_l, mk_arrow(A, A))
+local id_def = Fun(A, U_l, Fun(x, A, x))
+env = add_decl(env, mk_definition(env, "id", {l_name}, id_ty, id_def, {opaque=false}))
+local ok, ex = pcall(function()
+                        env = add_decl(env, mk_definition(env, "id2", {"l2"}, id_ty, id_def, {opaque=false}))
+                     end
+)
+assert(not ok)
+print(ex:what())
+local tc     = type_checker(env)
+local ok, ex = pcall(function()
+                        local id     = Const("id")
+                        tc:check(id)
+                     end
+)
+assert(not ok)
+print(ex:what())
+local id_1 = Const("id", {mk_level_one()})
+print(tc:check(id_1))
+assert(not pcall(function()
+                    id_u = Const("id", {mk_global_univ("u")})
+                    print(tc:check(id_u))
+                 end
+))
+assert(not pcall(function()
+                    id_1_1 = Const("id", {mk_level_one(), mk_level_one()})
+                    print(tc:check(id_1_1))
+                 end
+))
+local env2 = env:add_global_level("u")
+assert(env2:is_descendant(env))
+assert(not env:is_descendant(env2))
+local tc2 = type_checker(env2)
+id_u = Const("id", {mk_global_univ("u")})
+print(tc2:check(id_u))
+print(tc2:check(tc2:check(id_u)))
+print(tc2:check(tc2:check(tc2:check(id_u))))
+env2 = add_decl(env2, mk_var_decl("a", Type))
+local tc2  = type_checker(env2)
+local a    = Const("a")
+local id_2 = Const("id", {mk_level_succ(mk_level_one())})
+print(tc2:check(id_2(Type, a)))
+assert(tc2:check(id_2(Type, a)) == Type)
+assert(not pcall(function() print(tc2:check(id_1(Type, a))) end))
+assert(tc2:whnf(id_2(Type, a)) == a)
+assert(tc2:whnf(id_2(Type, id_2(Type, a))) == a)
+local tc3 = type_checker(env, name_generator("foo"), {extra_opaque=name_set("id")})
+assert(tc3:whnf(id_2(Type, id_2(Type, a))) == id_2(Type, id_2(Type, a)))
+print(id_2(Type, id_2(Type, a)))