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

test(lua): add constraint API tests, and fix minor bugs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-02 13:37:46 -07:00
parent 91069c5f7f
commit dc627c9965
2 changed files with 37 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/kernel_bindings.cpp
View file

@ -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>},

35
tests/lua/cnstr1.lua Normal file
View file

@ -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)