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

chore(library): rename local_context to old_local_context

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-11 11:59:11 -08:00
parent 74192b0cb8
commit 632d4fae36
14 changed files with 83 additions and 84 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/calc_proof_elaborator.cpp
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "library/unifier.h"
#include "library/reducible.h"
#include "library/metavar_closure.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
#include "library/relation_manager.h"
#include "frontends/lean/util.h"
#include "frontends/lean/info_manager.h"
@ -41,7 +41,7 @@ bool get_elaborator_calc_assistant(options const & o) {
return o.get_bool(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT);
}
static optional<pair<expr, expr>> mk_op(environment const & env, local_context & ctx, type_checker_ptr & tc,
static optional<pair<expr, expr>> mk_op(environment const & env, old_local_context & ctx, type_checker_ptr & tc,
name const & op, unsigned nunivs, unsigned nargs, std::initializer_list<expr> const & explicit_args,
constraint_seq & cs, tag g) {
levels lvls;
@ -71,7 +71,7 @@ static optional<pair<expr, expr>> mk_op(environment const & env, local_context &
return some(mk_pair(r, op_type));
}
static optional<pair<expr, expr>> apply_symmetry(environment const & env, local_context & ctx, type_checker_ptr & tc,
static optional<pair<expr, expr>> apply_symmetry(environment const & env, old_local_context & ctx, type_checker_ptr & tc,
expr const & e, expr const & e_type, constraint_seq & cs, tag g) {
buffer<expr> args;
expr const & op = get_app_args(e_type, args);
@ -84,7 +84,7 @@ static optional<pair<expr, expr>> apply_symmetry(environment const & env, local_
return optional<pair<expr, expr>>();
}
static optional<pair<expr, expr>> apply_subst(environment const & env, local_context & ctx,
static optional<pair<expr, expr>> apply_subst(environment const & env, old_local_context & ctx,
type_checker_ptr & tc, expr const & e, expr const & e_type,
expr const & pred, constraint_seq & cs, tag g) {
buffer<expr> pred_args;
@ -132,12 +132,12 @@ bool try_normalize_to_head(environment const & env, name const & h, expr & e, co
- adding subst
*/
constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
local_context const & _ctx, expr const & m, expr const & _e,
old_local_context const & _ctx, expr const & m, expr const & _e,
constraint_seq const & cs, unifier_config const & cfg,
info_manager * im, update_type_info_fn const & fn) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & _meta_type, substitution const & _s) {
local_context ctx = _ctx;
old_local_context ctx = _ctx;
expr e = _e;
substitution s = _s;
expr meta_type = _meta_type;

4
src/frontends/lean/calc_proof_elaborator.h
View file

@ -7,7 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <functional>
#include "library/unifier.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
#include "frontends/lean/info_manager.h"
namespace lean {
@ -21,7 +21,7 @@ typedef std::function<void(expr const &)> update_type_info_fn;
- adding subst
*/
constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
local_context const & ctx, expr const & m, expr const & e,
old_local_context const & ctx, expr const & m, expr const & e,
constraint_seq const & cs, unifier_config const & cfg,
info_manager * im, update_type_info_fn const & fn);

40
src/frontends/lean/elaborator.cpp
View file

@ -35,7 +35,7 @@ Author: Leonardo de Moura
#include "library/deep_copy.h"
#include "library/typed_expr.h"
#include "library/metavar_closure.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
#include "library/constants.h"
#include "library/util.h"
#include "library/choice_iterator.h"
@ -130,15 +130,15 @@ type_checker_ptr mk_coercion_to_type_checker(environment const & env) {
*/
struct elaborator::choice_expr_elaborator : public choice_iterator {
elaborator & m_elab;
local_context m_context;
local_context m_full_context;
old_local_context m_context;
old_local_context m_full_context;
bool m_in_equation_lhs;
expr m_meta;
expr m_type;
expr m_choice;
unsigned m_idx;
choice_expr_elaborator(elaborator & elab, local_context const & ctx, local_context const & full_ctx, bool in_equation_lhs,
choice_expr_elaborator(elaborator & elab, old_local_context const & ctx, old_local_context const & full_ctx, bool in_equation_lhs,
expr const & meta, expr const & type, expr const & c):
m_elab(elab), m_context(ctx), m_full_context(full_ctx), m_in_equation_lhs(in_equation_lhs), m_meta(meta),
m_type(type), m_choice(c), m_idx(get_num_choices(m_choice)) {
@ -151,8 +151,8 @@ struct elaborator::choice_expr_elaborator : public choice_iterator {
expr const & f = get_app_fn(c);
m_elab.save_identifier_info(f);
try {
flet<local_context> set1(m_elab.m_context, m_context);
flet<local_context> set2(m_elab.m_full_context, m_full_context);
flet<old_local_context> set1(m_elab.m_context, m_context);
flet<old_local_context> set2(m_elab.m_full_context, m_full_context);
flet<bool> set3(m_elab.m_in_equation_lhs, m_in_equation_lhs);
pair<expr, constraint_seq> rcs = m_elab.visit(c);
expr r = rcs.first;
@ -391,8 +391,8 @@ expr elaborator::visit_choice(expr const & e, optional<expr> const & t, constrai
// Possible optimization: try to lookahead and discard some of the alternatives.
expr m = m_full_context.mk_meta(t, e.get_tag());
register_meta(m);
local_context ctx = m_context;
local_context full_ctx = m_full_context;
old_local_context ctx = m_context;
old_local_context full_ctx = m_full_context;
bool in_equation_lhs = m_in_equation_lhs;
auto fn = [=](expr const & meta, expr const & type, substitution const & /* s */) {
return choose(std::make_shared<choice_expr_elaborator>(*this, ctx, full_ctx, in_equation_lhs, meta, type, e));
@ -529,14 +529,14 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
save_coercion_info(old_f, f);
lean_assert(is_pi(f_type));
} else {
local_context ctx = m_context;
local_context full_ctx = m_full_context;
old_local_context ctx = m_context;
old_local_context full_ctx = m_full_context;
justification j = mk_justification(f, [=](formatter const & fmt, substitution const & subst, bool) {
return pp_function_expected(fmt, substitution(subst).instantiate(f));
});
auto choice_fn = [=](expr const & meta, expr const &, substitution const &) {
flet<local_context> save1(m_context, ctx);
flet<local_context> save2(m_full_context, full_ctx);
flet<old_local_context> save1(m_context, ctx);
flet<old_local_context> save2(m_full_context, full_ctx);
list<constraints> choices = map2<constraints>(coes, [&](expr const & coe) {
expr new_f = mk_coercion_app(coe, f);
constraint_seq cs;
@ -925,8 +925,8 @@ expr elaborator::instantiate_rev_locals(expr const & a, unsigned n, expr const *
}
expr elaborator::visit_binding(expr e, expr_kind k, constraint_seq & cs) {
flet<local_context> save1(m_context, m_context);
flet<local_context> save2(m_full_context, m_full_context);
flet<old_local_context> save1(m_context, m_context);
flet<old_local_context> save2(m_full_context, m_full_context);
buffer<expr> ds, ls, es;
while (e.kind() == k) {
es.push_back(e);
@ -1546,8 +1546,8 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
justification j = mk_type_mismatch_jst(new_from, goal_domain, from_type, src);
if (!is_def_eq(from_type, goal_domain, j, cs))
throw unifier_exception(j, substitution());
flet<local_context> save1(m_context, m_context);
flet<local_context> save2(m_full_context, m_full_context);
flet<old_local_context> save1(m_context, m_context);
flet<old_local_context> save2(m_full_context, m_full_context);
m_context.add_local(new_from);
m_full_context.add_local(new_from);
expr new_goal = instantiate(binding_body(goal), new_from);
@ -1702,12 +1702,12 @@ expr elaborator::visit_checkpoint_expr(expr const & e, constraint_seq & cs) {
else
m = m_full_context.mk_meta(none_expr(), e.get_tag());
register_meta(m);
local_context ctx = m_context;
local_context full_ctx = m_full_context;
old_local_context ctx = m_context;
old_local_context full_ctx = m_full_context;
bool in_equation_lhs = m_in_equation_lhs;
auto fn = [=](expr const & meta, expr const & /* type */, substitution const & /* s */) {
flet<local_context> set1(m_context, ctx);
flet<local_context> set2(m_full_context, full_ctx);
flet<old_local_context> set1(m_context, ctx);
flet<old_local_context> set2(m_full_context, full_ctx);
flet<bool> set3(m_in_equation_lhs, in_equation_lhs);
pair<expr, constraint_seq> rcs = visit(arg);
expr r = rcs.first;

6
src/frontends/lean/elaborator.h
View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "library/expr_lt.h"
#include "library/unifier.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
#include "library/tactic/tactic.h"
#include "library/tactic/elaborate.h"
#include "frontends/lean/elaborator_context.h"
@ -36,8 +36,8 @@ class elaborator : public coercion_info_manager {
type_checker_ptr m_coercion_to_tc;
// mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
// representing the context where ?m was created.
local_context m_context; // current local context: a list of local constants
local_context m_full_context; // superset of m_context, it also contains non-contextual locals.
old_local_context m_context; // current local context: a list of local constants
old_local_context m_full_context; // superset of m_context, it also contains non-contextual locals.
mvar2meta m_mvar2meta;
cache m_cache;
// The following vector contains sorts that we should check

2
src/library/CMakeLists.txt
View file

@ -11,7 +11,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
typed_expr.cpp let.cpp type_util.cpp protected.cpp
metavar_closure.cpp reducible.cpp init_module.cpp
generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
local_context.cpp choice_iterator.cpp pp_options.cpp
old_local_context.cpp choice_iterator.cpp pp_options.cpp
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
composition_manager.cpp tc_multigraph.cpp noncomputable.cpp

32
src/library/class_instance_resolution.cpp
View file

@ -16,7 +16,7 @@ Author: Leonardo de Moura
#include "library/normalize.h"
#include "library/reducible.h"
#include "library/class.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
#include "library/generic_exception.h"
#include "library/io_state_stream.h"
#include "library/replace_visitor.h"
@ -127,11 +127,11 @@ public:
}
};
static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, local_context const & _ctx, expr const & m, bool is_strict,
static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, old_local_context const & _ctx, expr const & m, bool is_strict,
bool use_local_instances, pos_info_provider const * pip) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s) {
local_context ctx;
old_local_context ctx;
if (use_local_instances)
ctx = _ctx.instantiate(substitution(s));
cienv & cenv = get_cienv();
@ -169,7 +169,7 @@ static constraint mk_class_instance_root_cnstr(environment const & env, io_state
solutions using class-instances
*/
pair<expr, constraint> mk_new_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
environment const & env, io_state const & ios, old_local_context const & ctx,
optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, pos_info_provider const * pip) {
expr m = ctx.mk_meta(suffix, type, g);
@ -178,14 +178,14 @@ pair<expr, constraint> mk_new_class_instance_elaborator(
return mk_pair(m, c);
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances) {
optional<expr> mk_class_instance(environment const & env, io_state const & ios, old_local_context const & ctx, expr const & type, bool use_local_instances) {
if (use_local_instances)
return mk_class_instance(env, ios.get_options(), ctx.get_data(), type, nullptr);
else
return mk_class_instance(env, ios.get_options(), list<expr>(), type, nullptr);
}
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type) {
optional<expr> mk_class_instance(environment const & env, old_local_context const & ctx, expr const & type) {
return mk_class_instance(env, ctx.get_data(), type, nullptr);
}
@ -273,7 +273,7 @@ struct class_instance_context {
};
static pair<expr, constraint>
mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, old_local_context const & ctx,
optional<expr> const & type, tag g, unsigned depth, bool use_globals);
/** \brief Choice function \c fn for synthesizing class instances.
@ -285,7 +285,7 @@ mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C,
*/
struct class_instance_elaborator : public choice_iterator {
std::shared_ptr<class_instance_context> m_C;
local_context m_ctx;
old_local_context m_ctx;
expr m_meta;
// elaborated type of the metavariable
expr m_meta_type;
@ -301,7 +301,7 @@ struct class_instance_elaborator : public choice_iterator {
unsigned m_depth;
bool m_displayed_trace_header;
class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, old_local_context const & ctx,
expr const & meta, expr const & meta_type,
list<expr> const & local_insts, list<name> const & trans_insts, list<name> const & instances,
justification const & j, unsigned depth):
@ -346,7 +346,7 @@ struct class_instance_elaborator : public choice_iterator {
type_checker & tc = m_C->tc();
tag g = inst.get_tag();
try {
flet<local_context> scope(m_ctx, m_ctx);
flet<old_local_context> scope(m_ctx, m_ctx);
buffer<expr> locals;
expr meta_type = m_meta_type;
while (true) {
@ -434,7 +434,7 @@ struct class_instance_elaborator : public choice_iterator {
// Remarks:
// - we only use get_class_instances and get_class_derived_trans_instances when use_globals is true
static constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const & C,
local_context const & ctx, expr const & m, unsigned depth, bool use_globals) {
old_local_context const & ctx, expr const & m, unsigned depth, bool use_globals) {
environment const & env = C->env();
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &) {
@ -463,14 +463,14 @@ static constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic), owner, j);
}
static pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
static pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, old_local_context const & ctx,
optional<expr> const & type, tag g, unsigned depth, bool use_globals) {
expr m = ctx.mk_meta(type, g);
constraint c = mk_class_instance_cnstr(C, ctx, m, depth, use_globals);
return mk_pair(m, c);
}
static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context> const & C, local_context const & _ctx,
static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context> const & C, old_local_context const & _ctx,
expr const & m, bool is_strict, unifier_config const & cfg, delay_factor const & factor) {
environment const & env = C->env();
justification j = mk_failed_to_synthesize_jst(env, m);
@ -482,7 +482,7 @@ static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_co
// do nothing, since type is not a class.
return lazy_list<constraints>(constraints());
}
local_context ctx = _ctx.instantiate(substitution(s));
old_local_context ctx = _ctx.instantiate(substitution(s));
pair<expr, justification> mj = update_meta(meta, s);
expr new_meta = mj.first;
justification new_j = mj.second;
@ -550,7 +550,7 @@ static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_co
solutions using class-instances
*/
pair<expr, constraint> mk_old_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
environment const & env, io_state const & ios, old_local_context const & ctx,
optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
pos_info_provider const * pip) {
@ -564,7 +564,7 @@ pair<expr, constraint> mk_old_class_instance_elaborator(
}
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
environment const & env, io_state const & ios, old_local_context const & ctx,
optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g,
pos_info_provider const * pip) {

8
src/library/class_instance_resolution.h
View file

@ -9,7 +9,7 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "kernel/pos_info_provider.h"
#include "library/io_state.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
namespace lean {
optional<expr> mk_class_instance(environment const & env, options const & o,
@ -33,12 +33,12 @@ optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx
\param tag To be associated with new metavariables and expressions (for error localization).
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
environment const & env, io_state const & ios, old_local_context const & ctx,
optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, pos_info_provider const * pip);
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances);
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type);
optional<expr> mk_class_instance(environment const & env, io_state const & ios, old_local_context const & ctx, expr const & type, bool use_local_instances);
optional<expr> mk_class_instance(environment const & env, old_local_context const & ctx, expr const & type);
optional<expr> mk_hset_instance(type_checker & tc, options const & o, list<expr> const & ctx, expr const & type);
optional<expr> mk_subsingleton_instance(environment const & env, options const & o,
list<expr> const & ctx, expr const & type);

32
src/library/local_context.cpp → src/library/old_local_context.cpp
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/replace_fn.h"
#include "kernel/metavar.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
namespace lean {
/** \brief Given a list of local constants \c locals
@ -18,7 +18,7 @@ namespace lean {
return
t[#n, ..., #0]
*/
expr local_context::abstract_locals(expr const & e, list<expr> const & locals) {
expr old_local_context::abstract_locals(expr const & e, list<expr> const & locals) {
lean_assert(std::all_of(locals.begin(), locals.end(), [](expr const & e) { return closed(e) && is_local(e); }));
if (!has_local(e))
return e;
@ -38,16 +38,16 @@ expr local_context::abstract_locals(expr const & e, list<expr> const & locals) {
});
}
auto local_context::to_local_decl(expr const & l, list<expr> const & ctx) -> local_decl {
auto old_local_context::to_local_decl(expr const & l, list<expr> const & ctx) -> local_decl {
return local_decl(local_pp_name(l), abstract_locals(mlocal_type(l), ctx), local_info(l));
}
local_context::local_context() {}
local_context::local_context(list<expr> const & ctx) {
old_local_context::old_local_context() {}
old_local_context::old_local_context(list<expr> const & ctx) {
set_ctx(ctx);
}
void local_context::set_ctx(list<expr> const & ctx) {
void old_local_context::set_ctx(list<expr> const & ctx) {
m_ctx = ctx;
buffer<local_decl> tmp;
list<expr> it = ctx;
@ -58,7 +58,7 @@ void local_context::set_ctx(list<expr> const & ctx) {
m_ctx_abstracted = to_list(tmp.begin(), tmp.end());
}
expr local_context::pi_abstract_context(expr e, tag g) const {
expr old_local_context::pi_abstract_context(expr e, tag g) const {
e = abstract_locals(e, m_ctx);
for (local_decl const & l : m_ctx_abstracted)
e = mk_pi(std::get<0>(l), std::get<1>(l), e, std::get<2>(l), g);
@ -72,22 +72,22 @@ static expr apply_context_core(expr const & f, list<expr> const & ctx, tag g) {
return f;
}
expr local_context::apply_context(expr const & f, tag g) const {
expr old_local_context::apply_context(expr const & f, tag g) const {
return apply_context_core(f, m_ctx, g);
}
expr local_context::mk_type_metavar(tag g) const {
expr old_local_context::mk_type_metavar(tag g) const {
name n = mk_fresh_name();
expr s = mk_sort(mk_meta_univ(mk_fresh_name()), g);
expr t = pi_abstract_context(s, g);
return ::lean::mk_metavar(n, t, g);
}
expr local_context::mk_type_meta(tag g) const {
expr old_local_context::mk_type_meta(tag g) const {
return apply_context(mk_type_metavar(g), g);
}
expr local_context::mk_metavar(optional<name> const & suffix, optional<expr> const & type, tag g) const {
expr old_local_context::mk_metavar(optional<name> const & suffix, optional<expr> const & type, tag g) const {
name n = mk_fresh_name();
if (suffix)
n = n + *suffix;
@ -96,20 +96,20 @@ expr local_context::mk_metavar(optional<name> const & suffix, optional<expr> con
return ::lean::mk_metavar(n, t, g);
}
expr local_context::mk_meta(optional<name> const & suffix, optional<expr> const & type, tag g) const {
expr old_local_context::mk_meta(optional<name> const & suffix, optional<expr> const & type, tag g) const {
expr mvar = mk_metavar(suffix, type, g);
expr meta = apply_context(mvar, g);
return meta;
}
void local_context::add_local(expr const & l) {
void old_local_context::add_local(expr const & l) {
lean_assert(is_local(l));
m_ctx_abstracted = cons(to_local_decl(l, m_ctx), m_ctx_abstracted);
m_ctx = cons(l, m_ctx);
lean_assert(length(m_ctx) == length(m_ctx_abstracted));
}
list<expr> const & local_context::get_data() const {
list<expr> const & old_local_context::get_data() const {
return m_ctx;
}
@ -117,7 +117,7 @@ static list<expr> instantiate_locals(list<expr> const & ls, substitution & s) {
return map(ls, [&](expr const & l) { return update_mlocal(l, s.instantiate(mlocal_type(l))); });
}
local_context local_context::instantiate(substitution s) const {
return local_context(instantiate_locals(m_ctx, s));
old_local_context old_local_context::instantiate(substitution s) const {
return old_local_context(instantiate_locals(m_ctx, s));
}
}

10
src/library/local_context.h → src/library/old_local_context.h
View file

@ -12,7 +12,7 @@ namespace lean {
/** \brief Auxiliary data-structure for storing the local context,
and creating metavariables in the scope of the local context efficiently
*/
class local_context {
class old_local_context {
list<expr> m_ctx; // current local context: a list of local constants
typedef std::tuple<name, expr, binder_info> local_decl;
list<local_decl> m_ctx_abstracted; // m_ctx where elements have been abstracted
@ -20,8 +20,8 @@ class local_context {
// convert a local constant into a local_decl
static local_decl to_local_decl(expr const & l, list<expr> const & ctx);
public:
local_context();
local_context(list<expr> const & ctx);
old_local_context();
old_local_context(list<expr> const & ctx);
void set_ctx(list<expr> const & ctx);
@ -89,7 +89,7 @@ public:
void add_local(expr const & l);
/** \brief Instantiate metavariables occurring this local context using \c s, and return updated local_context */
local_context instantiate(substitution s) const;
/** \brief Instantiate metavariables occurring this local context using \c s, and return updated old_local_context */
old_local_context instantiate(substitution s) const;
};
}

3
src/library/tactic/apply_tactic.cpp
View file

@ -20,7 +20,6 @@ Author: Leonardo de Moura
#include "library/occurs.h"
#include "library/constants.h"
#include "library/type_util.h"
#include "library/local_context.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/apply_tactic.h"
@ -86,7 +85,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
e_t_cs.second.linearize(cs);
expr e_t = e_t_cs.first;
buffer<expr> metas;
local_context ctx;
old_local_context ctx;
bool initialized_ctx = false;
unifier_config cfg(ios.get_options());
if (uk)

4
src/library/tactic/goal.cpp
View file

@ -18,11 +18,11 @@ Author: Leonardo de Moura
#include "library/tactic/goal.h"
namespace lean {
local_context goal::to_local_context() const {
old_local_context goal::to_local_context() const {
buffer<expr> hyps;
get_hyps(hyps);
std::reverse(hyps.begin(), hyps.end());
return local_context(to_list(hyps));
return old_local_context(to_list(hyps));
}
format goal::pp(formatter const & fmt) const {

4
src/library/tactic/goal.h
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "kernel/formatter.h"
#include "kernel/environment.h"
#include "library/io_state_stream.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
namespace lean {
/**
@ -71,7 +71,7 @@ public:
*/
list<expr> to_context() const;
local_context to_local_context() const;
old_local_context to_local_context() const;
/** \brief Apply given substitution to goal */
goal instantiate(substitution const & s) const;

6
src/library/tactic/induction_tactic.cpp
View file

@ -62,9 +62,9 @@ class induction_tac {
}
expr mk_type_class_param(goal const & g, expr const & type) {
bool use_local_insts = true;
bool is_strict = false;
local_context ctx = g.to_local_context();
bool use_local_insts = true;
bool is_strict = false;
old_local_context ctx = g.to_local_context();
auto mc = mk_class_instance_elaborator(
m_env, m_ios, ctx, optional<name>(),
use_local_insts, is_strict,

4
src/library/tactic/rewrite_tactic.cpp
View file

@ -26,7 +26,7 @@ Author: Leonardo de Moura
#include "library/match.h"
#include "library/choice.h"
#include "library/projection.h"
#include "library/local_context.h"
#include "library/old_local_context.h"
#include "library/unifier.h"
#include "library/locals.h"
#include "library/constants.h"
@ -574,7 +574,7 @@ class rewrite_fn {
type_checker_ptr m_relaxed_tc; // reduce_to and check_trivial
rewrite_match_plugin m_mplugin;
goal m_g;
local_context m_ctx;
old_local_context m_ctx;
substitution m_subst;
expr m_expr_loc; // auxiliary expression used for error localization