feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/bindings/lua/CMakeLists.txt

@@ -1,6 +1,6 @@
 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 state.cpp leanlua_state.cpp)
+formatter.cpp state.cpp leanlua_state.cpp frontend_lean.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/environment.cpp

@@ -21,14 +21,24 @@ Author: Leonardo de Moura
 namespace lean {
 DECL_UDATA(environment)
 
+static environment get_global_environment(lua_State * L);
+
 ro_environment::ro_environment(lua_State * L, int idx):
     read_only_environment(to_environment(L, idx)) {
 }
 
+ro_environment::ro_environment(lua_State * L):
+    read_only_environment(get_global_environment(L)) {
+}
+
 rw_environment::rw_environment(lua_State * L, int idx):
     read_write_environment(to_environment(L, idx)) {
 }
 
+rw_environment::rw_environment(lua_State * L):
+    read_write_environment(get_global_environment(L)) {
+}
+
 static int mk_environment(lua_State * L) {
     return push_environment(L, environment());
 }
@@ -136,7 +146,6 @@ static int environment_normalize(lua_State * L) {
         return push_expr(L, env->normalize(to_nonnull_expr(L, 2), to_context(L, 3)));
 }
 
-
 /**
    \brief Iterator (closure base function) for kernel objects.
 
@@ -223,12 +232,18 @@ set_environment::~set_environment() {
     lua_settable(m_state, LUA_REGISTRYINDEX);
 }
 
-int get_environment(lua_State * L) {
+static environment get_global_environment(lua_State * L) {
     lua_pushlightuserdata(L, static_cast<void *>(&g_set_environment_key));
     lua_gettable(L, LUA_REGISTRYINDEX);
     if (!is_environment(L, -1))
         throw exception("Lua registry does not contain a Lean environment");
-    return push_environment(L, to_environment(L, -1));
+    environment r = to_environment(L, -1);
+    lua_pop(L, 1);
+    return r;
+}
+
+int get_environment(lua_State * L) {
+    return push_environment(L, get_global_environment(L));
 }
 
 void open_environment(lua_State * L) {

src/bindings/lua/environment.h

@@ -29,6 +29,7 @@ public:
 class ro_environment : public read_only_environment {
 public:
     ro_environment(lua_State * L, int idx);
+    ro_environment(lua_State * L);
 };
 
 /**
@@ -38,5 +39,6 @@ public:
 class rw_environment : public read_write_environment {
 public:
     rw_environment(lua_State * L, int idx);
+    rw_environment(lua_State * L);
 };
 }

src/bindings/lua/frontend_lean.cpp

@@ -0,0 +1,128 @@
+/*
+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 "library/state.h"
+#include "frontends/lean/parser.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/expr.h"
+#include "bindings/lua/environment.h"
+#include "bindings/lua/options.h"
+#include "bindings/lua/formatter.h"
+#include "bindings/lua/state.h"
+#include "bindings/lua/leanlua_state.h"
+
+namespace lean {
+/** \see parse_lean_expr */
+static int parse_lean_expr_core(lua_State * L, ro_environment const & env, state & st) {
+    char const * src = luaL_checkstring(L, 1);
+    std::istringstream in(src);
+    leanlua_state S   = to_leanlua_state(L);
+    push_expr(L, parse_expr(env, st, in, &S));
+    return 1;
+}
+
+/** \see parse_lean_expr */
+static int parse_lean_expr_core(lua_State * L, ro_environment const & env) {
+    state * st = get_state(L);
+    if (st == nullptr) {
+        state st(get_global_options(L), get_global_formatter(L));
+        return parse_lean_expr_core(L, env, st);
+    } else {
+        return parse_lean_expr_core(L, env, *st);
+    }
+}
+
+static int parse_lean_expr(lua_State * L) {
+    /*
+      The parse_lean_expr function in the Lua API supports different calling arguments:
+      1. (string) : simplest form, it is just a string in Lean default syntax.
+         The string is parsed using the global environment in the Lua registry.
+         If the Lua registry does not contain an environment, then commands fails.
+
+         It also uses the global state object in the registry. If there is no
+         state object, it will tries to create one using the global options and formatter
+         in the registry.
+
+         It returns a Lean expression.
+
+      2. (string, env) : similar to the previous one, but the environment is explicitly
+         provided.
+
+      3. (string, env, options, formatter?) : Everything is explicitly provided in this
+         version. We also support a variation where the formmater is omitted.
+    */
+    int nargs = lua_gettop(L);
+    if (nargs == 1) {
+        ro_environment env(L); // get global environment
+        return parse_lean_expr_core(L, env);
+    } else {
+        ro_environment env(L, 2);
+        if (nargs == 2) {
+            return parse_lean_expr_core(L, env);
+        } else {
+            options opts    = to_options(L, 3);
+            formatter fmt   = nargs == 3 ? get_global_formatter(L) : to_formatter(L, 4);
+            state st(opts, fmt);
+            return parse_lean_expr_core(L, env, st);
+        }
+    }
+}
+
+/** \see parse_lean_cmds */
+static void parse_lean_cmds_core(lua_State * L, rw_environment & env, state & st) {
+    char const * src = luaL_checkstring(L, 1);
+    std::istringstream in(src);
+    leanlua_state S   = to_leanlua_state(L);
+    parse_commands(env, st, in, &S);
+}
+
+/** \see parse_lean_cmds */
+static void parse_lean_cmds_core(lua_State * L, rw_environment & env) {
+    state * st = get_state(L);
+    if (st == nullptr) {
+        state st(get_global_options(L), get_global_formatter(L));
+        parse_lean_cmds_core(L, env, st);
+        set_global_options(L, st.get_options());
+    } else {
+        parse_lean_cmds_core(L, env, *st);
+    }
+}
+
+static int parse_lean_cmds(lua_State * L) {
+    /*
+      The parse_lean_cmds function reads a sequence of Lean commands from the input string.
+      The supported calling arguments are equal to the ones used in parse_lean_expr.
+      The main difference is the function result. When calling with explicit options
+      the function returns an updated set of options. Otherwise it does not return anything.
+    */
+    int nargs = lua_gettop(L);
+    if (nargs == 1) {
+        rw_environment env(L); // get global environment
+        parse_lean_cmds_core(L, env);
+        return 0;
+    } else {
+        rw_environment env(L, 2);
+        if (nargs == 2) {
+            parse_lean_cmds_core(L, env);
+            return 0;
+        } else {
+            options opts    = to_options(L, 3);
+            formatter fmt   = nargs == 3 ? get_global_formatter(L) : to_formatter(L, 4);
+            state st(opts, fmt);
+            parse_lean_cmds_core(L, env, st);
+            push_options(L, st.get_options());
+            return 1;
+        }
+    }
+}
+
+void open_frontend_lean(lua_State * L) {
+    SET_GLOBAL_FUN(parse_lean_expr,   "parse_lean");
+    SET_GLOBAL_FUN(parse_lean_cmds,   "parse_lean_cmds");
+}
+}

