refactor(library/aliases,frontends/lean/local_ref_info): merge aliases and local_ref_info modules

src/frontends/lean/CMakeLists.txt

@@ -4,7 +4,7 @@ parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmds.cpp dependencies.cpp
 pp.cpp structure_cmd.cpp structure_instance.cpp
-init_module.cpp type_util.cpp local_ref_info.cpp decl_attributes.cpp
+init_module.cpp type_util.cpp decl_attributes.cpp
 opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp elaborator_exception.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp)

src/frontends/lean/init_module.cpp

@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/pp.h"
-#include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/prenum.h"
 #include "frontends/lean/elaborator.h"
@@ -41,7 +40,6 @@ void initialize_frontend_lean_module() {
     initialize_inductive_cmds();
     initialize_structure_instance();
     initialize_pp();
-    initialize_local_ref_info();
     initialize_decl_cmds();
     initialize_match_expr();
     initialize_elaborator();
@@ -54,7 +52,6 @@ void finalize_frontend_lean_module() {
     finalize_elaborator();
     finalize_match_expr();
     finalize_decl_cmds();
-    finalize_local_ref_info();
     finalize_pp();
     finalize_structure_instance();
     finalize_inductive_cmds();

src/frontends/lean/local_ref_info.cpp

@@ -1,77 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/scoped_ext.h"
-
-namespace lean {
-/*
-When we declare a definition in a section, we create an alias for it that fixes the parameters in
-universe parameters. We have to store the number of parameters and universes that have been fixed
-to be able to correctly pretty print terms.
-*/
-struct local_ref_entry {
-    name     m_name;
-    expr     m_ref;
-    local_ref_entry() {}
-    local_ref_entry(name const & n, expr const & ref):
-    m_name(n), m_ref(ref) {}
-};
-
-static name * g_local_ref_name  = nullptr;
-static std::string * g_key      = nullptr;
-
-struct local_ref_config {
-    typedef name_map<expr>   state;
-    typedef local_ref_entry  entry;
-
-    static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
-        s.insert(e.m_name, e.m_ref);
-    }
-    static name const & get_class_name() {
-        return *g_local_ref_name;
-    }
-    static std::string const & get_serialization_key() {
-        return *g_key;
-    }
-    static void  write_entry(serializer &, entry const &) {
-        lean_unreachable();
-    }
-    static entry read_entry(deserializer &) {
-        lean_unreachable();
-    }
-    static optional<unsigned> get_fingerprint(entry const &) {
-        return optional<unsigned>();
-    }
-};
-
-template class scoped_ext<local_ref_config>;
-typedef scoped_ext<local_ref_config> local_ref_ext;
-
-environment save_local_ref_info(environment const & env, name const & n, expr const & ref) {
-    bool persistent = false;
-    return local_ref_ext::add_entry(env, get_dummy_ios(), local_ref_entry(n, ref), persistent);
-}
-
-optional<expr> get_local_ref_info(environment const & env, name const & n) {
-    if (auto r = local_ref_ext::get_state(env).find(n))
-        return some_expr(*r);
-    else
-        return none_expr();
-}
-
-void initialize_local_ref_info() {
-    g_local_ref_name = new name("localrefinfo");
-    g_key            = new std::string("localrefinfo");
-    local_ref_ext::initialize();
-}
-
-void finalize_local_ref_info() {
-    local_ref_ext::finalize();
-    delete g_local_ref_name;
-    delete g_key;
-}
-}

src/frontends/lean/local_ref_info.h

@@ -1,14 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-
-namespace lean {
-environment save_local_ref_info(environment const & env, name const & n, expr const & ref);
-optional<expr> get_local_ref_info(environment const & env, name const & n);
-void initialize_local_ref_info();
-void finalize_local_ref_info();
-}

src/frontends/lean/parser.cpp

@@ -56,7 +56,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/parser_pos_provider.h"
 #include "frontends/lean/update_environment_exception.h"
-#include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/opt_cmd.h"
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/prenum.h"
@@ -568,12 +567,12 @@ environment parser::add_local_ref(environment const & env, name const & n, expr
         if (is_explicit(f))
             f = get_explicit_arg(f);
         if (is_constant(f)) {
-            return save_local_ref_info(env, const_name(f), ref);
+            return ::lean::add_local_ref(env, const_name(f), ref);
         } else {
             return env;
         }
     } else if (is_constant(ref) && const_levels(ref)) {
-        return save_local_ref_info(env, const_name(ref), ref);
+        return ::lean::add_local_ref(env, const_name(ref), ref);
     } else {
         return env;
     }

src/frontends/lean/pp.cpp

@@ -45,7 +45,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/parser_config.h"
-#include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/scanner.h"
 
 namespace lean {
@@ -455,7 +454,7 @@ static local_ref_kind check_local_ref(environment const & env, expr const & e, u
     expr const & rfn = get_app_fn(e);
     if (!is_constant(rfn))
         return NotLocalRef;
-    auto ref = get_local_ref_info(env, const_name(rfn));
+    auto ref = get_local_ref(env, const_name(rfn));
     if (!ref)
         return NotLocalRef;
     if (is_as_atomic(*ref))

src/library/aliases.cpp

@@ -28,6 +28,7 @@ struct aliases_ext : public environment_extension {
         name_map<name>        m_inv_aliases;
         name_map<name>        m_level_aliases;
         name_map<name>        m_inv_level_aliases;
+        name_map<expr>        m_local_refs;
         state():m_in_section(false) {}
 
         void add_expr_alias(name const & a, name const & e, bool overwrite) {
@@ -76,6 +77,10 @@ struct aliases_ext : public environment_extension {
         add_expr_alias(a, e, overwrite);
     }
 
+    void add_local_ref(name const & a, expr const & ref) {
+        m_state.m_local_refs.insert(a, ref);
+    }
+
     void push(bool in_section) {
         m_scopes = cons(m_state, m_scopes);
         m_state.m_in_section = in_section;
@@ -140,6 +145,20 @@ list<name> get_expr_aliases(environment const & env, name const & n) {
     return ptr_to_list(get_extension(env).m_state.m_aliases.find(n));
 }
 
+environment add_local_ref(environment const & env, name const & a, expr const & ref) {
+    aliases_ext ext = get_extension(env);
+    ext.add_local_ref(a, ref);
+    return update(env, ext);
+}
+
+optional<expr> get_local_ref(environment const & env, name const & n) {
+    aliases_ext const & ext = get_extension(env);
+    if (auto r = ext.m_state.m_local_refs.find(n))
+        return some_expr(*r);
+    else
+        return none_expr();
+}
+
 static void check_no_shadow(environment const & env, name const & a) {
     if (env.is_universe(a))
         throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");

src/library/aliases.h

@@ -56,6 +56,12 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
 
 void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn);
 
+/* When we declare a definition in a section, we create an alias for it that fixes the parameters in
+   universe parameters. */
+environment add_local_ref(environment const & env, name const & a, expr const & ref);
+
+optional<expr> get_local_ref(environment const & env, name const & n);
+
 void initialize_aliases();
 void finalize_aliases();
 }