From a7aacaa782d7106dfa893d25923412fc94757b2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 May 2014 15:18:48 -0700 Subject: [PATCH] feat(library/kernel_bindings): improve list_level support in the Lua interface Signed-off-by: Leonardo de Moura --- src/library/kernel_bindings.cpp | 3 ++- tests/lua/ind1.lua | 17 ++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index cd64e6d04..63feebeed 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -43,7 +43,6 @@ io_state * get_io_state(lua_State * L); // Level DECL_UDATA(level) -DEFINE_LUA_LIST(level, push_level, to_level) int push_optional_level(lua_State * L, optional const & l) { return l ? push_level(L, *l) : push_nil(L); } @@ -67,6 +66,8 @@ static level to_level_ext(lua_State * L, int idx) { return to_level(L, idx); } +DEFINE_LUA_LIST(level, push_level, to_level_ext) + static int level_add(lua_State * L) { return push_level(L, mk_offset(to_level(L, 1), luaL_checkinteger(L, 2))); } diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua index 0786e184d..f5212c38b 100644 --- a/tests/lua/ind1.lua +++ b/tests/lua/ind1.lua @@ -67,9 +67,9 @@ env = add_inductive(env, {l}, 1, "consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))}) local tc = type_checker(env) -display_type(env, Const("forest", {mk_level_zero()})) -display_type(env, Const("vcons", {mk_level_zero()})) -display_type(env, Const("consf", {mk_level_zero()})) +display_type(env, Const("forest", {0})) +display_type(env, Const("vcons", {0})) +display_type(env, Const("consf", {0})) display_type(env, Const("forest_rec", {v, u})) display_type(env, Const("nat_rec", {v})) display_type(env, Const("or_rec")) @@ -103,10 +103,9 @@ display_type(env, Const("and_rec", {v})) display_type(env, Const("vec_rec", {v, u})) display_type(env, Const("flist_rec", {v, u})) -local U_1 = mk_level_one() local n = Const("n") local c = Const("c") -local nat_rec1 = Const("nat_rec", {U_1}) +local nat_rec1 = Const("nat_rec", {1}) local add = Fun({{a, Nat}, {b, Nat}}, nat_rec1(mk_lambda("_", Nat, Nat), b, Fun({{n, Nat}, {c, Nat}}, succ(c)), a)) display_type(env, add) local tc = type_checker(env) @@ -115,15 +114,15 @@ assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)), assert(tc:is_def_eq(add(succ(succ(succ(zero))), succ(succ(zero))), succ(succ(succ(succ(succ(zero))))))) -local list_nat = Const("list", {U_1})(Nat) -local list_nat_rec1 = Const("list_rec", {U_1, U_1})(Nat) +local list_nat = Const("list", {1})(Nat) +local list_nat_rec1 = Const("list_rec", {1, 1})(Nat) display_type(env, list_nat_rec1) local h = Const("h") local t = Const("t") local lst = Const("lst") local length = Fun(lst, list_nat, list_nat_rec1(mk_lambda("_", list_nat, Nat), zero, Fun({{h, Nat}, {t, list_nat}, {c, Nat}}, succ(c)), lst)) -local nil_nat = Const("nil", {U_1})(Nat) -local cons_nat = Const("cons", {U_1})(Nat) +local nil_nat = Const("nil", {1})(Nat) +local cons_nat = Const("cons", {1})(Nat) print(tc:whnf(length(nil_nat))) assert(tc:is_def_eq(length(nil_nat), zero)) assert(tc:is_def_eq(length(cons_nat(zero, nil_nat)), succ(zero)))