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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-27 19:23:58 -07:00
parent 01f8bcfc87
commit 299c27252a
19 changed files with 14 additions and 1792 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
stage0/src/library/CMakeLists.txt generated
View file

@ -4,8 +4,7 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
class.cpp util.cpp print.cpp annotation.cpp
protected.cpp reducible.cpp init_module.cpp exception.cpp
pp_options.cpp projection.cpp
idx_metavar.cpp aux_recursors.cpp trace.cpp
local_context.cpp metavar_context.cpp
aux_recursors.cpp trace.cpp
type_context.cpp
locals.cpp messages.cpp message_builder.cpp check.cpp
profiling.cpp time_task.cpp

4
stage0/src/library/abstract_type_context.h generated
View file

@ -6,16 +6,12 @@ Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "library/local_context.h"
#include "library/metavar_context.h"
namespace lean {
class abstract_type_context {
public:
virtual ~abstract_type_context() {}
virtual environment const & env() const = 0;
virtual local_context const & lctx() const = 0;
virtual metavar_context const & mctx() const = 0;
virtual expr whnf(expr const & e) = 0;
virtual name next_name() = 0;
virtual expr relaxed_whnf(expr const & e) { return whnf(e); }

34
stage0/src/library/cache_helper.h generated
View file

@ -1,34 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "library/type_context.h"
namespace lean {
/** \brief Helper class for making sure we have a cache that is compatible
with a given environment and transparency mode. */
template<typename Cache>
class cache_compatibility_helper {
std::unique_ptr<Cache> m_cache_ptr[LEAN_NUM_TRANSPARENCY_MODES];
public:
Cache & get_cache_for(environment const & env, transparency_mode m) {
unsigned midx = static_cast<unsigned>(m);
if (!m_cache_ptr[midx] || !is_eqp(env, m_cache_ptr[midx]->env())) {
m_cache_ptr[midx].reset(new Cache(env));
}
return *m_cache_ptr[midx].get();
}
Cache & get_cache_for(type_context_old const & ctx) {
return get_cache_for(ctx.env(), ctx.mode());
}
void clear() {
for (unsigned i = 0; i < LEAN_NUM_TRANSPARENCY_MODES; i++) m_cache_ptr[i].reset();
}
};
}

123
stage0/src/library/check.cpp generated
View file

@ -13,131 +13,12 @@ namespace lean {
struct check_fn {
type_context_old & m_ctx;
expr_set m_visited;
void visit_constant(expr const & e) {
constant_info info = m_ctx.env().get(const_name(e));
if (info.get_num_lparams() != length(const_levels(e))) {
lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
tout() << "incorrect of universe levels at " << e << "\n";);
throw exception("check failed, incorrect number of universe levels "
"(use 'set_option trace.check true' for additional details)");
}
}
void ensure_type(expr const & e) {
expr S = m_ctx.relaxed_whnf(m_ctx.infer(e));
if (is_sort(S)) return;
if (is_metavar(S)) {
level u = m_ctx.mk_univ_metavar_decl();
if (m_ctx.is_def_eq(S, mk_sort(u)))
return;
}
lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
tout() << "type expected at " << e << "\n";);
throw exception("check failed, type expected "
"(use 'set_option trace.check true' for additional details)");
}
void visit_binding(expr const & e, bool is_pi) {
type_context_old::tmp_locals locals(m_ctx);
expr it = e;
while (it.kind() == e.kind()) {
expr d = instantiate_rev(binding_domain(it), locals.size(), locals.data());
visit(d);
locals.push_local(binding_name(it), d, binding_info(it));
ensure_type(d);
it = binding_body(it);
}
expr b = instantiate_rev(it, locals.size(), locals.data());
visit(b);
if (is_pi)
ensure_type(b);
}
void visit_lambda(expr const & e) {
visit_binding(e, false);
}
void visit_pi(expr const & e) {
visit_binding(e, true);
}
void visit_let(expr const & e) {
visit(let_value(e));
visit(let_type(e));
expr v_type = m_ctx.infer(let_value(e));
if (!m_ctx.relaxed_is_def_eq(let_type(e), v_type)) {
lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
tout() << "type mismatch at let binder\n " << e << "\n";);
throw exception("check failed, type mismatch at let binder "
"(use 'set_option trace.check true' for additional details)");
}
/* Improve performance if bottleneck */
type_context_old::tmp_locals locals(m_ctx);
expr local = locals.push_local_from_let(e);
visit(instantiate(let_body(e), local));
}
void visit_app(expr const & e) {
visit(app_fn(e));
visit(app_arg(e));
expr f_type = m_ctx.relaxed_whnf(m_ctx.infer(app_fn(e)));
if (!is_pi(f_type)) {
lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
tout() << "function expected at\n " << e << "\ntype\n " << f_type << "\n";);
throw exception("check failed, function expected (use 'set_option trace.check true' for additional details)");
}
expr a_type = m_ctx.infer(app_arg(e));
expr d_type = binding_domain(f_type);
if (!m_ctx.relaxed_is_def_eq(a_type, d_type)) {
lean_trace("check", scope_trace_env _(m_ctx.env(), m_ctx);
tout() << "application type mismatch at\n " << e << "\nargument type\n "
<< a_type << "\nexpected type\n " << d_type;);
throw exception("check failed, application type mismatch "
"(use 'set_option trace.check true' for additional details)");
}
}
void visit(expr const & e) {
if (m_visited.find(e) != m_visited.end())
return;
m_visited.insert(e);
switch (e.kind()) {
case expr_kind::FVar:
case expr_kind::MVar:
case expr_kind::Sort:
case expr_kind::Lit:
case expr_kind::Local:
break; /* do nothing */
case expr_kind::Const:
return visit_constant(e);
case expr_kind::BVar:
lean_unreachable(); // LCOV_EXCL_LINE
case expr_kind::Lambda:
return visit_lambda(e);
case expr_kind::Pi:
return visit_pi(e);
case expr_kind::App:
return visit_app(e);
case expr_kind::Let:
return visit_let(e);
case expr_kind::MData:
return visit(mdata_expr(e));
case expr_kind::Proj:
return visit(proj_expr(e));
}
}
public:
check_fn(type_context_old & ctx):m_ctx(ctx) {}
void operator()(expr const & e) { return visit(e); }
};
void check(type_context_old & ctx, expr const & e) {
metavar_context mctx = ctx.mctx();
check_fn checker(ctx);
checker(e);
ctx.set_mctx(mctx);
void check(type_context_old &, expr const &) {
lean_unreachable();
}
void initialize_check() {

2
stage0/src/library/compiler/util.cpp generated
View file

@ -416,7 +416,7 @@ bool is_irrelevant_type(type_checker::state & st, local_ctx lctx, expr const & t
bool is_irrelevant_type(environment const & env, expr const & type) {
type_checker::state st(env);
return is_irrelevant_type(st, local_context(), type);
return is_irrelevant_type(st, local_ctx(), type);
}
void collect_used(expr const & e, name_hash_set & S) {

2
stage0/src/library/expr_lt.cpp generated
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "library/expr_lt.h"
namespace lean {
bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * lctx) {
bool is_lt(expr const & a, expr const & b, bool use_hash, local_ctx const * lctx) {
if (is_eqp(a, b)) return false;
if (a.kind() != b.kind()) return a.kind() < b.kind();
if (use_hash) {

4
stage0/src/library/expr_lt.h generated
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include "kernel/expr.h"
#include "util/rb_map.h"
#include "library/local_context.h"
#include "kernel/local_ctx.h"
namespace lean {
/** \brief Total order on expressions.
@ -18,7 +18,7 @@ namespace lean {
\remark If lctx is not nullptr, then we use the local_decl index to compare local constants.
*/
bool is_lt(expr const & a, expr const & b, bool use_hash, local_context const * lctx = nullptr);
bool is_lt(expr const & a, expr const & b, bool use_hash, local_ctx const * lctx = nullptr);
/** \brief Similar to is_lt, but universe level parameter names are ignored. */
bool is_lt_no_level_params(expr const & a, expr const & b);
inline bool is_hash_lt(expr const & a, expr const & b) { return is_lt(a, b, true); }

104
stage0/src/library/idx_metavar.cpp generated
View file

@ -1,104 +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 <lean/interrupt.h>
#include "kernel/for_each_fn.h"
#include "library/idx_metavar.h"
#include "library/metavar_context.h"
#include "library/replace_visitor.h"
#ifndef LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY
#define LEAN_INSTANTIATE_METAIDX_CACHE_CAPACITY 1024*8
#endif
namespace lean {
static name * g_tmp_prefix = nullptr;
void initialize_idx_metavar() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
mark_persistent(g_tmp_prefix->raw());
}
void finalize_idx_metavar() {
delete g_tmp_prefix;
}
level mk_idx_metauniv(unsigned i) {
return mk_univ_mvar(name(*g_tmp_prefix, i));
}
expr mk_idx_metavar(unsigned i) {
return mk_metavar(name(*g_tmp_prefix, i));
}
bool is_idx_metauniv(level const & l) {
if (!is_mvar(l))
return false;
name const & n = mvar_id(l);
return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
}
unsigned to_meta_idx(level const & l) {
lean_assert(is_idx_metauniv(l));
return mvar_id(l).get_numeral().get_small_value();
}
bool is_idx_metavar(expr const & e) {
if (!is_metavar(e))
return false;
name const & n = mvar_name(e);
return !n.is_atomic() && n.is_numeral() && n.get_prefix() == *g_tmp_prefix;
}
unsigned to_meta_idx(expr const & e) {
lean_assert(is_idx_metavar(e));
return mvar_name(e).get_numeral().get_small_value();
}
bool has_idx_metauniv(level const & l) {
if (!has_mvar(l))
return false;
bool found = false;
for_each(l, [&](level const & l) {
if (found) return false;
if (!has_mvar(l)) return false;
if (is_idx_metauniv(l))
found = true;
return true;
});
return found;
}
bool has_idx_metavar(expr const & e) {
if (!has_univ_metavar(e) && !has_expr_metavar(e))
return false;
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
if (found) return false;
if (!has_univ_metavar(e) && !has_expr_metavar(e)) return false;
if (is_idx_metavar(e))
found = true;
else if (is_constant(e) && std::any_of(const_levels(e).begin(), const_levels(e).end(), has_idx_metauniv))
found = true;
else if (is_sort(e) && has_idx_metauniv(sort_level(e)))
found = true;
return true;
});
return found;
}
bool has_idx_expr_metavar(expr const & e) {
if (!has_expr_metavar(e))
return false;
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
if (found || !has_expr_metavar(e)) return false;
if (is_idx_metavar(e)) found = true;
return true;
});
return found;
}
}

39
stage0/src/library/idx_metavar.h generated
View file

@ -1,39 +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
#include "kernel/expr.h"
namespace lean {
/** \brief Create a universe level metavariable that can be used as a placeholder in #match.
\remark The index \c i is encoded in the hierarchical name, and can be quickly accessed.
In the match procedure the substitution is also efficiently represented as an array (aka buffer).
*/
level mk_idx_metauniv(unsigned i);
/** \brief Return true iff \c l is a metauniverse created using \c mk_idx_metauniv */
bool is_idx_metauniv(level const & l);
unsigned to_meta_idx(level const & l);
/** \brief Create a special metavariable that can be used as a placeholder in #match.
\remark The index \c i is encoded in the hierarchical name, and can be quickly accessed.
In the match procedure the substitution is also efficiently represented as an array (aka buffer).
*/
expr mk_idx_metavar(unsigned i);
/** \brief Return true iff \c l is a metavariable created using \c mk_idx_metavar */
bool is_idx_metavar(expr const & l);
unsigned to_meta_idx(expr const & e);
/** \brief Return true iff \c e contains idx metavariables or universe metavariables */
bool has_idx_metavar(expr const & e);
bool has_idx_expr_metavar(expr const & e);
bool has_idx_metauniv(level const & l);
class metavar_context;
void initialize_idx_metavar();
void finalize_idx_metavar();
}

9
stage0/src/library/init_module.cpp generated
View file

@ -11,14 +11,11 @@ Author: Leonardo de Moura
#include "library/annotation.h"
#include "library/protected.h"
#include "library/io_state.h"
#include "library/idx_metavar.h"
#include "library/placeholder.h"
#include "library/print.h"
#include "library/util.h"
#include "library/pp_options.h"
#include "library/type_context.h"
#include "library/local_context.h"
#include "library/metavar_context.h"
#include "library/check.h"
#include "library/profiling.h"
#include "library/time_task.h"
@ -43,11 +40,8 @@ void finalize_library_core_module() {
}
void initialize_library_module() {
initialize_local_context();
initialize_metavar_context();
initialize_print();
initialize_placeholder();
initialize_idx_metavar();
initialize_io_state();
initialize_num();
initialize_annotation();
@ -69,10 +63,7 @@ void finalize_library_module() {
finalize_annotation();
finalize_num();
finalize_io_state();
finalize_idx_metavar();
finalize_placeholder();
finalize_print();
finalize_metavar_context();
finalize_local_context();
}
}

437
stage0/src/library/local_context.cpp generated
View file

@ -1,437 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include <limits>
#include "util/fresh_name.h"
#include "util/list_fn.h"
#include "kernel/for_each_fn.h"
#include "kernel/find_fn.h"
#include "kernel/replace_fn.h"
#include "library/pp_options.h"
#include "library/local_context.h"
#include "library/metavar_context.h"
#include "library/trace.h"
namespace lean {
name mk_local_decl_name() {
return mk_fresh_name();
}
struct depends_on_fn {
metavar_context const & m_mctx;
local_context const * m_lctx;
unsigned m_num;
expr const * m_locals;
name_set m_visited_mvars;
name_set m_visited_decls;
depends_on_fn(metavar_context const & mctx, local_context const & lctx, unsigned num, expr const * locals):
m_mctx(mctx), m_lctx(&lctx), m_num(num), m_locals(locals) {
lean_assert(std::all_of(locals, locals+num, is_fvar));
}
depends_on_fn(metavar_context const & mctx, unsigned num, expr const * locals):
m_mctx(mctx), m_lctx(nullptr), m_num(num), m_locals(locals) {
lean_assert(std::all_of(locals, locals+num, is_fvar));
}
bool visit_local(expr const & e) {
lean_assert(is_fvar(e));
if (std::any_of(m_locals, m_locals + m_num,
[&](expr const & l) { return fvar_name(e) == fvar_name(l); }))
return true;
if (!m_lctx || m_visited_decls.contains(fvar_name(e)))
return false;
m_visited_decls.insert(fvar_name(e));
optional<local_decl> decl = m_lctx->find_local_decl(e);
if (!decl)
return false;
if (visit(decl->get_type()))
return true;
if (optional<expr> v = decl->get_value())
return visit(*v);
else
return false;
}
bool visit_metavar(expr const & e) {
lean_assert(is_metavar_decl_ref(e));
if (m_visited_mvars.contains(mvar_name(e)))
return false;
m_visited_mvars.insert(mvar_name(e));
optional<metavar_decl> decl = m_mctx.find_metavar_decl(e);
if (!decl)
return false;
if (visit(decl->get_type()))
return true;
if (auto v = m_mctx.get_assignment(e)) {
if (visit(*v))
return true;
}
return false;
}
bool visit(expr const & e) {
if (!has_local(e) && !has_expr_metavar(e))
return false;
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
if (found) return false;
if (!has_local(e) && !has_expr_metavar(e)) return false;
if (is_fvar(e) && visit_local(e)) {
found = true;
return false;
}
if (is_metavar_decl_ref(e) && visit_metavar(e)) {
found = true;
return false;
}
return true;
});
return found;
}
bool operator()(expr const & e) { return visit(e); }
};
bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals) {
return depends_on_fn(mctx, num, locals)(e);
}
bool depends_on(local_decl const & d, metavar_context const & mctx, unsigned num, expr const * locals) {
depends_on_fn fn(mctx, num, locals);
if (fn(d.get_type()))
return true;
if (auto v = d.get_value()) {
return fn(*v);
}
return false;
}
bool depends_on(expr const & e, metavar_context const & mctx, buffer<expr> const & locals) {
return depends_on_fn(mctx, locals.size(), locals.data())(e);
}
bool depends_on(local_decl const & d, metavar_context const & mctx, buffer<expr> const & locals) {
return depends_on(d, mctx, locals.size(), locals.data());
}
bool depends_on(expr const & e, metavar_context const & mctx, local_context const & lctx, unsigned num, expr const * locals) {
return depends_on_fn(mctx, lctx, num, locals)(e);
}
local_decl local_context::mk_local_decl_core(name const & n, name const & un, expr const & type, binder_info bi) {
return local_ctx::mk_local_decl(n, un, type, bi);
}
local_decl local_context::mk_local_decl_core(name const & n, name const & un, expr const & type, expr const & value) {
return local_ctx::mk_local_decl(n, un, type, value);
}
expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, optional<expr> const & value, binder_info bi) {
local_decl d = value ? local_ctx::mk_local_decl(n, un, type, *value) : local_ctx::mk_local_decl(n, un, type, bi);
expr r = d.mk_ref();
lean_assert(is_fvar(r));
return r;
}
expr local_context::mk_local_decl(expr const & type, binder_info bi) {
name n = mk_local_decl_name();
return mk_local_decl(n, n, type, none_expr(), bi);
}
expr local_context::mk_local_decl(expr const & type, expr const & value) {
name n = mk_local_decl_name();
return mk_local_decl(n, n, type, some_expr(value), mk_binder_info());
}
expr local_context::mk_local_decl(name const & un, expr const & type, binder_info bi) {
return mk_local_decl(mk_local_decl_name(), un, type, none_expr(), bi);
}
expr local_context::mk_local_decl(name const & un, expr const & type, expr const & value) {
return mk_local_decl(mk_local_decl_name(), un, type, some_expr(value), mk_binder_info());
}
expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi) {
return mk_local_decl(n, un, type, none_expr(), bi);
}
expr local_context::mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) {
return mk_local_decl(n, un, type, some_expr(value), mk_binder_info());
}
extern "C" object* lean_local_ctx_num_indices(object* lctx);
extern "C" object* lean_local_ctx_get(object* lctx, object* idx);
unsigned local_context::num_indices() const {
return unbox(lean_local_ctx_num_indices(to_obj_arg()));
}
optional<local_decl> local_context::get_decl_at(unsigned idx) const {
return to_optional<local_decl>(lean_local_ctx_get(to_obj_arg(), box(idx)));
}
optional<local_decl> local_context::back_find_if(std::function<bool(local_decl const &)> const & pred) const { // NOLINT
unsigned i = num_indices();
while (i > 0) {
--i;
optional<local_decl> decl = get_decl_at(i);
if (decl && pred(*decl)) return decl;
}
return optional<local_decl>();
}
optional<local_decl> local_context::find_local_decl_from_user_name(name const & n) const {
return back_find_if([&](local_decl const & d) { return d.get_user_name() == n; });
}
optional<local_decl> local_context::find_last_local_decl() const {
unsigned i = num_indices();
while (i > 0) {
--i;
optional<local_decl> decl = get_decl_at(i);
if (decl) return decl;
}
return optional<local_decl>();
}
local_decl local_context::get_last_local_decl() const {
if (auto decl = find_last_local_decl())
return *decl;
throw("unknown local constant, context is empty");
}
void local_context::for_each(std::function<void(local_decl const &)> const & fn) const {
unsigned num = num_indices();
for (unsigned i = 0; i < num; i++) {
optional<local_decl> decl = get_decl_at(i);
if (decl) fn(*decl);
}
}
optional<local_decl> local_context::find_if(std::function<bool(local_decl const &)> const & pred) const {
unsigned num = num_indices();
for (unsigned i = 0; i < num; i++) {
optional<local_decl> decl = get_decl_at(i);
if (decl && pred(*decl)) return decl;
}
return optional<local_decl>();
}
void local_context::for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const {
unsigned num = num_indices();
for (unsigned i = d.get_idx() + 1; i < num; i++) {
optional<local_decl> decl = get_decl_at(i);
if (decl) fn(*decl);
}
}
extern "C" object* lean_local_ctx_pop(object* lctx);
void local_context::pop_local_decl() {
m_obj = lean_local_ctx_pop(m_obj);
}
optional<local_decl> local_context::has_dependencies(local_decl const & d, metavar_context const & mctx) const {
lean_assert(find_local_decl(d.get_name()));
expr l = d.mk_ref();
optional<local_decl> r;
for_each_after(d, [&](local_decl const & d2) {
if (r) return;
if (depends_on(d2, mctx, 1, &l))
r = d2;
});
return r;
}
bool local_context::is_subset_of(name_set const & ls) const {
// TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class
return !static_cast<bool>(find_if([&](local_decl const & d) {
return !ls.contains(d.get_name());
}));
}
bool local_context::is_subset_of(local_context const & ctx) const {
// TODO(Leo): we can improve performance by implementing the subset operation in the rb_map/rb_tree class
return !static_cast<bool>(find_if([&](local_decl const & d) {
return !ctx.find_local_decl(d.get_name());
}));
}
local_context local_context::remove(buffer<expr> const & locals) const {
lean_assert(std::all_of(locals.begin(), locals.end(),
[&](expr const & l) {
return is_fvar(l) && find_local_decl(l);
}));
/* TODO(Leo): check whether the following loop is a performance bottleneck. */
local_context r = *this;
for (expr const & l : locals) {
local_decl d = get_local_decl(l);
r.clear(d);
}
lean_assert(r.well_formed());
return r;
}
/* Return true iff all local_decl references in \c e are in \c s. */
static bool locals_subset_of(expr const & e, name_set const & s) {
bool ok = true;
for_each(e, [&](expr const & e, unsigned) {
if (!ok) return false; // stop search
if (is_fvar(e) && !s.contains(fvar_name(e))) {
ok = false;
return false;
}
return true;
});
return ok;
}
bool local_context::well_formed() const {
bool ok = true;
name_set found_locals;
for_each([&](local_decl const & d) {
if (!locals_subset_of(d.get_type(), found_locals)) {
ok = false;
lean_unreachable();
}
if (auto v = d.get_value()) {
if (!locals_subset_of(*v, found_locals)) {
ok = false;
lean_unreachable();
}
}
found_locals.insert(d.get_name());
});
return ok;
}
bool local_context::well_formed(expr const & e) const {
bool ok = true;
::lean::for_each(e, [&](expr const & e, unsigned) {
if (!ok) return false;
if (is_fvar(e) && !find_local_decl(e)) {
ok = false;
}
return true;
});
return ok;
}
format local_context::pp(formatter const & fmt) const { // NOLINT
options const & opts = fmt.get_options();
unsigned indent = get_pp_indent(opts);
unsigned max_hs = get_pp_goal_max_hyps(opts);
bool first = true;
unsigned i = 0;
format ids;
optional<expr> type;
format r;
for_each([&](local_decl const & d) {
if (i >= max_hs)
return;
i++;
if (type && (d.get_type() != *type || d.get_value())) {
// add (ids : type) IF the d.get_type() != type OR d is a let-decl
if (first) first = false;
else r += format(",") + line();
r += group(ids + space() + format(":") + nest(indent, line() + fmt(*type)));
type = optional<expr>();
ids = format();
}
name n = sanitize_if_fresh(d.get_user_name());
n = sanitize_name_generator_name(n);
if (d.get_value()) {
if (first) first = false;
else r += format(",") + line();
r += group(format(n) + space() + format(":") + space() + fmt(d.get_type()) +
space() + format(":=") + nest(indent, line() + fmt(*d.get_value())));
} else if (!type) {
lean_assert(!d.get_value());
ids = format(n);
type = d.get_type();
} else {
lean_assert(!d.get_value());
lean_assert(type && d.get_type() == *type);
ids += space() + format(n);
}
});
if (type) {
if (!first) r += format(",") + line();
r += group(ids + space() + format(":") + nest(indent, line() + fmt(*type)));
}
if (get_pp_goal_compact(opts))
r = group(r);
return r;
}
bool local_context::uses_user_name(name const & n) const {
return static_cast<bool>(find_if([&](local_decl const & d) { return d.get_user_name() == n; }));
}
name local_context::get_unused_name(name const & prefix, unsigned & idx) const {
while (true) {
name curr = prefix.append_after(idx);
idx++;
if (!uses_user_name(curr))
return curr;
}
}
name local_context::get_unused_name(name const & suggestion) const {
if (!uses_user_name(suggestion))
return suggestion;
unsigned idx = 1;
return get_unused_name(suggestion, idx);
}
local_context local_context::instantiate_mvars(metavar_context & mctx) const {
local_context r;
for_each([&](local_decl const & d) {
expr new_type = mctx.instantiate_mvars(d.get_type());
if (auto v = d.get_value())
r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, mctx.instantiate_mvars(*v));
else
r.mk_local_decl_core(d.get_name(), d.get_user_name(), new_type, d.get_info());
});
return r;
}
bool contains_let_local_decl(local_context const & lctx, expr const & e) {
if (!has_local(e)) return false;
return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
if (!is_fvar(e)) return false;
optional<local_decl> d = lctx.find_local_decl(e);
return d && d->get_value();
}));
}
expr zeta_expand(local_context const & lctx, expr const & e) {
if (!contains_let_local_decl(lctx, e)) return e;
return replace(e, [&](expr const & e, unsigned) {
if (!has_local(e)) return some_expr(e);
if (is_fvar(e)) {
if (auto d = lctx.find_local_decl(e)) {
if (auto v = d->get_value())
return some_expr(zeta_expand(lctx, *v));
}
}
return none_expr();
});
}
void initialize_local_context() {
}
void finalize_local_context() {
}
}

