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

refactor(lua): cleanup Lua bindings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-13 13:54:03 -08:00
parent b5f0185729
commit ba0889265e
6 changed files with 55 additions and 111 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

61
src/bindings/lua/expr.cpp
View file

@ -209,55 +209,22 @@ static int expr_get_kind(lua_State * L) {
return 1; return 1;
} }
static int expr_is_constant(lua_State * L) { #define EXPR_PRED(P) \
lua_pushboolean(L, is_constant(to_nonnull_expr(L, 1))); static int expr_ ## P(lua_State * L) { \
return 1; lua_pushboolean(L, P(to_nonnull_expr(L, 1))); \
return 1; \
} }
static int expr_is_var(lua_State * L) { EXPR_PRED(is_constant)
lua_pushboolean(L, is_var(to_nonnull_expr(L, 1))); EXPR_PRED(is_var)
return 1; EXPR_PRED(is_app)
} EXPR_PRED(is_eq)
EXPR_PRED(is_lambda)
static int expr_is_app(lua_State * L) { EXPR_PRED(is_pi)
lua_pushboolean(L, is_app(to_nonnull_expr(L, 1))); EXPR_PRED(is_abstraction)
return 1; EXPR_PRED(is_let)
} EXPR_PRED(is_value)
EXPR_PRED(is_metavar)
static int expr_is_eq(lua_State * L) {
lua_pushboolean(L, is_eq(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_lambda(lua_State * L) {
lua_pushboolean(L, is_lambda(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_pi(lua_State * L) {
lua_pushboolean(L, is_lambda(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_abstraction(lua_State * L) {
lua_pushboolean(L, is_abstraction(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_let(lua_State * L) {
lua_pushboolean(L, is_let(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_value(lua_State * L) {
lua_pushboolean(L, is_value(to_nonnull_expr(L, 1)));
return 1;
}
static int expr_is_metavar(lua_State * L) {
lua_pushboolean(L, is_metavar(to_nonnull_expr(L, 1)));
return 1;
}
/** /**
\brief Iterator (closure base function) for application args. See \c expr_args \brief Iterator (closure base function) for application args. See \c expr_args

25
src/bindings/lua/level.cpp
View file

@ -76,25 +76,16 @@ static int mk_level(lua_State * L) {
} }
} }
static int level_is_bottom(lua_State * L) { #define LEVEL_PRED(P) \
lua_pushboolean(L, to_level(L, 1).is_bottom()); static int level_ ## P(lua_State * L) { \
return 1; lua_pushboolean(L, P(to_level(L, 1))); \
return 1; \
} }
static int level_is_uvar(lua_State * L) { LEVEL_PRED(is_bottom)
lua_pushboolean(L, is_uvar(to_level(L, 1))); LEVEL_PRED(is_uvar)
return 1; LEVEL_PRED(is_lift)
} LEVEL_PRED(is_max)
static int level_is_lift(lua_State * L) {
lua_pushboolean(L, is_lift(to_level(L, 1)));
return 1;
}
static int level_is_max(lua_State * L) {
lua_pushboolean(L, is_max(to_level(L, 1)));
return 1;
}
static int level_name(lua_State * L) { static int level_name(lua_State * L) {
if (!is_uvar(to_level(L, 1))) if (!is_uvar(to_level(L, 1)))

43
src/bindings/lua/object.cpp
View file

@ -90,16 +90,6 @@ static int object_get_cnstr_level(lua_State * L) {
return push_level(L, to_nonnull_object(L, 1).get_cnstr_level()); return push_level(L, to_nonnull_object(L, 1).get_cnstr_level());
} }
static int object_is_definition(lua_State * L) {
lua_pushboolean(L, to_nonnull_object(L, 1).is_definition());
return 1;
}
static int object_is_opaque(lua_State * L) {
lua_pushboolean(L, to_nonnull_object(L, 1).is_opaque());
return 1;
}
static int object_get_value(lua_State * L) { static int object_get_value(lua_State * L) {
if (!to_nonnull_object(L, 1).is_definition()) if (!to_nonnull_object(L, 1).is_definition())
throw exception("kernel object is not a definition/theorem"); throw exception("kernel object is not a definition/theorem");
@ -113,30 +103,19 @@ static int object_get_weight(lua_State * L) {
return 1; return 1;
} }
static int object_is_axiom(lua_State * L) { #define OBJECT_PRED(P) \
lua_pushboolean(L, to_nonnull_object(L, 1).is_axiom()); static int object_ ## P(lua_State * L) { \
return 1; lua_pushboolean(L, to_nonnull_object(L, 1).P()); \
return 1; \
} }
static int object_is_theorem(lua_State * L) { OBJECT_PRED(is_definition)
lua_pushboolean(L, to_nonnull_object(L, 1).is_theorem()); OBJECT_PRED(is_opaque)
return 1; OBJECT_PRED(is_axiom)
} OBJECT_PRED(is_theorem)
OBJECT_PRED(is_var_decl)
static int object_is_var_decl(lua_State * L) { OBJECT_PRED(is_builtin)
lua_pushboolean(L, to_nonnull_object(L, 1).is_var_decl()); OBJECT_PRED(is_builtin_set)
return 1;
}
static int object_is_builtin(lua_State * L) {
lua_pushboolean(L, to_nonnull_object(L, 1).is_builtin());
return 1;
}
static int object_is_builtin_set(lua_State * L) {
lua_pushboolean(L, to_nonnull_object(L, 1).is_builtin_set());
return 1;
}
static int object_in_builtin_set(lua_State * L) { static int object_in_builtin_set(lua_State * L) {
lua_pushboolean(L, to_nonnull_object(L, 1).in_builtin_set(to_expr(L, 2))); lua_pushboolean(L, to_nonnull_object(L, 1).in_builtin_set(to_expr(L, 2)));

1
src/bindings/lua/options.cpp
View file

@ -35,7 +35,6 @@ int push_options(lua_State * L, options const & o) {
} }
static int mk_options(lua_State * L) { static int mk_options(lua_State * L) {
// int nargs = lua_gettop(L);
options r; options r;
return push_options(L, r); return push_options(L, r);
} }

29
src/bindings/lua/sexpr.cpp
View file

@ -82,17 +82,24 @@ static int mk_sexpr(lua_State * L) {
static int sexpr_eq(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); return 1; } static int sexpr_eq(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); return 1; }
static int sexpr_lt(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); return 1; } static int sexpr_lt(lua_State * L) { lua_pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); return 1; }
static int sexpr_is_nil(lua_State * L) { lua_pushboolean(L, is_nil(to_sexpr(L, 1))); return 1; }
static int sexpr_is_cons(lua_State * L) { lua_pushboolean(L, is_cons(to_sexpr(L, 1))); return 1; } #define SEXPR_PRED(P) \
static int sexpr_is_list(lua_State * L) { lua_pushboolean(L, is_list(to_sexpr(L, 1))); return 1; } static int sexpr_ ## P(lua_State * L) { \
static int sexpr_is_atom(lua_State * L) { lua_pushboolean(L, is_atom(to_sexpr(L, 1))); return 1; } lua_pushboolean(L, P(to_sexpr(L, 1))); \
static int sexpr_is_string(lua_State * L) { lua_pushboolean(L, is_string(to_sexpr(L, 1))); return 1; } return 1; \
static int sexpr_is_bool(lua_State * L) { lua_pushboolean(L, is_bool(to_sexpr(L, 1))); return 1; } }
static int sexpr_is_int(lua_State * L) { lua_pushboolean(L, is_int(to_sexpr(L, 1))); return 1; }
static int sexpr_is_double(lua_State * L) { lua_pushboolean(L, is_double(to_sexpr(L, 1))); return 1; } SEXPR_PRED(is_nil)
static int sexpr_is_name(lua_State * L) { lua_pushboolean(L, is_name(to_sexpr(L, 1))); return 1; } SEXPR_PRED(is_cons)
static int sexpr_is_mpz(lua_State * L) { lua_pushboolean(L, is_mpz(to_sexpr(L, 1))); return 1; } SEXPR_PRED(is_list)
static int sexpr_is_mpq(lua_State * L) { lua_pushboolean(L, is_mpq(to_sexpr(L, 1))); return 1; } SEXPR_PRED(is_atom)
SEXPR_PRED(is_string)
SEXPR_PRED(is_bool)
SEXPR_PRED(is_int)
SEXPR_PRED(is_double)
SEXPR_PRED(is_name)
SEXPR_PRED(is_mpz)
SEXPR_PRED(is_mpq)
static int sexpr_length(lua_State * L) { static int sexpr_length(lua_State * L) {
sexpr const & e = to_sexpr(L, 1); sexpr const & e = to_sexpr(L, 1);

7
src/kernel/level.h
View file

@ -61,9 +61,10 @@ level max(level const & l1, level const & l2);
level max(std::initializer_list<level> const & l); level max(std::initializer_list<level> const & l);
level operator+(level const & l, unsigned k); level operator+(level const & l, unsigned k);
inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; } inline bool is_bottom(level const & l) { return l.is_bottom(); }
inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; } inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; }
inline bool is_max (level const & l) { return kind(l) == level_kind::Max; } inline bool is_lift(level const & l) { return kind(l) == level_kind::Lift; }
inline bool is_max (level const & l) { return kind(l) == level_kind::Max; }
/** \brief Return a */ /** \brief Return a */
inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); } inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); }