refactor(frontends/lean): move choice_iterator to library

src/frontends/lean/CMakeLists.txt

@@ -5,10 +5,10 @@ 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 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)
+info_annotation.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)
 
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/coercion_elaborator.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/constraint.h"
 #include "library/coercion.h"
 #include "library/unifier.h"
-#include "frontends/lean/choice_iterator.h"
+#include "library/choice_iterator.h"
 #include "frontends/lean/coercion_elaborator.h"
 
 namespace lean {

src/frontends/lean/coercion_elaborator.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "kernel/type_checker.h"
-#include "frontends/lean/choice_iterator.h"
+#include "library/choice_iterator.h"
 
 namespace lean {
 /** \brief Abstract class for hiding details of the info_manager from the coercion_elaborator */

src/frontends/lean/elaborator.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "library/typed_expr.h"
 #include "library/local_context.h"
 #include "library/util.h"
+#include "library/choice_iterator.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/error_handling/error_handling.h"
 #include "library/definitional/equations.h"
@@ -41,7 +42,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/info_annotation.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"

src/frontends/lean/placeholder_elaborator.cpp

@@ -17,8 +17,8 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 #include "library/class.h"
 #include "library/local_context.h"
+#include "library/choice_iterator.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/pp_options.h"
 

src/library/CMakeLists.txt

@@ -11,6 +11,6 @@ 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)
+  local_context.cpp choice_iterator.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/choice_iterator.cpp

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontends/lean/choice_iterator.h"
+#include "library/choice_iterator.h"
 
 namespace lean {
 lazy_list<constraints> choose(std::shared_ptr<choice_iterator> c, bool ignore_failure) {