136
stage0/src/library/local_context.h generated
View file

@ -1,136 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/name_map.h"
#include "util/name_set.h"
#include "kernel/local_ctx.h"
#include "kernel/expr.h"
#include "library/formatter.h"
namespace lean {
class metavar_context;
class local_context;
bool depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals);
bool depends_on(local_decl const & d, metavar_context const & mctx, unsigned num, expr const * locals);
bool depends_on(expr const & e, metavar_context const & mctx, buffer<expr> const & locals);
bool depends_on(local_decl const & d, metavar_context const & mctx, buffer<expr> const & locals);
/* Similar to depends_on(expr const & e, metavar_context const & mctx, unsigned num, expr const * locals), but it
will also visit the value v of local definitions (x : t := v) if x occurs in e (directly or indirectly). */
bool depends_on(expr const & e, metavar_context const & mctx, local_context const & lctx, unsigned num, expr const * locals);
inline bool depends_on(expr const & e, metavar_context const & mctx, local_context const & lctx, expr const & local) {
return depends_on(e, mctx, lctx, 1, &local);
}
/* Create an unieq local_decl name.
This is a low-level function. The high-level methods
at local_context use this function internally. */
name mk_local_decl_name();
class metavar_context;
/* Extend kernel local context object with support for generating "unused" user-names and
"freezing" local instances. */
class local_context : public local_ctx {
friend class type_context_old;
local_context remove(buffer<expr> const & locals) const;
expr mk_local_decl(name const & n, name const & un, expr const & type,
optional<expr> const & value, binder_info bi);
local_decl mk_local_decl_core(name const & n, name const & un, expr const & type, binder_info bi);
local_decl mk_local_decl_core(name const & n, name const & un, expr const & type, expr const & value);
unsigned num_indices() const;
optional<local_decl> get_decl_at(unsigned idx) const;
public:
local_context() {}
explicit local_context(obj_arg o):local_ctx(o) {}
local_context(b_obj_arg o, bool):local_ctx(o, true) {}
expr mk_local_decl(expr const & type, binder_info bi = mk_binder_info());
expr mk_local_decl(expr const & type, expr const & value);
expr mk_local_decl(name const & un, expr const & type, binder_info bi = mk_binder_info());
expr mk_local_decl(name const & un, expr const & type, expr const & value);
/* Low-level version of the methods above.
\pre `n` was created using mk_local_decl_name
\pre there is no local_decl named `n` in this local_context. */
expr mk_local_decl(name const & n, name const & un, expr const & type, binder_info bi = mk_binder_info());
expr mk_local_decl(name const & n, name const & un, expr const & type, expr const & value);
/** \brief Return the most recently added local_decl \c d s.t. d.get_user_name() == n
\remark This method is used to implement tactics such as 'revert'. */
optional<local_decl> find_local_decl_from_user_name(name const & n) const;
optional<local_decl> find_last_local_decl() const;
local_decl get_last_local_decl() const;
/** \brief Execute fn for each local declaration created after \c d. */
void for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const;
/** \brief Return a non-none iff other local decls depends on \c d. If the result is not none,
then it is the name of the local decl that depends on d.
\pre \c d is in this local context. */
optional<local_decl> has_dependencies(local_decl const & d, metavar_context const & mctx) const;
/** \brief Return an unused hypothesis "user name" with the given prefix, the suffix is an
unsigned >= idx. */
name get_unused_name(name const & prefix, unsigned & idx) const;
name get_unused_name(name const & suggestion) const;
bool uses_user_name(name const & n) const;
/** \brief Return true iff all locals in this context are in the set \c ls. */
bool is_subset_of(name_set const & ls) const;
/** \brief Return true iff all locals in this context are also in \c ctx. */
bool is_subset_of(local_context const & ctx) const;
void pop_local_decl();
/** \brief Traverse local declarations based on the order they were created */
void for_each(std::function<void(local_decl const &)> const & fn) const;
optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
optional<local_decl> back_find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
/** \brief We say a local context is well-formed iff all local declarations only
contain local_decl references that were defined before them.
\remark This method is for debugging purposes. */
bool well_formed() const;
/** \brief Return true iff \c e is well-formed with respect to this local context.
That is, all local_decl references in \c e are defined in this context. */
bool well_formed(expr const & e) const;
format pp(formatter const & fmt) const; // NOLINT
/** \brief Replaced assigned metavariables with their values.
This method is a little bit hackish since it reuses the names and ids of
the existing local_decls. So, it may affect cached information.
This method is mainly used in the elaborator for reporting errors,
and for instantiating metavariables created by the elaborator before
invoking the tactic framework. */
local_context instantiate_mvars(metavar_context & ctx) const;
/** \brief Erase inaccessible annotations from the local context.
This function is defined in the file library/equations_compiler/util.h.
It is a little bit hackish (like instantiate_mvars) since it reuses the names
and ids of existing local_decls. So, it may affect cached information.
This function is used in the elaborator before invoking the tactic framework. */
friend local_context erase_inaccessible_annotations(local_context const & lctx);
};
/** \brief Return true iff `e` contains a local_decl_ref that contains a value */
bool contains_let_local_decl(local_context const & lctx, expr const & e);
/** \brief Expand all local_decl_refs (that have values) in `e` */
expr zeta_expand(local_context const & lctx, expr const & e);
void initialize_local_context();
void finalize_local_context();
}

