From eea561c74be33afb3c06442d73d37537504aa988 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 May 2014 09:19:48 -0700 Subject: [PATCH] test(lua): add more expr API unit tests Signed-off-by: Leonardo de Moura --- tests/lua/expr3.lua | 99 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 99 insertions(+) create mode 100644 tests/lua/expr3.lua diff --git a/tests/lua/expr3.lua b/tests/lua/expr3.lua new file mode 100644 index 000000000..eb2bf2695 --- /dev/null +++ b/tests/lua/expr3.lua @@ -0,0 +1,99 @@ +local b1 = binder_info() +assert(not b1:is_implicit()) +assert(not b1:is_cast()) + +local f = Const("f") +local a = Const("a") +local t = f(a) +assert(t:fn() == f) +assert(t:arg() == a) +assert(not pcall(function() f:fn() end)) + +local pi1 = Pi(a, Bool, Type) +assert(pi1:is_pi()) +assert(not pcall(function() f:binder_name() end)) +local pi2 = mk_pi("a", Bool, Type, binder_info(true, true)) +local pi3 = mk_pi("a", Bool, Type) +assert(pi2:binder_info():is_implicit()) +assert(not pi3:binder_info():is_implicit()) + +local l1 = mk_lambda("a", Bool, Var(0)) +local l2 = mk_lambda("a", Bool, Var(0), binder_info(true, false)) +assert(not l1:binder_info():is_implicit()) +assert(l2:binder_info():is_implicit()) + +local let1 = mk_let("a", Bool, Const("true"), f(Var(0))) + +local b = Const("b") +local pi3 = Pi({{a, Bool}, {b, Bool}}, a) +print(pi3) +assert(not pcall(function() Pi(a) end)) +local pi4 = Pi(a, Bool, b, Bool, a) +print(pi4) +assert(not pcall(function() Pi(a, Bool, b, Bool) end)) +assert(not pcall(function() Pi({}, Bool) end)) +assert(pi4:binder_name() == name("a")) +assert(pi4:binder_domain() == Bool) +assert(pi4:binder_body():is_pi()) + + +assert(f:kind() == expr_kind.Constant) +assert(pi3:kind() == expr_kind.Pi) + +assert(f:is_constant()) +assert(Var(0):is_var()) +assert(f(a):is_app()) +assert(l1:is_lambda()) +assert(pi3:is_pi()) +assert(l1:is_binder()) +assert(pi3:is_binder()) +assert(mk_metavar("m", Bool):is_metavar()) +assert(mk_local("m", Bool):is_local()) +assert(mk_metavar("m", Bool):is_mlocal()) +assert(mk_local("m", Bool):is_mlocal()) +assert(mk_metavar("m", Bool):is_meta()) +assert(mk_metavar("m", Bool)(a):is_meta()) +assert(f(mk_metavar("m", Bool)):has_metavar()) +assert(f(mk_local("l", Bool)):has_local()) +assert(not f(mk_metavar("m", Bool)):has_local()) +assert(not f(mk_local("l", Bool)):has_metavar()) +assert(f(mk_sort(mk_param_univ("l"))):has_param_univ()) +assert(f(Var(0)):has_free_vars()) +assert(not f(Var(0)):closed()) +assert(f(a):closed()) + +assert(Var(0):data() == 0) +assert(Const("a"):data() == name("a")) +assert(mk_sort(mk_param_univ("l")):data() == mk_param_univ("l")) +local f1, a1 = f(a):data() +assert(f1 == f) +assert(a1 == a) +local m1, t1 = mk_metavar("a", Bool):data() +assert(m1 == name("a")) +assert(t1 == Bool) +local m1, t1 = mk_local("a", Bool):data() +assert(m1 == name("a")) +assert(t1 == Bool) +local a1, t, b1, bi = mk_pi("a", Bool, Var(0), binder_info(true)):data() +assert(a1 == name("a")) +assert(t == Bool) +assert(b1 == Var(0)) +assert(bi:is_implicit()) +assert(not bi:is_cast()) +assert(f:is_constant()) +f(f(a)):for_each(function (e, o) print(tostring(e)); return true; end) +assert(f(Var(0)):lift_free_vars(1) == f(Var(1))) +assert(f(Var(1)):lift_free_vars(1, 1) == f(Var(2))) +assert(f(Var(1)):lift_free_vars(2, 1) == f(Var(1))) +assert(f(Var(1)):lower_free_vars(1, 1) == f(Var(0))) +assert(f(Var(1)):lower_free_vars(4, 1) == f(Var(1))) +assert(f(Var(0), Var(1)):instantiate(a) == f(a, Var(0))) +assert(f(Var(0), Var(1)):instantiate({a, b}) == f(a, b)) +assert(f(a, b):abstract(a) == f(Var(0), b)) +assert(f(a, b):abstract({a, b}) == f(Var(1), Var(0))) + +assert(a:occurs(f(a))) +assert(not f(a):is_eqp(f(a))) +assert(f(a):arg():is_eqp(a)) +assert(f(a):depth() == 2) +print(f(a):hash())