max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/private): more deterministic private names

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-12 13:43:20 -08:00
parent 88de217cb7
commit 888252b5db
3 changed files with 24 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/library/private.cpp
View file

@ -18,7 +18,8 @@ struct private_ext : public environment_extension {
/* We store private prefixes to make sure register_private_name is used correctly.
This information does not need to be stored in .olean files. */
name_set m_private_prefixes;
private_ext():m_counter(0) {}
name m_mod_name;
private_ext():m_counter(1) {}
};
struct private_ext_reg {
@ -34,6 +35,12 @@ static environment update(environment const & env, private_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<private_ext>(ext));
}
environment set_main_module_name(environment const & env, name const & mod_name) {
private_ext ext = get_extension(env);
ext.m_mod_name = mod_name;
return update(env, ext);
}
static name * g_private = nullptr;
struct private_modification : public modification {
@ -48,7 +55,6 @@ struct private_modification : public modification {
private_ext ext = get_extension(env);
// we restore only the mapping hidden-name -> user-name (for pretty printing purposes)
ext.m_inv_map.insert(m_real, m_name);
ext.m_counter++;
env = update(env, ext);
}
@ -69,16 +75,13 @@ static environment preserve_private_data(environment const & env, name const & r
return module::add(env, std::make_shared<private_modification>(n, r));
}
static name mk_private_name_core(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
static name mk_private_name_core(environment const & env, name const & n) {
private_ext const & ext = get_extension(env);
unsigned h = hash(n.hash(), ext.m_counter);
if (extra_hash)
h = hash(h, *extra_hash);
return name(*g_private, h) + n;
return name(name(*g_private) + ext.m_mod_name, ext.m_counter) + n;
}
pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
name r = mk_private_name_core(env, n, extra_hash);
pair<environment, name> add_private_name(environment const & env, name const & n) {
name r = mk_private_name_core(env, n);
private_ext ext = get_extension(env);
ext.m_inv_map.insert(r, n);
ext.m_counter++;
@ -87,22 +90,8 @@ pair<environment, name> add_private_name(environment const & env, name const & n
return mk_pair(new_env, r);
}
static unsigned mk_extra_hash_using_pos() {
unsigned h = 31;
if (auto pinfo = get_pos_info_provider()) {
h = hash(pinfo->get_some_pos().first, pinfo->get_some_pos().second);
char const * fname = pinfo->get_file_name();
h = hash_str(strlen(fname), fname, h);
}
return h;
}
pair<environment, name> mk_private_name(environment const & env, name const & c) {
return add_private_name(env, c, optional<unsigned>(mk_extra_hash_using_pos()));
}
pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash) {
name r = mk_private_name_core(env, name(), extra_hash);
pair<environment, name> mk_private_prefix(environment const & env) {
name r = mk_private_name_core(env, name());
private_ext ext = get_extension(env);
ext.m_private_prefixes.insert(r);
ext.m_counter++;
@ -110,10 +99,6 @@ pair<environment, name> mk_private_prefix(environment const & env, optional<unsi
return mk_pair(new_env, r);
}
pair<environment, name> mk_private_prefix(environment const & env) {
return mk_private_prefix(env, optional<unsigned>(mk_extra_hash_using_pos()));
}
static optional<name> get_private_prefix(private_ext const & ext, name n) {
while (true) {
if (ext.m_private_prefixes.contains(n))

24
src/library/private.h
View file

@ -10,17 +10,11 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
namespace lean {
environment set_main_module_name(environment const & env, name const & mod_name);
/**
\brief This is an auxiliary function used to simulate private declarations. Whenever we want to create a "private"
declaration, this module creates an internal "hidden" name that is not accessible to users.
In principle, users can access the internal names if they want by applying themselves the procedure used to create
the "hidden" names.
The optional \c base_hash can be used to influence the "hidden" name associated with \c n.
The mapping between \c n and the "hidden" name is saved in the .olean files.
\brief This is an auxiliary function used to simulate private declarations.
*/
pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & base_hash);
pair<environment, name> add_private_name(environment const & env, name const & n);
/**
\brief Return the user name associated with the hidden name \c n.
@ -32,18 +26,14 @@ optional<name> hidden_to_user_name(environment const & env, name const & n);
bool is_private(environment const & env, name const & n);
pair<environment, name> mk_private_prefix(environment const & env, name const & n, optional<unsigned> const & base_hash);
/* Create a private prefix that is going to be use to generate many private names.
This function registers the private prefix in the environment. */
pair<environment, name> mk_private_prefix(environment const & env);
pair<environment, name> mk_private_prefix(environment const & env, name const & n);
/* Create a private name based on \c c and get_pos_info_provider(), and register it using \c add_private_name */
pair<environment, name> mk_private_name(environment const & env, name const & c);
/* Create a private prefix that is going to be use to generate many private names.
This function registers the private prefix in the environment. */
pair<environment, name> mk_private_prefix(environment const & env, optional<unsigned> const & extra_hash);
/* Similar to the previous function, but generate an extra_hash using get_pos_info_provider */
pair<environment, name> mk_private_prefix(environment const & env);
/* Register a \c n as the name for private name \c prv_n. \c prv_n must have been constructed using
a prefix returned by \c mk_private_prefix. */
environment register_private_name(environment const & env, name const & n, name const & prv_n);

3
src/shell/lean.cpp
View file

@ -34,6 +34,7 @@ Author: Leonardo de Moura
#include "library/io_state_stream.h"
#include "library/message_builder.h"
#include "library/time_task.h"
#include "library/private.h"
#include "library/compiler/emit_cpp.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/pp.h"
@ -451,6 +452,7 @@ int main(int argc, char ** argv) {
std::stringstream buf;
buf << std::cin.rdbuf();
contents = buf.str();
env = set_main_module_name(env, "_stdin");
} else {
if (argc - optind != 1) {
std::cerr << "Expected exactly one file name\n";
@ -459,6 +461,7 @@ int main(int argc, char ** argv) {
}
mod_fn = lrealpath(argv[optind]);
contents = read_file(mod_fn);
env = set_main_module_name(env, module_name_of_file(path.get_path(), mod_fn));
}
try {
message_log l;