29
stage0/src/library/local_instances.h generated
View file

@ -1,29 +0,0 @@
/*
Copyright (c) 2018 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/expr.h"
namespace lean {
class local_instance {
name m_class_name;
expr m_local;
public:
local_instance(name const & n, expr const & e):
m_class_name(n), m_local(e) {}
name const & get_class_name() const { return m_class_name; }
expr const & get_local() const { return m_local; }
friend bool operator==(local_instance const & l1, local_instance const & l2) {
return local_name(l1.m_local) == local_name(l2.m_local);
}
};
inline bool operator!=(local_instance const & l1, local_instance const & l2) {
return !(l1 == l2);
}
typedef list<local_instance> local_instances;
}

376
stage0/src/library/metavar_context.cpp generated
View file

@ -1,376 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/fresh_name.h"
#include "util/array_ref.h"
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
#include "library/metavar_util.h"
#include "library/metavar_context.h"
#include "library/idx_metavar.h"
namespace lean {
static name * g_meta_prefix;
static expr * g_dummy_type;
extern "C" object * lean_mk_metavar_decl(object * user_name, object * lctx, object * type, object * depth, object * local_insts, uint8 k);
metavar_decl::metavar_decl(name const & user_name, local_context const & lctx, expr const & type):
object_ref(lean_mk_metavar_decl(user_name.to_obj_arg(), lctx.to_obj_arg(), type.to_obj_arg(), nat(0).to_obj_arg(), box(0), 0)) {
}
metavar_decl::metavar_decl():
metavar_decl(name(), local_context(), expr()) {}
static expr mk_meta_ref(name const & n) {
return mk_metavar(n);
}
bool is_metavar_decl_ref(level const & u) {
return is_mvar(u) && is_prefix_of(*g_meta_prefix, mvar_id(u));
}
bool is_metavar_decl_ref(expr const & e) {
return is_mvar(e) && !is_idx_metavar(e);
}
name get_metavar_decl_ref_suffix(level const & u) {
lean_assert(is_metavar_decl_ref(u));
return mvar_id(u).replace_prefix(*g_meta_prefix, name());
}
name get_metavar_decl_ref_suffix(expr const & e) {
lean_assert(is_metavar_decl_ref(e));
return mvar_name(e).replace_prefix(*g_meta_prefix, name());
}
// Hack for interfacing with new DelayedMVarAssignment
typedef array_ref<expr> array_expr;
static inline array_expr to_array_expr(exprs const & locals) {
buffer<expr> tmp;
to_buffer(locals, tmp);
return array_expr(tmp);
}
// Hack for interfacing with new DelayedMVarAssignment
static inline exprs to_exprs(array_expr const & locals) {
exprs r;
size_t i = locals.size();
while (i > 0) {
--i;
r = cons(locals[i], r);
}
return r;
}
metavar_context::delayed_assignment::delayed_assignment(local_context const & lctx, exprs const & locals, expr const & v):
object_ref(mk_cnstr(0, lctx, to_array_expr(locals), v)) {
}
metavar_context::delayed_assignment::delayed_assignment():
delayed_assignment(local_context(), exprs(), expr()) {
}
exprs metavar_context::delayed_assignment::get_locals() const {
return to_exprs(static_cast<array_expr const &>(cnstr_get_ref(raw(), 1)));
}
// TODO(Leo): fix this
static name mk_meta_decl_name() {
return mk_tagged_fresh_name(*g_meta_prefix);
}
extern "C" object* lean_mk_metavar_ctx(object*);
extern "C" object* lean_metavar_ctx_mk_decl(object*, object*, object*, object*, object*, object*, uint8);
extern "C" object* lean_metavar_ctx_find_decl(object*, object*);
extern "C" object* lean_metavar_ctx_assign_level(object*, object*, object*);
extern "C" object* lean_metavar_ctx_assign_expr(object*, object*, object*);
extern "C" object* lean_metavar_ctx_assign_delayed(object*, object*, object*, object*, object*);
extern "C" object* lean_metavar_ctx_get_level_assignment(object*, object*);
extern "C" object* lean_metavar_ctx_get_expr_assignment(object*, object*);
extern "C" object* lean_metavar_ctx_get_delayed_assignment(object*, object*);
extern "C" uint8 lean_metavar_ctx_is_level_assigned(object*, object*);
extern "C" uint8 lean_metavar_ctx_is_expr_assigned(object*, object*);
extern "C" uint8 lean_metavar_ctx_is_delayed_assigned(object*, object*);
extern "C" object* lean_metavar_ctx_erase_delayed(object*, object*);
metavar_context::metavar_context():
object_ref(lean_mk_metavar_ctx(box(0))) {
}
bool metavar_context::is_assigned(level const & l) const {
lean_assert(is_metavar_decl_ref(l));
return lean_metavar_ctx_is_level_assigned(to_obj_arg(), mvar_id(l).to_obj_arg());
}
bool metavar_context::is_assigned(expr const & m) const {
lean_assert(is_metavar_decl_ref(m));
return lean_metavar_ctx_is_expr_assigned(to_obj_arg(), mvar_name(m).to_obj_arg());
}
bool metavar_context::is_delayed_assigned(expr const & m) const {
lean_assert(is_metavar_decl_ref(m));
return lean_metavar_ctx_is_delayed_assigned(to_obj_arg(), mvar_name(m).to_obj_arg());
}
level metavar_context::mk_univ_metavar_decl() {
// TODO(Leo): should use name_generator
return mk_univ_mvar(mk_meta_decl_name());
}
expr metavar_context::mk_metavar_decl(name const & user_name, local_context const & lctx, expr const & type) {
// TODO(Leo): should use name_generator
name n = mk_meta_decl_name();
m_obj = lean_metavar_ctx_mk_decl(m_obj, n.to_obj_arg(), user_name.to_obj_arg(), lctx.to_obj_arg(), array_mk_empty(), head_beta_reduce(type).to_obj_arg(), false);
lean_assert(find_metavar_decl(mk_meta_ref(n)));
return mk_meta_ref(n);
}
optional<metavar_decl> metavar_context::find_metavar_decl(expr const & e) const {
lean_assert(is_metavar_decl_ref(e));
return to_optional<metavar_decl>(lean_metavar_ctx_find_decl(to_obj_arg(), mvar_name(e).to_obj_arg()));
}
metavar_decl metavar_context::get_metavar_decl(expr const & e) const {
if (auto r = find_metavar_decl(e))
return *r;
else
throw exception("unknown metavariable");
}
optional<local_decl> metavar_context::find_local_decl(expr const & mvar, name const & n) const {
auto mdecl = find_metavar_decl(mvar);
if (!mdecl) return optional<local_decl>();
return mdecl->get_context().find_local_decl(n);
}
local_decl metavar_context::get_local_decl(expr const & mvar, name const & n) const {
return get_metavar_decl(mvar).get_context().get_local_decl(n);
}
expr metavar_context::get_local(expr const & mvar, name const & n) const {
return get_local_decl(mvar, n).mk_ref();
}
void metavar_context::assign(level const & u, level const & l) {
m_obj = lean_metavar_ctx_assign_level(m_obj, mvar_id(u).to_obj_arg(), l.to_obj_arg());
lean_assert(is_assigned(u));
}
void metavar_context::assign(expr const & e, expr const & v) {
lean_assert(!is_delayed_assigned(e));
m_obj = lean_metavar_ctx_assign_expr(m_obj, mvar_name(e).to_obj_arg(), v.to_obj_arg());
lean_assert(is_assigned(e));
}
void metavar_context::assign_delayed(expr const & e, local_context const & lctx, exprs const & locals, expr const & v) {
m_obj = lean_metavar_ctx_assign_delayed(m_obj, mvar_name(e).to_obj_arg(), lctx.to_obj_arg(), to_array_expr(locals).steal(), v.to_obj_arg());
lean_assert(is_delayed_assigned(e));
}
optional<level> metavar_context::get_assignment(level const & l) const {
lean_assert(is_metavar_decl_ref(l));
return to_optional<level>(lean_metavar_ctx_get_level_assignment(to_obj_arg(), mvar_id(l).to_obj_arg()));
}
optional<expr> metavar_context::get_assignment(expr const & e) const {
lean_assert(is_metavar_decl_ref(e));
return to_optional<expr>(lean_metavar_ctx_get_expr_assignment(to_obj_arg(), mvar_name(e).to_obj_arg()));
}
optional<metavar_context::delayed_assignment> metavar_context::get_delayed_assignment(expr const & e) const {
lean_assert(is_metavar_decl_ref(e));
return to_optional<metavar_context::delayed_assignment>(lean_metavar_ctx_get_delayed_assignment(to_obj_arg(), mvar_name(e).to_obj_arg()));
}
struct metavar_context::interface_impl {
metavar_context & m_ctx;
/* We store the set of delayed assigned variables that have been found to prevent their values
from being visited over and over again. */
name_set m_delayed_found;
interface_impl(metavar_context const & ctx):m_ctx(const_cast<metavar_context&>(ctx)) {}
static bool is_mvar(level const & l) { return is_metavar_decl_ref(l); }
bool is_assigned(level const & l) const { return m_ctx.is_assigned(l); }
optional<level> get_assignment(level const & l) const { return m_ctx.get_assignment(l); }
void assign(level const & u, level const & v) { m_ctx.assign(u, v); }
static bool is_mvar(expr const & e) { return is_metavar_decl_ref(e); }
optional<expr> check_delayed_assignment(expr const & e) {
lean_assert(is_metavar_decl_ref(e));
optional<delayed_assignment> d = m_ctx.get_delayed_assignment(e);
if (!d)
return none_expr();
if (m_delayed_found.contains(mvar_name(e)))
return none_expr();
/* Remark: a delayed assignment can be transformed in a regular assignment
as soon as all metavariables occurring in the assigned value have
been assigned. */
expr new_v = m_ctx.instantiate_mvars(d->get_val());
if (has_expr_metavar(new_v)) {
m_delayed_found.insert(mvar_name(e));
if (!is_eqp(new_v, d->get_val()))
m_ctx.assign_delayed(e, d->get_lctx(), d->get_locals(), new_v);
return none_expr();
} else {
m_ctx.m_obj = lean_metavar_ctx_erase_delayed(m_ctx.m_obj, mvar_name(e).to_obj_arg());
lean_assert(!m_ctx.is_delayed_assigned(e));
buffer<expr> locals;
to_buffer(d->get_locals(), locals);
new_v = abstract(new_v, locals.size(), locals.data());
unsigned i = locals.size();
while (i > 0) {
--i;
local_decl decl = d->get_lctx().get_local_decl(locals[i]);
expr type = abstract(decl.get_type(), i, locals.data());
if (optional<expr> letval = decl.get_value()) {
letval = abstract(*letval, i, locals.data());
new_v = mk_let(decl.get_user_name(), type, *letval, new_v);
} else {
new_v = mk_lambda(decl.get_user_name(), type, new_v, decl.get_info());
}
}
m_ctx.assign(e, new_v);
return some_expr(new_v);
}
}
bool is_assigned(expr const & e) const {
lean_assert(is_metavar_decl_ref(e));
return m_ctx.is_assigned(e) || const_cast<metavar_context::interface_impl*>(this)->check_delayed_assignment(e);
}
optional<expr> get_assignment(expr const & e) const {
if (optional<expr> v = m_ctx.get_assignment(e))
return v;
if (optional<expr> v = const_cast<metavar_context::interface_impl*>(this)->check_delayed_assignment(e))
return v;
return none_expr();
}
void assign(expr const & m, expr const & v) { m_ctx.assign(m, v); }
bool in_tmp_mode() const { return false; }
};
bool metavar_context::has_assigned(level const & l) const {
return ::lean::has_assigned(interface_impl(*this), l);
}
bool metavar_context::has_assigned(expr const & e) const {
return ::lean::has_assigned(interface_impl(*this), e);
}
level metavar_context::instantiate_mvars(level const & l) {
interface_impl impl(*this);
return ::lean::instantiate_mvars(impl, l);
}
expr metavar_context::instantiate_mvars(expr const & e) {
interface_impl impl(*this);
return ::lean::instantiate_mvars(impl, e);
}
void metavar_context::instantiate_mvars_at_type_of(expr const & m) {
metavar_decl d = get_metavar_decl(m);
expr type = d.get_type();
expr new_type = instantiate_mvars(type);
if (new_type != type) {
m_obj = lean_metavar_ctx_mk_decl(m_obj,
mvar_name(m).to_obj_arg(),
d.get_user_name().to_obj_arg(),
d.get_context().to_obj_arg(),
array_mk_empty(),
new_type.to_obj_arg(),
false);
}
}
template<typename C>
static bool well_formed_metavar_occs(expr const & e, C const & ds, metavar_context const & ctx) {
bool ok = true;
for_each(e, [&](expr const & e, unsigned) {
if (!ok) return false;
if (!has_expr_metavar(e)) return false;
if (is_metavar_decl_ref(e)) {
if (auto d = ctx.find_metavar_decl(e)) {
if (!d->get_context().is_subset_of(ds)) {
/* invalid metavariable context */
ok = false;
return false;
}
} else {
/* undefined metavariable */
ok = false;
return false;
}
}
return true;
});
return ok;
}
bool metavar_context::well_formed(local_context const & ctx) const {
bool ok = true;
name_set visited;
ctx.for_each([&](local_decl const & d) {
if (!well_formed_metavar_occs(d.get_type(), visited, *this)) {
ok = false;
lean_unreachable();
}
if (auto v = d.get_value()) {
if (!well_formed_metavar_occs(*v, visited, *this)) {
ok = false;
lean_unreachable();
}
}
visited.insert(d.get_name());
});
return ok;
}
bool metavar_context::well_formed(local_context const & ctx, expr const & e) const {
return well_formed_metavar_occs(e, ctx, *this);
}
bool well_formed(local_context const & lctx, metavar_context const & mctx) {
if (!lctx.well_formed()) {
lean_unreachable();
return false;
}
if (!mctx.well_formed(lctx)) {
lean_unreachable();
return false;
}
return true;
}
bool well_formed(local_context const & lctx, metavar_context const & mctx, expr const & e) {
if (!lctx.well_formed(e)) {
lean_unreachable();
return false;
}
if (!mctx.well_formed(lctx, e)) {
lean_unreachable();
return false;
}
return true;
}
void initialize_metavar_context() {
g_meta_prefix = new name("_mlocal");
mark_persistent(g_meta_prefix->raw());
register_name_generator_prefix(*g_meta_prefix);
g_dummy_type = new expr(mk_constant(name::mk_internal_unique_name()));
mark_persistent(g_dummy_type->raw());
}
void finalize_metavar_context() {
delete g_meta_prefix;
delete g_dummy_type;
}
}