src/bindings/lua/frontend_lean.h

@@ -0,0 +1,11 @@
+/*
+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 {
+void open_frontend_lean(lua_State * L);
+}

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/state.h"
+#include "bindings/lua/frontend_lean.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); }
@@ -129,10 +130,27 @@ static void copy_values(lua_State * src, int first, int last, lua_State * tgt) {
     }
 }
 
+static char g_weak_ptr_key; // key for Lua registry (used at get_weak_ptr and save_weak_ptr)
+
 struct leanlua_state::imp {
     lua_State * m_state;
     std::mutex  m_mutex;
 
+    static std::weak_ptr<imp> * get_weak_ptr(lua_State * L) {
+        lua_pushlightuserdata(L, static_cast<void *>(&g_weak_ptr_key));
+        lua_gettable(L, LUA_REGISTRYINDEX);
+        std::weak_ptr<imp> * ptr = static_cast<std::weak_ptr<imp>*>(lua_touserdata(L, -1));
+        lua_pop(L, 1);
+        return ptr;
+    }
+
+    void save_weak_ptr(std::shared_ptr<imp> & ptr) {
+        lua_pushlightuserdata(m_state, static_cast<void *>(&g_weak_ptr_key));
+        void * mem = lua_newuserdata(m_state, sizeof(std::weak_ptr<imp>));
+        new (mem) std::weak_ptr<imp>(ptr);
+        lua_settable(m_state, LUA_REGISTRYINDEX);
+    }
+
     imp() {
         // TODO(Leo) investigate why TCMALLOC + lua_realloc do not work together
         // #ifdef LEAN_USE_LUA_NEWSTATE
@@ -159,12 +177,16 @@ struct leanlua_state::imp {
         open_object(m_state);
         open_environment(m_state);
         open_state(m_state);
+        open_frontend_lean(m_state);
         open_thread(m_state);
         open_interrupt(m_state);
         dostring(g_leanlua_extra);
     }
 
     ~imp() {
+        typedef std::weak_ptr<imp> wptr;
+        wptr * ptr = get_weak_ptr(m_state);
+        ptr->~wptr(); // destruct weak pointer
         lua_close(m_state);
     }
 
@@ -185,8 +207,17 @@ struct leanlua_state::imp {
     }
 };
 
+leanlua_state to_leanlua_state(lua_State * L) {
+    return leanlua_state(*leanlua_state::imp::get_weak_ptr(L));
+}
+
 leanlua_state::leanlua_state():
     m_ptr(new imp()) {
+    m_ptr->save_weak_ptr(m_ptr);
+}
+
+leanlua_state::leanlua_state(std::weak_ptr<imp> const & ptr):m_ptr(ptr.lock()) {
+    lean_assert(m_ptr);
 }
 
 leanlua_state::~leanlua_state() {

src/bindings/lua/leanlua_state.h

@@ -17,14 +17,18 @@ class state;
    \brief Wrapper for lua_State objects which contains all Lean bindings.
 */
 class leanlua_state : public script_evaluator {
+public:
     struct imp;
+private:
     std::shared_ptr<imp> m_ptr;
+    leanlua_state(std::weak_ptr<imp> const & ptr);
     friend class leanlua_thread;
     friend class data_channel;
     friend int state_dostring(lua_State * L);
     friend int state_set_global(lua_State * L);
     friend int mk_thread(lua_State * L);
     friend int thread_wait(lua_State * L);
+    friend leanlua_state to_leanlua_state(lua_State * L);
 public:
     leanlua_state();
     virtual ~leanlua_state();
@@ -47,4 +51,8 @@ public:
     */
     virtual void dostring(char const * str, environment & env, state & st);
 };
