michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library): remove dead files

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-23 10:28:20 -07:00
parent 83b22823a6
commit 27ff42d2e0
2 changed files with 0 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

73
src/library/opaque_hints.cpp
View file

@ -1,73 +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 "util/sstream.h"
#include "kernel/environment.h"
#include "kernel/type_checker.h"
#include "library/module.h"
namespace lean {
struct opaque_hints_ext : public environment_extension {
name_set m_opaque;
name_set m_transparent;
opaque_hints_ext() {}
};
struct opaque_hints_ext_reg {
unsigned m_ext_id;
opaque_hints_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<opaque_hints_ext>()); }
};
static opaque_hints_ext_reg g_ext;
static opaque_hints_ext const & get_extension(environment const & env) {
return static_cast<opaque_hints_ext const &>(env.get_extension(g_ext.m_ext_id));
}
static environment update(environment const & env, opaque_hints_ext const & ext) {
return env.update(g_ext.m_ext_id, std::make_shared<opaque_hints_ext>(ext));
}
static void check_definition(environment const & env, name const & n) {
declaration d = env.get(n);
if (!d.is_definition())
throw exception(sstream() << "invalid opaque/transparent, '" << n << "' is not a definition");
}
environment hide_definition(environment const & env, name const & n) {
check_definition(env, n);
auto ext = get_extension(env);
ext.m_opaque.insert(n);
ext.m_transparent.erase(n);
return update(env, ext);
}
environment expose_definition(environment const & env, name const & n) {
check_definition(env, n);
auto ext = get_extension(env);
ext.m_opaque.erase(n);
ext.m_transparent.insert(n);
return update(env, ext);
}
bool is_exposed(environment const & env, name const & n) {
auto const & ext = get_extension(env);
return ext.m_transparent.contains(n);
}
std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env, name_generator const & ngen,
bool relax_main_opaque, bool only_main_transparent) {
auto const & ext = get_extension(env);
if (only_main_transparent) {
name_set extra_opaque = ext.m_opaque;
name_set extra_transparent = ext.m_transparent;
extra_opaque_pred pred([=](name const & n) {
return
(!module::is_definition(env, n) || extra_opaque.contains(n)) &&
(!extra_transparent.contains(n));
});
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
true, pred)));
} else {
name_set extra_opaque = ext.m_opaque;
extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); });
return std::unique_ptr<type_checker>(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque,
true, pred)));
}
}
}

42
src/library/opaque_hints.h
View file

@ -1,42 +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 "kernel/environment.h"
namespace lean {
/*
Opaque hints are used to 'help/guide' the elaborator and unifier.
We can use them to mark additional definitions as opaque.
Note that we are not changing the status of the definitions, we are
only changing how the elaborator/unifier treats them.
These hints are not used when we type check a definition before
adding it to the kernel.
*/
/** \brief Mark the definition named \c n as opaque for the elaborator/unifier. */
environment hide_definition(environment const & env, name const & n);
/** \brief Undo the modification made with \c hide_definition. */
environment expose_definition(environment const & env, name const & n);
/** \brief Return true iff \c n was exposed using \c expose_definition */
bool is_exposed(environment const & env, name const & n);
/** \brief Create a type checker that uses a converter based on the opaque/transparent hints
provided by the user.
If \c relax_main_opaque is true, then all opaque definitions from the main module
are treated as transparent.
If \c only_main_transparent is true, then only transparent definitions from the main module
are treated as transparent.
The hints provided using #hide_definition and #expose_definition override this behavior.
*/
std::unique_ptr<type_checker> mk_type_checker_with_hints(environment const & env,
name_generator const & ngen,
bool relax_main_opaque,
bool only_main_transparent = false);
}