From 516c5c8feaead767df3cfafa74d19abd9bd95aeb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 16 Nov 2013 14:44:33 -0800 Subject: [PATCH] feat(lua): add metavar_env objects to Lua API Signed-off-by: Leonardo de Moura --- src/bindings/lua/CMakeLists.txt | 4 +- src/bindings/lua/leanlua_state.cpp | 2 + src/bindings/lua/metavar_env.cpp | 162 +++++++++++++++++++++++++++++ src/bindings/lua/metavar_env.h | 12 +++ src/kernel/metavar.cpp | 4 + src/kernel/metavar.h | 1 + 6 files changed, 183 insertions(+), 2 deletions(-) create mode 100644 src/bindings/lua/metavar_env.cpp create mode 100644 src/bindings/lua/metavar_env.h diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index b94decdb65..092770a253 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -1,7 +1,7 @@ add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp lref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp local_context.cpp expr.cpp context.cpp object.cpp environment.cpp -formatter.cpp justification.cpp state.cpp leanlua_state.cpp -frontend_lean.cpp) +formatter.cpp justification.cpp metavar_env.cpp state.cpp +leanlua_state.cpp frontend_lean.cpp) target_link_libraries(lua ${LEAN_LIBS}) diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 7887e1bbdc..db97ee2b05 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -31,6 +31,7 @@ Author: Leonardo de Moura #include "bindings/lua/object.h" #include "bindings/lua/environment.h" #include "bindings/lua/justification.h" +#include "bindings/lua/metavar_env.h" #include "bindings/lua/state.h" #include "bindings/lua/frontend_lean.h" #include "bindings/lua/lean.lua" @@ -178,6 +179,7 @@ struct leanlua_state::imp { open_object(m_state); open_environment(m_state); open_justification(m_state); + open_metavar_env(m_state); open_state(m_state); open_frontend_lean(m_state); open_thread(m_state); diff --git a/src/bindings/lua/metavar_env.cpp b/src/bindings/lua/metavar_env.cpp new file mode 100644 index 0000000000..f2229655d6 --- /dev/null +++ b/src/bindings/lua/metavar_env.cpp @@ -0,0 +1,162 @@ +/* +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 +#include "util/sstream.h" +#include "kernel/metavar.h" +#include "bindings/lua/util.h" +#include "bindings/lua/name.h" +#include "bindings/lua/expr.h" +#include "bindings/lua/context.h" +#include "bindings/lua/justification.h" + +namespace lean { +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), 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_expr(L, to_metavar_env(L, 1).get_subst(to_metavar(L, 2))); + else + return push_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_justification(L, to_metavar_env(L, 1).get_justification(to_metavar(L, 2))); + else + return push_justification(L, to_metavar_env(L, 1).get_justification(to_name_ext(L, 2))); +} + +static int menv_get_subst_jst(lua_State * L) { + if (is_expr(L, 2)) { + auto p = to_metavar_env(L, 1).get_subst_jst(to_metavar(L, 2)); + push_expr(L, p.first); + push_justification(L, p.second); + } else { + auto p = to_metavar_env(L, 1).get_subst_jst(to_name_ext(L, 2)); + push_expr(L, p.first); + push_justification(L, p.second); + } + return 2; +} + +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))); +} + +static const struct luaL_Reg metavar_env_m[] = { + {"__gc", metavar_env_gc}, // never throws + {"mk_metavar", safe_function}, + {"get_timestamp", safe_function}, + {"get_context", safe_function}, + {"has_type", safe_function}, + {"get_type", safe_function}, + {"is_assigned", safe_function}, + {"assign", safe_function}, + {"get_subst", safe_function}, + {"get_justification", safe_function}, + {"get_subt_jst", safe_function}, + {"for_each_subst", safe_function}, + {"copy", safe_function}, + {0, 0} +}; + +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"); +} +} diff --git a/src/bindings/lua/metavar_env.h b/src/bindings/lua/metavar_env.h new file mode 100644 index 0000000000..ad97d0076b --- /dev/null +++ b/src/bindings/lua/metavar_env.h @@ -0,0 +1,12 @@ +/* +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 +namespace lean { +UDATA_DEFS(metavar_env) +void open_metavar_env(lua_State * L); +} diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 433e0f2b18..120016b439 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -221,6 +221,10 @@ std::pair metavar_env::get_subst_jst(name const & m) const } } +expr metavar_env::get_subst(name const & m) const { + return get_subst_jst(m).first; +} + expr metavar_env::get_subst(expr const & m) const { return get_subst_jst(m).first; } diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index d1c05a08a1..8917b47255 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -149,6 +149,7 @@ public: \pre is_metavar(m) */ expr get_subst(expr const & m) const; + expr get_subst(name const & m) const; /** \brief Apply f to each substitution in the metavariable environment.