From 756fae7c2a501adbf4d4ebef5bd1f768dd512824 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Dec 2014 12:43:32 -0800 Subject: [PATCH] refactor(frontends/lean): move local_context to library --- src/frontends/lean/CMakeLists.txt | 4 ++-- src/frontends/lean/calc_proof_elaborator.cpp | 2 +- src/frontends/lean/calc_proof_elaborator.h | 2 +- src/frontends/lean/elaborator.cpp | 4 ++-- src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/placeholder_elaborator.cpp | 2 +- src/frontends/lean/placeholder_elaborator.h | 2 +- src/library/CMakeLists.txt | 2 +- src/{frontends/lean => library}/local_context.cpp | 2 +- src/{frontends/lean => library}/local_context.h | 0 10 files changed, 11 insertions(+), 11 deletions(-) rename src/{frontends/lean => library}/local_context.cpp (98%) rename src/{frontends/lean => library}/local_context.h (100%) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index aee1afffa..aace07a93 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -4,8 +4,8 @@ parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp -theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp -local_context.cpp choice_iterator.cpp find_cmd.cpp +theorem_queue.cpp structure_cmd.cpp info_manager.cpp +info_annotation.cpp choice_iterator.cpp find_cmd.cpp placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp type_util.cpp elaborator_exception.cpp) diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index e5852e092..7d0b93c74 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/src/frontends/lean/calc_proof_elaborator.cpp @@ -10,8 +10,8 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/reducible.h" #include "library/metavar_closure.h" +#include "library/local_context.h" #include "frontends/lean/util.h" -#include "frontends/lean/local_context.h" #include "frontends/lean/info_manager.h" #include "frontends/lean/calc.h" #include "frontends/lean/calc_proof_elaborator.h" diff --git a/src/frontends/lean/calc_proof_elaborator.h b/src/frontends/lean/calc_proof_elaborator.h index 0e5d35570..cc3a5dfb8 100644 --- a/src/frontends/lean/calc_proof_elaborator.h +++ b/src/frontends/lean/calc_proof_elaborator.h @@ -7,8 +7,8 @@ Author: Leonardo de Moura #pragma once #include #include "library/unifier.h" +#include "library/local_context.h" #include "frontends/lean/info_manager.h" -#include "frontends/lean/local_context.h" namespace lean { typedef std::function update_type_info_fn; diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index ac1d702db..1cd707db8 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -30,16 +30,16 @@ Author: Leonardo de Moura #include "library/deep_copy.h" #include "library/metavar_closure.h" #include "library/typed_expr.h" +#include "library/local_context.h" #include "library/tactic/expr_to_tactic.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/local_decls.h" #include "frontends/lean/class.h" #include "frontends/lean/tactic_hint.h" #include "frontends/lean/info_manager.h" -#include "frontends/lean/elaborator.h" #include "frontends/lean/info_annotation.h" -#include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" +#include "frontends/lean/elaborator.h" #include "frontends/lean/placeholder_elaborator.h" #include "frontends/lean/proof_qed_elaborator.h" #include "frontends/lean/calc_proof_elaborator.h" diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 4cf472414..3196022c3 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -13,10 +13,10 @@ Author: Leonardo de Moura #include "library/expr_lt.h" #include "library/unifier.h" #include "library/tactic/tactic.h" +#include "library/local_context.h" #include "frontends/lean/elaborator_context.h" #include "frontends/lean/coercion_elaborator.h" #include "frontends/lean/util.h" -#include "frontends/lean/local_context.h" #include "frontends/lean/calc_proof_elaborator.h" namespace lean { diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index ff964e819..56b39f639 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -16,8 +16,8 @@ Author: Leonardo de Moura #include "library/metavar_closure.h" #include "library/error_handling/error_handling.h" #include "library/class.h" +#include "library/local_context.h" #include "frontends/lean/util.h" -#include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" #include "frontends/lean/elaborator_exception.h" #include "frontends/lean/pp_options.h" diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/frontends/lean/placeholder_elaborator.h index 184d85140..3178bbd3e 100644 --- a/src/frontends/lean/placeholder_elaborator.h +++ b/src/frontends/lean/placeholder_elaborator.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include "kernel/expr.h" #include "library/io_state.h" -#include "frontends/lean/local_context.h" +#include "library/local_context.h" namespace lean { /** \brief Create a metavariable, and attach choice constraint for generating diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 40a67c178..a64f44280 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -10,6 +10,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp definition_cache.cpp declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp - fingerprint.cpp flycheck.cpp hott_kernel.cpp) + fingerprint.cpp flycheck.cpp hott_kernel.cpp local_context.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/frontends/lean/local_context.cpp b/src/library/local_context.cpp similarity index 98% rename from src/frontends/lean/local_context.cpp rename to src/library/local_context.cpp index f16f404b0..0231fef94 100644 --- a/src/frontends/lean/local_context.cpp +++ b/src/library/local_context.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/metavar.h" -#include "frontends/lean/local_context.h" +#include "library/local_context.h" namespace lean { /** \brief Given a list of local constants \c locals diff --git a/src/frontends/lean/local_context.h b/src/library/local_context.h similarity index 100% rename from src/frontends/lean/local_context.h rename to src/library/local_context.h