141
stage0/src/library/metavar_context.h generated
View file

@ -1,141 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/local_context.h"
namespace lean {
class metavar_decl : public object_ref {
public:
metavar_decl();
metavar_decl(name const & user_name, local_context const & ctx, expr const & type);
metavar_decl(metavar_decl const & other):object_ref(other) {}
metavar_decl(metavar_decl && other):object_ref(other) {}
metavar_decl(obj_arg o):object_ref(o) {}
metavar_decl(b_obj_arg o, bool):object_ref(o, true) {}
metavar_decl & operator=(metavar_decl const & other) { object_ref::operator=(other); return *this; }
metavar_decl & operator=(metavar_decl && other) { object_ref::operator=(other); return *this; }
name const & get_user_name() const { return static_cast<name const &>(cnstr_get_ref(raw(), 0)); }
local_context const & get_context() const { return static_cast<local_context const &>(cnstr_get_ref(raw(), 1)); }
expr const & get_type() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
};
bool is_metavar_decl_ref(level const & l);
bool is_metavar_decl_ref(expr const & e);
name get_metavar_decl_ref_suffix(level const & l);
name get_metavar_decl_ref_suffix(expr const & e);
class metavar_context : public object_ref {
class delayed_assignment : public object_ref {
public:
delayed_assignment();
delayed_assignment(local_context const & lctx, exprs const & locals, expr const & v);
delayed_assignment(delayed_assignment const & other):object_ref(other) {}
delayed_assignment(delayed_assignment && other):object_ref(other) {}
delayed_assignment(obj_arg o):object_ref(o) {}
delayed_assignment(b_obj_arg o, bool):object_ref(o, true) {}
delayed_assignment & operator=(delayed_assignment const & other) { object_ref::operator=(other); return *this; }
delayed_assignment & operator=(delayed_assignment && other) { object_ref::operator=(other); return *this; }
local_context const & get_lctx() const { return static_cast<local_context const &>(cnstr_get_ref(raw(), 0)); }
exprs get_locals() const;
expr const & get_val() const { return static_cast<expr const &>(cnstr_get_ref(raw(), 2)); }
};
struct interface_impl;
friend struct interface_impl;
public:
metavar_context();
explicit metavar_context(obj_arg o):object_ref(o) {}
metavar_context(b_obj_arg o, bool):object_ref(o, true) {}
metavar_context(metavar_context const & other):object_ref(other) {}
metavar_context(metavar_context && other):object_ref(other) {}
metavar_context & operator=(metavar_context const & other) { object_ref::operator=(other); return *this; }
metavar_context & operator=(metavar_context && other) { object_ref::operator=(other); return *this; }
level mk_univ_metavar_decl();
expr mk_metavar_decl(name const & user_name, local_context const & ctx, expr const & type);
expr mk_metavar_decl(local_context const & ctx, expr const & type) {
return mk_metavar_decl(name(), ctx, type);
}
optional<metavar_decl> find_metavar_decl(expr const & mvar) const;
metavar_decl get_metavar_decl(expr const & mvar) const;
/** \brief Return the local_decl for `n` in the local context for the metavariable `mvar`
\pre is_metavar(mvar) */
optional<local_decl> find_local_decl(expr const & mvar, name const & n) const;
local_decl get_local_decl(expr const & mvar, name const & n) const;
/** \brief Return the local_decl_ref for `n` in the local context for the metavariable `mvar`
\pre is_metavar(mvar)
\pre find_metavar_decl(mvar)
\pre find_metavar_decl(mvar)->get_context().get_local_decl(n) */
expr get_local(expr const & mvar, name const & n) const;
bool is_assigned(level const & l) const;
bool is_assigned(expr const & m) const;
bool is_delayed_assigned(expr const & m) const;
void assign(level const & u, level const & l);
void assign(expr const & e, expr const & v);
/*
Add the delayed assignment
```
e := Fun(locals, v)
```
This kind of assignment is created by the `intro` tactic.
The term `v` contains metavariables that have not been instantiated yet.
So, `abstract_locals(locals, v)` would not work correctly.
We also cannot create an auxiliary metavariable in this case since it would "solve" the new goal
created by the `intro` tactic.
\pre is_metavar_decl_ref(e)
*/
void assign_delayed(expr const & e, local_context const & lctx, exprs const & locals, expr const & v);
level instantiate_mvars(level const & l);
expr instantiate_mvars(expr const & e);
bool has_assigned(level const & l) const;
bool has_assigned(levels const & ls) const;
bool has_assigned(expr const & e) const;
optional<level> get_assignment(level const & l) const;
optional<expr> get_assignment(expr const & e) const;
optional<delayed_assignment> get_delayed_assignment(expr const & e) const;
/** \brief Instantiate the assigned meta-variables in the type of \c m
\pre get_metavar_decl(m) is not none */
void instantiate_mvars_at_type_of(expr const & m);
/** \brief Return true iff \c ctx is well-formed with respect to this metavar context.
That is, every metavariable ?M occurring in \c ctx is declared here, and
for every metavariable ?M occurring in a declaration \c d, the context of ?M
must be a subset of the declarations declared *before* \c d.
\remark This method is used for debugging purposes. */
bool well_formed(local_context const & ctx) const;
/** \brief Return true iff all metavariables ?M in \c e are declared in this metavar context,
and context of ?M is a subset of \c ctx */
bool well_formed(local_context const & ctx, expr const & e) const;
};
/** \brief Check whether the local context lctx is well-formed and well-formed with respect to \c mctx.
\remark This procedure is used for debugging purposes. */
bool well_formed(local_context const & lctx, metavar_context const & mctx);
/** \brief Check whether \c e is well-formed with respect to \c lctx and \c mctx. */
bool well_formed(local_context const & lctx, metavar_context const & mctx, expr const & e);
void initialize_metavar_context();
void finalize_metavar_context();
}

