refactor(frontends/lean): combine info annotations in a single module

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 no_info.cpp
+theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp
-extra_info.cpp local_context.cpp choice_iterator.cpp
+local_context.cpp choice_iterator.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)

src/frontends/lean/builtin_exprs.cpp

@@ -23,10 +23,10 @@ Author: Leonardo de Moura
 #include "frontends/lean/calc.h"
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/parser.h"
-#include "frontends/lean/extra_info.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/info_tactic.h"
+#include "frontends/lean/info_annotation.h"
 
 namespace lean {
 namespace notation {

src/frontends/lean/elaborator.cpp

@@ -37,8 +37,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/no_info.h"
+#include "frontends/lean/info_annotation.h"
-#include "frontends/lean/extra_info.h"
 #include "frontends/lean/local_context.h"
 #include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/placeholder_elaborator.h"

src/frontends/lean/extra_info.h

@@ -1,21 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/annotation.h"
-
-namespace lean {
-/** \brief Annotate \c e with "extra-info" annotation.
-    It instructs elaborator to store the type of \c e.
-*/
-expr mk_extra_info(expr const & e, tag g);
-expr mk_extra_info(expr const & e);
-/** \brief Return true iff \c e is a term annotated with mk_extra_info */
-bool is_extra_info(expr const & e);
-
-void initialize_extra_info();
-void finalize_extra_info();
-}

src/frontends/lean/info_annotation.cpp

@@ -4,9 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "frontends/lean/extra_info.h"
+#include "frontends/lean/info_annotation.h"
 
 namespace lean {
+static name * g_no_info = nullptr;
+name const & get_no_info() { return *g_no_info; }
+
+expr mk_no_info(expr const & e) { return mk_annotation(get_no_info(), e); }
+bool is_no_info(expr const & e) { return is_annotation(e, get_no_info()); }
+
 static name * g_extra_info = nullptr;
 name const & get_extra_info() { return *g_extra_info; }
 
@@ -14,12 +20,15 @@ expr mk_extra_info(expr const & e, tag g) { return mk_annotation(get_extra_info(
 expr mk_extra_info(expr const & e) { return mk_annotation(get_extra_info(), e); }
 bool is_extra_info(expr const & e) { return is_annotation(e, get_extra_info()); }
 
-void initialize_extra_info() {
+void initialize_info_annotation() {
+    g_no_info = new name("no_info");
+    register_annotation(*g_no_info);
     g_extra_info = new name("extra_info");
     register_annotation(*g_extra_info);
 }
 
-void finalize_extra_info() {
+void finalize_info_annotation() {
+    delete g_no_info;
     delete g_extra_info;
 }
 }

src/frontends/lean/info_annotation.h

@@ -7,6 +7,9 @@ Author: Leonardo de Moura
 #pragma once
 #include "library/annotation.h"
 
+// Auxiliary expression annotations for helping the generation
+// of information for the info_manager
+
 namespace lean {
 /** \brief Annotate \c e with no-information generation.
 
@@ -17,6 +20,14 @@ expr mk_no_info(expr const & e);
 /** \brief Return true iff \c e is a term annotated with mk_no_info */
 bool is_no_info(expr const & e);
 
-void initialize_no_info();
+/** \brief Annotate \c e with "extra-info" annotation.
-void finalize_no_info();
+    It instructs elaborator to store the type of \c e.
+*/
+expr mk_extra_info(expr const & e, tag g);
+expr mk_extra_info(expr const & e);
+/** \brief Return true iff \c e is a term annotated with mk_extra_info */
+bool is_extra_info(expr const & e);
+
+void initialize_info_annotation();
+void finalize_info_annotation();
 }

src/frontends/lean/init_module.cpp

@@ -9,8 +9,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/pp_options.h"
 #include "frontends/lean/parser.h"
-#include "frontends/lean/no_info.h"
+#include "frontends/lean/info_annotation.h"
-#include "frontends/lean/extra_info.h"
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/class.h"
 #include "frontends/lean/parser_config.h"
@@ -42,8 +41,7 @@ void initialize_frontend_lean_module() {
     initialize_pp_options();
     initialize_scanner();
     initialize_parser();
-    initialize_no_info();
+    initialize_info_annotation();
-    initialize_extra_info();
     initialize_tactic_hint();
     initialize_class();
     initialize_parser_config();
@@ -72,8 +70,7 @@ void finalize_frontend_lean_module() {
     finalize_parser_config();
     finalize_class();
     finalize_tactic_hint();
-    finalize_extra_info();
+    finalize_info_annotation();
-    finalize_no_info();
     finalize_parser();
     finalize_scanner();
     finalize_pp_options();

src/frontends/lean/no_info.cpp

@@ -1,24 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "frontends/lean/no_info.h"
-
-namespace lean {
-static name * g_no_info = nullptr;
-name const & get_no_info() { return *g_no_info; }
-
-expr mk_no_info(expr const & e) { return mk_annotation(get_no_info(), e); }
-bool is_no_info(expr const & e) { return is_annotation(e, get_no_info()); }
-
-void initialize_no_info() {
-    g_no_info = new name("no_info");
-    register_annotation(*g_no_info);
-}
-
-void finalize_no_info() {
-    delete g_no_info;
-}
-}

src/frontends/lean/parse_table.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "library/kernel_bindings.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/parser.h"
-#include "frontends/lean/no_info.h"
+#include "frontends/lean/info_annotation.h"
 
 namespace lean {
 namespace notation {