lean2/tests/lua/env5.lua
Leonardo de Moura 9f86aa73c8 test(lua): add basic universe level tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:51:18 -07:00

56 lines
2 KiB
Lua

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)))