From 984048f40dd7604a09d551eb23b6dfe285daa22d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Apr 2014 15:08:58 -0700 Subject: [PATCH] feat(library/kernel_bindings): new level Lua API Signed-off-by: Leonardo de Moura --- src/library/kernel_bindings.cpp | 53 ++++++++++++++++++++++++++------- tests/lua/level1.lua | 28 +++++++++++++++++ 2 files changed, 70 insertions(+), 11 deletions(-) create mode 100644 tests/lua/level1.lua diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 1769ae18c..2375d010b 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -35,23 +35,45 @@ static int mk_level_max(lua_State * L) { return push_level(L, mk_max(to_level(L static int mk_level_imax(lua_State * L) { return push_level(L, mk_imax(to_level(L, 1), to_level(L, 2))); } static int mk_param_univ(lua_State * L) { return push_level(L, mk_param_univ(to_name_ext(L, 1))); } static int mk_meta_univ(lua_State * L) { return push_level(L, mk_meta_univ(to_name_ext(L, 1))); } - -#define LEVEL_PRED(P) \ -static int level_ ## P(lua_State * L) { \ - lua_pushboolean(L, P(to_level(L, 1))); \ - return 1; \ -} - +#define LEVEL_PRED(P) static int level_ ## P(lua_State * L) { return pushboolean(L, P(to_level(L, 1))); } LEVEL_PRED(is_zero) LEVEL_PRED(is_param) LEVEL_PRED(is_meta) LEVEL_PRED(is_succ) LEVEL_PRED(is_max) LEVEL_PRED(is_imax) +LEVEL_PRED(is_explicit) +LEVEL_PRED(has_meta) +LEVEL_PRED(has_param) +LEVEL_PRED(is_not_zero) +static int level_get_kind(lua_State * L) { return pushinteger(L, static_cast(kind(to_level(L, 1)))); } +static int level_trivially_leq(lua_State * L) { return pushboolean(L, is_trivial(to_level(L, 1), to_level(L, 2))); } -static int level_get_kind(lua_State * L) { - lua_pushinteger(L, static_cast(kind(to_level(L, 1)))); - return 1; +static int level_id(lua_State * L) { + level const & l = to_level(L, 1); + if (is_param(l)) return push_name(L, param_id(l)); + else if (is_meta(l)) return push_name(L, meta_id(l)); + else throw exception("arg #1 must be a level parameter/metavariable"); +} + +static int level_lhs(lua_State * L) { + level const & l = to_level(L, 1); + if (is_max(l)) return push_level(L, max_lhs(l)); + else if (is_imax(l)) return push_level(L, imax_lhs(l)); + else throw exception("arg #1 must be a level max/imax expression"); +} + +static int level_rhs(lua_State * L) { + level const & l = to_level(L, 1); + if (is_max(l)) return push_level(L, max_rhs(l)); + else if (is_imax(l)) return push_level(L, imax_rhs(l)); + else throw exception("arg #1 must be a level max/imax expression"); +} + +static int level_succ_of(lua_State * L) { + level const & l = to_level(L, 1); + if (is_succ(l)) return push_level(L, succ_of(l)); + else throw exception("arg #1 must be a level succ expression"); } static const struct luaL_Reg level_m[] = { @@ -59,6 +81,7 @@ static const struct luaL_Reg level_m[] = { {"__tostring", safe_function}, {"__eq", safe_function}, {"__lt", safe_function}, + {"succ", safe_function}, {"kind", safe_function}, {"is_zero", safe_function}, {"is_param", safe_function}, @@ -66,7 +89,15 @@ static const struct luaL_Reg level_m[] = { {"is_succ", safe_function}, {"is_max", safe_function}, {"is_imax", safe_function}, - {"succ", safe_function}, + {"is_explicit", safe_function}, + {"has_meta", safe_function}, + {"has_param", safe_function}, + {"is_not_zero", safe_function}, + {"trivially_leq", safe_function}, + {"id", safe_function}, + {"lhs", safe_function}, + {"rhs", safe_function}, + {"succ_of", safe_function}, {0, 0} }; diff --git a/tests/lua/level1.lua b/tests/lua/level1.lua new file mode 100644 index 000000000..90e3a309a --- /dev/null +++ b/tests/lua/level1.lua @@ -0,0 +1,28 @@ +assert(level():is_zero()) +assert(mk_level_zero():is_zero()) +assert(mk_level_one():is_succ()) +assert(not mk_level_one():is_zero()) +assert(mk_level_max(mk_level_zero(), mk_level_one()):is_succ()) +assert(mk_level_max(mk_param_univ("a"), mk_param_univ("b")):is_max()) +assert(mk_level_max(mk_level_one(), mk_level_zero()):is_succ()) +assert(level():succ():is_succ()) +assert(mk_level_imax(mk_level_one(), mk_level_zero()):is_zero()) +assert(is_level(mk_level_one())) +assert(not is_level(1)) +assert(mk_level_one():succ_of() == mk_level_zero()) +assert(mk_level_one():succ_of():is_zero()) +assert(mk_level_succ(mk_level_succ(level())):is_not_zero()) +assert(not mk_param_univ("a"):is_not_zero()) +assert(mk_level_max(mk_param_univ("a"), mk_param_univ("b")):lhs() == mk_param_univ("a")) +assert(mk_level_max(mk_param_univ("a"), mk_param_univ("b")):rhs() == mk_param_univ("b")) +assert(mk_level_imax(mk_param_univ("a"), mk_param_univ("b")):lhs() == mk_param_univ("a")) +assert(mk_level_imax(mk_param_univ("a"), mk_param_univ("b")):rhs() == mk_param_univ("b")) +assert(mk_param_univ("a"):id() == name("a")) +assert(mk_meta_univ("b"):id() == name("b")) +assert(level():trivially_leq(mk_level_one())) +assert(level():trivially_leq(mk_param_univ("a"))) +assert(not mk_param_univ("b"):trivially_leq(mk_param_univ("a"))) +assert(mk_level_one():kind() == level_kind.Succ) +assert(not mk_level_one():has_meta()) +assert(not mk_level_succ(mk_param_univ("a")):has_meta()) +assert(mk_level_succ(mk_meta_univ("a")):has_meta())