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

test(lua): unit tests for let expressions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-14 14:29:44 -07:00
parent 893e4d4ae2
commit 52d682b832
1 changed files with 25 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
tests/lua/let1.lua Normal file
View file

@ -0,0 +1,25 @@
assert(not mk_let("a", Type, Var(0), Var(0)):closed())
local env = empty_environment()
local A = Const("A")
env = add_decl(env, mk_var_decl("A", Type))
env = add_decl(env, mk_var_decl("g", mk_arrow(A, mk_arrow(A, A))))
env = add_decl(env, mk_var_decl("f", mk_arrow(A, Bool)))
env = add_decl(env, mk_var_decl("a", A))
local a = Const("a")
local b = Const("b")
local x = Const("x")
local y = Const("y")
local g = Const("g")
local f = Const("f")
local tc = type_checker(env)
print(Let(x, A, a, f(x)))
print(Let(x, A, a, y, A, f(f(x)), f(x)))
assert(Let(x, A, a, y, A, f(f(x)), f(x)) == Let({{x, A, a}, {y, A, f(f(x))}}, f(x)))
print(Let({{x, A, a}, {y, A, g(g(x), x, a)}}, f(y)))
local t = Let({{x, A, a}, {y, A, g(g(x), x, a)}}, f(y))
assert(t:let_name() == name("x"))
assert(t:let_type() == A)
assert(t:let_value() == a)
assert(t:let_body():is_let())
print(tc:check(Let({{x, A, a}, {y, A, g(g(x, a), x)}}, f(y))))