Move frontend to frontends/lean

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

src/CMakeLists.txt

@@ -68,7 +68,7 @@ include_directories(${LEAN_SOURCE_DIR}/kernel)
 include_directories(${LEAN_SOURCE_DIR}/kernel/arith)
 include_directories(${LEAN_SOURCE_DIR}/exprlib)
 include_directories(${LEAN_SOURCE_DIR}/parsers)
-include_directories(${LEAN_SOURCE_DIR}/frontend)
+include_directories(${LEAN_SOURCE_DIR}/frontends/lean)
 
 add_subdirectory(util)
 set(LEAN_LIBS ${LEAN_LIBS} util)
@@ -84,8 +84,8 @@ add_subdirectory(kernel/arith)
 set(LEAN_LIBS ${LEAN_LIBS} kernel_arith)
 add_subdirectory(exprlib)
 set(LEAN_LIBS ${LEAN_LIBS} exprlib)
-add_subdirectory(frontend)
-set(LEAN_LIBS ${LEAN_LIBS} frontend)
+add_subdirectory(frontends/lean)
+set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 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")
 set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
@@ -94,4 +94,4 @@ add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
 add_subdirectory(tests/interval)
 add_subdirectory(tests/kernel)
-add_subdirectory(tests/frontend)
+add_subdirectory(tests/frontends/lean)

src/frontend/CMakeLists.txt

@@ -1,2 +0,0 @@
-add_library(frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp builtin_notation.cpp)
-target_link_libraries(frontend ${LEAN_LIBS})

src/frontends/lean/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(lean_frontend lean_frontend.cpp lean_operator_info.cpp lean_scanner.cpp lean_parser.cpp lean_pp.cpp lean_notation.cpp)
+target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/lean_frontend.cpp

@@ -5,14 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <atomic>
-#include "map.h"
-#include "frontend.h"
 #include "environment.h"
-#include "operator_info.h"
 #include "toplevel.h"
-#include "builtin_notation.h"
+#include "map.h"
 #include "state.h"
