From 26097475fd4c0037cc890fbdda0cfc2be9eb0ded Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Sep 2013 20:04:10 -0700 Subject: [PATCH] Use fullpath in #include directives. Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 12 +---- src/frontends/lean/lean_coercion.h | 2 +- src/frontends/lean/lean_elaborator.cpp | 28 ++++++------ src/frontends/lean/lean_elaborator.h | 4 +- .../lean/lean_elaborator_exception.cpp | 4 +- .../lean/lean_elaborator_exception.h | 6 +-- src/frontends/lean/lean_frontend.cpp | 24 +++++----- src/frontends/lean/lean_frontend.h | 6 +-- src/frontends/lean/lean_notation.cpp | 10 ++--- src/frontends/lean/lean_operator_info.cpp | 4 +- src/frontends/lean/lean_operator_info.h | 8 ++-- src/frontends/lean/lean_parser.cpp | 44 +++++++++---------- src/frontends/lean/lean_parser.h | 4 +- src/frontends/lean/lean_pp.cpp | 36 +++++++-------- src/frontends/lean/lean_pp.h | 6 +-- src/frontends/lean/lean_scanner.cpp | 6 +-- src/frontends/lean/lean_scanner.h | 6 +-- src/interval/interval.cpp | 6 +-- src/interval/interval.h | 4 +- src/interval/interval_def.h | 6 +-- src/kernel/context.cpp | 4 +- src/kernel/context.h | 4 +- src/kernel/environment.cpp | 10 ++--- src/kernel/expr.cpp | 8 ++-- src/kernel/expr.h | 12 ++--- src/kernel/expr_eq.h | 4 +- src/kernel/expr_sets.h | 4 +- src/kernel/instantiate.cpp | 4 +- src/kernel/kernel_exception.h | 6 +-- src/kernel/level.cpp | 12 ++--- src/kernel/level.h | 6 +-- src/kernel/normalizer.cpp | 24 +++++----- src/kernel/object.cpp | 4 +- src/kernel/object.h | 4 +- src/kernel/replace.h | 7 +-- src/kernel/type_checker.cpp | 16 +++---- src/library/arith/arithlibs.cpp | 2 +- src/library/arith/arithlibs.h | 8 ++-- src/library/arith/intlib.cpp | 10 ++--- src/library/arith/intlib.h | 6 +-- src/library/arith/natlib.cpp | 8 ++-- src/library/arith/natlib.h | 6 +-- src/library/arith/numtype.h | 4 +- src/library/arith/reallib.cpp | 12 ++--- src/library/arith/reallib.h | 6 +-- src/library/arith/specialfnlib.cpp | 8 ++-- src/library/arith/specialfnlib.h | 2 +- src/library/basic_thms.cpp | 8 ++-- src/library/basic_thms.h | 2 +- src/library/cast/castlib.cpp | 10 ++--- src/library/cast/castlib.h | 2 +- src/library/context_to_lambda.cpp | 2 +- src/library/context_to_lambda.h | 2 +- src/library/deep_copy.cpp | 6 +-- src/library/deep_copy.h | 2 +- src/library/expr_pair.h | 4 +- src/library/formatter.cpp | 6 +-- src/library/formatter.h | 4 +- src/library/import_all/import_all.cpp | 10 ++--- src/library/import_all/import_all.h | 2 +- src/library/kernel_exception_formatter.cpp | 2 +- src/library/kernel_exception_formatter.h | 6 +-- src/library/light_checker.cpp | 18 ++++---- src/library/light_checker.h | 4 +- src/library/max_sharing.cpp | 4 +- src/library/max_sharing.h | 2 +- src/library/metavar.cpp | 14 +++--- src/library/metavar.h | 6 +-- src/library/printer.cpp | 8 ++-- src/library/printer.h | 4 +- src/library/reduce.cpp | 12 ++--- src/library/reduce.h | 6 +-- src/library/state.cpp | 2 +- src/library/state.h | 6 +-- src/library/update_expr.cpp | 4 +- src/library/update_expr.h | 2 +- src/shell/lean.cpp | 12 +++-- src/tests/frontends/lean/implicit_args.cpp | 26 +++++------ src/tests/frontends/lean/lean_frontend.cpp | 18 ++++---- src/tests/frontends/lean/lean_parser.cpp | 12 ++--- src/tests/frontends/lean/lean_pp.cpp | 12 ++--- src/tests/frontends/lean/lean_scanner.cpp | 8 ++-- src/tests/interval/double_interval.cpp | 10 ++--- src/tests/interval/float_interval.cpp | 10 ++--- src/tests/interval/interval.cpp | 12 ++--- src/tests/interval/mpfp_interval.cpp | 10 ++--- src/tests/kernel/arith.cpp | 18 ++++---- src/tests/kernel/environment.cpp | 24 +++++----- src/tests/kernel/expr.cpp | 20 ++++----- src/tests/kernel/free_vars.cpp | 6 +-- src/tests/kernel/level.cpp | 8 ++-- src/tests/kernel/normalizer.cpp | 20 ++++----- src/tests/kernel/occurs.cpp | 8 ++-- src/tests/kernel/replace.cpp | 18 ++++---- src/tests/kernel/threads.cpp | 18 ++++---- src/tests/kernel/type_checker.cpp | 24 +++++----- src/tests/library/light_checker.cpp | 18 ++++---- src/tests/library/metavar.cpp | 8 ++-- src/tests/util/buffer.cpp | 4 +- src/tests/util/format.cpp | 10 ++--- src/tests/util/list.cpp | 6 +-- src/tests/util/name.cpp | 4 +- src/tests/util/numerics/mpbq.cpp | 6 +-- src/tests/util/numerics/mpfp.cpp | 4 +- src/tests/util/numerics/mpq.cpp | 4 +- src/tests/util/options.cpp | 6 +-- src/tests/util/pdeque.cpp | 4 +- src/tests/util/pvector.cpp | 6 +-- src/tests/util/scoped_map.cpp | 4 +- src/tests/util/scoped_set.cpp | 4 +- src/tests/util/sexpr.cpp | 14 +++--- src/util/numerics/double.cpp | 4 +- src/util/numerics/double.h | 2 +- src/util/numerics/float.cpp | 4 +- src/util/numerics/float.h | 2 +- src/util/numerics/mpbq.cpp | 2 +- src/util/numerics/mpbq.h | 6 +-- src/util/numerics/mpfp.cpp | 2 +- src/util/numerics/mpfp.h | 6 +-- src/util/numerics/mpq.cpp | 4 +- src/util/numerics/mpq.h | 2 +- src/util/numerics/mpz.h | 4 +- src/util/numerics/xnumeral.h | 4 +- src/util/sexpr/format.cpp | 10 ++--- src/util/sexpr/format.h | 8 ++-- src/util/sexpr/options.h | 6 +-- src/util/sexpr/sexpr.cpp | 14 +++--- src/util/sexpr/sexpr_fn.h | 4 +- 128 files changed, 532 insertions(+), 535 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1ab13b0825..eaa4949b8b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -77,17 +77,7 @@ if("${READLINE}" MATCHES "ON") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DLEAN_USE_READLINE") endif() -include_directories(${LEAN_SOURCE_DIR}/util) -include_directories(${LEAN_SOURCE_DIR}/util/numerics) -include_directories(${LEAN_SOURCE_DIR}/util/sexpr) -include_directories(${LEAN_SOURCE_DIR}/interval) -include_directories(${LEAN_SOURCE_DIR}/kernel) -include_directories(${LEAN_SOURCE_DIR}/library) -include_directories(${LEAN_SOURCE_DIR}/library/arith) -include_directories(${LEAN_SOURCE_DIR}/library/cast) -include_directories(${LEAN_SOURCE_DIR}/library/import_all) -include_directories(${LEAN_SOURCE_DIR}/parsers) -include_directories(${LEAN_SOURCE_DIR}/frontends/lean) +include_directories(${LEAN_SOURCE_DIR}) add_subdirectory(util) set(LEAN_LIBS ${LEAN_LIBS} util) diff --git a/src/frontends/lean/lean_coercion.h b/src/frontends/lean/lean_coercion.h index 182eaeb866..378c425a0e 100644 --- a/src/frontends/lean/lean_coercion.h +++ b/src/frontends/lean/lean_coercion.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "object.h" +#include "kernel/object.h" namespace lean { /** diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index 99277cb934..30a4701b06 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -5,20 +5,20 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "normalizer.h" -#include "metavar.h" -#include "printer.h" -#include "context.h" -#include "builtin.h" -#include "free_vars.h" -#include "for_each.h" -#include "update_expr.h" -#include "replace.h" -#include "expr_pair.h" -#include "flet.h" -#include "lean_frontend.h" -#include "lean_elaborator.h" -#include "lean_elaborator_exception.h" +#include "util/flet.h" +#include "kernel/normalizer.h" +#include "kernel/context.h" +#include "kernel/builtin.h" +#include "kernel/free_vars.h" +#include "kernel/for_each.h" +#include "kernel/replace.h" +#include "library/metavar.h" +#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" 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/lean_elaborator.h index fd3ed88448..f1c23059de 100644 --- a/src/frontends/lean/lean_elaborator.h +++ b/src/frontends/lean/lean_elaborator.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include "environment.h" -#include "formatter.h" +#include "kernel/environment.h" +#include "library/formatter.h" namespace lean { class frontend; diff --git a/src/frontends/lean/lean_elaborator_exception.cpp b/src/frontends/lean/lean_elaborator_exception.cpp index 3478df8ba9..1ef405322c 100644 --- a/src/frontends/lean/lean_elaborator_exception.cpp +++ b/src/frontends/lean/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 "lean_elaborator_exception.h" -#include "lean_elaborator.h" +#include "frontends/lean/lean_elaborator_exception.h" +#include "frontends/lean/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/lean_elaborator_exception.h index 7f74061344..32ee874f00 100644 --- a/src/frontends/lean/lean_elaborator_exception.h +++ b/src/frontends/lean/lean_elaborator_exception.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "lean_elaborator.h" -#include "kernel_exception.h" -#include "state.h" +#include "kernel/kernel_exception.h" +#include "library/state.h" +#include "frontends/lean/lean_elaborator.h" namespace lean { /** diff --git a/src/frontends/lean/lean_frontend.cpp b/src/frontends/lean/lean_frontend.cpp index 2cdfc8476d..401dcdd8dd 100644 --- a/src/frontends/lean/lean_frontend.cpp +++ b/src/frontends/lean/lean_frontend.cpp @@ -6,18 +6,18 @@ Author: Leonardo de Moura */ #include #include -#include "environment.h" -#include "import_all.h" -#include "map.h" -#include "state.h" -#include "sstream.h" -#include "exception.h" -#include "expr_pair.h" -#include "lean_operator_info.h" -#include "lean_coercion.h" -#include "lean_frontend.h" -#include "lean_notation.h" -#include "lean_pp.h" +#include "util/map.h" +#include "util/sstream.h" +#include "util/exception.h" +#include "kernel/environment.h" +#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" namespace lean { static std::vector g_empty_vector; diff --git a/src/frontends/lean/lean_frontend.h b/src/frontends/lean/lean_frontend.h index 2211639647..b8641599a8 100644 --- a/src/frontends/lean/lean_frontend.h +++ b/src/frontends/lean/lean_frontend.h @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #pragma once #include -#include "environment.h" -#include "state.h" -#include "lean_operator_info.h" +#include "kernel/environment.h" +#include "library/state.h" +#include "frontends/lean/lean_operator_info.h" namespace lean { /** diff --git a/src/frontends/lean/lean_notation.cpp b/src/frontends/lean/lean_notation.cpp index 7df78dfb7c..1d1c46617c 100644 --- a/src/frontends/lean/lean_notation.cpp +++ b/src/frontends/lean/lean_notation.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "builtin.h" -#include "basic_thms.h" -#include "lean_frontend.h" -#include "arithlibs.h" -#include "castlib.h" +#include "kernel/builtin.h" +#include "library/basic_thms.h" +#include "library/arith/arithlibs.h" +#include "library/cast/castlib.h" +#include "frontends/lean/lean_frontend.h" namespace lean { /** diff --git a/src/frontends/lean/lean_operator_info.cpp b/src/frontends/lean/lean_operator_info.cpp index cd56843cc6..4402051fee 100644 --- a/src/frontends/lean/lean_operator_info.cpp +++ b/src/frontends/lean/lean_operator_info.cpp @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "lean_operator_info.h" -#include "rc.h" +#include "util/rc.h" +#include "frontends/lean/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/lean_operator_info.h index b51c515159..8da83514cc 100644 --- a/src/frontends/lean/lean_operator_info.h +++ b/src/frontends/lean/lean_operator_info.h @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "name.h" -#include "list.h" -#include "format.h" -#include "object.h" +#include "util/name.h" +#include "util/list.h" +#include "util/sexpr/format.h" +#include "kernel/object.h" namespace lean { /** diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp index c9a82cbc9b..ee70b37cbb 100644 --- a/src/frontends/lean/lean_parser.cpp +++ b/src/frontends/lean/lean_parser.cpp @@ -5,28 +5,28 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "scoped_map.h" -#include "exception.h" -#include "normalizer.h" -#include "type_checker.h" -#include "free_vars.h" -#include "builtin.h" -#include "arithlibs.h" -#include "printer.h" -#include "state.h" -#include "option_declarations.h" -#include "expr_maps.h" -#include "sstream.h" -#include "kernel_exception.h" -#include "kernel_exception_formatter.h" -#include "metavar.h" -#include "lean_frontend.h" -#include "lean_elaborator.h" -#include "lean_elaborator_exception.h" -#include "lean_parser.h" -#include "lean_scanner.h" -#include "lean_notation.h" -#include "lean_pp.h" +#include "util/scoped_map.h" +#include "util/exception.h" +#include "util/sstream.h" +#include "util/sexpr/option_declarations.h" +#include "kernel/normalizer.h" +#include "kernel/type_checker.h" +#include "kernel/free_vars.h" +#include "kernel/builtin.h" +#include "kernel/kernel_exception.h" +#include "kernel/expr_maps.h" +#include "library/arith/arithlibs.h" +#include "library/printer.h" +#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" #ifdef LEAN_USE_READLINE #include #include diff --git a/src/frontends/lean/lean_parser.h b/src/frontends/lean/lean_parser.h index e9b2f6d01c..a3037e18b3 100644 --- a/src/frontends/lean/lean_parser.h +++ b/src/frontends/lean/lean_parser.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include "lean_frontend.h" -#include "interruptable_ptr.h" +#include "util/interruptable_ptr.h" +#include "frontends/lean/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/lean_pp.cpp index b43b0471f3..6d02f0fe81 100644 --- a/src/frontends/lean/lean_pp.cpp +++ b/src/frontends/lean/lean_pp.cpp @@ -6,24 +6,24 @@ Author: Leonardo de Moura */ #include #include -#include "context.h" -#include "scoped_map.h" -#include "scoped_set.h" -#include "for_each.h" -#include "instantiate.h" -#include "occurs.h" -#include "builtin.h" -#include "free_vars.h" -#include "context_to_lambda.h" -#include "options.h" -#include "interruptable_ptr.h" -#include "metavar.h" -#include "exception.h" -#include "lean_notation.h" -#include "lean_pp.h" -#include "lean_frontend.h" -#include "lean_coercion.h" -#include "lean_elaborator.h" +#include "util/scoped_map.h" +#include "util/exception.h" +#include "util/scoped_set.h" +#include "util/sexpr/options.h" +#include "util/interruptable_ptr.h" +#include "kernel/context.h" +#include "kernel/for_each.h" +#include "kernel/instantiate.h" +#include "kernel/occurs.h" +#include "kernel/builtin.h" +#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" #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/lean_pp.h index ccb124af43..346225878b 100644 --- a/src/frontends/lean/lean_pp.h +++ b/src/frontends/lean/lean_pp.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "context.h" -#include "formatter.h" -#include "options.h" +#include "util/sexpr/options.h" +#include "kernel/context.h" +#include "library/formatter.h" namespace lean { class frontend; diff --git a/src/frontends/lean/lean_scanner.cpp b/src/frontends/lean/lean_scanner.cpp index 119b83bb4a..5ca7018648 100644 --- a/src/frontends/lean/lean_scanner.cpp +++ b/src/frontends/lean/lean_scanner.cpp @@ -7,9 +7,9 @@ Author: Leonardo de Moura #include #include #include -#include "lean_scanner.h" -#include "debug.h" -#include "exception.h" +#include "util/debug.h" +#include "util/exception.h" +#include "frontends/lean/lean_scanner.h" namespace lean { diff --git a/src/frontends/lean/lean_scanner.h b/src/frontends/lean/lean_scanner.h index 8a02555c1d..1ef34ec4d4 100644 --- a/src/frontends/lean/lean_scanner.h +++ b/src/frontends/lean/lean_scanner.h @@ -7,9 +7,9 @@ Author: Leonardo de Moura #pragma once #include #include -#include "mpq.h" -#include "name.h" -#include "list.h" +#include "util/name.h" +#include "util/list.h" +#include "util/numerics/mpq.h" namespace lean { /** diff --git a/src/interval/interval.cpp b/src/interval/interval.cpp index 8c612c56be..fcfc735abc 100644 --- a/src/interval/interval.cpp +++ b/src/interval/interval.cpp @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "interval_def.h" -#include "mpq.h" -#include "double.h" +#include "util/numerics/mpq.h" +#include "util/numerics/double.h" +#include "interval/interval_def.h" namespace lean { template class interval; diff --git a/src/interval/interval.h b/src/interval/interval.h index 3222de143f..44c55615a5 100644 --- a/src/interval/interval.h +++ b/src/interval/interval.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura Soonho Kong */ #pragma once -#include "numeric_traits.h" -#include "xnumeral.h" +#include "util/numerics/numeric_traits.h" +#include "util/numerics/xnumeral.h" namespace lean { diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h index c9a01bce20..1847ef8f1b 100644 --- a/src/interval/interval_def.h +++ b/src/interval/interval_def.h @@ -9,9 +9,9 @@ Author: Leonardo de Moura #include #include #include -#include "interval.h" -#include "trace.h" -#include "mpz.h" +#include "util/trace.h" +#include "util/numerics/mpz.h" +#include "interval/interval.h" namespace lean { diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp index d8a96c4013..2ebdb462d3 100644 --- a/src/kernel/context.cpp +++ b/src/kernel/context.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "context.h" -#include "exception.h" +#include "util/exception.h" +#include "kernel/context.h" namespace lean { std::pair context::lookup_ext(unsigned i) const { diff --git a/src/kernel/context.h b/src/kernel/context.h index 537db6101c..b0bb98c598 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "list.h" +#include "util/list.h" +#include "kernel/expr.h" namespace lean { /** diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 99dffee2d2..4ea011ec3e 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -8,11 +8,11 @@ Author: Leonardo de Moura #include #include #include -#include "kernel_exception.h" -#include "environment.h" -#include "safe_arith.h" -#include "type_checker.h" -#include "normalizer.h" +#include "util/safe_arith.h" +#include "kernel/kernel_exception.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" +#include "kernel/normalizer.h" namespace lean { diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index c646e4863e..507d1bfb05 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -7,10 +7,10 @@ Author: Leonardo de Moura */ #include #include -#include "expr.h" -#include "free_vars.h" -#include "expr_eq.h" -#include "hash.h" +#include "util/hash.h" +#include "kernel/expr.h" +#include "kernel/free_vars.h" +#include "kernel/expr_eq.h" namespace lean { unsigned hash_args(unsigned size, expr const * args) { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index b420df9ddf..90bf973caf 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -8,12 +8,12 @@ Author: Leonardo de Moura #include #include #include -#include "rc.h" -#include "name.h" -#include "level.h" -#include "hash.h" -#include "buffer.h" -#include "format.h" +#include "util/rc.h" +#include "util/name.h" +#include "util/hash.h" +#include "util/buffer.h" +#include "util/sexpr/format.h" +#include "kernel/level.h" namespace lean { class value; diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index ed026544c3..b7327a852d 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "expr_sets.h" +#include "kernel/expr.h" +#include "kernel/expr_sets.h" namespace lean { /** \brief Identity function for expressions. */ diff --git a/src/kernel/expr_sets.h b/src/kernel/expr_sets.h index 5e78f9e0bc..93a923305b 100644 --- a/src/kernel/expr_sets.h +++ b/src/kernel/expr_sets.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include "expr.h" -#include "hash.h" +#include "util/hash.h" +#include "kernel/expr.h" namespace lean { diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index 033223634f..3ab414fd27 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "free_vars.h" -#include "replace.h" +#include "kernel/free_vars.h" +#include "kernel/replace.h" namespace lean { expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 70948afb09..932dcb5e07 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "exception.h" -#include "context.h" -#include "environment.h" +#include "util/exception.h" +#include "kernel/context.h" +#include "kernel/environment.h" namespace lean { class environment; diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 35a0160c35..48e0ed9db9 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "safe_arith.h" -#include "level.h" -#include "buffer.h" -#include "rc.h" -#include "debug.h" -#include "hash.h" +#include "util/safe_arith.h" +#include "util/buffer.h" +#include "util/rc.h" +#include "util/debug.h" +#include "util/hash.h" +#include "kernel/level.h" namespace lean { /** \brief Base class for representing universe level cells. */ diff --git a/src/kernel/level.h b/src/kernel/level.h index a59c898a53..d6c3ab29ad 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #pragma once #include -#include "name.h" -#include "format.h" -#include "options.h" +#include "util/name.h" +#include "util/sexpr/format.h" +#include "util/sexpr/options.h" namespace lean { class environment; diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index f9a2eb6c9d..bdc0b16c60 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -5,18 +5,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "normalizer.h" -#include "expr.h" -#include "context.h" -#include "environment.h" -#include "scoped_map.h" -#include "builtin.h" -#include "free_vars.h" -#include "list.h" -#include "flet.h" -#include "buffer.h" -#include "kernel_exception.h" -#include "options.h" +#include "util/scoped_map.h" +#include "util/list.h" +#include "util/flet.h" +#include "util/buffer.h" +#include "util/sexpr/options.h" +#include "kernel/normalizer.h" +#include "kernel/expr.h" +#include "kernel/context.h" +#include "kernel/environment.h" +#include "kernel/builtin.h" +#include "kernel/free_vars.h" +#include "kernel/kernel_exception.h" #ifndef LEAN_KERNEL_NORMALIZER_MAX_DEPTH #define LEAN_KERNEL_NORMALIZER_MAX_DEPTH std::numeric_limits::max() diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp index 15fee829f9..8139bdd5fc 100644 --- a/src/kernel/object.cpp +++ b/src/kernel/object.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "object.h" -#include "environment.h" +#include "kernel/object.h" +#include "kernel/environment.h" namespace lean { neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {} diff --git a/src/kernel/object.h b/src/kernel/object.h index 8794ff4a7b..14b8c343d2 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "rc.h" +#include "util/rc.h" +#include "kernel/expr.h" /* Kernel objects. diff --git a/src/kernel/replace.h b/src/kernel/replace.h index 883def2466..7ba2a56a3e 100644 --- a/src/kernel/replace.h +++ b/src/kernel/replace.h @@ -5,9 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "buffer.h" -#include "expr.h" -#include "expr_maps.h" +#include "util/buffer.h" +#include "kernel/expr.h" +#include "kernel/expr_maps.h" + namespace lean { /** \brief Default replace_fn postprocessor functional object. It is a diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 5cb89b7ae1..0f8e5dcc54 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "type_checker.h" -#include "environment.h" -#include "kernel_exception.h" -#include "normalizer.h" -#include "instantiate.h" -#include "scoped_map.h" -#include "builtin.h" -#include "free_vars.h" +#include "util/scoped_map.h" +#include "kernel/type_checker.h" +#include "kernel/environment.h" +#include "kernel/kernel_exception.h" +#include "kernel/normalizer.h" +#include "kernel/instantiate.h" +#include "kernel/builtin.h" +#include "kernel/free_vars.h" namespace lean { /** \brief Auxiliary functional object used to implement infer_type. */ diff --git a/src/library/arith/arithlibs.cpp b/src/library/arith/arithlibs.cpp index ad54417f74..6890f1e5c6 100644 --- a/src/library/arith/arithlibs.cpp +++ b/src/library/arith/arithlibs.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "arithlibs.h" +#include "library/arith/arithlibs.h" namespace lean { void import_arithlibs(environment & env) { diff --git a/src/library/arith/arithlibs.h b/src/library/arith/arithlibs.h index 2584183f90..7175b21631 100644 --- a/src/library/arith/arithlibs.h +++ b/src/library/arith/arithlibs.h @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "natlib.h" -#include "intlib.h" -#include "reallib.h" -#include "specialfnlib.h" +#include "library/arith/natlib.h" +#include "library/arith/intlib.h" +#include "library/arith/reallib.h" +#include "library/arith/specialfnlib.h" namespace lean { class environment; diff --git a/src/library/arith/intlib.cpp b/src/library/arith/intlib.cpp index 31ae459e3a..28e777db7d 100644 --- a/src/library/arith/intlib.cpp +++ b/src/library/arith/intlib.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "intlib.h" -#include "natlib.h" -#include "numtype.h" -#include "abstract.h" -#include "environment.h" +#include "kernel/abstract.h" +#include "kernel/environment.h" +#include "library/arith/intlib.h" +#include "library/arith/natlib.h" +#include "library/arith/numtype.h" namespace lean { class int_type_value : public num_type_value { diff --git a/src/library/arith/intlib.h b/src/library/arith/intlib.h index 452b6c46d5..0fe4775f3e 100644 --- a/src/library/arith/intlib.h +++ b/src/library/arith/intlib.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "builtin.h" -#include "mpz.h" +#include "util/numerics/mpz.h" +#include "kernel/expr.h" +#include "kernel/builtin.h" namespace lean { /** \brief Integer numbers type */ diff --git a/src/library/arith/natlib.cpp b/src/library/arith/natlib.cpp index 6f975337fb..59bf168365 100644 --- a/src/library/arith/natlib.cpp +++ b/src/library/arith/natlib.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "natlib.h" -#include "numtype.h" -#include "abstract.h" -#include "environment.h" +#include "kernel/abstract.h" +#include "kernel/environment.h" +#include "library/arith/natlib.h" +#include "library/arith/numtype.h" namespace lean { class nat_type_value : public num_type_value { diff --git a/src/library/arith/natlib.h b/src/library/arith/natlib.h index 401e083805..6c8c31757a 100644 --- a/src/library/arith/natlib.h +++ b/src/library/arith/natlib.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "builtin.h" -#include "mpz.h" +#include "kernel/expr.h" +#include "kernel/builtin.h" +#include "util/numerics/mpz.h" namespace lean { /** \brief Natural numbers type */ diff --git a/src/library/arith/numtype.h b/src/library/arith/numtype.h index a1582002dd..f136404381 100644 --- a/src/library/arith/numtype.h +++ b/src/library/arith/numtype.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "value.h" +#include "kernel/expr.h" +#include "kernel/value.h" namespace lean { /** \brief Base class for numeric types */ diff --git a/src/library/arith/reallib.cpp b/src/library/arith/reallib.cpp index ca0b0c702d..8c0e98ba9b 100644 --- a/src/library/arith/reallib.cpp +++ b/src/library/arith/reallib.cpp @@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "reallib.h" -#include "intlib.h" -#include "natlib.h" -#include "numtype.h" -#include "abstract.h" -#include "environment.h" +#include "kernel/abstract.h" +#include "kernel/environment.h" +#include "library/arith/reallib.h" +#include "library/arith/intlib.h" +#include "library/arith/natlib.h" +#include "library/arith/numtype.h" namespace lean { class real_type_value : public num_type_value { diff --git a/src/library/arith/reallib.h b/src/library/arith/reallib.h index 0a24e37fd2..a771a6a394 100644 --- a/src/library/arith/reallib.h +++ b/src/library/arith/reallib.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "builtin.h" -#include "mpq.h" +#include "util/numerics/mpq.h" +#include "kernel/expr.h" +#include "kernel/builtin.h" namespace lean { /** \brief Real numbers type */ diff --git a/src/library/arith/specialfnlib.cpp b/src/library/arith/specialfnlib.cpp index ea985d6bc2..0c3b316fe5 100644 --- a/src/library/arith/specialfnlib.cpp +++ b/src/library/arith/specialfnlib.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "specialfnlib.h" -#include "reallib.h" -#include "abstract.h" -#include "environment.h" +#include "kernel/environment.h" +#include "kernel/abstract.h" +#include "library/arith/specialfnlib.h" +#include "library/arith/reallib.h" namespace lean { MK_CONSTANT(exp_fn, name("exp")); diff --git a/src/library/arith/specialfnlib.h b/src/library/arith/specialfnlib.h index 82c17df1c8..525cec5109 100644 --- a/src/library/arith/specialfnlib.h +++ b/src/library/arith/specialfnlib.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" +#include "kernel/expr.h" namespace lean { // Special functions library diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index 41a75b2463..66831fad77 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "basic_thms.h" -#include "environment.h" -#include "abstract.h" -#include "type_checker.h" +#include "kernel/environment.h" +#include "kernel/abstract.h" +#include "kernel/type_checker.h" +#include "library/basic_thms.h" namespace lean { diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h index 8d7332759f..696b023761 100644 --- a/src/library/basic_thms.h +++ b/src/library/basic_thms.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "builtin.h" +#include "kernel/builtin.h" namespace lean { expr mk_trivial(); diff --git a/src/library/cast/castlib.cpp b/src/library/cast/castlib.cpp index 5890924bbe..5f47169599 100644 --- a/src/library/cast/castlib.cpp +++ b/src/library/cast/castlib.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "castlib.h" -#include "environment.h" -#include "abstract.h" -#include "basic_thms.h" -#include "builtin.h" +#include "kernel/environment.h" +#include "kernel/abstract.h" +#include "kernel/builtin.h" +#include "library/basic_thms.h" +#include "library/cast/castlib.h" namespace lean { // Cast builtin operator diff --git a/src/library/cast/castlib.h b/src/library/cast/castlib.h index 715f41614f..b350005834 100644 --- a/src/library/cast/castlib.h +++ b/src/library/cast/castlib.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" +#include "kernel/expr.h" namespace lean { /** \brief Type Cast. It has type Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B */ diff --git a/src/library/context_to_lambda.cpp b/src/library/context_to_lambda.cpp index c451d77b83..9680263cab 100644 --- a/src/library/context_to_lambda.cpp +++ b/src/library/context_to_lambda.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "context_to_lambda.h" +#include "library/context_to_lambda.h" namespace lean { static expr g_fake = Const(name(name(0u), "context_to_lambda")); diff --git a/src/library/context_to_lambda.h b/src/library/context_to_lambda.h index 0f2618bf88..fec661c300 100644 --- a/src/library/context_to_lambda.h +++ b/src/library/context_to_lambda.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "context.h" +#include "kernel/context.h" namespace lean { /** \brief Given the context (n_1 : T_1 [:= V_1]) ... (n_k : T_k [:= V_k]) and expression e into, diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp index 8ea6c76561..c787293d73 100644 --- a/src/library/deep_copy.cpp +++ b/src/library/deep_copy.cpp @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "expr.h" -#include "expr_maps.h" -#include "buffer.h" +#include "util/buffer.h" +#include "kernel/expr.h" +#include "kernel/expr_maps.h" namespace lean { /** \brief Implements deep copy of kernel expressions. */ diff --git a/src/library/deep_copy.h b/src/library/deep_copy.h index 6c1091f066..d32b83b93d 100644 --- a/src/library/deep_copy.h +++ b/src/library/deep_copy.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" +#include "kernel/expr.h" namespace lean { /** diff --git a/src/library/expr_pair.h b/src/library/expr_pair.h index 4e93adb286..2694406aaa 100644 --- a/src/library/expr_pair.h +++ b/src/library/expr_pair.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "hash.h" +#include "util/hash.h" +#include "kernel/expr.h" namespace lean { typedef std::pair expr_pair; diff --git a/src/library/formatter.cpp b/src/library/formatter.cpp index a48f4407c7..a773f0a313 100644 --- a/src/library/formatter.cpp +++ b/src/library/formatter.cpp @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "formatter.h" -#include "printer.h" -#include "kernel_exception.h" +#include "kernel/kernel_exception.h" +#include "library/printer.h" +#include "library/formatter.h" namespace lean { class simple_formatter_cell : public formatter_cell { diff --git a/src/library/formatter.h b/src/library/formatter.h index 470488a8e0..957325b24a 100644 --- a/src/library/formatter.h +++ b/src/library/formatter.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include "context.h" -#include "options.h" +#include "util/sexpr/options.h" +#include "kernel/context.h" namespace lean { class environment; diff --git a/src/library/import_all/import_all.cpp b/src/library/import_all/import_all.cpp index 3a73373f20..77fb27d0a6 100644 --- a/src/library/import_all/import_all.cpp +++ b/src/library/import_all/import_all.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "import_all.h" -#include "builtin.h" -#include "basic_thms.h" -#include "arithlibs.h" -#include "castlib.h" +#include "kernel/builtin.h" +#include "library/basic_thms.h" +#include "library/arith/arithlibs.h" +#include "library/cast/castlib.h" +#include "library/import_all/import_all.h" namespace lean { void import_all(environment & env) { diff --git a/src/library/import_all/import_all.h b/src/library/import_all/import_all.h index 7668b2ed40..a4f84830df 100644 --- a/src/library/import_all/import_all.h +++ b/src/library/import_all/import_all.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "environment.h" +#include "kernel/environment.h" namespace lean { /** \brief Import all builtin libraries and theorems */ diff --git a/src/library/kernel_exception_formatter.cpp b/src/library/kernel_exception_formatter.cpp index c21e4f94b1..4fdd96af2d 100644 --- a/src/library/kernel_exception_formatter.cpp +++ b/src/library/kernel_exception_formatter.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel_exception_formatter.h" +#include "library/kernel_exception_formatter.h" namespace lean { /* diff --git a/src/library/kernel_exception_formatter.h b/src/library/kernel_exception_formatter.h index 09dea1fc6f..ee24ae7fe6 100644 --- a/src/library/kernel_exception_formatter.h +++ b/src/library/kernel_exception_formatter.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel_exception.h" -#include "formatter.h" -#include "state.h" +#include "kernel/kernel_exception.h" +#include "library/formatter.h" +#include "library/state.h" namespace lean { /** \brief Pretty print an arbitrary kernel exception using the given formatter */ diff --git a/src/library/light_checker.cpp b/src/library/light_checker.cpp index 473b9ab88e..385366fdf3 100644 --- a/src/library/light_checker.cpp +++ b/src/library/light_checker.cpp @@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "light_checker.h" -#include "environment.h" -#include "reduce.h" -#include "scoped_map.h" -#include "normalizer.h" -#include "builtin.h" -#include "kernel_exception.h" -#include "instantiate.h" -#include "free_vars.h" +#include "util/scoped_map.h" +#include "kernel/environment.h" +#include "kernel/normalizer.h" +#include "kernel/builtin.h" +#include "kernel/kernel_exception.h" +#include "kernel/instantiate.h" +#include "kernel/free_vars.h" +#include "library/reduce.h" +#include "library/light_checker.h" namespace lean { class light_checker::imp { diff --git a/src/library/light_checker.h b/src/library/light_checker.h index c872a52f34..6e7c26d767 100644 --- a/src/library/light_checker.h +++ b/src/library/light_checker.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include "expr.h" -#include "context.h" +#include "kernel/expr.h" +#include "kernel/context.h" namespace lean { class environment; diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp index 06d1773630..212bdbc473 100644 --- a/src/library/max_sharing.cpp +++ b/src/library/max_sharing.cpp @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "buffer.h" -#include "max_sharing.h" +#include "util/buffer.h" +#include "library/max_sharing.h" namespace lean { /** diff --git a/src/library/max_sharing.h b/src/library/max_sharing.h index 34da4382c2..4c58d00221 100644 --- a/src/library/max_sharing.h +++ b/src/library/max_sharing.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include -#include "expr.h" +#include "kernel/expr.h" namespace lean { /** diff --git a/src/library/metavar.cpp b/src/library/metavar.cpp index 8660e07042..bb5fccb3ab 100644 --- a/src/library/metavar.cpp +++ b/src/library/metavar.cpp @@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "metavar.h" -#include "replace.h" -#include "for_each.h" -#include "environment.h" -#include "occurs.h" -#include "update_expr.h" -#include "printer.h" +#include "kernel/replace.h" +#include "kernel/for_each.h" +#include "kernel/environment.h" +#include "kernel/occurs.h" +#include "library/update_expr.h" +#include "library/printer.h" +#include "library/metavar.h" namespace lean { static name g_placeholder_name("_"); diff --git a/src/library/metavar.h b/src/library/metavar.h index e94e6d555c..2a7cc64c50 100644 --- a/src/library/metavar.h +++ b/src/library/metavar.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" -#include "environment.h" -#include "name_set.h" +#include "util/name_set.h" +#include "kernel/expr.h" +#include "kernel/environment.h" namespace lean { /** diff --git a/src/library/printer.cpp b/src/library/printer.cpp index d6944b840e..e403c87386 100644 --- a/src/library/printer.cpp +++ b/src/library/printer.cpp @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "printer.h" -#include "metavar.h" -#include "environment.h" -#include "exception.h" +#include "util/exception.h" +#include "library/printer.h" +#include "library/metavar.h" +#include "kernel/environment.h" namespace lean { bool is_atomic(expr const & e) { diff --git a/src/library/printer.h b/src/library/printer.h index f71e65ae1a..057a5a1dc9 100644 --- a/src/library/printer.h +++ b/src/library/printer.h @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #pragma once #include -#include "expr.h" -#include "context.h" +#include "kernel/expr.h" +#include "kernel/context.h" namespace lean { std::ostream & operator<<(std::ostream & out, context const & ctx); diff --git a/src/library/reduce.cpp b/src/library/reduce.cpp index 52f5d36020..cf2e021e07 100644 --- a/src/library/reduce.cpp +++ b/src/library/reduce.cpp @@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "context.h" -#include "instantiate.h" -#include "environment.h" -#include "name_set.h" -#include "update_expr.h" -#include "free_vars.h" +#include "util/name_set.h" +#include "kernel/context.h" +#include "kernel/instantiate.h" +#include "kernel/environment.h" +#include "kernel/free_vars.h" +#include "library/update_expr.h" namespace lean { bool is_head_beta(expr const & t) { diff --git a/src/library/reduce.h b/src/library/reduce.h index 2fe1620e3e..4ed2c0cbcc 100644 --- a/src/library/reduce.h +++ b/src/library/reduce.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "context.h" -#include "environment.h" -#include "name_set.h" +#include "util/name_set.h" +#include "kernel/context.h" +#include "kernel/environment.h" namespace lean { bool is_head_beta(expr const & t); diff --git a/src/library/state.cpp b/src/library/state.cpp index bd32f5879b..737d2d3d48 100644 --- a/src/library/state.cpp +++ b/src/library/state.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "state.h" +#include "library/state.h" namespace lean { state::state(): diff --git a/src/library/state.h b/src/library/state.h index fe6eb56c8c..62873fa597 100644 --- a/src/library/state.h +++ b/src/library/state.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "output_channel.h" -#include "formatter.h" -#include "options.h" +#include "util/output_channel.h" +#include "util/sexpr/options.h" +#include "library/formatter.h" namespace lean { /** diff --git a/src/library/update_expr.cpp b/src/library/update_expr.cpp index 8f5416d32a..395a2166d8 100644 --- a/src/library/update_expr.cpp +++ b/src/library/update_expr.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "update_expr.h" -#include "buffer.h" +#include "util/buffer.h" +#include "library/update_expr.h" namespace lean { expr update_app(expr const & app, unsigned i, expr const & new_arg) { diff --git a/src/library/update_expr.h b/src/library/update_expr.h index 9e09c06859..c6c31d6e95 100644 --- a/src/library/update_expr.h +++ b/src/library/update_expr.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "expr.h" +#include "kernel/expr.h" namespace lean { /** diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 8809d1e36e..551c238689 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -1,10 +1,16 @@ +/* +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 #include +#include "util/interruptable_ptr.h" +#include "library/printer.h" +#include "frontends/lean/lean_parser.h" #include "version.h" -#include "printer.h" -#include "interruptable_ptr.h" -#include "lean_parser.h" using namespace lean; static interruptable_ptr g_lean_shell; diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp index 9a9969f43a..05d53dea81 100644 --- a/src/tests/frontends/lean/implicit_args.cpp +++ b/src/tests/frontends/lean/implicit_args.cpp @@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "test.h" -#include "metavar.h" -#include "free_vars.h" -#include "printer.h" -#include "occurs.h" -#include "abstract.h" -#include "import_all.h" -#include "basic_thms.h" -#include "type_checker.h" -#include "kernel_exception.h" -#include "lean_frontend.h" -#include "lean_elaborator.h" -#include "lean_elaborator_exception.h" +#include "util/test.h" +#include "kernel/type_checker.h" +#include "kernel/kernel_exception.h" +#include "kernel/occurs.h" +#include "kernel/abstract.h" +#include "kernel/free_vars.h" +#include "library/metavar.h" +#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" 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 9de1648b70..8c91562327 100644 --- a/src/tests/frontends/lean/lean_frontend.cpp +++ b/src/tests/frontends/lean/lean_frontend.cpp @@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "test.h" -#include "environment.h" -#include "kernel_exception.h" -#include "builtin.h" -#include "printer.h" -#include "abstract.h" -#include "lean_frontend.h" -#include "lean_operator_info.h" -#include "lean_pp.h" +#include "util/test.h" +#include "kernel/environment.h" +#include "kernel/kernel_exception.h" +#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" 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 97eb9a921e..ff59b74464 100644 --- a/src/tests/frontends/lean/lean_parser.cpp +++ b/src/tests/frontends/lean/lean_parser.cpp @@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "builtin.h" -#include "lean_parser.h" -#include "lean_pp.h" -#include "printer.h" -#include "exception.h" -#include "test.h" +#include "util/test.h" +#include "util/exception.h" +#include "kernel/builtin.h" +#include "library/printer.h" +#include "frontends/lean/lean_parser.h" +#include "frontends/lean/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 12b0baf14d..f65c86d4ea 100644 --- a/src/tests/frontends/lean/lean_pp.cpp +++ b/src/tests/frontends/lean/lean_pp.cpp @@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "printer.h" -#include "abstract.h" -#include "builtin.h" -#include "lean_frontend.h" -#include "lean_pp.h" -#include "test.h" +#include "util/test.h" +#include "kernel/abstract.h" +#include "kernel/builtin.h" +#include "library/printer.h" +#include "frontends/lean/lean_frontend.h" +#include "frontends/lean/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 b5cd99a18d..65c2279544 100644 --- a/src/tests/frontends/lean/lean_scanner.cpp +++ b/src/tests/frontends/lean/lean_scanner.cpp @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "test.h" -#include "lean_scanner.h" -#include "exception.h" -#include "escaped.h" +#include "util/test.h" +#include "util/exception.h" +#include "util/escaped.h" +#include "frontends/lean/lean_scanner.h" using namespace lean; #define st scanner::token diff --git a/src/tests/interval/double_interval.cpp b/src/tests/interval/double_interval.cpp index c2c76cb7cd..243e28a442 100644 --- a/src/tests/interval/double_interval.cpp +++ b/src/tests/interval/double_interval.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ -#include "test.h" -#include "trace.h" -#include "double.h" -#include "interval_def.h" -#include "check.h" +#include "util/test.h" +#include "util/trace.h" +#include "util/numerics/double.h" +#include "interval/interval_def.h" +#include "tests/interval/check.h" using namespace lean; diff --git a/src/tests/interval/float_interval.cpp b/src/tests/interval/float_interval.cpp index 45705a7d1b..3729724b63 100644 --- a/src/tests/interval/float_interval.cpp +++ b/src/tests/interval/float_interval.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ -#include "test.h" -#include "trace.h" -#include "float.h" -#include "interval_def.h" -#include "check.h" +#include "util/test.h" +#include "util/trace.h" +#include "util/numerics/float.h" +#include "interval/interval_def.h" +#include "tests/interval/check.h" using namespace lean; diff --git a/src/tests/interval/interval.cpp b/src/tests/interval/interval.cpp index 24c67ab1ec..0c39fd904b 100644 --- a/src/tests/interval/interval.cpp +++ b/src/tests/interval/interval.cpp @@ -5,12 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "test.h" -#include "trace.h" -#include "double.h" -#include "mpq.h" -#include "mpfp.h" -#include "interval_def.h" +#include "util/test.h" +#include "util/trace.h" +#include "util/numerics/double.h" +#include "util/numerics/mpq.h" +#include "util/numerics/mpfp.h" +#include "interval/interval_def.h" using namespace lean; diff --git a/src/tests/interval/mpfp_interval.cpp b/src/tests/interval/mpfp_interval.cpp index e5a0192edb..39e0e82693 100644 --- a/src/tests/interval/mpfp_interval.cpp +++ b/src/tests/interval/mpfp_interval.cpp @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ -#include "test.h" -#include "trace.h" -#include "mpfp.h" -#include "interval_def.h" -#include "check.h" +#include "util/test.h" +#include "util/trace.h" +#include "util/numerics/mpfp.h" +#include "interval/interval_def.h" +#include "tests/interval/check.h" using namespace lean; diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp index ef22ec8292..12d150dcf3 100644 --- a/src/tests/kernel/arith.cpp +++ b/src/tests/kernel/arith.cpp @@ -5,15 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "environment.h" -#include "type_checker.h" -#include "builtin.h" -#include "arithlibs.h" -#include "normalizer.h" -#include "import_all.h" -#include "abstract.h" -#include "printer.h" -#include "test.h" +#include "util/test.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" +#include "kernel/builtin.h" +#include "kernel/normalizer.h" +#include "kernel/abstract.h" +#include "library/printer.h" +#include "library/arith/arithlibs.h" +#include "library/import_all/import_all.h" using namespace lean; static void tst1() { diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index bcebe5712c..d69319a26c 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -4,18 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel_exception.h" -#include "environment.h" -#include "type_checker.h" -#include "printer.h" -#include "import_all.h" -#include "builtin.h" -#include "arithlibs.h" -#include "normalizer.h" -#include "abstract.h" -#include "exception.h" -#include "trace.h" -#include "test.h" +#include "util/test.h" +#include "util/exception.h" +#include "util/trace.h" +#include "kernel/kernel_exception.h" +#include "kernel/environment.h" +#include "kernel/type_checker.h" +#include "kernel/builtin.h" +#include "kernel/normalizer.h" +#include "kernel/abstract.h" +#include "library/printer.h" +#include "library/arith/arithlibs.h" +#include "library/import_all/import_all.h" using namespace lean; static void tst1() { diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 4ce817f517..60ec2c0e2c 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -6,16 +6,16 @@ Author: Leonardo de Moura Soonho Kong */ #include -#include "expr.h" -#include "expr_sets.h" -#include "max_sharing.h" -#include "free_vars.h" -#include "test.h" -#include "abstract.h" -#include "instantiate.h" -#include "printer.h" -#include "deep_copy.h" -#include "arithlibs.h" +#include "util/test.h" +#include "kernel/expr.h" +#include "kernel/expr_sets.h" +#include "kernel/free_vars.h" +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "library/max_sharing.h" +#include "library/deep_copy.h" +#include "library/printer.h" +#include "library/arith/arithlibs.h" using namespace lean; void tst1() { diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp index 2208ca51f9..245243e7ab 100644 --- a/src/tests/kernel/free_vars.cpp +++ b/src/tests/kernel/free_vars.cpp @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "free_vars.h" -#include "abstract.h" -#include "test.h" +#include "util/test.h" +#include "kernel/free_vars.h" +#include "kernel/abstract.h" using namespace lean; static void tst1() { diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index 0e6525ce60..f1bc09a864 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "environment.h" -#include "exception.h" -#include "printer.h" -#include "test.h" +#include "util/test.h" +#include "util/exception.h" +#include "kernel/environment.h" +#include "library/printer.h" using namespace lean; static void tst0() { diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 9e219d52b0..6329f01277 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -7,16 +7,16 @@ Author: Leonardo de Moura #include #include #include -#include "exception.h" -#include "normalizer.h" -#include "builtin.h" -#include "trace.h" -#include "test.h" -#include "expr_sets.h" -#include "abstract.h" -#include "kernel_exception.h" -#include "import_all.h" -#include "printer.h" +#include "util/test.h" +#include "util/trace.h" +#include "util/exception.h" +#include "kernel/normalizer.h" +#include "kernel/builtin.h" +#include "kernel/expr_sets.h" +#include "kernel/abstract.h" +#include "kernel/kernel_exception.h" +#include "library/printer.h" +#include "library/import_all/import_all.h" using namespace lean; expr normalize(expr const & e) { diff --git a/src/tests/kernel/occurs.cpp b/src/tests/kernel/occurs.cpp index 14a443a3e1..9099d3e133 100644 --- a/src/tests/kernel/occurs.cpp +++ b/src/tests/kernel/occurs.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "test.h" -#include "occurs.h" -#include "abstract.h" -#include "printer.h" +#include "util/test.h" +#include "kernel/occurs.h" +#include "kernel/abstract.h" +#include "library/printer.h" using namespace lean; static void tst1() { diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index 6389c6d399..294d1bb378 100644 --- a/src/tests/kernel/replace.cpp +++ b/src/tests/kernel/replace.cpp @@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "expr.h" -#include "abstract.h" -#include "instantiate.h" -#include "deep_copy.h" -#include "expr_maps.h" -#include "replace.h" -#include "printer.h" -#include "name.h" -#include "test.h" +#include "util/test.h" +#include "util/name.h" +#include "kernel/expr.h" +#include "kernel/abstract.h" +#include "kernel/instantiate.h" +#include "kernel/expr_maps.h" +#include "kernel/replace.h" +#include "library/deep_copy.h" +#include "library/printer.h" using namespace lean; expr mk_big(expr f, unsigned depth, unsigned val) { diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 6133511144..d96a2c615a 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -7,15 +7,15 @@ Author: Leonardo de Moura #include #include #include -#include "expr.h" -#include "max_sharing.h" -#include "free_vars.h" -#include "deep_copy.h" -#include "abstract.h" -#include "normalizer.h" -#include "import_all.h" -#include "arithlibs.h" -#include "test.h" +#include "util/test.h" +#include "kernel/expr.h" +#include "kernel/free_vars.h" +#include "kernel/abstract.h" +#include "kernel/normalizer.h" +#include "library/max_sharing.h" +#include "library/deep_copy.h" +#include "library/import_all/import_all.h" +#include "library/arith/arithlibs.h" using namespace lean; expr norm(expr const & e, environment & env) { diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 96b3965329..59a64f7870 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -7,18 +7,18 @@ Author: Leonardo de Moura #include #include #include -#include "type_checker.h" -#include "environment.h" -#include "abstract.h" -#include "exception.h" -#include "import_all.h" -#include "basic_thms.h" -#include "builtin.h" -#include "arithlibs.h" -#include "normalizer.h" -#include "printer.h" -#include "trace.h" -#include "test.h" +#include "util/test.h" +#include "util/trace.h" +#include "util/exception.h" +#include "kernel/type_checker.h" +#include "kernel/environment.h" +#include "kernel/abstract.h" +#include "kernel/builtin.h" +#include "kernel/normalizer.h" +#include "library/printer.h" +#include "library/import_all/import_all.h" +#include "library/basic_thms.h" +#include "library/arith/arithlibs.h" using namespace lean; expr c(char const * n) { return mk_constant(n); } diff --git a/src/tests/library/light_checker.cpp b/src/tests/library/light_checker.cpp index 4331bd289d..392dab945f 100644 --- a/src/tests/library/light_checker.cpp +++ b/src/tests/library/light_checker.cpp @@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "test.h" -#include "light_checker.h" -#include "type_checker.h" -#include "environment.h" -#include "arithlibs.h" -#include "import_all.h" -#include "abstract.h" -#include "printer.h" -#include "timeit.h" +#include "util/test.h" +#include "util/timeit.h" +#include "kernel/type_checker.h" +#include "kernel/environment.h" +#include "kernel/abstract.h" +#include "library/arith/arithlibs.h" +#include "library/import_all/import_all.h" +#include "library/light_checker.h" +#include "library/printer.h" using namespace lean; static void tst1() { diff --git a/src/tests/library/metavar.cpp b/src/tests/library/metavar.cpp index 4480429b2b..4e6198d379 100644 --- a/src/tests/library/metavar.cpp +++ b/src/tests/library/metavar.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "test.h" -#include "metavar.h" -#include "abstract.h" -#include "printer.h" +#include "util/test.h" +#include "kernel/abstract.h" +#include "library/metavar.h" +#include "library/printer.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/buffer.cpp b/src/tests/util/buffer.cpp index f7e7172c85..c7075b3e26 100644 --- a/src/tests/util/buffer.cpp +++ b/src/tests/util/buffer.cpp @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "buffer.h" -#include "test.h" +#include "util/buffer.h" +#include "util/test.h" using namespace lean; template diff --git a/src/tests/util/format.cpp b/src/tests/util/format.cpp index 02fc71c9ba..53f51373a8 100644 --- a/src/tests/util/format.cpp +++ b/src/tests/util/format.cpp @@ -7,11 +7,11 @@ Author: Soonho Kong #include #include #include -#include "format.h" -#include "test.h" -#include "sexpr_fn.h" -#include "options.h" -#include "mpq.h" +#include "util/test.h" +#include "util/numerics/mpq.h" +#include "util/sexpr/format.h" +#include "util/sexpr/sexpr_fn.h" +#include "util/sexpr/options.h" using namespace lean; using std::cout; diff --git a/src/tests/util/list.cpp b/src/tests/util/list.cpp index e7eaa2fb54..f5443d9801 100644 --- a/src/tests/util/list.cpp +++ b/src/tests/util/list.cpp @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "list.h" -#include "list_fn.h" -#include "test.h" +#include "util/list.h" +#include "util/list_fn.h" +#include "util/test.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/name.cpp b/src/tests/util/name.cpp index 4192655e58..272ee4f2bf 100644 --- a/src/tests/util/name.cpp +++ b/src/tests/util/name.cpp @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #include #include -#include "test.h" -#include "name.h" +#include "util/test.h" +#include "util/name.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/numerics/mpbq.cpp b/src/tests/util/numerics/mpbq.cpp index 6840d660e7..6b5c9ad986 100644 --- a/src/tests/util/numerics/mpbq.cpp +++ b/src/tests/util/numerics/mpbq.cpp @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #include #include -#include "test.h" -#include "mpbq.h" -#include "mpq.h" +#include "util/test.h" +#include "util/numerics/mpbq.h" +#include "util/numerics/mpq.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/numerics/mpfp.cpp b/src/tests/util/numerics/mpfp.cpp index dcd8b5f000..000e454766 100644 --- a/src/tests/util/numerics/mpfp.cpp +++ b/src/tests/util/numerics/mpfp.cpp @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ #include -#include "test.h" -#include "mpfp.h" +#include "util/test.h" +#include "util/numerics/mpfp.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/numerics/mpq.cpp b/src/tests/util/numerics/mpq.cpp index 85b5af69d8..6099cd8a8c 100644 --- a/src/tests/util/numerics/mpq.cpp +++ b/src/tests/util/numerics/mpq.cpp @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #include #include -#include "test.h" -#include "mpq.h" +#include "util/test.h" +#include "util/numerics/mpq.h" using namespace lean; static void tst0() { diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp index c0bef23aaa..3690759ed2 100644 --- a/src/tests/util/options.cpp +++ b/src/tests/util/options.cpp @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #include #include -#include "test.h" -#include "options.h" -#include "option_declarations.h" +#include "util/test.h" +#include "util/sexpr/options.h" +#include "util/sexpr/option_declarations.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/pdeque.cpp b/src/tests/util/pdeque.cpp index 5bca60c28d..406b8d3897 100644 --- a/src/tests/util/pdeque.cpp +++ b/src/tests/util/pdeque.cpp @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include #include #include -#include "test.h" -#include "pdeque.h" +#include "util/test.h" +#include "util/pdeque.h" using namespace lean; // #define PDEQUE_PERF_TEST diff --git a/src/tests/util/pvector.cpp b/src/tests/util/pvector.cpp index 5735b877d8..020763dcf8 100644 --- a/src/tests/util/pvector.cpp +++ b/src/tests/util/pvector.cpp @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #include #include -#include "test.h" -#include "pvector.h" -#include "timeit.h" +#include "util/test.h" +#include "util/pvector.h" +#include "util/timeit.h" using namespace lean; // #define PVECTOR_PERF_TEST diff --git a/src/tests/util/scoped_map.cpp b/src/tests/util/scoped_map.cpp index 78a8d6434a..306b11f8ff 100644 --- a/src/tests/util/scoped_map.cpp +++ b/src/tests/util/scoped_map.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "scoped_map.h" -#include "test.h" +#include "util/scoped_map.h" +#include "util/test.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/scoped_set.cpp b/src/tests/util/scoped_set.cpp index ee70dd19b2..9e2cf06a68 100644 --- a/src/tests/util/scoped_set.cpp +++ b/src/tests/util/scoped_set.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "scoped_set.h" -#include "test.h" +#include "util/scoped_set.h" +#include "util/test.h" using namespace lean; static void tst1() { diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp index aa54cdfcf6..05b7bfe4ba 100644 --- a/src/tests/util/sexpr.cpp +++ b/src/tests/util/sexpr.cpp @@ -5,13 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "sexpr.h" -#include "sexpr_fn.h" -#include "mpq.h" -#include "name.h" -#include "test.h" -#include "format.h" -#include "options.h" +#include "util/name.h" +#include "util/test.h" +#include "util/numerics/mpq.h" +#include "util/sexpr/sexpr.h" +#include "util/sexpr/sexpr_fn.h" +#include "util/sexpr/format.h" +#include "util/sexpr/options.h" using namespace lean; static void tst1() { diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp index 40480fe7a8..aaabd97bbe 100644 --- a/src/util/numerics/double.cpp +++ b/src/util/numerics/double.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ -#include "numeric_traits.h" -#include "double.h" +#include "util/numerics/numeric_traits.h" +#include "util/numerics/double.h" #include namespace lean { diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h index 7af3833832..34305f472a 100644 --- a/src/util/numerics/double.h +++ b/src/util/numerics/double.h @@ -6,7 +6,7 @@ Author: Soonho Kong */ #pragma once #include -#include "mpfp.h" +#include "util/numerics/mpfp.h" namespace lean { diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp index 55d2f9263d..2a273722cb 100644 --- a/src/util/numerics/float.cpp +++ b/src/util/numerics/float.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ -#include "numeric_traits.h" -#include "float.h" +#include "util/numerics/numeric_traits.h" +#include "util/numerics/float.h" #include namespace lean { diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h index e37777c2a0..c33b8f27b8 100644 --- a/src/util/numerics/float.h +++ b/src/util/numerics/float.h @@ -6,7 +6,7 @@ Author: Soonho Kong */ #pragma once #include -#include "mpfp.h" +#include "util/numerics/mpfp.h" namespace lean { diff --git a/src/util/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp index fcb8d4eee3..9b6456acf7 100644 --- a/src/util/numerics/mpbq.cpp +++ b/src/util/numerics/mpbq.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "mpbq.h" +#include "util/numerics/mpbq.h" namespace lean { diff --git a/src/util/numerics/mpbq.h b/src/util/numerics/mpbq.h index e4b1e0b7b8..70926662e2 100644 --- a/src/util/numerics/mpbq.h +++ b/src/util/numerics/mpbq.h @@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "mpz.h" -#include "mpq.h" -#include "bit_tricks.h" +#include "util/bit_tricks.h" +#include "util/numerics/mpz.h" +#include "util/numerics/mpq.h" namespace lean { diff --git a/src/util/numerics/mpfp.cpp b/src/util/numerics/mpfp.cpp index 3994cfe658..076d880d37 100644 --- a/src/util/numerics/mpfp.cpp +++ b/src/util/numerics/mpfp.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ #include -#include "mpfp.h" +#include "util/numerics/mpfp.h" namespace lean { static thread_local mpfr_rnd_t g_mpfp_rnd = MPFR_RNDN; diff --git a/src/util/numerics/mpfp.h b/src/util/numerics/mpfp.h index d44920b9e3..e3b2a78d77 100644 --- a/src/util/numerics/mpfp.h +++ b/src/util/numerics/mpfp.h @@ -7,9 +7,9 @@ Author: Soonho Kong #pragma once #include #include -#include "mpz.h" -#include "mpq.h" -#include "mpbq.h" +#include "util/numerics/mpz.h" +#include "util/numerics/mpq.h" +#include "util/numerics/mpbq.h" namespace lean { diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index 0f7c69d032..d03fb5546d 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "mpq.h" -#include "mpbq.h" +#include "util/numerics/mpq.h" +#include "util/numerics/mpbq.h" namespace lean { diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h index ecd30ec2f8..7b5284ac94 100644 --- a/src/util/numerics/mpq.h +++ b/src/util/numerics/mpq.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "mpz.h" +#include "util/numerics/mpz.h" namespace lean { class mpbq; diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h index 49d90c34c8..eecb7bb066 100644 --- a/src/util/numerics/mpz.h +++ b/src/util/numerics/mpz.h @@ -7,8 +7,8 @@ Author: Leonardo de Moura #pragma once #include #include -#include "debug.h" -#include "numeric_traits.h" +#include "util/debug.h" +#include "util/numerics/numeric_traits.h" namespace lean { class mpq; diff --git a/src/util/numerics/xnumeral.h b/src/util/numerics/xnumeral.h index fed5abb921..e563146fb1 100644 --- a/src/util/numerics/xnumeral.h +++ b/src/util/numerics/xnumeral.h @@ -7,8 +7,8 @@ Author: Leonardo de Moura #pragma once #include -#include "numeric_traits.h" -#include "debug.h" +#include "util/debug.h" +#include "util/numerics/numeric_traits.h" namespace lean { diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp index 057c3ad51f..b5f3227818 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/sexpr/format.cpp @@ -5,11 +5,11 @@ Author: Soonho Kong */ #include -#include "sexpr.h" -#include "format.h" -#include "escaped.h" -#include "sexpr_fn.h" -#include "options.h" +#include "util/escaped.h" +#include "util/sexpr/sexpr.h" +#include "util/sexpr/format.h" +#include "util/sexpr/sexpr_fn.h" +#include "util/sexpr/options.h" #ifndef LEAN_DEFAULT_PP_INDENTATION #define LEAN_DEFAULT_PP_INDENTATION 4 diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index d96b23210d..84c992d23d 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -5,14 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Soonho Kong */ #pragma once -#include "sexpr.h" -#include "debug.h" #include #include #include #include -#include "mpz.h" -#include "pair.h" +#include "util/pair.h" +#include "util/debug.h" +#include "util/numerics/mpz.h" +#include "util/sexpr/sexpr.h" namespace lean { class options; diff --git a/src/util/sexpr/options.h b/src/util/sexpr/options.h index d8a5832620..f7f47e6a12 100644 --- a/src/util/sexpr/options.h +++ b/src/util/sexpr/options.h @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #pragma once #include -#include "sexpr.h" -#include "format.h" -#include "name.h" +#include "util/name.h" +#include "util/sexpr/sexpr.h" +#include "util/sexpr/format.h" namespace lean { enum option_kind { BoolOption, IntOption, UnsignedOption, DoubleOption, StringOption, SExprOption }; diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp index da31b91081..5ea1923125 100644 --- a/src/util/sexpr/sexpr.cpp +++ b/src/util/sexpr/sexpr.cpp @@ -5,13 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "rc.h" -#include "hash.h" -#include "sexpr.h" -#include "name.h" -#include "mpz.h" -#include "mpq.h" -#include "escaped.h" +#include "util/rc.h" +#include "util/hash.h" +#include "util/name.h" +#include "util/escaped.h" +#include "util/numerics/mpz.h" +#include "util/numerics/mpq.h" +#include "util/sexpr/sexpr.h" namespace lean { /** \brief Base class used to represent S-expression cells. */ diff --git a/src/util/sexpr/sexpr_fn.h b/src/util/sexpr/sexpr_fn.h index 6f93269957..15e6de8bf0 100644 --- a/src/util/sexpr/sexpr_fn.h +++ b/src/util/sexpr/sexpr_fn.h @@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "sexpr.h" -#include "debug.h" +#include "util/sexpr/sexpr.h" +#include "util/debug.h" namespace lean {