chore(util/lua): name convention
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
7cd892464f
commit
a5229e5283
12 changed files with 92 additions and 451 deletions
|
|
@ -30,7 +30,7 @@ io_state * get_io_state(lua_State * L);
|
|||
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) : pushnil(L); }
|
||||
int push_optional_level(lua_State * L, optional<level> const & l) { return l ? push_level(L, *l) : push_nil(L); }
|
||||
|
||||
static int level_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
|
|
@ -40,8 +40,8 @@ static int level_tostring(lua_State * L) {
|
|||
return 1;
|
||||
}
|
||||
|
||||
static int level_eq(lua_State * L) { return pushboolean(L, to_level(L, 1) == to_level(L, 2)); }
|
||||
static int level_lt(lua_State * L) { return pushboolean(L, is_lt(to_level(L, 1), to_level(L, 2))); }
|
||||
static int level_eq(lua_State * L) { return push_boolean(L, to_level(L, 1) == to_level(L, 2)); }
|
||||
static int level_lt(lua_State * L) { return push_boolean(L, is_lt(to_level(L, 1), to_level(L, 2))); }
|
||||
static int mk_level_zero(lua_State * L) { return push_level(L, mk_level_zero()); }
|
||||
static int mk_level_one(lua_State * L) { return push_level(L, mk_level_one()); }
|
||||
static int mk_level_succ(lua_State * L) { return push_level(L, mk_succ(to_level(L, 1))); }
|
||||
|
|
@ -49,7 +49,7 @@ 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) { return pushboolean(L, P(to_level(L, 1))); }
|
||||
#define LEVEL_PRED(P) static int level_ ## P(lua_State * L) { return push_boolean(L, P(to_level(L, 1))); }
|
||||
LEVEL_PRED(is_zero)
|
||||
LEVEL_PRED(is_param)
|
||||
LEVEL_PRED(is_meta)
|
||||
|
|
@ -60,9 +60,9 @@ 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<int>(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_is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_level(L, 1), to_level(L, 2))); }
|
||||
static int level_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(kind(to_level(L, 1)))); }
|
||||
static int level_trivially_leq(lua_State * L) { return push_boolean(L, is_trivial(to_level(L, 1), to_level(L, 2))); }
|
||||
static int level_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_level(L, 1), to_level(L, 2))); }
|
||||
|
||||
static int level_id(lua_State * L) {
|
||||
level const & l = to_level(L, 1);
|
||||
|
|
@ -164,8 +164,8 @@ static int mk_binder_info(lua_State * L) {
|
|||
else
|
||||
return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
|
||||
}
|
||||
static int binder_info_is_implicit(lua_State * L) { return pushboolean(L, to_expr_binder_info(L, 1).is_implicit()); }
|
||||
static int binder_info_is_cast(lua_State * L) { return pushboolean(L, to_expr_binder_info(L, 1).is_cast()); }
|
||||
static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_implicit()); }
|
||||
static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_cast()); }
|
||||
static const struct luaL_Reg binder_info_m[] = {
|
||||
{"__gc", expr_binder_info_gc},
|
||||
{"is_implicit", safe_function<binder_info_is_implicit>},
|
||||
|
|
@ -186,7 +186,7 @@ static void open_binder_info(lua_State * L) {
|
|||
DECL_UDATA(expr)
|
||||
DEFINE_LUA_LIST(expr, push_expr, to_expr)
|
||||
|
||||
int push_optional_expr(lua_State * L, optional<expr> const & e) { return e ? push_expr(L, *e) : pushnil(L); }
|
||||
int push_optional_expr(lua_State * L, optional<expr> const & e) { return e ? push_expr(L, *e) : push_nil(L); }
|
||||
|
||||
expr & to_app(lua_State * L, int idx) {
|
||||
expr & r = to_expr(L, idx);
|
||||
|
|
@ -215,11 +215,11 @@ static int expr_tostring(lua_State * L) {
|
|||
options opts = get_global_options(L);
|
||||
environment env = get_global_environment(L);
|
||||
out << mk_pair(fmt(env, to_expr(L, 1), opts), opts);
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int expr_eq(lua_State * L) { return pushboolean(L, to_expr(L, 1) == to_expr(L, 2)); }
|
||||
static int expr_lt(lua_State * L) { return pushboolean(L, to_expr(L, 1) < to_expr(L, 2)); }
|
||||
static int expr_eq(lua_State * L) { return push_boolean(L, to_expr(L, 1) == to_expr(L, 2)); }
|
||||
static int expr_lt(lua_State * L) { return push_boolean(L, to_expr(L, 1) < to_expr(L, 2)); }
|
||||
static int expr_mk_constant(lua_State * L) { return push_expr(L, mk_constant(to_name_ext(L, 1))); }
|
||||
static int expr_mk_var(lua_State * L) { return push_expr(L, mk_var(luaL_checkinteger(L, 1))); }
|
||||
static int expr_mk_app(lua_State * L) {
|
||||
|
|
@ -309,9 +309,9 @@ static int expr_pi(lua_State * L) { return expr_abst<Pi, Pi>(L); }
|
|||
static int expr_mk_sort(lua_State * L) { return push_expr(L, mk_sort(to_level(L, 1))); }
|
||||
static int expr_mk_metavar(lua_State * L) { return push_expr(L, mk_metavar(to_name_ext(L, 1), to_expr(L, 2))); }
|
||||
static int expr_mk_local(lua_State * L) { return push_expr(L, mk_local(to_name_ext(L, 1), to_expr(L, 2))); }
|
||||
static int expr_get_kind(lua_State * L) { return pushinteger(L, static_cast<int>(to_expr(L, 1).kind())); }
|
||||
static int expr_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(to_expr(L, 1).kind())); }
|
||||
|
||||
#define EXPR_PRED(P) static int expr_ ## P(lua_State * L) { return pushboolean(L, P(to_expr(L, 1))); }
|
||||
#define EXPR_PRED(P) static int expr_ ## P(lua_State * L) { return push_boolean(L, P(to_expr(L, 1))); }
|
||||
|
||||
EXPR_PRED(is_constant)
|
||||
EXPR_PRED(is_var)
|
||||
|
|
@ -335,7 +335,7 @@ static int expr_fields(lua_State * L) {
|
|||
expr & e = to_expr(L, 1);
|
||||
switch (e.kind()) {
|
||||
case expr_kind::Var:
|
||||
return pushinteger(L, var_idx(e));
|
||||
return push_integer(L, var_idx(e));
|
||||
case expr_kind::Constant:
|
||||
push_name(L, const_name(e)); push_list_level(L, const_level_params(e)); return 2;
|
||||
case expr_kind::Sort:
|
||||
|
|
@ -380,10 +380,9 @@ static int expr_for_each(lua_State * L) {
|
|||
static int expr_has_free_var(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2)
|
||||
lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2)));
|
||||
return push_boolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2)));
|
||||
else
|
||||
lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3)));
|
||||
return 1;
|
||||
return push_boolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3)));
|
||||
}
|
||||
|
||||
static int expr_lift_free_vars(lua_State * L) {
|
||||
|
|
@ -441,11 +440,11 @@ static int binder_domain(lua_State * L) { return push_expr(L, binder_domain(to_b
|
|||
static int binder_body(lua_State * L) { return push_expr(L, binder_body(to_binder(L, 1))); }
|
||||
static int binder_info(lua_State * L) { return push_expr_binder_info(L, binder_info(to_binder(L, 1))); }
|
||||
|
||||
static int expr_occurs(lua_State * L) { return pushboolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); }
|
||||
static int expr_is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); }
|
||||
static int expr_hash(lua_State * L) { return pushinteger(L, to_expr(L, 1).hash()); }
|
||||
static int expr_depth(lua_State * L) { return pushinteger(L, get_depth(to_expr(L, 1))); }
|
||||
static int expr_is_lt(lua_State * L) { return pushboolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), false)); }
|
||||
static int expr_occurs(lua_State * L) { return push_boolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); }
|
||||
static int expr_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); }
|
||||
static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); }
|
||||
static int expr_depth(lua_State * L) { return push_integer(L, get_depth(to_expr(L, 1))); }
|
||||
static int expr_is_lt(lua_State * L) { return push_boolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), false)); }
|
||||
|
||||
static int expr_mk_macro(lua_State * L) {
|
||||
buffer<expr> args;
|
||||
|
|
@ -454,8 +453,8 @@ static int expr_mk_macro(lua_State * L) {
|
|||
}
|
||||
|
||||
static int macro_def(lua_State * L) { return push_macro_definition(L, macro_def(to_macro_app(L, 1))); }
|
||||
static int macro_num_args(lua_State * L) { return pushinteger(L, macro_num_args(to_macro_app(L, 1))); }
|
||||
static int macro_arg(lua_State * L) { return push_expr(L, macro_arg(to_macro_app(L, 1), pushinteger(L, 2))); }
|
||||
static int macro_num_args(lua_State * L) { return push_integer(L, macro_num_args(to_macro_app(L, 1))); }
|
||||
static int macro_arg(lua_State * L) { return push_expr(L, macro_arg(to_macro_app(L, 1), push_integer(L, 2))); }
|
||||
|
||||
static const struct luaL_Reg expr_m[] = {
|
||||
{"__gc", expr_gc}, // never throws
|
||||
|
|
@ -559,15 +558,15 @@ static void open_expr(lua_State * L) {
|
|||
DECL_UDATA(macro_definition)
|
||||
|
||||
int macro_get_name(lua_State * L) { return push_name(L, to_macro_definition(L, 1).get_name()); }
|
||||
int macro_trust_level(lua_State * L) { return pushinteger(L, to_macro_definition(L, 1).trust_level()); }
|
||||
int macro_eq(lua_State * L) { return pushboolean(L, to_macro_definition(L, 1) == to_macro_definition(L, 2)); }
|
||||
int macro_hash(lua_State * L) { return pushinteger(L, to_macro_definition(L, 1).hash()); }
|
||||
int macro_trust_level(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).trust_level()); }
|
||||
int macro_eq(lua_State * L) { return push_boolean(L, to_macro_definition(L, 1) == to_macro_definition(L, 2)); }
|
||||
int macro_hash(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).hash()); }
|
||||
static int macro_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
formatter fmt = get_global_formatter(L);
|
||||
options opts = get_global_options(L);
|
||||
out << mk_pair(to_macro_definition(L, 1).pp(fmt, opts), opts);
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static const struct luaL_Reg macro_definition_m[] = {
|
||||
|
|
@ -885,7 +884,7 @@ io_state * get_io_state(lua_State * L) {
|
|||
// Justification
|
||||
DECL_UDATA(justification)
|
||||
|
||||
int push_optional_justification(lua_State * L, optional<justification> const & j) { return j ? push_justification(L, *j) : pushnil(L); }
|
||||
int push_optional_justification(lua_State * L, optional<justification> const & j) { return j ? push_justification(L, *j) : push_nil(L); }
|
||||
|
||||
static int justification_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
|
|
@ -895,7 +894,7 @@ static int justification_tostring(lua_State * L) {
|
|||
return 1;
|
||||
}
|
||||
|
||||
#define JST_PRED(P) static int justification_ ## P(lua_State * L) { return pushboolean(L, to_justification(L, 1).P()); }
|
||||
#define JST_PRED(P) static int justification_ ## P(lua_State * L) { return push_boolean(L, to_justification(L, 1).P()); }
|
||||
JST_PRED(is_none)
|
||||
JST_PRED(is_asserted)
|
||||
JST_PRED(is_assumption)
|
||||
|
|
@ -920,7 +919,7 @@ static int justification_pp(lua_State * L) {
|
|||
static int justification_assumption_idx(lua_State * L) {
|
||||
if (!to_justification(L, 1).is_assumption())
|
||||
throw exception("arg #1 must be an assumption justification");
|
||||
return pushinteger(L, assumption_idx(to_justification(L, 1)));
|
||||
return push_integer(L, assumption_idx(to_justification(L, 1)));
|
||||
}
|
||||
static int justification_child1(lua_State * L) {
|
||||
if (!to_justification(L, 1).is_composite())
|
||||
|
|
@ -932,8 +931,8 @@ static int justification_child2(lua_State * L) {
|
|||
throw exception("arg #1 must be a composite justification");
|
||||
return push_justification(L, composite_child2(to_justification(L, 1)));
|
||||
}
|
||||
static int justification_depends_on(lua_State * L) { return pushboolean(L, depends_on(to_justification(L, 1), pushinteger(L, 2))); }
|
||||
static int mk_assumption_justification(lua_State * L) { return push_justification(L, mk_assumption_justification(pushinteger(L, 1))); }
|
||||
static int justification_depends_on(lua_State * L) { return push_boolean(L, depends_on(to_justification(L, 1), push_integer(L, 2))); }
|
||||
static int mk_assumption_justification(lua_State * L) { return push_justification(L, mk_assumption_justification(push_integer(L, 1))); }
|
||||
static int mk_justification(lua_State * L) { return push_justification(L, justification()); }
|
||||
static int mk_composite1(lua_State * L) { return push_justification(L, mk_composite1(to_justification(L, 1), to_justification(L, 2))); }
|
||||
|
||||
|
|
@ -1010,21 +1009,21 @@ static int subst_assign(lua_State * L) {
|
|||
}
|
||||
static int subst_is_assigned(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
return pushboolean(L, to_substitution(L, 1).is_assigned(to_expr(L, 2)));
|
||||
return push_boolean(L, to_substitution(L, 1).is_assigned(to_expr(L, 2)));
|
||||
else
|
||||
return pushboolean(L, to_substitution(L, 1).is_assigned(to_level(L, 2)));
|
||||
return push_boolean(L, to_substitution(L, 1).is_assigned(to_level(L, 2)));
|
||||
}
|
||||
static int subst_is_expr_assigned(lua_State * L) { return pushboolean(L, to_substitution(L, 1).is_expr_assigned(to_name_ext(L, 2))); }
|
||||
static int subst_is_level_assigned(lua_State * L) { return pushboolean(L, to_substitution(L, 1).is_level_assigned(to_name_ext(L, 2))); }
|
||||
static int subst_occurs(lua_State * L) { return pushboolean(L, to_substitution(L, 1).occurs(to_expr(L, 2), to_expr(L, 3))); }
|
||||
static int subst_occurs_expr(lua_State * L) { return pushboolean(L, to_substitution(L, 1).occurs_expr(to_name_ext(L, 2), to_expr(L, 3))); }
|
||||
static int subst_is_expr_assigned(lua_State * L) { return push_boolean(L, to_substitution(L, 1).is_expr_assigned(to_name_ext(L, 2))); }
|
||||
static int subst_is_level_assigned(lua_State * L) { return push_boolean(L, to_substitution(L, 1).is_level_assigned(to_name_ext(L, 2))); }
|
||||
static int subst_occurs(lua_State * L) { return push_boolean(L, to_substitution(L, 1).occurs(to_expr(L, 2), to_expr(L, 3))); }
|
||||
static int subst_occurs_expr(lua_State * L) { return push_boolean(L, to_substitution(L, 1).occurs_expr(to_name_ext(L, 2), to_expr(L, 3))); }
|
||||
static int subst_get_expr_assignment(lua_State * L) {
|
||||
auto r = to_substitution(L, 1).get_expr_assignment(to_name_ext(L, 2));
|
||||
if (r) {
|
||||
push_expr(L, r->first);
|
||||
push_justification(L, r->second);
|
||||
} else {
|
||||
pushnil(L); pushnil(L);
|
||||
push_nil(L); push_nil(L);
|
||||
}
|
||||
return 2;
|
||||
}
|
||||
|
|
@ -1034,7 +1033,7 @@ static int subst_get_level_assignment(lua_State * L) {
|
|||
push_level(L, r->first);
|
||||
push_justification(L, r->second);
|
||||
} else {
|
||||
pushnil(L); pushnil(L);
|
||||
push_nil(L); push_nil(L);
|
||||
}
|
||||
return 2;
|
||||
}
|
||||
|
|
@ -1045,7 +1044,7 @@ static int subst_get_assignment(lua_State * L) {
|
|||
push_expr(L, r->first);
|
||||
push_justification(L, r->second);
|
||||
} else {
|
||||
pushnil(L); pushnil(L);
|
||||
push_nil(L); push_nil(L);
|
||||
}
|
||||
} else {
|
||||
auto r = to_substitution(L, 1).get_assignment(to_level(L, 2));
|
||||
|
|
@ -1053,7 +1052,7 @@ static int subst_get_assignment(lua_State * L) {
|
|||
push_level(L, r->first);
|
||||
push_justification(L, r->second);
|
||||
} else {
|
||||
pushnil(L); pushnil(L);
|
||||
push_nil(L); push_nil(L);
|
||||
}
|
||||
}
|
||||
return 2;
|
||||
|
|
@ -1111,361 +1110,3 @@ void open_kernel_module(lua_State * L) {
|
|||
open_substitution(L);
|
||||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
namespace lean {
|
||||
|
||||
DECL_UDATA(object)
|
||||
|
||||
int push_optional_object(lua_State * L, optional<object> const & o) {
|
||||
if (o)
|
||||
push_object(L, *o);
|
||||
else
|
||||
lua_pushnil(L);
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int object_keyword(lua_State * L) {
|
||||
lua_pushstring(L, to_object(L, 1).keyword());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int object_has_name(lua_State * L) {
|
||||
lua_pushboolean(L, to_object(L, 1).has_name());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int object_get_name(lua_State * L) {
|
||||
object const & o = to_object(L, 1);
|
||||
if (!o.has_name())
|
||||
throw exception("kernel object does not have a name");
|
||||
return push_name(L, o.get_name());
|
||||
}
|
||||
|
||||
static int object_has_type(lua_State * L) {
|
||||
lua_pushboolean(L, to_object(L, 1).has_type());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int object_get_type(lua_State * L) {
|
||||
object const & o = to_object(L, 1);
|
||||
if (!o.has_type())
|
||||
throw exception("kernel object does not have a type");
|
||||
return push_expr(L, o.get_type());
|
||||
}
|
||||
|
||||
static int object_has_cnstr_level(lua_State * L) {
|
||||
lua_pushboolean(L, to_object(L, 1).has_cnstr_level());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int object_get_cnstr_level(lua_State * L) {
|
||||
object const & o = to_object(L, 1);
|
||||
if (!o.has_cnstr_level())
|
||||
throw exception("kernel object does not have a constraint level");
|
||||
return push_level(L, o.get_cnstr_level());
|
||||
}
|
||||
|
||||
static int object_get_value(lua_State * L) {
|
||||
object const & o = to_object(L, 1);
|
||||
if (!o.is_definition() && !o.is_builtin())
|
||||
throw exception("kernel object is not a definition/theorem/builtin");
|
||||
return push_expr(L, o.get_value());
|
||||
}
|
||||
|
||||
static int object_get_weight(lua_State * L) {
|
||||
object const & o = to_object(L, 1);
|
||||
if (!o.is_definition())
|
||||
throw exception("kernel object is not a definition");
|
||||
lua_pushinteger(L, o.get_weight());
|
||||
return 1;
|
||||
}
|
||||
|
||||
#define OBJECT_PRED(P) \
|
||||
static int object_ ## P(lua_State * L) { \
|
||||
lua_pushboolean(L, to_object(L, 1).P()); \
|
||||
return 1; \
|
||||
}
|
||||
|
||||
OBJECT_PRED(is_definition)
|
||||
OBJECT_PRED(is_opaque)
|
||||
OBJECT_PRED(is_axiom)
|
||||
OBJECT_PRED(is_theorem)
|
||||
OBJECT_PRED(is_var_decl)
|
||||
OBJECT_PRED(is_builtin)
|
||||
OBJECT_PRED(is_builtin_set)
|
||||
|
||||
#define OBJECT_EXTRA_PRED(P) \
|
||||
static int object_ ## P(lua_State * L) { \
|
||||
lua_pushboolean(L, P(to_object(L, 1))); \
|
||||
return 1; \
|
||||
}
|
||||
|
||||
OBJECT_EXTRA_PRED(is_begin_import)
|
||||
OBJECT_EXTRA_PRED(is_begin_builtin_import)
|
||||
OBJECT_EXTRA_PRED(is_end_import)
|
||||
|
||||
static int object_in_builtin_set(lua_State * L) {
|
||||
lua_pushboolean(L, to_object(L, 1).in_builtin_set(to_expr(L, 2)));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int object_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
formatter fmt = get_global_formatter(L);
|
||||
options opts = get_global_options(L);
|
||||
out << mk_pair(fmt(to_object(L, 1), opts), opts);
|
||||
lua_pushstring(L, out.str().c_str());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static const struct luaL_Reg object_m[] = {
|
||||
{"__gc", object_gc}, // never throws
|
||||
{"__tostring", safe_function<object_tostring>},
|
||||
{"keyword", safe_function<object_keyword>},
|
||||
{"has_name", safe_function<object_has_name>},
|
||||
{"get_name", safe_function<object_get_name>},
|
||||
{"has_type", safe_function<object_has_type>},
|
||||
{"get_type", safe_function<object_get_type>},
|
||||
{"has_cnstr_level", safe_function<object_has_cnstr_level>},
|
||||
{"get_cnstr_level", safe_function<object_get_cnstr_level>},
|
||||
{"is_definition", safe_function<object_is_definition>},
|
||||
{"is_opaque", safe_function<object_is_opaque>},
|
||||
{"get_value", safe_function<object_get_value>},
|
||||
{"get_weight", safe_function<object_get_weight>},
|
||||
{"is_axiom", safe_function<object_is_axiom>},
|
||||
{"is_theorem", safe_function<object_is_theorem>},
|
||||
{"is_var_decl", safe_function<object_is_var_decl>},
|
||||
{"is_builtin", safe_function<object_is_builtin>},
|
||||
{"is_builtin_set", safe_function<object_is_builtin_set>},
|
||||
{"in_builtin_set", safe_function<object_in_builtin_set>},
|
||||
{"is_begin_import", safe_function<object_is_begin_import>},
|
||||
{"is_begin_builtin_import", safe_function<object_is_begin_builtin_import>},
|
||||
{"is_end_import", safe_function<object_is_end_import>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
static void open_object(lua_State * L) {
|
||||
luaL_newmetatable(L, object_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, object_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(object_pred, "is_kernel_object");
|
||||
}
|
||||
|
||||
|
||||
DECL_UDATA(metavar_env)
|
||||
|
||||
static int menv_mk_metavar(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 1) {
|
||||
return push_expr(L, to_metavar_env(L, 1)->mk_metavar());
|
||||
} else if (nargs == 2) {
|
||||
return push_expr(L, to_metavar_env(L, 1)->mk_metavar(to_context(L, 2)));
|
||||
} else {
|
||||
return push_expr(L, to_metavar_env(L, 1)->mk_metavar(to_context(L, 2), some_expr(to_expr(L, 3))));
|
||||
}
|
||||
}
|
||||
|
||||
static expr & to_metavar(lua_State * L, int i, bool lctx = true) {
|
||||
expr & e = to_expr(L, i);
|
||||
if (is_metavar(e)) {
|
||||
if (lctx || !has_local_context(e))
|
||||
return e;
|
||||
throw exception(sstream() << "arg #" << i << " must be a metavariable without a local context");
|
||||
}
|
||||
throw exception(sstream() << "arg #" << i << " must be a metavariable");
|
||||
}
|
||||
|
||||
static int menv_get_timestamp(lua_State * L) {
|
||||
lua_pushinteger(L, to_metavar_env(L, 1)->get_timestamp());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int menv_get_context(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
return push_context(L, to_metavar_env(L, 1)->get_context(to_metavar(L, 2, false)));
|
||||
else
|
||||
return push_context(L, to_metavar_env(L, 1)->get_context(to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int menv_has_type(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
lua_pushboolean(L, to_metavar_env(L, 1)->has_type(to_metavar(L, 2)));
|
||||
else
|
||||
lua_pushboolean(L, to_metavar_env(L, 1)->has_type(to_name_ext(L, 2)));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int menv_get_type(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
return push_expr(L, to_metavar_env(L, 1)->get_type(to_metavar(L, 2)));
|
||||
else
|
||||
return push_expr(L, to_metavar_env(L, 1)->get_type(to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int menv_is_assigned(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
lua_pushboolean(L, to_metavar_env(L, 1)->is_assigned(to_metavar(L, 2)));
|
||||
else
|
||||
lua_pushboolean(L, to_metavar_env(L, 1)->is_assigned(to_name_ext(L, 2)));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int menv_assign(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
justification jst;
|
||||
if (nargs == 4)
|
||||
jst = to_justification(L, 4);
|
||||
if (is_expr(L, 2))
|
||||
to_metavar_env(L, 1)->assign(to_metavar(L, 2, false), to_expr(L, 3), jst);
|
||||
else
|
||||
to_metavar_env(L, 1)->assign(to_name_ext(L, 2), to_expr(L, 3), jst);
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int menv_get_subst(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
return push_optional_expr(L, to_metavar_env(L, 1)->get_subst(to_metavar(L, 2)));
|
||||
else
|
||||
return push_optional_expr(L, to_metavar_env(L, 1)->get_subst(to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int menv_get_justification(lua_State * L) {
|
||||
if (is_expr(L, 2))
|
||||
return push_optional_justification(L, to_metavar_env(L, 1)->get_justification(to_metavar(L, 2)));
|
||||
else
|
||||
return push_optional_justification(L, to_metavar_env(L, 1)->get_justification(to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int menv_get_subst_jst(lua_State * L) {
|
||||
optional<std::pair<expr, justification>> r;
|
||||
if (is_expr(L, 2)) {
|
||||
r = to_metavar_env(L, 1)->get_subst_jst(to_metavar(L, 2));
|
||||
} else {
|
||||
r = to_metavar_env(L, 1)->get_subst_jst(to_name_ext(L, 2));
|
||||
}
|
||||
if (r) {
|
||||
push_expr(L, r->first);
|
||||
push_justification(L, r->second);
|
||||
return 2;
|
||||
} else {
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
|
||||
static int menv_for_each_subst(lua_State * L) {
|
||||
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
|
||||
to_metavar_env(L, 1)->for_each_subst([&](name const & n, expr const & e) {
|
||||
lua_pushvalue(L, 2); // push user-fun
|
||||
push_name(L, n);
|
||||
push_expr(L, e);
|
||||
pcall(L, 2, 0, 0);
|
||||
});
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int mk_metavar_env(lua_State * L) {
|
||||
if (lua_gettop(L) == 1)
|
||||
return push_metavar_env(L, metavar_env(to_name_ext(L, 1)));
|
||||
else
|
||||
return push_metavar_env(L, metavar_env());
|
||||
}
|
||||
|
||||
static int menv_copy(lua_State * L) {
|
||||
return push_metavar_env(L, metavar_env(to_metavar_env(L, 1).copy()));
|
||||
}
|
||||
|
||||
static int instantiate_metavars(lua_State * L) {
|
||||
return push_expr(L, to_metavar_env(L, 2)->instantiate_metavars(to_expr(L, 1)));
|
||||
}
|
||||
|
||||
static const struct luaL_Reg metavar_env_m[] = {
|
||||
{"__gc", metavar_env_gc}, // never throws
|
||||
{"mk_metavar", safe_function<menv_mk_metavar>},
|
||||
{"get_timestamp", safe_function<menv_get_timestamp>},
|
||||
{"get_context", safe_function<menv_get_context>},
|
||||
{"has_type", safe_function<menv_has_type>},
|
||||
{"get_type", safe_function<menv_get_type>},
|
||||
{"is_assigned", safe_function<menv_is_assigned>},
|
||||
{"assign", safe_function<menv_assign>},
|
||||
{"get_subst", safe_function<menv_get_subst>},
|
||||
{"get_justification", safe_function<menv_get_justification>},
|
||||
{"get_subst_jst", safe_function<menv_get_subst_jst>},
|
||||
{"for_each_subst", safe_function<menv_for_each_subst>},
|
||||
{"copy", safe_function<menv_copy>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
static void open_metavar_env(lua_State * L) {
|
||||
luaL_newmetatable(L, metavar_env_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, metavar_env_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_metavar_env, "metavar_env");
|
||||
SET_GLOBAL_FUN(metavar_env_pred, "is_metavar_env");
|
||||
SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars");
|
||||
}
|
||||
|
||||
constexpr char const * type_inferer_mt = "type_inferer";
|
||||
type_inferer & to_type_inferer(lua_State * L, int i) { return *static_cast<type_inferer*>(luaL_checkudata(L, i, type_inferer_mt)); }
|
||||
DECL_PRED(type_inferer)
|
||||
DECL_GC(type_inferer)
|
||||
|
||||
static int type_inferer_call(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
type_inferer & inferer = to_type_inferer(L, 1);
|
||||
if (nargs == 2)
|
||||
return push_expr(L, inferer(to_expr(L, 2)));
|
||||
else
|
||||
return push_expr(L, inferer(to_expr(L, 2), to_context(L, 3)));
|
||||
}
|
||||
|
||||
static int type_inferer_clear(lua_State * L) {
|
||||
to_type_inferer(L, 1).clear();
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int mk_type_inferer(lua_State * L) {
|
||||
void * mem = lua_newuserdata(L, sizeof(type_inferer));
|
||||
new (mem) type_inferer(to_environment(L, 1));
|
||||
luaL_getmetatable(L, type_inferer_mt);
|
||||
lua_setmetatable(L, -2);
|
||||
return 1;
|
||||
}
|
||||
|
||||
static const struct luaL_Reg type_inferer_m[] = {
|
||||
{"__gc", type_inferer_gc}, // never throws
|
||||
{"__call", safe_function<type_inferer_call>},
|
||||
{"clear", safe_function<type_inferer_clear>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_type_inferer(lua_State * L) {
|
||||
luaL_newmetatable(L, type_inferer_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, type_inferer_m, 0);
|
||||
|
||||
SET_GLOBAL_FUN(mk_type_inferer, "type_inferer");
|
||||
SET_GLOBAL_FUN(type_inferer_pred, "is_type_inferer");
|
||||
}
|
||||
|
||||
|
||||
void open_kernel_module(lua_State * L) {
|
||||
open_level(L);
|
||||
open_local_context(L);
|
||||
open_expr(L);
|
||||
open_context(L);
|
||||
open_formatter(L);
|
||||
open_environment(L);
|
||||
open_object(L);
|
||||
open_justification(L);
|
||||
open_metavar_env(L);
|
||||
open_type_inferer(L);
|
||||
open_io_state(L);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -69,7 +69,7 @@ bool is_exception(lua_State * L, int i) {
|
|||
}
|
||||
|
||||
static int exception_what(lua_State * L) {
|
||||
return pushstring(L, to_exception(L, 1).what());
|
||||
return push_string(L, to_exception(L, 1).what());
|
||||
}
|
||||
|
||||
static int exception_rethrow(lua_State * L) {
|
||||
|
|
@ -78,7 +78,7 @@ static int exception_rethrow(lua_State * L) {
|
|||
}
|
||||
|
||||
static int exception_pred(lua_State * L) {
|
||||
return pushboolean(L, is_exception(L, 1));
|
||||
return push_boolean(L, is_exception(L, 1));
|
||||
}
|
||||
|
||||
static const struct luaL_Reg exception_m[] = {
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ static int list_ ## T ## _mk(lua_State * L) { \
|
|||
int nargs = lua_gettop(L); \
|
||||
return (nargs == 0) ? list_ ## T ## _nil(L) : list_ ## T ## _cons(L); \
|
||||
} \
|
||||
static int list_ ## T ## _is_nil(lua_State * L) { return pushboolean(L, is_nil(to_list_ ## T(L, 1))); } \
|
||||
static int list_ ## T ## _is_nil(lua_State * L) { return push_boolean(L, is_nil(to_list_ ## T(L, 1))); } \
|
||||
static int list_ ## T ## _car(lua_State * L) { \
|
||||
list<T> & l = to_list_ ## T(L, 1); \
|
||||
if (is_nil(l)) throw exception("arg #1 must be a cons cell"); \
|
||||
|
|
@ -45,8 +45,8 @@ static int list_ ## T ## _cdr(lua_State * L) { \
|
|||
if (is_nil(l)) throw exception("arg #1 must be a cons cell"); \
|
||||
return push_list_ ## T(L, cdr(l)); \
|
||||
} \
|
||||
static int list_ ## T ## _eq(lua_State * L) { return pushboolean(L, to_list_ ## T(L, 1) == to_list_ ## T(L, 2)); } \
|
||||
static int list_ ## T ## _is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_list_ ## T(L, 1), to_list_ ## T(L, 2))); } \
|
||||
static int list_ ## T ## _eq(lua_State * L) { return push_boolean(L, to_list_ ## T(L, 1) == to_list_ ## T(L, 2)); } \
|
||||
static int list_ ## T ## _is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_list_ ## T(L, 1), to_list_ ## T(L, 2))); } \
|
||||
static const struct luaL_Reg list_ ## T ## _m[] = { \
|
||||
{"__gc", list_ ## T ## _gc}, \
|
||||
{"__eq", safe_function<list_ ## T ## _eq>}, \
|
||||
|
|
|
|||
|
|
@ -132,11 +132,11 @@ lua_migrate_fn get_migrate_fn(lua_State * src, int i);
|
|||
|
||||
// =======================================
|
||||
// Useful macros
|
||||
inline int pushboolean(lua_State * L, bool b) { lua_pushboolean(L, b); return 1; }
|
||||
inline int pushstring(lua_State * L, char const * s) { lua_pushstring(L, s); return 1; }
|
||||
inline int pushinteger(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); return 1; }
|
||||
inline int pushnumber(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; }
|
||||
inline int pushnil(lua_State * L) { lua_pushnil(L); return 1; }
|
||||
inline int push_boolean(lua_State * L, bool b) { lua_pushboolean(L, b); return 1; }
|
||||
inline int push_string(lua_State * L, char const * s) { lua_pushstring(L, s); return 1; }
|
||||
inline int push_integer(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); return 1; }
|
||||
inline int push_number(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; }
|
||||
inline int push_nil(lua_State * L) { lua_pushnil(L); return 1; }
|
||||
// =======================================
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -473,11 +473,11 @@ name to_name_ext(lua_State * L, int idx) {
|
|||
}
|
||||
}
|
||||
|
||||
static int name_tostring(lua_State * L) { return pushstring(L, to_name(L, 1).to_string().c_str()); }
|
||||
static int name_eq(lua_State * L) { return pushboolean(L, to_name(L, 1) == to_name(L, 2)); }
|
||||
static int name_lt(lua_State * L) { return pushboolean(L, to_name(L, 1) < to_name(L, 2)); }
|
||||
static int name_hash(lua_State * L) { return pushinteger(L, to_name(L, 1).hash()); }
|
||||
#define NAME_PRED(P) static int name_ ## P(lua_State * L) { return pushboolean(L, to_name(L, 1).P()); }
|
||||
static int name_tostring(lua_State * L) { return push_string(L, to_name(L, 1).to_string().c_str()); }
|
||||
static int name_eq(lua_State * L) { return push_boolean(L, to_name(L, 1) == to_name(L, 2)); }
|
||||
static int name_lt(lua_State * L) { return push_boolean(L, to_name(L, 1) < to_name(L, 2)); }
|
||||
static int name_hash(lua_State * L) { return push_integer(L, to_name(L, 1).hash()); }
|
||||
#define NAME_PRED(P) static int name_ ## P(lua_State * L) { return push_boolean(L, to_name(L, 1).P()); }
|
||||
NAME_PRED(is_atomic)
|
||||
NAME_PRED(is_anonymous)
|
||||
NAME_PRED(is_string)
|
||||
|
|
@ -492,13 +492,13 @@ static int name_get_prefix(lua_State * L) {
|
|||
static int name_get_numeral(lua_State * L) {
|
||||
if (!to_name(L, 1).is_numeral())
|
||||
throw exception("invalid get_numeral, hierarchical name with numeric head expected");
|
||||
return pushinteger(L, to_name(L, 1).get_numeral());
|
||||
return push_integer(L, to_name(L, 1).get_numeral());
|
||||
}
|
||||
|
||||
static int name_get_string(lua_State * L) {
|
||||
if (!to_name(L, 1).is_string())
|
||||
throw exception("invalid get_string, hierarchical name with string head expected");
|
||||
return pushstring(L, to_name(L, 1).get_string());
|
||||
return push_string(L, to_name(L, 1).get_string());
|
||||
}
|
||||
|
||||
static const struct luaL_Reg name_m[] = {
|
||||
|
|
|
|||
|
|
@ -173,15 +173,15 @@ static int mpq_tostring(lua_State * L) {
|
|||
mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, mpq_mt));
|
||||
std::ostringstream out;
|
||||
out << *n;
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int mpq_eq(lua_State * L) {
|
||||
return pushboolean(L, to_mpq<1>(L) == to_mpq<2>(L));
|
||||
return push_boolean(L, to_mpq<1>(L) == to_mpq<2>(L));
|
||||
}
|
||||
|
||||
static int mpq_lt(lua_State * L) {
|
||||
return pushboolean(L, to_mpq<1>(L) < to_mpq<2>(L));
|
||||
return push_boolean(L, to_mpq<1>(L) < to_mpq<2>(L));
|
||||
}
|
||||
|
||||
static int mpq_add(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -121,15 +121,15 @@ static int mpz_tostring(lua_State * L) {
|
|||
mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, mpz_mt));
|
||||
std::ostringstream out;
|
||||
out << *n;
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int mpz_eq(lua_State * L) {
|
||||
return pushboolean(L, to_mpz<1>(L) == to_mpz<2>(L));
|
||||
return push_boolean(L, to_mpz<1>(L) == to_mpz<2>(L));
|
||||
}
|
||||
|
||||
static int mpz_lt(lua_State * L) {
|
||||
return pushboolean(L, to_mpz<1>(L) < to_mpz<2>(L));
|
||||
return push_boolean(L, to_mpz<1>(L) < to_mpz<2>(L));
|
||||
}
|
||||
|
||||
static int mpz_add(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -18,15 +18,15 @@ static int mk_lua_rb_map(lua_State * L) {
|
|||
}
|
||||
|
||||
static int lua_rb_map_size(lua_State * L) {
|
||||
return pushinteger(L, to_lua_rb_map(L, 1).size());
|
||||
return push_integer(L, to_lua_rb_map(L, 1).size());
|
||||
}
|
||||
|
||||
static int lua_rb_map_contains(lua_State * L) {
|
||||
return pushboolean(L, to_lua_rb_map(L, 1).contains(luaref(L, 2)));
|
||||
return push_boolean(L, to_lua_rb_map(L, 1).contains(luaref(L, 2)));
|
||||
}
|
||||
|
||||
static int lua_rb_map_empty(lua_State * L) {
|
||||
return pushboolean(L, to_lua_rb_map(L, 1).empty());
|
||||
return push_boolean(L, to_lua_rb_map(L, 1).empty());
|
||||
}
|
||||
|
||||
static int lua_rb_map_insert(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -298,7 +298,7 @@ int state_set_global(lua_State * L) {
|
|||
}
|
||||
|
||||
static int state_pred(lua_State * L) {
|
||||
return pushboolean(L, is_state(L, 1));
|
||||
return push_boolean(L, is_state(L, 1));
|
||||
}
|
||||
|
||||
static const struct luaL_Reg state_m[] = {
|
||||
|
|
@ -537,7 +537,7 @@ static int thread_gc(lua_State * L) {
|
|||
}
|
||||
|
||||
static int thread_pred(lua_State * L) {
|
||||
return pushboolean(L, is_thread(L, 1));
|
||||
return push_boolean(L, is_thread(L, 1));
|
||||
}
|
||||
|
||||
static int thread_write(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -416,7 +416,7 @@ format to_format_elem(lua_State * L, int idx) {
|
|||
static int format_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
out << mk_pair(to_format(L, 1), get_global_options(L));
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int format_concat(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -231,49 +231,49 @@ static int mk_options(lua_State * L) {
|
|||
static int options_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
out << to_options(L, 1);
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static int options_size(lua_State * L) {
|
||||
return pushinteger(L, to_options(L, 1).size());
|
||||
return push_integer(L, to_options(L, 1).size());
|
||||
}
|
||||
|
||||
static int options_contains(lua_State * L) {
|
||||
return pushboolean(L, to_options(L, 1).contains(to_name_ext(L, 2)));
|
||||
return push_boolean(L, to_options(L, 1).contains(to_name_ext(L, 2)));
|
||||
}
|
||||
|
||||
static int options_empty(lua_State * L) {
|
||||
return pushboolean(L, to_options(L, 1).empty());
|
||||
return push_boolean(L, to_options(L, 1).empty());
|
||||
}
|
||||
|
||||
static int options_get_bool(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
bool defval = nargs < 3 ? false : lua_toboolean(L, 3);
|
||||
return pushboolean(L, to_options(L, 1).get_bool(to_name_ext(L, 2), defval));
|
||||
return push_boolean(L, to_options(L, 1).get_bool(to_name_ext(L, 2), defval));
|
||||
}
|
||||
|
||||
static int options_get_int(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
int defval = nargs < 3 ? 0 : lua_tointeger(L, 3);
|
||||
return pushinteger(L, to_options(L, 1).get_int(to_name_ext(L, 2), defval));
|
||||
return push_integer(L, to_options(L, 1).get_int(to_name_ext(L, 2), defval));
|
||||
}
|
||||
|
||||
static int options_get_unsigned(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
unsigned defval = nargs < 3 ? 0 : lua_tointeger(L, 3);
|
||||
return pushnumber(L, to_options(L, 1).get_unsigned(to_name_ext(L, 2), defval));
|
||||
return push_number(L, to_options(L, 1).get_unsigned(to_name_ext(L, 2), defval));
|
||||
}
|
||||
|
||||
static int options_get_double(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
double defval = nargs < 3 ? 0.0 : lua_tonumber(L, 3);
|
||||
return pushnumber(L, to_options(L, 1).get_double(to_name_ext(L, 2), defval));
|
||||
return push_number(L, to_options(L, 1).get_double(to_name_ext(L, 2), defval));
|
||||
}
|
||||
|
||||
static int options_get_string(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
char const * defval = nargs < 3 ? "" : lua_tostring(L, 3);
|
||||
return pushstring(L, to_options(L, 1).get_string(to_name_ext(L, 2), defval));
|
||||
return push_string(L, to_options(L, 1).get_string(to_name_ext(L, 2), defval));
|
||||
}
|
||||
|
||||
static int options_update_bool(lua_State * L) {
|
||||
|
|
|
|||
|
|
@ -365,7 +365,7 @@ DECL_UDATA(sexpr)
|
|||
static int sexpr_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
out << to_sexpr(L, 1);
|
||||
return pushstring(L, out.str().c_str());
|
||||
return push_string(L, out.str().c_str());
|
||||
}
|
||||
|
||||
static sexpr to_sexpr_elem(lua_State * L, int idx) {
|
||||
|
|
@ -405,10 +405,10 @@ static int mk_sexpr(lua_State * L) {
|
|||
return push_sexpr(L, r);
|
||||
}
|
||||
|
||||
static int sexpr_eq(lua_State * L) { return pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); }
|
||||
static int sexpr_lt(lua_State * L) { return pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); }
|
||||
static int sexpr_eq(lua_State * L) { return push_boolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); }
|
||||
static int sexpr_lt(lua_State * L) { return push_boolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); }
|
||||
|
||||
#define SEXPR_PRED(P) static int sexpr_ ## P(lua_State * L) { return pushboolean(L, P(to_sexpr(L, 1))); }
|
||||
#define SEXPR_PRED(P) static int sexpr_ ## P(lua_State * L) { return push_boolean(L, P(to_sexpr(L, 1))); }
|
||||
|
||||
SEXPR_PRED(is_nil)
|
||||
SEXPR_PRED(is_cons)
|
||||
|
|
@ -426,7 +426,7 @@ static int sexpr_length(lua_State * L) {
|
|||
sexpr const & e = to_sexpr(L, 1);
|
||||
if (!is_list(e))
|
||||
throw exception("s-expression is not a list");
|
||||
return pushinteger(L, length(e));
|
||||
return push_integer(L, length(e));
|
||||
}
|
||||
|
||||
static int sexpr_head(lua_State * L) {
|
||||
|
|
@ -447,28 +447,28 @@ static int sexpr_to_bool(lua_State * L) {
|
|||
sexpr const & e = to_sexpr(L, 1);
|
||||
if (!is_bool(e))
|
||||
throw exception("s-expression is not a Boolean");
|
||||
return pushboolean(L, to_bool(e));
|
||||
return push_boolean(L, to_bool(e));
|
||||
}
|
||||
|
||||
static int sexpr_to_string(lua_State * L) {
|
||||
sexpr const & e = to_sexpr(L, 1);
|
||||
if (!is_string(e))
|
||||
throw exception("s-expression is not a string");
|
||||
return pushstring(L, to_string(e).c_str());
|
||||
return push_string(L, to_string(e).c_str());
|
||||
}
|
||||
|
||||
static int sexpr_to_int(lua_State * L) {
|
||||
sexpr const & e = to_sexpr(L, 1);
|
||||
if (!is_int(e))
|
||||
throw exception("s-expression is not an integer");
|
||||
return pushinteger(L, to_int(e));
|
||||
return push_integer(L, to_int(e));
|
||||
}
|
||||
|
||||
static int sexpr_to_double(lua_State * L) {
|
||||
sexpr const & e = to_sexpr(L, 1);
|
||||
if (!is_double(e))
|
||||
throw exception("s-expression is not a double");
|
||||
return pushnumber(L, to_double(e));
|
||||
return push_number(L, to_double(e));
|
||||
}
|
||||
|
||||
static int sexpr_to_name(lua_State * L) {
|
||||
|
|
@ -493,7 +493,7 @@ static int sexpr_to_mpq(lua_State * L) {
|
|||
}
|
||||
|
||||
static int sexpr_get_kind(lua_State * L) {
|
||||
return pushinteger(L, static_cast<int>(to_sexpr(L, 1).kind()));
|
||||
return push_integer(L, static_cast<int>(to_sexpr(L, 1).kind()));
|
||||
}
|
||||
|
||||
static int sexpr_fields(lua_State * L) {
|
||||
|
|
|
|||
Loading…
Reference in a new issue