+/**
+   \brief Return a reference to the leanlua_state object that is wrapping \c L.
+*/
+leanlua_state to_leanlua_state(lua_State * L);
 }

src/frontends/lean/parser.cpp

@@ -1726,4 +1726,26 @@ bool shell::operator()() {
     return p();
 #endif
 }
+
+bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
+    return parser(fe, in, S, use_exceptions, interactive)();
+}
+
+bool parse_commands(environment const & env, state & st, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
+    frontend f(env, st);
+    bool r = parse_commands(f, in, S, use_exceptions, interactive);
+    st = f.get_state();
+    return r;
+}
+
+expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions) {
+    return parser(fe, in, S, use_exceptions).parse_expr();
+}
+
+expr parse_expr(environment const & env, state & st, std::istream & in, script_evaluator * S, bool use_exceptions) {
+    frontend f(env, st);
+    expr r = parse_expr(f, in, S, use_exceptions);
+    st = f.get_state();
+    return r;
+}
 }

src/frontends/lean/parser.h

@@ -6,10 +6,12 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
-#include "frontends/lean/frontend.h"
 
 namespace lean {
 class script_evaluator;
+class frontend;
+class state;
+class environment;
 /** \brief Functional object for parsing commands and expressions */
 class parser {
     class imp;
@@ -36,10 +38,8 @@ public:
     bool operator()();
 };
 
-inline bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false) {
-    return parser(fe, in, S, use_exceptions, interactive)();
-}
-inline expr parse_expr(frontend & fe, std::istream & in) {
-    return parser(fe, in, nullptr).parse_expr();
-}
+bool parse_commands(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
+bool parse_commands(environment const & env, state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true, bool interactive = false);
+expr parse_expr(frontend & fe, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
+expr parse_expr(environment const & env, state & st, std::istream & in, script_evaluator * S = nullptr, bool use_exceptions = true);
 }

src/kernel/environment.cpp

@@ -564,7 +564,7 @@ read_only_environment::read_only_environment(environment const & env):
 }
 read_only_environment::~read_only_environment() {}
 
