From 9e55c8766fa48fdc6f420cc2d66aa3ee9d5e2ab4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 May 2014 09:56:27 -0700 Subject: [PATCH] test(lua): add normalize and type_check tests for terms containing metavariables Signed-off-by: Leonardo de Moura --- tests/lua/expr9.lua | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 tests/lua/expr9.lua diff --git a/tests/lua/expr9.lua b/tests/lua/expr9.lua new file mode 100644 index 0000000000..295bec3b22 --- /dev/null +++ b/tests/lua/expr9.lua @@ -0,0 +1,23 @@ +local env = environment() +local m = mk_metavar("m", mk_arrow(Bool, Bool)) +local a = Local("a", Bool) +print(env:normalize(Fun(a, m))) +print(env:normalize(Fun(a, m(a)))) +local m2 = mk_metavar("m2", mk_arrow(Bool, Bool, Bool)) +print(env:normalize(Fun(a, (m2(a))(a)))) +env:type_check(m) +env:type_check(Fun(a, m(a))) +env:type_check(Fun(a, (m2(a))(a))) +local m3 = mk_metavar("m3", mk_metavar("m4", mk_sort(mk_meta_univ("l")))) +env:type_check(m3) +-- The following call fails, because the type checker will try to +-- create a constraint, but constraint generation is not supported by +-- the type checker used to implement the method type_check +assert(not pcall(function() + env:type_check(m3(a)) + end +)) + + + +