199
stage0/src/library/metavar_util.h generated
View file

@ -1,199 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/instantiate.h"
#include "library/replace_visitor.h"
namespace lean {
/*
Helper functions for metavariable assignments.
The template parameter CTX must be an object that
provides the following API:
bool is_mvar(level const & l) const;
bool is_assigned(level const & l) const;
optional<level> get_assignment(level const & l) const;
void assign(level const & u, level const & v);
bool is_mvar(expr const & e) const;
bool is_assigned(expr const & e) const;
optional<expr> get_assignment(expr const & e) const;
void assign(expr const & m, expr const & v);
bool in_tmp_mode() const;
*/
template<typename CTX>
bool has_assigned(CTX const & ctx, level const & l) {
if (!has_mvar(l))
return false;
bool found = false;
for_each(l, [&](level const & l) {
if (!has_mvar(l))
return false; // stop search
if (found)
return false; // stop search
if (ctx.is_mvar(l) && ctx.is_assigned(l)) {
found = true;
return false; // stop search
}
return true; // continue search
});
return found;
}
template<typename CTX>
bool has_assigned(CTX const & ctx, levels const & ls) {
for (level const & l : ls) {
if (has_assigned(ctx, l))
return true;
}
return false;
}
template<typename CTX>
bool has_assigned(CTX const & ctx, expr const & e) {
if (!has_expr_metavar(e) && !has_univ_metavar(e))
return false;
bool found = false;
for_each(e, [&](expr const & e, unsigned) {
if (!has_expr_metavar(e) && !has_univ_metavar(e))
return false; // stop search
if (found)
return false; // stop search
if ((ctx.is_mvar(e) && ctx.is_assigned(e)) ||
(is_constant(e) && has_assigned(ctx, const_levels(e))) ||
(is_sort(e) && has_assigned(ctx, sort_level(e)))) {
found = true;
return false; // stop search
}
if (is_metavar(e))
return false; // do not search type
return true; // continue search
});
return found;
}
template<typename CTX>
level instantiate_mvars(CTX & ctx, level const & l) {
if (!has_assigned(ctx, l))
return l;
return replace(l, [&](level const & l) {
if (!has_mvar(l)) {
return some_level(l);
} else if (ctx.is_mvar(l)) {
if (auto v1 = ctx.get_assignment(l)) {
level v2 = instantiate_mvars(ctx, *v1);
if (*v1 != v2) {
if (!ctx.in_tmp_mode())
ctx.assign(l, v2);
return some_level(v2);
} else {
return some_level(*v1);
}
}
}
return none_level();
});
}
template<typename CTX>
class instantiate_mvars_fn : public replace_visitor {
CTX & m_ctx;
level visit_level(level const & l) {
return instantiate_mvars(m_ctx, l);
}
levels visit_levels(levels const & ls) {
return map_reuse(ls, [&](level const & l) { return visit_level(l); });
}
virtual expr visit_sort(expr const & s) override {
return update_sort(s, visit_level(sort_level(s)));
}
virtual expr visit_constant(expr const & c) override {
return update_constant(c, visit_levels(const_levels(c)));
}
virtual expr visit_local(expr const & e) override {
return update_local(e, visit(local_type(e)));
}
virtual expr visit_meta(expr const & m) override {
if (m_ctx.is_mvar(m)) {
if (auto v1 = m_ctx.get_assignment(m)) {
if (!has_metavar(*v1)) {
return *v1;
} else {
expr v2 = visit(*v1);
if (!m_ctx.in_tmp_mode() && v2 != *v1)
m_ctx.assign(m, v2);
return v2;
}
} else {
return m;
}
} else {
return m;
}
}
virtual expr visit_app(expr const & e) override {
buffer<expr> args;
expr const & f = get_app_rev_args(e, args);
if (m_ctx.is_mvar(f)) {
if (auto v = m_ctx.get_assignment(f)) {
expr new_app = apply_beta(*v, args.size(), args.data());
if (has_metavar(new_app))
return visit(new_app);
else
return new_app;
}
}
expr new_f = visit(f);
buffer<expr> new_args;
bool modified = !is_eqp(new_f, f);
for (expr const & arg : args) {
expr new_arg = visit(arg);
if (!is_eqp(arg, new_arg))
modified = true;
new_args.push_back(new_arg);
}
if (!modified)
return e;
else
return mk_rev_app(new_f, new_args);
}
virtual expr visit_mdata(expr const & e) override {
return update_mdata(e, visit(mdata_expr(e)));
}
virtual expr visit(expr const & e) override {
if (!has_expr_metavar(e) && !has_univ_metavar(e))
return e;
else
return replace_visitor::visit(e);
}
public:
instantiate_mvars_fn(CTX & ctx):m_ctx(ctx) {}
expr operator()(expr const & e) {
return visit(e);
}
};
template<typename CTX>
expr instantiate_mvars(CTX & ctx, expr const & e) {
if (!has_assigned(ctx, e))
return e;
expr r = instantiate_mvars_fn<CTX>(ctx)(e);
lean_assert(!has_assigned(ctx, r));
return r;
}
}

