From d547698a56ef91d2102b5eedbfee5bbb225c7f03 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Jun 2015 16:30:40 -0700 Subject: [PATCH] refactor(library,library/tactic): move class_instance_synth to library This module will be needed by the simplifier --- src/frontends/lean/elaborator.cpp | 2 +- src/library/CMakeLists.txt | 7 ++++--- src/library/{tactic => }/class_instance_synth.cpp | 3 +-- src/library/{tactic => }/class_instance_synth.h | 0 src/library/init_module.cpp | 3 +++ src/library/tactic/CMakeLists.txt | 14 +++++++------- src/library/tactic/apply_tactic.cpp | 2 +- src/library/tactic/induction_tactic.cpp | 2 +- src/library/tactic/init_module.cpp | 3 --- src/library/tactic/inversion_tactic.cpp | 2 +- src/library/tactic/rewrite_tactic.cpp | 2 +- 11 files changed, 20 insertions(+), 20 deletions(-) rename src/library/{tactic => }/class_instance_synth.cpp (99%) rename src/library/{tactic => }/class_instance_synth.h (100%) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 8b63d0af9..363565c0b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -38,8 +38,8 @@ Author: Leonardo de Moura #include "library/choice_iterator.h" #include "library/projection.h" #include "library/pp_options.h" +#include "library/class_instance_synth.h" #include "library/tactic/expr_to_tactic.h" -#include "library/tactic/class_instance_synth.h" #include "library/error_handling/error_handling.h" #include "library/definitional/equations.h" #include "frontends/lean/local_decls.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index efc6311f1..bb6347d17 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -11,8 +11,9 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp - local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp - app_builder.cpp projection.cpp abbreviation.cpp - relation_manager.cpp export.cpp user_recursors.cpp) + local_context.cpp choice_iterator.cpp pp_options.cpp + unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp + relation_manager.cpp export.cpp user_recursors.cpp + class_instance_synth.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/class_instance_synth.cpp similarity index 99% rename from src/library/tactic/class_instance_synth.cpp rename to src/library/class_instance_synth.cpp index 209330af7..a53c3c512 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/class_instance_synth.cpp @@ -22,8 +22,7 @@ Author: Leonardo de Moura #include "library/generic_exception.h" #include "library/util.h" #include "library/constants.h" -#include "library/tactic/util.h" -#include "library/tactic/class_instance_synth.h" +#include "library/class_instance_synth.h" #ifndef LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES #define LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES false diff --git a/src/library/tactic/class_instance_synth.h b/src/library/class_instance_synth.h similarity index 100% rename from src/library/tactic/class_instance_synth.h rename to src/library/class_instance_synth.h diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index ee91c0fb4..dc0ac2cb4 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -38,6 +38,7 @@ Author: Leonardo de Moura #include "library/abbreviation.h" #include "library/relation_manager.h" #include "library/user_recursors.h" +#include "library/class_instance_synth.h" namespace lean { void initialize_library_module() { @@ -75,9 +76,11 @@ void initialize_library_module() { initialize_abbreviation(); initialize_relation_manager(); initialize_user_recursors(); + initialize_class_instance_elaborator(); } void finalize_library_module() { + finalize_class_instance_elaborator(); finalize_user_recursors(); finalize_relation_manager(); finalize_abbreviation(); diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 019033227..4dcf672c0 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,11 +1,11 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp -exact_tactic.cpp generalize_tactic.cpp -inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp -assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp -rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp -change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp -exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp -congruence_tactic.cpp relation_tactics.cpp induction_tactic.cpp subst_tactic.cpp) +exact_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp +whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp +expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp +init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp +contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp +injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp +induction_tactic.cpp subst_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index d9a57e1e8..8b986ba89 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -23,9 +23,9 @@ Author: Leonardo de Moura #include "library/metavar_closure.h" #include "library/type_util.h" #include "library/local_context.h" +#include "library/class_instance_synth.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/apply_tactic.h" -#include "library/tactic/class_instance_synth.h" #ifndef LEAN_DEFAULT_APPLY_CLASS_INSTANCE #define LEAN_DEFAULT_APPLY_CLASS_INSTANCE true diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 57fa2f22e..68219401d 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -12,10 +12,10 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/reducible.h" #include "library/locals.h" +#include "library/class_instance_synth.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" #include "library/tactic/generalize_tactic.h" -#include "library/tactic/class_instance_synth.h" namespace lean { class rec_opaque_converter : public default_converter { diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 58c1a6343..95b9fcffd 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -18,7 +18,6 @@ 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/class_instance_synth.h" #include "library/tactic/rewrite_tactic.h" #include "library/tactic/change_tactic.h" #include "library/tactic/check_expr_tactic.h" @@ -47,7 +46,6 @@ void initialize_tactic_module() { initialize_revert_tactic(); initialize_inversion_tactic(); initialize_assert_tactic(); - initialize_class_instance_elaborator(); initialize_rewrite_tactic(); initialize_change_tactic(); initialize_check_expr_tactic(); @@ -75,7 +73,6 @@ void finalize_tactic_module() { finalize_check_expr_tactic(); finalize_change_tactic(); finalize_rewrite_tactic(); - finalize_class_instance_elaborator(); finalize_assert_tactic(); finalize_inversion_tactic(); finalize_revert_tactic(); diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 0fdb2db12..a0ad8cbb5 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -15,9 +15,9 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/constants.h" #include "library/reducible.h" +#include "library/class_instance_synth.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" -#include "library/tactic/class_instance_synth.h" #include "library/tactic/inversion_tactic.h" #include "library/tactic/generalize_tactic.h" #include "library/tactic/clear_tactic.h" diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp index 63b2b2d3f..c2076b0ea 100644 --- a/src/library/tactic/rewrite_tactic.cpp +++ b/src/library/tactic/rewrite_tactic.cpp @@ -31,11 +31,11 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/unfold_macros.h" #include "library/generic_exception.h" +#include "library/class_instance_synth.h" #include "library/tactic/clear_tactic.h" #include "library/tactic/trace_tactic.h" #include "library/tactic/rewrite_tactic.h" #include "library/tactic/expr_to_tactic.h" -#include "library/tactic/class_instance_synth.h" #include "library/tactic/relation_tactics.h" // #define TRACE_MATCH_PLUGIN