From 4c19cc695785b830b0a6fa6c64a43d2ce7827d0e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Sep 2013 20:09:35 -0700 Subject: [PATCH] Rename lean frontend files. The prefix lean_ is not necessary anymore. Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 4 ++-- src/frontends/lean/{lean_coercion.h => coercion.h} | 0 .../lean/{lean_elaborator.cpp => elaborator.cpp} | 6 +++--- .../lean/{lean_elaborator.h => elaborator.h} | 0 ...ator_exception.cpp => elaborator_exception.cpp} | 4 ++-- ...aborator_exception.h => elaborator_exception.h} | 2 +- .../lean/{lean_frontend.cpp => frontend.cpp} | 10 +++++----- src/frontends/lean/{lean_frontend.h => frontend.h} | 2 +- .../lean/{lean_notation.cpp => notation.cpp} | 2 +- src/frontends/lean/{lean_notation.h => notation.h} | 0 .../{lean_operator_info.cpp => operator_info.cpp} | 2 +- .../lean/{lean_operator_info.h => operator_info.h} | 0 src/frontends/lean/{lean_parser.cpp => parser.cpp} | 14 +++++++------- src/frontends/lean/{lean_parser.h => parser.h} | 2 +- src/frontends/lean/{lean_pp.cpp => pp.cpp} | 10 +++++----- src/frontends/lean/{lean_pp.h => pp.h} | 0 .../lean/{lean_scanner.cpp => scanner.cpp} | 2 +- src/frontends/lean/{lean_scanner.h => scanner.h} | 0 src/shell/lean.cpp | 2 +- src/tests/frontends/lean/implicit_args.cpp | 6 +++--- src/tests/frontends/lean/lean_frontend.cpp | 6 +++--- src/tests/frontends/lean/lean_parser.cpp | 4 ++-- src/tests/frontends/lean/lean_pp.cpp | 4 ++-- src/tests/frontends/lean/lean_scanner.cpp | 2 +- 24 files changed, 42 insertions(+), 42 deletions(-) rename src/frontends/lean/{lean_coercion.h => coercion.h} (100%) rename src/frontends/lean/{lean_elaborator.cpp => elaborator.cpp} (99%) rename src/frontends/lean/{lean_elaborator.h => elaborator.h} (100%) rename src/frontends/lean/{lean_elaborator_exception.cpp => elaborator_exception.cpp} (97%) rename src/frontends/lean/{lean_elaborator_exception.h => elaborator_exception.h} (99%) rename src/frontends/lean/{lean_frontend.cpp => frontend.cpp} (98%) rename src/frontends/lean/{lean_frontend.h => frontend.h} (99%) rename src/frontends/lean/{lean_notation.cpp => notation.cpp} (99%) rename src/frontends/lean/{lean_notation.h => notation.h} (100%) rename src/frontends/lean/{lean_operator_info.cpp => operator_info.cpp} (99%) rename src/frontends/lean/{lean_operator_info.h => operator_info.h} (100%) rename src/frontends/lean/{lean_parser.cpp => parser.cpp} (99%) rename src/frontends/lean/{lean_parser.h => parser.h} (97%) rename src/frontends/lean/{lean_pp.cpp => pp.cpp} (99%) rename src/frontends/lean/{lean_pp.h => pp.h} (100%) rename src/frontends/lean/{lean_scanner.cpp => scanner.cpp} (99%) rename src/frontends/lean/{lean_scanner.h => scanner.h} (100%) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index f40f93f1d..fa7b6b06b 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -1,3 +1,3 @@ -add_library(lean_frontend lean_frontend.cpp lean_operator_info.cpp lean_scanner.cpp lean_parser.cpp lean_pp.cpp - lean_notation.cpp lean_elaborator.cpp lean_elaborator_exception.cpp) +add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp + notation.cpp elaborator.cpp elaborator_exception.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/lean_coercion.h b/src/frontends/lean/coercion.h similarity index 100% rename from src/frontends/lean/lean_coercion.h rename to src/frontends/lean/coercion.h diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/elaborator.cpp similarity index 99% rename from src/frontends/lean/lean_elaborator.cpp rename to src/frontends/lean/elaborator.cpp index 30a4701b0..8ccba6729 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -16,9 +16,9 @@ Author: Leonardo de Moura #include "library/printer.h" #include "library/update_expr.h" #include "library/expr_pair.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_elaborator.h" -#include "frontends/lean/lean_elaborator_exception.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/elaborator.h" +#include "frontends/lean/elaborator_exception.h" namespace lean { static name g_choice_name(name(name(name(0u), "library"), "choice")); diff --git a/src/frontends/lean/lean_elaborator.h b/src/frontends/lean/elaborator.h similarity index 100% rename from src/frontends/lean/lean_elaborator.h rename to src/frontends/lean/elaborator.h diff --git a/src/frontends/lean/lean_elaborator_exception.cpp b/src/frontends/lean/elaborator_exception.cpp similarity index 97% rename from src/frontends/lean/lean_elaborator_exception.cpp rename to src/frontends/lean/elaborator_exception.cpp index 1ef405322..87ebb81e6 100644 --- a/src/frontends/lean/lean_elaborator_exception.cpp +++ b/src/frontends/lean/elaborator_exception.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "frontends/lean/lean_elaborator_exception.h" -#include "frontends/lean/lean_elaborator.h" +#include "frontends/lean/elaborator_exception.h" +#include "frontends/lean/elaborator.h" namespace lean { format pp_elaborator_state(formatter fmt, elaborator const & elb, options const & opts) { diff --git a/src/frontends/lean/lean_elaborator_exception.h b/src/frontends/lean/elaborator_exception.h similarity index 99% rename from src/frontends/lean/lean_elaborator_exception.h rename to src/frontends/lean/elaborator_exception.h index 32ee874f0..a2b03a2f1 100644 --- a/src/frontends/lean/lean_elaborator_exception.h +++ b/src/frontends/lean/elaborator_exception.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include "kernel/kernel_exception.h" #include "library/state.h" -#include "frontends/lean/lean_elaborator.h" +#include "frontends/lean/elaborator.h" namespace lean { /** diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/frontend.cpp similarity index 98% rename from src/frontends/lean/lean_frontend.cpp rename to src/frontends/lean/frontend.cpp index 401dcdd8d..2e3ef8acb 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -13,11 +13,11 @@ Author: Leonardo de Moura #include "library/expr_pair.h" #include "library/import_all/import_all.h" #include "library/state.h" -#include "frontends/lean/lean_operator_info.h" -#include "frontends/lean/lean_coercion.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_notation.h" -#include "frontends/lean/lean_pp.h" +#include "frontends/lean/operator_info.h" +#include "frontends/lean/coercion.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/notation.h" +#include "frontends/lean/pp.h" namespace lean { static std::vector g_empty_vector; diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/frontend.h similarity index 99% rename from src/frontends/lean/lean_frontend.h rename to src/frontends/lean/frontend.h index b8641599a..8c472686a 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/frontend.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "kernel/environment.h" #include "library/state.h" -#include "frontends/lean/lean_operator_info.h" +#include "frontends/lean/operator_info.h" namespace lean { /** diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/notation.cpp similarity index 99% rename from src/frontends/lean/lean_notation.cpp rename to src/frontends/lean/notation.cpp index 1d1c46617..c07d496fa 100644 --- a/src/frontends/lean/lean_notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/basic_thms.h" #include "library/arith/arithlibs.h" #include "library/cast/castlib.h" -#include "frontends/lean/lean_frontend.h" +#include "frontends/lean/frontend.h" namespace lean { /** diff --git a/src/frontends/lean/lean_notation.h b/src/frontends/lean/notation.h similarity index 100% rename from src/frontends/lean/lean_notation.h rename to src/frontends/lean/notation.h diff --git a/src/frontends/lean/lean_operator_info.cpp b/src/frontends/lean/operator_info.cpp similarity index 99% rename from src/frontends/lean/lean_operator_info.cpp rename to src/frontends/lean/operator_info.cpp index 4402051fe..71e245dba 100644 --- a/src/frontends/lean/lean_operator_info.cpp +++ b/src/frontends/lean/operator_info.cpp @@ -6,7 +6,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/rc.h" -#include "frontends/lean/lean_operator_info.h" +#include "frontends/lean/operator_info.h" namespace lean { /** \brief Actual implementation of operator_info */ diff --git a/src/frontends/lean/lean_operator_info.h b/src/frontends/lean/operator_info.h similarity index 100% rename from src/frontends/lean/lean_operator_info.h rename to src/frontends/lean/operator_info.h diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/parser.cpp similarity index 99% rename from src/frontends/lean/lean_parser.cpp rename to src/frontends/lean/parser.cpp index ee70b37cb..e0e9c5949 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -20,13 +20,13 @@ Author: Leonardo de Moura #include "library/state.h" #include "library/kernel_exception_formatter.h" #include "library/metavar.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_elaborator.h" -#include "frontends/lean/lean_elaborator_exception.h" -#include "frontends/lean/lean_parser.h" -#include "frontends/lean/lean_scanner.h" -#include "frontends/lean/lean_notation.h" -#include "frontends/lean/lean_pp.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/elaborator.h" +#include "frontends/lean/elaborator_exception.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/scanner.h" +#include "frontends/lean/notation.h" +#include "frontends/lean/pp.h" #ifdef LEAN_USE_READLINE #include #include diff --git a/src/frontends/lean/lean_parser.h b/src/frontends/lean/parser.h similarity index 97% rename from src/frontends/lean/lean_parser.h rename to src/frontends/lean/parser.h index a3037e18b..a7ecb0f56 100644 --- a/src/frontends/lean/lean_parser.h +++ b/src/frontends/lean/parser.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "util/interruptable_ptr.h" -#include "frontends/lean/lean_frontend.h" +#include "frontends/lean/frontend.h" namespace lean { /** \brief Functional object for parsing commands and expressions */ diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/pp.cpp similarity index 99% rename from src/frontends/lean/lean_pp.cpp rename to src/frontends/lean/pp.cpp index 6d02f0fe8..8266ee7d7 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -19,11 +19,11 @@ Author: Leonardo de Moura #include "kernel/free_vars.h" #include "library/context_to_lambda.h" #include "library/metavar.h" -#include "frontends/lean/lean_notation.h" -#include "frontends/lean/lean_pp.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_coercion.h" -#include "frontends/lean/lean_elaborator.h" +#include "frontends/lean/notation.h" +#include "frontends/lean/pp.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/coercion.h" +#include "frontends/lean/elaborator.h" #ifndef LEAN_DEFAULT_PP_MAX_DEPTH #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits::max() diff --git a/src/frontends/lean/lean_pp.h b/src/frontends/lean/pp.h similarity index 100% rename from src/frontends/lean/lean_pp.h rename to src/frontends/lean/pp.h diff --git a/src/frontends/lean/lean_scanner.cpp b/src/frontends/lean/scanner.cpp similarity index 99% rename from src/frontends/lean/lean_scanner.cpp rename to src/frontends/lean/scanner.cpp index 5ca701864..a2665eace 100644 --- a/src/frontends/lean/lean_scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include #include "util/debug.h" #include "util/exception.h" -#include "frontends/lean/lean_scanner.h" +#include "frontends/lean/scanner.h" namespace lean { diff --git a/src/frontends/lean/lean_scanner.h b/src/frontends/lean/scanner.h similarity index 100% rename from src/frontends/lean/lean_scanner.h rename to src/frontends/lean/scanner.h diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 551c23868..06f22e71c 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include #include "util/interruptable_ptr.h" #include "library/printer.h" -#include "frontends/lean/lean_parser.h" +#include "frontends/lean/parser.h" #include "version.h" using namespace lean; diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp index 05d53dea8..fb1709113 100644 --- a/src/tests/frontends/lean/implicit_args.cpp +++ b/src/tests/frontends/lean/implicit_args.cpp @@ -14,9 +14,9 @@ Author: Leonardo de Moura #include "library/printer.h" #include "library/basic_thms.h" #include "library/import_all/import_all.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_elaborator.h" -#include "frontends/lean/lean_elaborator_exception.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/elaborator.h" +#include "frontends/lean/elaborator_exception.h" using namespace lean; expr elaborate(expr const & e, frontend const & env) { diff --git a/src/tests/frontends/lean/lean_frontend.cpp b/src/tests/frontends/lean/lean_frontend.cpp index 8c9156232..7ea6730c9 100644 --- a/src/tests/frontends/lean/lean_frontend.cpp +++ b/src/tests/frontends/lean/lean_frontend.cpp @@ -10,9 +10,9 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "kernel/abstract.h" #include "library/printer.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_operator_info.h" -#include "frontends/lean/lean_pp.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/operator_info.h" +#include "frontends/lean/pp.h" using namespace lean; static void tst1() { diff --git a/src/tests/frontends/lean/lean_parser.cpp b/src/tests/frontends/lean/lean_parser.cpp index ff59b7446..cbde2e044 100644 --- a/src/tests/frontends/lean/lean_parser.cpp +++ b/src/tests/frontends/lean/lean_parser.cpp @@ -9,8 +9,8 @@ Author: Leonardo de Moura #include "util/exception.h" #include "kernel/builtin.h" #include "library/printer.h" -#include "frontends/lean/lean_parser.h" -#include "frontends/lean/lean_pp.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/pp.h" using namespace lean; static void parse(frontend & fe, char const * str) { diff --git a/src/tests/frontends/lean/lean_pp.cpp b/src/tests/frontends/lean/lean_pp.cpp index f65c86d4e..71e22b3f0 100644 --- a/src/tests/frontends/lean/lean_pp.cpp +++ b/src/tests/frontends/lean/lean_pp.cpp @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/builtin.h" #include "library/printer.h" -#include "frontends/lean/lean_frontend.h" -#include "frontends/lean/lean_pp.h" +#include "frontends/lean/frontend.h" +#include "frontends/lean/pp.h" using namespace lean; static expr mk_shared_expr(unsigned depth) { diff --git a/src/tests/frontends/lean/lean_scanner.cpp b/src/tests/frontends/lean/lean_scanner.cpp index 65c227954..5f8b0adb2 100644 --- a/src/tests/frontends/lean/lean_scanner.cpp +++ b/src/tests/frontends/lean/lean_scanner.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "util/exception.h" #include "util/escaped.h" -#include "frontends/lean/lean_scanner.h" +#include "frontends/lean/scanner.h" using namespace lean; #define st scanner::token