From d4ac482d76dfc42e49fbb7fa649f198fdc82d3da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Aug 2014 10:38:10 -0700 Subject: [PATCH] refactor(kernel): move annotation to library Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/noinfo.h | 2 +- src/frontends/lean/pp.cpp | 2 +- src/kernel/CMakeLists.txt | 2 +- src/library/CMakeLists.txt | 2 +- src/{kernel => library}/annotation.cpp | 2 +- src/{kernel => library}/annotation.h | 0 src/library/explicit.cpp | 2 +- src/library/kernel_serializer.cpp | 2 +- src/library/print.cpp | 2 +- src/library/tactic/expr_to_tactic.cpp | 2 +- 11 files changed, 10 insertions(+), 10 deletions(-) rename src/{kernel => library}/annotation.cpp (99%) rename src/{kernel => library}/annotation.h (100%) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 4a8eed6578..f7a0c80eac 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "util/sstream.h" #include "kernel/abstract.h" -#include "kernel/annotation.h" +#include "library/annotation.h" #include "library/placeholder.h" #include "library/explicit.h" #include "library/tactic/tactic.h" diff --git a/src/frontends/lean/noinfo.h b/src/frontends/lean/noinfo.h index 82430b9af5..1c13a008bc 100644 --- a/src/frontends/lean/noinfo.h +++ b/src/frontends/lean/noinfo.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/annotation.h" +#include "library/annotation.h" namespace lean { /** \brief Annotate \c e with no-information generation. diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 2cd2dadc49..9ed7740f38 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "util/flet.h" #include "kernel/replace_fn.h" #include "kernel/free_vars.h" -#include "kernel/annotation.h" +#include "library/annotation.h" #include "library/aliases.h" #include "library/scoped_ext.h" #include "library/coercion.h" diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index ac82da438c..38471249a2 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -3,6 +3,6 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp formatter.cpp declaration.cpp replace_visitor.cpp environment.cpp justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp -annotation.cpp normalizer_extension.cpp) +normalizer_extension.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index fe81461a83..cc698e9256 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -8,6 +8,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp match.cpp definition_cache.cpp declaration_index.cpp - print.cpp) + print.cpp annotation.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/kernel/annotation.cpp b/src/library/annotation.cpp similarity index 99% rename from src/kernel/annotation.cpp rename to src/library/annotation.cpp index 54eb9fe0d0..587e5ee406 100644 --- a/src/kernel/annotation.cpp +++ b/src/library/annotation.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/sstream.h" -#include "kernel/annotation.h" +#include "library/annotation.h" namespace lean { name const & get_annotation_name() { diff --git a/src/kernel/annotation.h b/src/library/annotation.h similarity index 100% rename from src/kernel/annotation.h rename to src/library/annotation.h diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 039c26dbd8..f285521bc5 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sstream.h" -#include "kernel/annotation.h" +#include "library/annotation.h" #include "library/explicit.h" #include "library/kernel_bindings.h" diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index d573ca95d0..8fdadd01c7 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/object_serializer.h" #include "kernel/expr.h" #include "kernel/declaration.h" -#include "kernel/annotation.h" +#include "library/annotation.h" #include "library/max_sharing.h" #include "library/kernel_serializer.h" diff --git a/src/library/print.cpp b/src/library/print.cpp index 41f209bf24..e30f861b35 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/instantiate.h" #include "kernel/free_vars.h" -#include "kernel/annotation.h" +#include "library/annotation.h" #include "library/print.h" namespace lean { diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 3240a4ff89..2725e412a1 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "util/sstream.h" #include "kernel/instantiate.h" #include "kernel/type_checker.h" -#include "kernel/annotation.h" +#include "library/annotation.h" #include "library/string.h" #include "library/num.h" #include "library/tactic/expr_to_tactic.h"