refactor(bindings/lua): move to frontends/lua

Lua API is an integral part of Lean. It does *not* have the same status
of external APIs (e.g., Python) we will add in the future.

We will reserve the directory bindings for external APIs for using Lean
as a library.

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

src/CMakeLists.txt

@@ -161,7 +161,7 @@ add_subdirectory(library/tactic)
 set(LEAN_LIBS ${LEAN_LIBS} tactic)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
-add_subdirectory(bindings/lua)
+add_subdirectory(frontends/lua)
 set(LEAN_LIBS ${LEAN_LIBS} leanlua)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")

src/frontends/lua/frontend_lean.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 #include "library/kernel_bindings.h"
 #include "frontends/lean/parser.h"
-#include "bindings/lua/leanlua_state.h"
+#include "frontends/lua/leanlua_state.h"
 
 namespace lean {
 /** \see parse_lean_expr */

src/frontends/lua/leanlua_state.cpp

@@ -24,9 +24,9 @@ Author: Leonardo de Moura
 #include "library/tactic/open_module.h"
 #include "library/elaborator/elaborator_exception.h"
 #include "frontends/lean/frontend.h"
-#include "bindings/lua/leanlua_state.h"
-#include "bindings/lua/frontend_lean.h"
-#include "bindings/lua/lean.lua"
+#include "frontends/lua/leanlua_state.h"
+#include "frontends/lua/frontend_lean.h"
+#include "frontends/lua/lean.lua"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
 
@@ -71,6 +71,7 @@ struct leanlua_state::imp {
         open_kernel_module(m_state);
         open_arith_module(m_state);
         open_tactic_module(m_state);
+        open_frontend_lean(m_state);
         open_extra(m_state);
 
         dostring(g_leanlua_extra);

src/shell/lean.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"
-#include "bindings/lua/leanlua_state.h"
+#include "frontends/lua/leanlua_state.h"
 #include "version.h"
 
 using lean::shell;