From 27ff42d2e0a42e88cd7267cf327995358cfd2fca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Sep 2014 10:28:20 -0700 Subject: [PATCH] refactor(library): remove dead files --- src/library/opaque_hints.cpp | 73 ------------------------------------ src/library/opaque_hints.h | 42 --------------------- 2 files changed, 115 deletions(-) delete mode 100644 src/library/opaque_hints.cpp delete mode 100644 src/library/opaque_hints.h diff --git a/src/library/opaque_hints.cpp b/src/library/opaque_hints.cpp deleted file mode 100644 index c71b523e3b..0000000000 --- a/src/library/opaque_hints.cpp +++ /dev/null @@ -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()); } -}; -static opaque_hints_ext_reg g_ext; -static opaque_hints_ext const & get_extension(environment const & env) { - return static_cast(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(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 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(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(new type_checker(env, ngen, mk_default_converter(env, relax_main_opaque, - true, pred))); - } -} -} diff --git a/src/library/opaque_hints.h b/src/library/opaque_hints.h deleted file mode 100644 index 39bb49dd12..0000000000 --- a/src/library/opaque_hints.h +++ /dev/null @@ -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 mk_type_checker_with_hints(environment const & env, - name_generator const & ngen, - bool relax_main_opaque, - bool only_main_transparent = false); -}