From ba0889265ea624f593f18cf408fd9c8bf8bca042 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Nov 2013 13:54:03 -0800 Subject: [PATCH] refactor(lua): cleanup Lua bindings Signed-off-by: Leonardo de Moura --- src/bindings/lua/expr.cpp | 61 +++++++++--------------------------- src/bindings/lua/level.cpp | 25 +++++---------- src/bindings/lua/object.cpp | 43 +++++++------------------ src/bindings/lua/options.cpp | 1 - src/bindings/lua/sexpr.cpp | 29 ++++++++++------- src/kernel/level.h | 7 +++-- 6 files changed, 55 insertions(+), 111 deletions(-) diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp index 4dd2db45f..b25eea297 100644 --- a/src/bindings/lua/expr.cpp +++ b/src/bindings/lua/expr.cpp @@ -209,55 +209,22 @@ static int expr_get_kind(lua_State * L) { return 1; } -static int expr_is_constant(lua_State * L) { - lua_pushboolean(L, is_constant(to_nonnull_expr(L, 1))); - return 1; +#define EXPR_PRED(P) \ +static int expr_ ## P(lua_State * L) { \ + lua_pushboolean(L, P(to_nonnull_expr(L, 1))); \ + return 1; \ } -static int expr_is_var(lua_State * L) { - lua_pushboolean(L, is_var(to_nonnull_expr(L, 1))); - return 1; -} - -static int expr_is_app(lua_State * L) { - lua_pushboolean(L, is_app(to_nonnull_expr(L, 1))); - return 1; -} - -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; -} +EXPR_PRED(is_constant) +EXPR_PRED(is_var) +EXPR_PRED(is_app) +EXPR_PRED(is_eq) +EXPR_PRED(is_lambda) +EXPR_PRED(is_pi) +EXPR_PRED(is_abstraction) +EXPR_PRED(is_let) +EXPR_PRED(is_value) +EXPR_PRED(is_metavar) /** \brief Iterator (closure base function) for application args. See \c expr_args diff --git a/src/bindings/lua/level.cpp b/src/bindings/lua/level.cpp index 01149f01e..a2e164c97 100644 --- a/src/bindings/lua/level.cpp +++ b/src/bindings/lua/level.cpp @@ -76,25 +76,16 @@ static int mk_level(lua_State * L) { } } -static int level_is_bottom(lua_State * L) { - lua_pushboolean(L, to_level(L, 1).is_bottom()); - return 1; +#define LEVEL_PRED(P) \ +static int level_ ## P(lua_State * L) { \ + lua_pushboolean(L, P(to_level(L, 1))); \ + return 1; \ } -static int level_is_uvar(lua_State * L) { - lua_pushboolean(L, is_uvar(to_level(L, 1))); - return 1; -} - -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; -} +LEVEL_PRED(is_bottom) +LEVEL_PRED(is_uvar) +LEVEL_PRED(is_lift) +LEVEL_PRED(is_max) static int level_name(lua_State * L) { if (!is_uvar(to_level(L, 1))) diff --git a/src/bindings/lua/object.cpp b/src/bindings/lua/object.cpp index 52f2ef0ac..b9ab57fdc 100644 --- a/src/bindings/lua/object.cpp +++ b/src/bindings/lua/object.cpp @@ -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()); } -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) { if (!to_nonnull_object(L, 1).is_definition()) throw exception("kernel object is not a definition/theorem"); @@ -113,30 +103,19 @@ static int object_get_weight(lua_State * L) { return 1; } -static int object_is_axiom(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).is_axiom()); - return 1; +#define OBJECT_PRED(P) \ +static int object_ ## P(lua_State * L) { \ + lua_pushboolean(L, to_nonnull_object(L, 1).P()); \ + return 1; \ } -static int object_is_theorem(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).is_theorem()); - return 1; -} - -static int object_is_var_decl(lua_State * L) { - lua_pushboolean(L, to_nonnull_object(L, 1).is_var_decl()); - 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; -} +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) static int object_in_builtin_set(lua_State * L) { lua_pushboolean(L, to_nonnull_object(L, 1).in_builtin_set(to_expr(L, 2))); diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp index 41b79b3c3..82e3044f4 100644 --- a/src/bindings/lua/options.cpp +++ b/src/bindings/lua/options.cpp @@ -35,7 +35,6 @@ int push_options(lua_State * L, options const & o) { } static int mk_options(lua_State * L) { - // int nargs = lua_gettop(L); options r; return push_options(L, r); } diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp index eb58b593d..f3b6b9982 100644 --- a/src/bindings/lua/sexpr.cpp +++ b/src/bindings/lua/sexpr.cpp @@ -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_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; } -static int sexpr_is_list(lua_State * L) { lua_pushboolean(L, is_list(to_sexpr(L, 1))); return 1; } -static int sexpr_is_atom(lua_State * L) { lua_pushboolean(L, is_atom(to_sexpr(L, 1))); return 1; } -static int sexpr_is_string(lua_State * L) { lua_pushboolean(L, is_string(to_sexpr(L, 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; } -static int sexpr_is_name(lua_State * L) { lua_pushboolean(L, is_name(to_sexpr(L, 1))); return 1; } -static int sexpr_is_mpz(lua_State * L) { lua_pushboolean(L, is_mpz(to_sexpr(L, 1))); return 1; } -static int sexpr_is_mpq(lua_State * L) { lua_pushboolean(L, is_mpq(to_sexpr(L, 1))); return 1; } + +#define SEXPR_PRED(P) \ +static int sexpr_ ## P(lua_State * L) { \ + lua_pushboolean(L, P(to_sexpr(L, 1))); \ + return 1; \ +} + +SEXPR_PRED(is_nil) +SEXPR_PRED(is_cons) +SEXPR_PRED(is_list) +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) { sexpr const & e = to_sexpr(L, 1); diff --git a/src/kernel/level.h b/src/kernel/level.h index 55dbfa258..2df7402a2 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -61,9 +61,10 @@ level max(level const & l1, level const & l2); level max(std::initializer_list const & l); level operator+(level const & l, unsigned k); -inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; } -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; } +inline bool is_bottom(level const & l) { return l.is_bottom(); } +inline bool is_uvar(level const & l) { return kind(l) == level_kind::UVar; } +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 */ inline level const * max_begin_levels(level const & l) { return &max_level(l, 0); }