michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua): add more tests for type checker

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 14:17:58 -07:00
parent 16553e77fa
commit da31e60b02
1 changed files with 47 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
tests/lua/tc5.lua Normal file
View file

@ -0,0 +1,47 @@
local env = empty_environment()
env = add_decl(env, mk_var_decl("A", Bool))
env = add_decl(env, mk_var_decl("T", Type))
env = add_decl(env, mk_definition("B2", Type, Bool, {opaque=false}))
env = add_decl(env, mk_var_decl("C", Const("B2")))
env = add_decl(env, mk_definition("BB", Type, mk_arrow(Bool, Bool), {opaque=false}))
local tc = type_checker(env)
assert(tc:is_prop(Const("A")))
assert(tc:is_prop(Const("C")))
assert(not tc:is_prop(Const("T")))
assert(not tc:is_prop(Const("B2")))
assert(not pcall(function()
print(tc:check(mk_lambda("x", mk_metavar("m", mk_metavar("t", mk_sort(mk_meta_univ("l")))), Var(0))))
end
))
print(tc:ensure_sort(Const("B2")))
assert(not pcall(function()
print(tc:ensure_sort(Const("A")))
end
))
print(tc:ensure_pi(Const("BB")))
assert(not pcall(function()
print(tc:ensure_pi(Const("A")))
end
))
assert(not pcall(function()
env = add_decl(env, mk_var_decl("A", mk_local("l1", Bool)))
end
))
assert(not pcall(function()
print(tc:check(Let("x", Type, Const("A"), Var(0))))
end
))
assert(not pcall(function()
print(tc:check(mk_lambda("x", Bool, Var(0))(Type)))
end
))
assert(not pcall(function()
print(tc:check(Var(0)))
end
))
assert(tc:check(mk_pi("x", Bool, Var(0))) == Bool)
local env = empty_environment({impredicative=false})
local tc = type_checker(env)
assert(tc:check(mk_pi("x", Bool, Var(0))) == Type)