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

feat(library/kernel_bindings): improve list_level support in the Lua interface

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-19 15:18:48 -07:00
parent 48b436c1c8
commit a7aacaa782
2 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/kernel_bindings.cpp
View file

@ -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<level> 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)));
}

17
tests/lua/ind1.lua
View file

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