From dc627c99650681981265895d0ab474d4dcfacf12 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 May 2014 13:37:46 -0700
Subject: [PATCH] test(lua): add constraint API tests, and fix minor bugs

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/kernel_bindings.cpp |  4 ++--
 tests/lua/cnstr1.lua            | 35 +++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 2 deletions(-)
 create mode 100644 tests/lua/cnstr1.lua

diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 663b3a7f6..f0cdc04f4 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1031,7 +1031,7 @@ static int constraint_tostring(lua_State * L) {
 static int mk_eq_cnstr(lua_State * L) { return push_constraint(L, mk_eq_cnstr(to_expr(L, 1), to_expr(L, 2), to_justification(L, 3))); }
 static int mk_conv_cnstr(lua_State * L) { return push_constraint(L, mk_conv_cnstr(to_expr(L, 1), to_expr(L, 2), to_justification(L, 3))); }
 static int mk_level_cnstr(lua_State * L) { return push_constraint(L, mk_level_cnstr(to_level(L, 1), to_level(L, 2), to_justification(L, 3))); }
-static int mk_choice_cnstr(lua_State * L) { return push_constraint(L, mk_choice_cnstr(to_expr(L, 1), to_list_expr_ext(L, 3), to_justification(L, 3))); }
+static int mk_choice_cnstr(lua_State * L) { return push_constraint(L, mk_choice_cnstr(to_expr(L, 1), to_list_expr_ext(L, 2), to_justification(L, 3))); }
 
 static const struct luaL_Reg constraint_m[] = {
     {"__gc",            constraint_gc}, // never throws
@@ -1042,7 +1042,7 @@ static const struct luaL_Reg constraint_m[] = {
     {"is_eqc",          safe_function<constraint_is_eqc_cnstr>},
     {"is_level",        safe_function<constraint_is_level_cnstr>},
     {"is_choice",       safe_function<constraint_is_choice_cnstr>},
-    {"is_choice",       safe_function<constraint_is_eqp>},
+    {"is_eqp",          safe_function<constraint_is_eqp>},
     {"kind",            safe_function<constraint_kind>},
     {"hash",            safe_function<constraint_hash>},
     {"lhs",             safe_function<constraint_lhs>},
diff --git a/tests/lua/cnstr1.lua b/tests/lua/cnstr1.lua
new file mode 100644
index 000000000..276ced0f4
--- /dev/null
+++ b/tests/lua/cnstr1.lua
@@ -0,0 +1,35 @@
+local a = Const("a")
+local f = Const("f")
+local m = mk_metavar("m", Bool)
+local j = justification("type match")
+local c = mk_eq_cnstr(f(a), m, j)
+assert(c:is_eq())
+assert(c:is_eqc())
+assert(not c:is_choice())
+assert(not c:is_level())
+assert(c:lhs() == f(a))
+assert(c:rhs() == m)
+assert(c:justification():is_eqp(j))
+print(c)
+local c2 = mk_conv_cnstr(f(m), f(a), j)
+print(c2)
+assert(not c2:is_eq())
+assert(c2:is_conv())
+assert(c2:is_eqc())
+assert(c2:lhs() == f(m))
+local c3 = mk_level_cnstr(mk_level_zero(), mk_level_one(), j)
+assert(c3:is_level())
+print(c3)
+assert(c ~= c2)
+assert(c == mk_eq_cnstr(f(a), m, j))
+assert(c:is_eqp(c))
+assert(not c:is_eqp(mk_eq_cnstr(f(a), m, j)))
+assert(c:hash() == mk_eq_cnstr(f(a), m, j):hash())
+local c4 = mk_choice_cnstr(m, {a, f(a), f(f(a))}, j)
+print(c4)
+assert(c4:is_choice())
+assert(c4:choice_expr() == m)
+print(c4:choice_set():head())
+assert(c4:choice_set():head() == a)
+assert(c4:choice_set():tail():head() == f(a))
+assert(#(c4:choice_set()) == 3)