feat(lua): expose level objects in the Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
5a97f730af
commit
ad2de3b53c
7 changed files with 229 additions and 5 deletions
|
@ -1,4 +1,5 @@
|
|||
add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
|
||||
options.cpp sexpr.cpp format.cpp level.cpp expr.cpp leanlua_state.cpp)
|
||||
options.cpp sexpr.cpp format.cpp level.cpp expr.cpp context.cpp
|
||||
leanlua_state.cpp)
|
||||
|
||||
target_link_libraries(lua ${LEAN_LIBS})
|
||||
|
|
164
src/bindings/lua/context.cpp
Normal file
164
src/bindings/lua/context.cpp
Normal file
|
@ -0,0 +1,164 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <sstream>
|
||||
#include <lua.hpp>
|
||||
#include "kernel/context.h"
|
||||
#include "bindings/lua/util.h"
|
||||
#include "bindings/lua/name.h"
|
||||
#include "bindings/lua/expr.h"
|
||||
#include "bindings/lua/context.h"
|
||||
|
||||
namespace lean {
|
||||
constexpr char const * context_entry_mt = "context_entry.mt";
|
||||
|
||||
bool is_context_entry(lua_State * L, int idx) {
|
||||
return testudata(L, idx, context_entry_mt);
|
||||
}
|
||||
|
||||
context_entry & to_context_entry(lua_State * L, int idx) {
|
||||
return *static_cast<context_entry*>(luaL_checkudata(L, idx, context_entry_mt));
|
||||
}
|
||||
|
||||
int push_context_entry(lua_State * L, context_entry const & e) {
|
||||
void * mem = lua_newuserdata(L, sizeof(context_entry));
|
||||
new (mem) context_entry(e);
|
||||
luaL_getmetatable(L, context_entry_mt);
|
||||
lua_setmetatable(L, -2);
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int context_entry_gc(lua_State * L) {
|
||||
to_context_entry(L, 1).~context_entry();
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int mk_context_entry(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 2)
|
||||
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_expr(L, 2)));
|
||||
else
|
||||
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3)));
|
||||
}
|
||||
|
||||
static int context_entry_pred(lua_State * L) {
|
||||
lua_pushboolean(L, is_context_entry(L, 1));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int context_entry_get_name(lua_State * L) { return push_name(L, to_context_entry(L, 1).get_name()); }
|
||||
static int context_entry_get_domain(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_domain()); }
|
||||
static int context_entry_get_body(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_body()); }
|
||||
|
||||
static const struct luaL_Reg context_entry_m[] = {
|
||||
{"__gc", context_entry_gc}, // never throws
|
||||
{"get_name", safe_function<context_entry_get_name>},
|
||||
{"get_domain", safe_function<context_entry_get_domain>},
|
||||
{"get_body", safe_function<context_entry_get_body>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
constexpr char const * context_mt = "context.mt";
|
||||
|
||||
bool is_context(lua_State * L, int idx) {
|
||||
return testudata(L, idx, context_mt);
|
||||
}
|
||||
|
||||
context & to_context(lua_State * L, int idx) {
|
||||
return *static_cast<context*>(luaL_checkudata(L, idx, context_mt));
|
||||
}
|
||||
|
||||
int push_context(lua_State * L, context const & e) {
|
||||
void * mem = lua_newuserdata(L, sizeof(context));
|
||||
new (mem) context(e);
|
||||
luaL_getmetatable(L, context_mt);
|
||||
lua_setmetatable(L, -2);
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int context_gc(lua_State * L) {
|
||||
to_context(L, 1).~context();
|
||||
return 0;
|
||||
}
|
||||
|
||||
static int context_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
// TODO(Leo): use pretty printer
|
||||
out << to_context(L, 1);
|
||||
lua_pushfstring(L, out.str().c_str());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int mk_context(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs == 0) {
|
||||
return push_context(L, context());
|
||||
} else if (nargs == 2) {
|
||||
context_entry & e = to_context_entry(L, 2);
|
||||
return push_context(L, context(to_context(L, 1), e.get_name(), e.get_domain(), e.get_body()));
|
||||
} else if (nargs == 3) {
|
||||
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3)));
|
||||
} else {
|
||||
return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4)));
|
||||
}
|
||||
}
|
||||
|
||||
static int context_pred(lua_State * L) {
|
||||
lua_pushboolean(L, is_context(L, 1));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int context_extend(lua_State * L) {
|
||||
int nargs = lua_gettop(L);
|
||||
if (nargs != 3 && nargs != 4)
|
||||
luaL_error(L, "extend expect 3 or 4 arguments");
|
||||
return mk_context(L);
|
||||
}
|
||||
|
||||
static int context_is_empty(lua_State * L) {
|
||||
lua_pushboolean(L, empty(to_context(L, 1)));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static int context_lookup(lua_State * L) {
|
||||
auto p = lookup_ext(to_context(L, 1), luaL_checkinteger(L, 2));
|
||||
push_context_entry(L, p.first);
|
||||
push_context(L, p.second);
|
||||
return 2;
|
||||
}
|
||||
|
||||
static int context_size(lua_State * L) {
|
||||
lua_pushinteger(L, to_context(L, 1).size());
|
||||
return 1;
|
||||
}
|
||||
|
||||
static const struct luaL_Reg context_m[] = {
|
||||
{"__gc", context_gc}, // never throws
|
||||
{"__tostring", safe_function<context_tostring>},
|
||||
{"__len", safe_function<context_size>},
|
||||
{"is_empty", safe_function<context_is_empty>},
|
||||
{"size", safe_function<context_size>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
void open_context(lua_State * L) {
|
||||
luaL_newmetatable(L, context_entry_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, context_entry_m, 0);
|
||||
set_global_function<mk_context_entry>(L, "context_entry");
|
||||
set_global_function<context_entry_pred>(L, "is_context_entry");
|
||||
|
||||
luaL_newmetatable(L, context_mt);
|
||||
lua_pushvalue(L, -1);
|
||||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, context_m, 0);
|
||||
set_global_function<mk_context>(L, "context");
|
||||
set_global_function<context_pred>(L, "is_context");
|
||||
set_global_function<context_extend>(L, "extend");
|
||||
set_global_function<context_lookup>(L, "lookup");
|
||||
}
|
||||
}
|
21
src/bindings/lua/context.h
Normal file
21
src/bindings/lua/context.h
Normal file
|
@ -0,0 +1,21 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <lua.hpp>
|
||||
namespace lean {
|
||||
class context_entry;
|
||||
bool is_context_entry(lua_State * L, int idx);
|
||||
context_entry & to_context_entry(lua_State * L, int idx);
|
||||
int push_context_entry(lua_State * L, context_entry const & o);
|
||||
|
||||
class context;
|
||||
bool is_context(lua_State * L, int idx);
|
||||
context & to_context(lua_State * L, int idx);
|
||||
int push_context(lua_State * L, context const & o);
|
||||
|
||||
void open_context(lua_State * L);
|
||||
}
|
|
@ -43,8 +43,13 @@ static int expr_gc(lua_State * L) {
|
|||
|
||||
static int expr_tostring(lua_State * L) {
|
||||
std::ostringstream out;
|
||||
// TODO(Leo): use pretty printer
|
||||
out << to_expr(L, 1);
|
||||
expr & e = to_expr(L, 1);
|
||||
if (e) {
|
||||
// TODO(Leo): use pretty printer
|
||||
out << to_expr(L, 1);
|
||||
} else {
|
||||
out << "<null-expr>";
|
||||
}
|
||||
lua_pushfstring(L, out.str().c_str());
|
||||
return 1;
|
||||
}
|
||||
|
@ -166,12 +171,18 @@ static int expr_type(lua_State * L) {
|
|||
return push_expr(L, Type(to_level(L, 1)));
|
||||
}
|
||||
|
||||
static int expr_is_null(lua_State * L) {
|
||||
lua_pushboolean(L, !to_expr(L, 1));
|
||||
return 1;
|
||||
}
|
||||
|
||||
static const struct luaL_Reg expr_m[] = {
|
||||
{"__gc", expr_gc}, // never throws
|
||||
{"__tostring", safe_function<expr_tostring>},
|
||||
{"__eq", safe_function<expr_eq>},
|
||||
{"__lt", safe_function<expr_lt>},
|
||||
{"__call", safe_function<expr_mk_app>},
|
||||
{"is_null", safe_function<expr_is_null>},
|
||||
{0, 0}
|
||||
};
|
||||
|
||||
|
|
|
@ -20,6 +20,7 @@ Author: Leonardo de Moura
|
|||
#include "bindings/lua/format.h"
|
||||
#include "bindings/lua/level.h"
|
||||
#include "bindings/lua/expr.h"
|
||||
#include "bindings/lua/context.h"
|
||||
#include "bindings/lua/lean.lua"
|
||||
|
||||
extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
|
||||
|
@ -46,6 +47,7 @@ struct leanlua_state::imp {
|
|||
lean::open_format(m_state);
|
||||
lean::open_level(m_state);
|
||||
lean::open_expr(m_state);
|
||||
lean::open_context(m_state);
|
||||
dostring(g_leanlua_extra);
|
||||
}
|
||||
|
||||
|
|
|
@ -32,7 +32,7 @@ int push_options(lua_State * L, options const & o) {
|
|||
return 1;
|
||||
}
|
||||
|
||||
static int mk_option(lua_State * L) {
|
||||
static int mk_options(lua_State * L) {
|
||||
// int nargs = lua_gettop(L);
|
||||
options r;
|
||||
return push_options(L, r);
|
||||
|
@ -199,7 +199,7 @@ void open_options(lua_State * L) {
|
|||
lua_setfield(L, -2, "__index");
|
||||
setfuncs(L, options_m, 0);
|
||||
|
||||
set_global_function<mk_option>(L, "options");
|
||||
set_global_function<mk_options>(L, "options");
|
||||
set_global_function<options_pred>(L, "is_options");
|
||||
}
|
||||
}
|
||||
|
|
25
tests/lua/context1.lua
Normal file
25
tests/lua/context1.lua
Normal file
|
@ -0,0 +1,25 @@
|
|||
c = context()
|
||||
assert(c:is_empty())
|
||||
print(c)
|
||||
e = context_entry("x", Const("N"))
|
||||
assert(e:get_name() == name("x"))
|
||||
assert(e:get_domain() == Const("N"))
|
||||
assert(e:get_body():is_null())
|
||||
print(e:get_body())
|
||||
c = context(c, e)
|
||||
print(c)
|
||||
assert(not c:is_empty())
|
||||
c = context(c, "y", Const("M"))
|
||||
assert(#c == 2)
|
||||
assert(c:size() == 2)
|
||||
e, c1 = lookup(c, 0)
|
||||
assert(c1:size() == 1)
|
||||
assert(e:get_name() == name("y"))
|
||||
c = context(c, "z", Const("N"), Const("a"))
|
||||
print(c)
|
||||
check_error(function() lookup(c, 10) end)
|
||||
assert(lookup(c, 0):get_body() == Const("a"))
|
||||
assert(not is_context_entry(c))
|
||||
assert(is_context(c))
|
||||
assert(is_context_entry(e))
|
||||
assert(not is_context_entry(c))
|
Loading…
Reference in a new issue