90bfd84a07
In the standard library, we should use explicit universe variables for universe polymorphic definitions. Users that want to declare universe polymorphic definitions but do not want to provide universe level parameters should use Type _ or Type*
109 lines
4.1 KiB
C++
109 lines
4.1 KiB
C++
/*
|
|
Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include "util/thread.h"
|
|
#include "kernel/find_fn.h"
|
|
#include "library/placeholder.h"
|
|
|
|
namespace lean {
|
|
static name * g_placeholder_one_name = nullptr;
|
|
static name * g_implicit_placeholder_name = nullptr;
|
|
static name * g_placeholder_name = nullptr;
|
|
static name * g_strict_placeholder_name = nullptr;
|
|
static name * g_explicit_placeholder_name = nullptr;
|
|
|
|
void initialize_placeholder() {
|
|
g_placeholder_one_name = new name(name::mk_internal_unique_name(), "_");
|
|
g_implicit_placeholder_name = new name(name::mk_internal_unique_name(), "_");
|
|
g_placeholder_name = g_implicit_placeholder_name;
|
|
g_strict_placeholder_name = new name(name::mk_internal_unique_name(), "_");
|
|
g_explicit_placeholder_name = new name(name::mk_internal_unique_name(), "_");
|
|
}
|
|
|
|
void finalize_placeholder() {
|
|
delete g_implicit_placeholder_name;
|
|
delete g_strict_placeholder_name;
|
|
delete g_explicit_placeholder_name;
|
|
delete g_placeholder_one_name;
|
|
}
|
|
|
|
LEAN_THREAD_VALUE(unsigned, g_placeholder_id, 0);
|
|
static unsigned next_placeholder_id() {
|
|
unsigned r = g_placeholder_id;
|
|
g_placeholder_id++;
|
|
return r;
|
|
}
|
|
level mk_level_placeholder() { return mk_global_univ(name(*g_placeholder_name, next_placeholder_id())); }
|
|
level mk_level_one_placeholder() { return mk_global_univ(*g_placeholder_one_name); }
|
|
static name const & to_prefix(expr_placeholder_kind k) {
|
|
switch (k) {
|
|
case expr_placeholder_kind::Implicit: return *g_implicit_placeholder_name;
|
|
case expr_placeholder_kind::StrictImplicit: return *g_strict_placeholder_name;
|
|
case expr_placeholder_kind::Explicit: return *g_explicit_placeholder_name;
|
|
}
|
|
lean_unreachable(); // LCOV_EXCL_LINE
|
|
}
|
|
expr mk_expr_placeholder(optional<expr> const & type, expr_placeholder_kind k) {
|
|
name n(to_prefix(k), next_placeholder_id());
|
|
if (type)
|
|
return mk_local(n, *type);
|
|
else
|
|
return mk_constant(n);
|
|
}
|
|
static bool is_placeholder(name const & n) {
|
|
if (n.is_atomic())
|
|
return false;
|
|
name const & p = n.get_prefix();
|
|
return p == *g_implicit_placeholder_name || p == *g_strict_placeholder_name || p == *g_explicit_placeholder_name;
|
|
}
|
|
static bool is_strict_placeholder(name const & n) {
|
|
return !n.is_atomic() && n.get_prefix() == *g_strict_placeholder_name;
|
|
}
|
|
static bool is_explicit_placeholder(name const & n) {
|
|
return !n.is_atomic() && n.get_prefix() == *g_explicit_placeholder_name;
|
|
}
|
|
bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); }
|
|
bool is_one_placeholder(level const & e) { return is_global(e) && global_id(e) == *g_placeholder_one_name; }
|
|
|
|
bool is_placeholder(expr const & e) {
|
|
return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(mlocal_name(e)));
|
|
}
|
|
bool is_strict_placeholder(expr const & e) {
|
|
return (is_constant(e) && is_strict_placeholder(const_name(e))) || (is_local(e) && is_strict_placeholder(mlocal_name(e)));
|
|
}
|
|
bool is_explicit_placeholder(expr const & e) {
|
|
return (is_constant(e) && is_explicit_placeholder(const_name(e))) || (is_local(e) && is_explicit_placeholder(mlocal_name(e)));
|
|
}
|
|
optional<expr> placeholder_type(expr const & e) {
|
|
if (is_local(e) && is_placeholder(e))
|
|
return some_expr(mlocal_type(e));
|
|
else
|
|
return none_expr();
|
|
}
|
|
|
|
bool has_placeholder(level const & l) {
|
|
bool r = false;
|
|
for_each(l, [&](level const & e) {
|
|
if (is_placeholder(e) || is_one_placeholder(e))
|
|
r = true;
|
|
return !r;
|
|
});
|
|
return r;
|
|
}
|
|
|
|
bool has_placeholder(expr const & e) {
|
|
return (bool) find(e, [](expr const & e, unsigned) { // NOLINT
|
|
if (is_placeholder(e))
|
|
return true;
|
|
else if (is_sort(e))
|
|
return has_placeholder(sort_level(e));
|
|
else if (is_constant(e))
|
|
return std::any_of(const_levels(e).begin(), const_levels(e).end(), [](level const & l) { return has_placeholder(l); });
|
|
else
|
|
return false;
|
|
});
|
|
}
|
|
}
|