-read_write_environment::read_write_environment(environment & env):
+read_write_environment::read_write_environment(environment const & env):
     m_env(env),
     m_lock(m_env.m_ptr->m_mutex) {
 }

src/kernel/threadsafe_environment.h

@@ -33,7 +33,7 @@ class read_write_environment {
     environment  m_env;
     unique_lock  m_lock;
 public:
-    read_write_environment(environment & env);
+    read_write_environment(environment const & env);
     ~read_write_environment();
     operator environment &() { return m_env; }
     environment * operator->() { return &m_env; }

src/shell/lean.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "kernel/printer.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/frontend.h"
 #include "bindings/lua/leanlua_state.h"
 #include "version.h"
 

src/tests/frontends/lean/parser.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <sstream>
+#include <memory>
 #include "util/test.h"
 #include "util/exception.h"
 #include "util/numerics/mpq.h"
@@ -12,6 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/frontend.h"
 #include "frontends/lean/pp.h"
 using namespace lean;
 

tests/lean/lua13.lean

@@ -0,0 +1,13 @@
+Variables x y z : Int
+Variable f : Int -> Int -> Int
+
+(**
+ local t = parse_lean("fun w, f w (f y 0)")
+ print(t)
+ assert(t:closed())
+ local n, d, b = t:fields()
+ print(b)
+ assert(not b:closed())
+ local env = get_environment()
+ assert(d == env:find_object("Int"):get_value())
+**)

tests/lean/lua13.lean.expected.out

@@ -0,0 +1,8 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+  Assumed: y
+  Assumed: z
+  Assumed: f
+λ w : ℤ, f w (f y 0)
+f #0 (f y 0)

tests/lean/lua14.lean

@@ -0,0 +1,22 @@
+Variables x y z : Int
+Variable f : Int -> Int -> Int
+
+(**
+ local t = parse_lean("fun w, f w (f y 0)")
+ print(t)
+ assert(t:closed())
+ local n, d, b = t:fields()
+ print(b)
+ assert(not b:closed())
+ local env = get_environment()
+ assert(d == env:find_object("Int"):get_value())
+ parse_lean_cmds([[
+    Eval 10 + 20
+    Check x + y
+    Variable g : Int -> Int
+ ]])
+
+**)
+
+Check g (f x 10)
+

tests/lean/lua14.lean.expected.out

@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+  Assumed: y
+  Assumed: z
+  Assumed: f
+λ w : ℤ, f w (f y 0)
+f #0 (f y 0)
+30
+x + y : ℤ
+  Assumed: g
+g (f x 10) : ℤ

tests/lua/parser1.lua

@@ -0,0 +1,12 @@
+local env  = environment()
+local opts = options()
+env:add_var("T", Type())
+local T = Const("T")
+env:add_var("x", T)
+env:add_var("y", T)
+env:add_var("f", mk_arrow(T, mk_arrow(T, T)))
+print(parse_lean("f x (f x y)", env, opts))
+-- parse_lean will use the elaborator to fill missing information
+local F = parse_lean("fun x, f x x", env, opts)
+print(F)
+print(env:check_type(F))