-#include "pp.h"
+#include "lean_operator_info.h"
+#include "lean_frontend.h"
+#include "lean_notation.h"
+#include "lean_pp.h"
 
 namespace lean {
 /** \brief Implementation of the Lean frontend */

src/frontends/lean/lean_frontend.h

@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include "environment.h"
-#include "operator_info.h"
 #include "state.h"
+#include "lean_operator_info.h"
 
 namespace lean {
 /**

src/frontends/lean/lean_notation.cpp

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontend.h"
 #include "builtin.h"
+#include "lean_frontend.h"
 
 namespace lean {
 /**

src/frontends/lean/lean_operator_info.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "operator_info.h"
+#include "lean_operator_info.h"
 #include "rc.h"
 
 namespace lean {

src/frontends/lean/lean_parser.cpp

@@ -5,18 +5,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <unordered_map>
-#include "frontend.h"
-#include "scanner.h"
 #include "scoped_map.h"
 #include "exception.h"
 #include "normalize.h"
 #include "type_check.h"
 #include "free_vars.h"
-#include "builtin_notation.h"
 #include "builtin.h"
 #include "arith.h"
-#include "pp.h"
 #include "printer.h"
+#include "lean_frontend.h"
+#include "lean_scanner.h"
+#include "lean_notation.h"
+#include "lean_pp.h"
 
 namespace lean {
 // ==========================================

src/frontends/lean/lean_parser.h

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
-#include "frontend.h"
+#include "lean_frontend.h"
 
 namespace lean {
 bool parse_commands(frontend & fe, std::istream & in,

src/frontends/lean/lean_pp.cpp

@@ -6,18 +6,18 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include <memory>
-#include "pp.h"
-#include "frontend.h"
 #include "context.h"
 #include "scoped_map.h"
-#include "occurs.h"
+#include "for_each.h"
 #include "instantiate.h"
+#include "occurs.h"
 #include "builtin.h"
-#include "builtin_notation.h"
 #include "free_vars.h"
 #include "context_to_lambda.h"
-#include "for_each.h"
 #include "options.h"
+#include "lean_notation.h"
+#include "lean_pp.h"
+#include "lean_frontend.h"
 
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
 #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()

src/frontends/lean/lean_scanner.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <cstdio>
 #include <string>
 #include <algorithm>
-#include "scanner.h"
+#include "lean_scanner.h"
 #include "debug.h"
 #include "exception.h"
 

src/shell/lean.cpp

@@ -1,8 +1,8 @@
 #include <iostream>
 #include <fstream>
 #include "version.h"
-#include "parser.h"
 #include "printer.h"
+#include "lean_parser.h"
 using namespace lean;
 
 

src/tests/frontend/CMakeLists.txt

@@ -1,12 +0,0 @@
-add_executable(frontend_tst frontend.cpp)
-target_link_libraries(frontend_tst ${EXTRA_LIBS})
-add_test(frontend ${CMAKE_CURRENT_BINARY_DIR}/frontend_tst)
-add_executable(scanner scanner.cpp)
-target_link_libraries(scanner ${EXTRA_LIBS})
-add_test(scanner ${CMAKE_CURRENT_BINARY_DIR}/scanner)
-add_executable(parser parser.cpp)
-target_link_libraries(parser ${EXTRA_LIBS})
-add_test(parser ${CMAKE_CURRENT_BINARY_DIR}/parser)
-add_executable(pp pp.cpp)
-target_link_libraries(pp ${EXTRA_LIBS})
-add_test(pp ${CMAKE_CURRENT_BINARY_DIR}/pp)

src/tests/frontends/lean/CMakeLists.txt

@@ -0,0 +1,12 @@
+add_executable(lean_frontend_tst lean_frontend.cpp)
+target_link_libraries(lean_frontend_tst ${EXTRA_LIBS})
+add_test(lean_frontend ${CMAKE_CURRENT_BINARY_DIR}/lean_frontend_tst)
+add_executable(lean_scanner lean_scanner.cpp)
+target_link_libraries(lean_scanner ${EXTRA_LIBS})
+add_test(lean_scanner ${CMAKE_CURRENT_BINARY_DIR}/lean_scanner)
+add_executable(lean_parser lean_parser.cpp)
+target_link_libraries(lean_parser ${EXTRA_LIBS})
+add_test(lean_parser ${CMAKE_CURRENT_BINARY_DIR}/lean_parser)
+add_executable(lean_pp lean_pp.cpp)
+target_link_libraries(lean_pp ${EXTRA_LIBS})
+add_test(lean_pp ${CMAKE_CURRENT_BINARY_DIR}/lean_pp)

src/tests/frontends/lean/lean_frontend.cpp

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontend.h"
 #include "environment.h"
-#include "operator_info.h"
 #include "kernel_exception.h"
 #include "builtin.h"
-#include "abstract.h"
-#include "pp.h"
 #include "printer.h"
+#include "abstract.h"
+#include "lean_frontend.h"
+#include "lean_operator_info.h"
+#include "lean_pp.h"
 #include "test.h"
 using namespace lean;
 

src/tests/frontends/lean/lean_parser.cpp

@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #include <sstream>
 #include "builtin.h"
-#include "parser.h"
-#include "pp.h"
+#include "lean_parser.h"
+#include "lean_pp.h"
 #include "printer.h"
 #include "exception.h"
 #include "test.h"

src/tests/frontends/lean/lean_pp.cpp

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontend.h"
 #include "printer.h"
 #include "abstract.h"
 #include "builtin.h"
-#include "pp.h"
+#include "lean_frontend.h"
+#include "lean_pp.h"
 #include "test.h"
 using namespace lean;
 

src/tests/frontends/lean/lean_scanner.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <sstream>
-#include "scanner.h"
+#include "lean_scanner.h"
 #include "exception.h"
 #include "escaped.h"
 #include "test.h"