diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 3e0ead475f..16a4c71060 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -373,8 +373,6 @@ add_subdirectory(library) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/tactic) set(LEAN_OBJS ${LEAN_OBJS} $) -add_subdirectory(library/tactic/simplifier) -set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/tactic/backward) set(LEAN_OBJS ${LEAN_OBJS} $) add_subdirectory(library/constructions) diff --git a/src/library/inductive_compiler/nested.cpp b/src/library/inductive_compiler/nested.cpp index 37a226bb02..6fc1fd9d5e 100644 --- a/src/library/inductive_compiler/nested.cpp +++ b/src/library/inductive_compiler/nested.cpp @@ -38,7 +38,7 @@ Author: Daniel Selsam #include "library/inductive_compiler/util.h" #include "library/tactic/induction_tactic.h" #include "library/tactic/simp_result.h" -#include "library/tactic/simplifier/simplifier.h" +#include "library/tactic/simplify.h" /** Notes: diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index d3c67121f2..a1bed88db5 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -7,4 +7,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp generalize_tactic.cpp rewrite_tactic.cpp unfold_tactic.cpp hsubstitution.cpp gexpr.cpp elaborate.cpp init_module.cpp simp_result.cpp user_attribute.cpp eval.cpp - simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp) + simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 363ac8baa7..c86bf72a26 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -31,7 +31,7 @@ Author: Leonardo de Moura #include "library/tactic/simp_lemmas.h" #include "library/tactic/eqn_lemmas.h" #include "library/tactic/dsimplify.h" -#include "library/tactic/simplifier/init_module.h" +#include "library/tactic/simplify.h" #include "library/tactic/backward/init_module.h" namespace lean { @@ -57,7 +57,7 @@ void initialize_tactic_module() { initialize_generalize_tactic(); initialize_rewrite_tactic(); initialize_unfold_tactic(); - initialize_simplifier_module(); + initialize_simplify(); initialize_backward_module(); initialize_elaborate(); initialize_user_attribute(); @@ -74,7 +74,7 @@ void finalize_tactic_module() { finalize_user_attribute(); finalize_elaborate(); finalize_backward_module(); - finalize_simplifier_module(); + finalize_simplify(); finalize_unfold_tactic(); finalize_rewrite_tactic(); finalize_generalize_tactic(); diff --git a/src/library/tactic/simplifier/CMakeLists.txt b/src/library/tactic/simplifier/CMakeLists.txt deleted file mode 100644 index 00f17f3e61..0000000000 --- a/src/library/tactic/simplifier/CMakeLists.txt +++ /dev/null @@ -1 +0,0 @@ -add_library(simplifier OBJECT init_module.cpp simplifier.cpp) diff --git a/src/library/tactic/simplifier/init_module.cpp b/src/library/tactic/simplifier/init_module.cpp deleted file mode 100644 index 06ab3b1b71..0000000000 --- a/src/library/tactic/simplifier/init_module.cpp +++ /dev/null @@ -1,20 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#include "library/trace.h" -#include "library/tactic/simplifier/simplifier.h" - -namespace lean { - -void initialize_simplifier_module() { - register_trace_class("simplifier"); - - initialize_simplifier(); -} - -void finalize_simplifier_module() { - finalize_simplifier(); -} -} diff --git a/src/library/tactic/simplifier/init_module.h b/src/library/tactic/simplifier/init_module.h deleted file mode 100644 index fcdafb04ad..0000000000 --- a/src/library/tactic/simplifier/init_module.h +++ /dev/null @@ -1,11 +0,0 @@ -/* -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam -*/ -#pragma once - -namespace lean { -void initialize_simplifier_module(); -void finalize_simplifier_module(); -} diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplify.cpp similarity index 99% rename from src/library/tactic/simplifier/simplifier.cpp rename to src/library/tactic/simplify.cpp index cbfdae5cc8..04aabee06e 100644 --- a/src/library/tactic/simplifier/simplifier.cpp +++ b/src/library/tactic/simplify.cpp @@ -36,7 +36,7 @@ Author: Daniel Selsam #include "library/tactic/ac_tactics.h" #include "library/tactic/app_builder_tactics.h" #include "library/tactic/simp_lemmas.h" -#include "library/tactic/simplifier/simplifier.h" +#include "library/tactic/simplify.h" #ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS #define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 10000 @@ -1055,7 +1055,8 @@ vm_obj simp_lemmas_simplify_core(vm_obj const & lemmas, vm_obj const & prove_fn, } /* Setup and teardown */ -void initialize_simplifier() { +void initialize_simplify() { + register_trace_class("simplifier"); register_trace_class(name({"simplifier", "congruence"})); register_trace_class(name({"simplifier", "failure"})); register_trace_class(name({"simplifier", "failed"})); @@ -1097,7 +1098,7 @@ void initialize_simplifier() { DECLARE_VM_BUILTIN(name({"simp_lemmas", "simplify_core"}), simp_lemmas_simplify_core); } -void finalize_simplifier() { +void finalize_simplify() { delete g_simplify_canonize_subsingletons; delete g_simplify_canonize_instances_fixed_point; delete g_simplify_canonize_proofs_fixed_point; diff --git a/src/library/tactic/simplifier/simplifier.h b/src/library/tactic/simplify.h similarity index 95% rename from src/library/tactic/simplifier/simplifier.h rename to src/library/tactic/simplify.h index 21e5583e5d..bb356647cf 100644 --- a/src/library/tactic/simplifier/simplifier.h +++ b/src/library/tactic/simplify.h @@ -29,7 +29,6 @@ name get_simplify_canonize_instances_fixed_point_name(); name get_simplify_canonize_proofs_fixed_point_name(); name get_simplify_canonize_subsingletons_name(); -void initialize_simplifier(); -void finalize_simplifier(); - +void initialize_simplify(); +void finalize_simplify(); }