43
stage0/src/library/type_context.cpp generated
View file

@ -18,11 +18,9 @@ Author: Leonardo de Moura
#include "library/class.h"
#include "library/pp_options.h"
#include "library/annotation.h"
#include "library/idx_metavar.h"
#include "library/reducible.h"
#include "library/suffixes.h"
#include "library/constants.h"
#include "library/metavar_util.h"
#include "library/exception.h"
#include "library/type_context.h"
#include "library/locals.h"
@ -33,54 +31,17 @@ Author: Leonardo de Moura
namespace lean {
/* =====================
type_context_old::tmp_locals
===================== */
type_context_old::tmp_locals::~tmp_locals() {
for (unsigned i = 0; i < m_locals.size(); i++)
m_ctx.pop_local();
}
/* =====================
type_context_old
===================== */
type_context_old::type_context_old(environment const & env, options const &, metavar_context const & mctx,
local_context const & lctx, transparency_mode):
m_env(env),
m_mctx(mctx), m_lctx(lctx) {
type_context_old::type_context_old(environment const & env, options const &, transparency_mode):
m_env(env) {
}
type_context_old::~type_context_old() {
}
/** \brief Helper class for pretty printing terms that contain local_decl_ref's and metavar_decl_ref's */
class pp_ctx {
type_context_old m_ctx;
formatter m_fmt;
public:
pp_ctx(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx):
m_ctx(env, opts, mctx, lctx),
m_fmt(get_global_ios().get_formatter_factory()(env, opts, m_ctx)) {}
format pp(expr const & e) {
return m_fmt(m_ctx.instantiate_mvars(e));
}
};
std::function<format(expr const &)>
mk_pp_ctx(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx) {
auto pp_fn = std::make_shared<pp_ctx>(env, opts, mctx, lctx);
return [=](expr const & e) { // NOLINT
metavar_context mctx_tmp(mctx);
return pp_fn->pp(mctx_tmp.instantiate_mvars(e));
};
}
std::function<format(expr const &)>
mk_pp_ctx(type_context_old const & ctx) {
return mk_pp_ctx(ctx.env(), ctx.get_options(), ctx.mctx(), ctx.lctx());
}
void initialize_type_context() {
}

120
stage0/src/library/type_context.h generated
View file

@ -11,13 +11,10 @@ Author: Leonardo de Moura
#include "util/lbool.h"
#include "util/fresh_name.h"
#include "kernel/environment.h"
#include "library/idx_metavar.h"
#include "library/projection.h"
#include "library/metavar_context.h"
#include "library/abstract_type_context.h"
#include "library/exception.h"
#include "library/expr_pair.h"
#include "library/local_instances.h"
namespace lean {
enum class transparency_mode { All = 0, Semireducible, Reducible };
@ -51,37 +48,11 @@ class type_context_old : public abstract_type_context {
typedef buffer<optional<level>> tmp_uassignment;
typedef buffer<expr> tmp_etype;
typedef buffer<optional<expr>> tmp_eassignment;
typedef buffer<metavar_context> mctx_stack;
enum class tmp_trail_kind { Level, Expr };
typedef buffer<pair<tmp_trail_kind, unsigned>> tmp_trail;
friend struct instance_synthesizer;
struct scope_data {
metavar_context m_mctx;
unsigned m_tmp_uassignment_sz;
unsigned m_tmp_eassignment_sz;
unsigned m_tmp_trail_sz;
scope_data(metavar_context const & mctx, unsigned usz, unsigned esz, unsigned tsz):
m_mctx(mctx), m_tmp_uassignment_sz(usz), m_tmp_eassignment_sz(esz), m_tmp_trail_sz(tsz) {}
};
public:
struct tmp_data {
tmp_uassignment & m_uassignment;
tmp_etype & m_etype;
tmp_eassignment & m_eassignment;
/* m_tmp_mvar_local_context contains m_lctx when tmp mode is activated.
This is the context for all temporary meta-variables. */
local_context m_mvar_lctx;
/* undo/trail stack for m_tmp_uassignment/m_tmp_eassignment */
tmp_trail m_trail;
tmp_data(tmp_uassignment & uassignment, tmp_etype & etype, tmp_eassignment & eassignment, local_context const & lctx):
m_uassignment(uassignment), m_etype(etype), m_eassignment(eassignment), m_mvar_lctx(lctx) {}
};
private:
typedef buffer<scope_data> scopes;
environment m_env;
metavar_context m_mctx;
local_context m_lctx;
local_instances m_local_instances;
/* We only cache results when m_used_assignment is false */
bool m_used_assignment{false};
transparency_mode m_transparency_mode;
@ -90,8 +61,6 @@ private:
/* m_is_def_eq_depth is only used for tracing purposes */
unsigned m_is_def_eq_depth{0};
/* Stack of backtracking point (aka scope) */
scopes m_scopes;
tmp_data * m_tmp_data{nullptr};
/* Higher-order unification approximation options.
Modules that use approximations:
@ -147,15 +116,9 @@ private:
optional<expr> reduce_projection_core(optional<projection_info> const & info, expr const & e);
public:
type_context_old(environment const & env, options const & o, metavar_context const & mctx, local_context const & lctx,
transparency_mode m = transparency_mode::Reducible);
type_context_old(environment const & env, options const & o, local_context const & lctx,
transparency_mode m = transparency_mode::Reducible):
type_context_old(env, o, metavar_context(), lctx, m) {}
type_context_old(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible);
explicit type_context_old(environment const & env, transparency_mode m = transparency_mode::Reducible):
type_context_old(env, options(), metavar_context(), local_context(), m) {}
type_context_old(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible):
type_context_old(env, o, metavar_context(), local_context(), m) {}
type_context_old(env, options(), m) {}
virtual ~type_context_old();
type_context_old & operator=(type_context_old const &) = delete;
@ -167,28 +130,11 @@ public:
// TODO(Leo): avoid ::lean::mk_fresh_name
virtual name next_name() override { return ::lean::mk_fresh_name(); }
virtual optional<name> get_local_pp_name(expr const & e) override {
if (optional<local_decl> decl = m_lctx.find_local_decl(e)) {
return optional<name>(decl->get_user_name());
}
return optional<name>();
virtual optional<name> get_local_pp_name(expr const &) override {
lean_unreachable();
}
virtual local_context const & lctx() const override { return m_lctx; }
virtual metavar_context const & mctx() const override { return m_mctx; }
expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
optional<metavar_decl> find_metavar_decl(expr const & mvar) const { return m_mctx.find_metavar_decl(mvar); }
level mk_univ_metavar_decl() { return m_mctx.mk_univ_metavar_decl(); }
name get_unused_name(name const & prefix, unsigned & idx) const { return m_lctx.get_unused_name(prefix, idx); }
name get_unused_name(name const & suggestion) const { return m_lctx.get_unused_name(suggestion); }
/* note: mctx must be a descendant of m_mctx */
void set_mctx(metavar_context const & mctx) { m_mctx = mctx; }
/* note: env must be a descendant of m_env */
void set_env(environment const & env);
/* Store the current local instances in the local context.
@ -233,7 +179,6 @@ public:
}
virtual bool is_def_eq(expr const &, expr const &) override { lean_unreachable(); }
bool is_def_eq_at(local_context const & lctx, expr const & a, expr const & b);
bool match(expr const & e1, expr const & e2) {
flet<bool> update_left(m_update_left, true);
@ -325,13 +270,6 @@ public:
*/
expr revert(buffer<expr> & locals, expr const & mvar, bool preserve_locals_order);
expr mk_lambda(local_context const & lctx, buffer<expr> const & locals, expr const & e);
expr mk_pi(local_context const & lctx, buffer<expr> const & locals, expr const & e);
expr mk_lambda(local_context const & lctx, expr const & local, expr const & e);
expr mk_pi(local_context const & lctx, expr const & local, expr const & e);
expr mk_lambda(local_context const & lctx, std::initializer_list<expr> const & locals, expr const & e);
expr mk_pi(local_context const & lctx, std::initializer_list<expr> const & locals, expr const & e);
expr mk_lambda(buffer<expr> const & locals, expr const & e);
expr mk_pi(buffer<expr> const & locals, expr const & e);
expr mk_lambda(expr const & local, expr const & e);
@ -349,7 +287,6 @@ public:
optional<expr> mk_class_instance(expr const & type);
optional<expr> mk_subsingleton_instance(expr const & type);
/* Create type class instance in a different local context */
optional<expr> mk_class_instance_at(local_context const & lctx, expr const & type);
transparency_mode mode() const { return m_transparency_mode; }
unsigned mode_idx() const { return static_cast<unsigned>(mode()); }
@ -413,33 +350,6 @@ public:
It is used when performing type class resolution and matching.
-------------------------- */
public:
struct tmp_mode_scope {
type_context_old & m_ctx;
buffer<optional<level>> m_tmp_uassignment;
buffer<expr> m_tmp_etype;
buffer<optional<expr>> m_tmp_eassignment;
tmp_data * m_old_data;
tmp_data m_data;
tmp_mode_scope(type_context_old & ctx):
m_ctx(ctx), m_old_data(ctx.m_tmp_data), m_data(m_tmp_uassignment, m_tmp_etype, m_tmp_eassignment, ctx.lctx()) {
m_ctx.m_tmp_data = &m_data;
}
~tmp_mode_scope() {
m_ctx.m_tmp_data = m_old_data;
}
};
struct tmp_mode_scope_with_data {
type_context_old & m_ctx;
tmp_data * m_old_data;
tmp_mode_scope_with_data(type_context_old & ctx, tmp_data & data):
m_ctx(ctx), m_old_data(ctx.m_tmp_data) {
m_ctx.m_tmp_data = &data;
}
~tmp_mode_scope_with_data() {
m_ctx.m_tmp_data = m_old_data;
}
};
bool in_tmp_mode() const { return m_tmp_data != nullptr; }
optional<level> get_tmp_uvar_assignment(unsigned idx) const;
optional<expr> get_tmp_mvar_assignment(unsigned idx) const;
optional<level> get_tmp_assignment(level const & l) const;
@ -478,12 +388,6 @@ private:
optional<constant_info> get_decl(name const &) { lean_unreachable(); }
private:
pair<local_context, expr> revert_core(buffer<expr> & to_revert, local_context const & ctx,
expr const & type, bool preserve_to_revert_order);
expr revert_core(buffer<expr> & to_revert, expr const & mvar, bool preserve_to_revert_order);
expr elim_mvar_deps(expr const & e, unsigned num, expr const * locals);
expr mk_binding(bool is_pi, local_context const & lctx, unsigned num_locals, expr const * locals, expr const & e);
/* ------------
Temporary metavariable assignment.
------------ */
@ -497,9 +401,6 @@ public:
bool is_mvar(level const & l) const;
/* Return true iff `e` is a regular or temporary metavar */
bool is_mvar(expr const & e) const;
bool is_regular_mvar(expr const & e) const { return is_metavar_decl_ref(e); }
bool is_tmp_mvar(level const & l) const { return is_idx_metauniv(l); }
bool is_tmp_mvar(expr const & e) const { return is_idx_metavar(e); }
/* Return true iff
1- `l` is a temporary universe metavariable and type_context_old is in tmp mode, OR
2- `l` is a regular universe metavariable an type_context_old is not in tmp_mode. */
@ -519,9 +420,6 @@ public:
expr instantiate_mvars(expr const &) { lean_unreachable(); }
/** \brief Instantiate the assigned meta-variables in the type of \c m
\pre get_metavar_decl(m) is not none */
void instantiate_mvars_at_type_of(expr const & m) {
m_mctx.instantiate_mvars_at_type_of(m);
}
/** Set the number of tmp metavars.
\pre in_tmp_mode() */
void resize_tmp_mvars(unsigned new_sz = 0);
@ -664,16 +562,6 @@ public:
friend class tmp_locals;
};
/** Create a formatting function that can 'decode' metavar_decl_refs and local_decl_refs
with declarations stored in mctx and lctx */
std::function<format(expr const &)>
mk_pp_ctx(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx);
/** Create a formatting function that can 'decode' metavar_decl_refs and local_decl_refs
with declarations stored in ctx */
std::function<format(expr const &)>
mk_pp_ctx(type_context_old const & ctx);
void initialize_type_context();
void finalize_type_context();
}

1
stage0/src/library/util.h generated
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <string>
#include "kernel/environment.h"
#include "library/expr_pair.h"
#include "library/abstract_type_context.h"
namespace lean {
/* If \c n is not in \c env, then return \c. Otherwise, find the first j >= idx s.t.