From ded869b7e0deb7811061e4dfff9bfbf42f4aae49 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Dec 2014 15:23:22 -0800 Subject: [PATCH] refactor(frontends/lean): move placeholder_elaborator to library/tactic --- src/frontends/lean/CMakeLists.txt | 6 ++---- src/frontends/lean/elaborator.cpp | 2 +- src/frontends/lean/init_module.cpp | 3 --- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/init_module.cpp | 3 +++ .../lean => library/tactic}/placeholder_elaborator.cpp | 3 ++- .../lean => library/tactic}/placeholder_elaborator.h | 1 + 7 files changed, 10 insertions(+), 10 deletions(-) rename src/{frontends/lean => library/tactic}/placeholder_elaborator.cpp (99%) rename src/{frontends/lean => library/tactic}/placeholder_elaborator.h (98%) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 8d823dd718..af0a33b0d4 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -3,12 +3,10 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp 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 tactic_hint.cpp pp.cpp -theorem_queue.cpp structure_cmd.cpp info_manager.cpp -info_annotation.cpp find_cmd.cpp placeholder_elaborator.cpp +begin_end_ext.cpp class.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp +structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.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) - target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4aae8ec837..314d133f1e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -36,6 +36,7 @@ Author: Leonardo de Moura #include "library/choice_iterator.h" #include "library/pp_options.h" #include "library/tactic/expr_to_tactic.h" +#include "library/tactic/placeholder_elaborator.h" #include "library/error_handling/error_handling.h" #include "library/definitional/equations.h" #include "frontends/lean/local_decls.h" @@ -44,7 +45,6 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" #include "frontends/lean/info_annotation.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" #include "frontends/lean/info_tactic.h" diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index bb59d8d4af..f69d3a6ab8 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "frontends/lean/parse_table.h" #include "frontends/lean/token_table.h" #include "frontends/lean/info_tactic.h" -#include "frontends/lean/placeholder_elaborator.h" #include "frontends/lean/calc_proof_elaborator.h" #include "frontends/lean/find_cmd.h" #include "frontends/lean/scanner.h" @@ -49,7 +48,6 @@ void initialize_frontend_lean_module() { initialize_info_manager(); initialize_info_tactic(); initialize_pp(); - initialize_placeholder_elaborator(); initialize_calc_proof_elaborator(); initialize_server(); initialize_find_cmd(); @@ -58,7 +56,6 @@ void finalize_frontend_lean_module() { finalize_find_cmd(); finalize_server(); finalize_calc_proof_elaborator(); - finalize_placeholder_elaborator(); finalize_pp(); finalize_info_tactic(); finalize_info_manager(); diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index f9b1050125..06756c71b7 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -3,6 +3,6 @@ apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp util.cpp -init_module.cpp) +placeholder_elaborator.cpp init_module.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 28647359a5..9e21b3ebba 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "library/tactic/revert_tactic.h" #include "library/tactic/inversion_tactic.h" #include "library/tactic/assert_tactic.h" +#include "library/tactic/placeholder_elaborator.h" namespace lean { void initialize_tactic_module() { @@ -37,9 +38,11 @@ void initialize_tactic_module() { initialize_revert_tactic(); initialize_inversion_tactic(); initialize_assert_tactic(); + initialize_placeholder_elaborator(); } void finalize_tactic_module() { + finalize_placeholder_elaborator(); finalize_assert_tactic(); finalize_inversion_tactic(); finalize_revert_tactic(); diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/library/tactic/placeholder_elaborator.cpp similarity index 99% rename from src/frontends/lean/placeholder_elaborator.cpp rename to src/library/tactic/placeholder_elaborator.cpp index 8d518f2194..5729133fdf 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/library/tactic/placeholder_elaborator.cpp @@ -20,7 +20,8 @@ Author: Leonardo de Moura #include "library/choice_iterator.h" #include "library/pp_options.h" #include "library/generic_exception.h" -#include "frontends/lean/util.h" +#include "library/util.h" +#include "library/tactic/util.h" #ifndef LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES #define LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES false diff --git a/src/frontends/lean/placeholder_elaborator.h b/src/library/tactic/placeholder_elaborator.h similarity index 98% rename from src/frontends/lean/placeholder_elaborator.h rename to src/library/tactic/placeholder_elaborator.h index 3178bbd3e4..9de3ffbdda 100644 --- a/src/frontends/lean/placeholder_elaborator.h +++ b/src/library/tactic/placeholder_elaborator.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include "kernel/expr.h" #include "library/io_state.h" +#include "library/unifier.h" #include "library/local_context.h" namespace lean {