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

feat(library,frontends/lean): use mdata instead of hacky cache for position information in preterms

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-02 16:19:15 -07:00
parent 0220af69b8
commit 39cdae50ee
26 changed files with 428 additions and 594 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/brackets.cpp
View file

@ -19,7 +19,7 @@ static expr parse_subtype(parser & p, pos_info const & pos, expr const & local)
p.add_local(local);
expr pred = p.parse_expr();
p.check_token_next(get_rcurly_tk(), "invalid subtype, '}' expected");
pred = p.save_pos(Fun(local, pred), pos);
pred = p.save_pos(Fun_p(local, pred), pos);
expr subtype = p.save_pos(mk_constant(get_subtype_name()), pos);
return p.mk_app(subtype, pred, pos);
}
@ -30,7 +30,7 @@ static expr parse_set_of(parser & p, pos_info const & pos, expr const & local) {
p.add_local(local);
expr pred = p.parse_expr();
p.check_token_next(get_rcurly_tk(), "invalid set_of, '}' expected");
pred = p.save_pos(Fun(local, pred), pos);
pred = p.save_pos(Fun_p(local, pred), pos);
expr set_of = p.save_pos(mk_constant(get_set_of_name()), pos);
return p.mk_app(set_of, pred, pos);
}
@ -65,7 +65,7 @@ static expr parse_sep(parser & p, pos_info const & pos, name const & id) {
p.add_local(local);
expr pred = p.parse_expr();
p.check_token_next(get_rcurly_tk(), "invalid sep expression, '}' expected");
pred = p.rec_save_pos(Fun(local, pred), pos);
pred = p.rec_save_pos(Fun_p(local, pred), pos);
return p.rec_save_pos(mk_app(mk_constant(get_has_sep_sep_name()), pred, s), pos);
}

4
src/frontends/lean/builtin_cmds.cpp
View file

@ -128,8 +128,8 @@ static environment redeclare_aliases(environment env, parser & p,
pair<name, expr> entry = head(old_entries);
if (is_local_ref(entry.second))
to_redeclare.push_back(entry);
else if (is_local(entry.second))
popped_locals.insert(local_name(entry.second));
else if (is_local_p(entry.second))
popped_locals.insert(local_name_p(entry.second));
old_entries = tail(old_entries);
old_len--;
}

18
src/frontends/lean/builtin_exprs.cpp
View file

@ -168,8 +168,8 @@ static expr parse_let(parser & p, pos_info const & pos, bool in_do_block) {
value = p.parse_scoped_expr(ps, lenv);
value = Fun(ps, value, p);
}
expr x = p.save_pos(mk_local(id, type), id_pos);
p.add_local_expr(id, x);
expr x = mk_local(id, type);
p.add_local_expr(id, p.save_pos(x, id_pos));
expr b = parse_let_body(p, pos, in_do_block);
return p.save_pos(mk_let(id, type, value, abstract(b, x)), pos);
} else {
@ -204,14 +204,14 @@ static std::tuple<optional<expr>, expr, expr, optional<expr>> parse_do_action(pa
if (p.curr_is_token(get_colon_tk())) {
p.next();
type = p.parse_expr();
if (is_placeholder(*lhs)) {
if (is_placeholder(unwrap_pos(*lhs))) {
lhs = mk_local("_x", type);
}
if (!is_local(*lhs)) {
if (!is_local(unwrap_pos(*lhs))) {
p.maybe_throw_error({"invalid 'do' block, unexpected ':' the left hand side is a pattern", lhs_pos});
lhs = mk_local("_x", type);
}
lhs = p.save_pos(mk_local(local_pp_name(*lhs), type), lhs_pos);
lhs = p.save_pos(mk_local(local_pp_name_p(*lhs), type), lhs_pos);
new_locals.clear();
new_locals.push_back(*lhs);
p.check_token_next(get_larrow_tk(), "invalid 'do' block, '←' expected");
@ -416,7 +416,7 @@ static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos)
expr l = p.save_pos(mk_local(id, prop), pos);
p.add_local(l);
expr body = p.parse_expr();
body = abstract(body, l);
body = abstract(body, unwrap_pos(l));
if (get_parser_checkpoint_have(p.get_options()))
body = mk_checkpoint_annotation(body);
expr r = p.save_pos(mk_have_annotation(p.save_pos(mk_lambda(id, prop, body), pos)), pos);
@ -515,7 +515,7 @@ static expr parse_if_then_else(parser & p, unsigned, expr const *, pos_info cons
static expr parse_explicit_core(parser & p, pos_info const & pos, bool partial) {
if (!p.curr_is_identifier())
return p.parser_error_or_expr({sstream() << "invalid '" << (partial ? "@@" : "@") << "', identifier expected", p.pos()});
expr fn = p.parse_id(/* allow_field_notation */ false);
expr fn = unwrap_pos(p.parse_id(/* allow_field_notation */ false));
if (is_choice(fn)) {
sstream s;
s << "invalid '" << (partial ? "@@" : "@") << "', function is overloaded, use fully qualified names (overloads: ";
@ -681,7 +681,7 @@ static expr parse_constructor_core(parser & p, pos_info const & pos) {
}
p.check_token_next(get_rangle_tk(), "invalid constructor, `⟩` expected");
expr fn = p.save_pos(mk_expr_placeholder(), pos);
return p.save_pos(mk_anonymous_constructor(p.save_pos(mk_app(fn, args), pos)), pos);
return p.save_pos(mk_anonymous_constructor(mk_app(fn, args)), pos);
}
static expr parse_constructor(parser & p, unsigned, expr const *, pos_info const & pos) {
@ -707,7 +707,7 @@ static expr parse_lambda_binder(parser & p, pos_info const & pos) {
p.maybe_throw_error({"invalid lambda expression, ',' or '⟨' expected", p.pos()});
body = p.parse_expr();
}
return p.rec_save_pos(Fun(locals, body), pos);
return p.rec_save_pos(Fun(locals, body, p), pos);
}
static name * g_lambda_match_name = nullptr;

64
src/frontends/lean/decl_util.cpp
View file

@ -75,13 +75,13 @@ expr parse_single_header(parser & p, declaration_name_scope & scope, buffer <nam
/* Try to synthesize name */
expr it = type;
while (is_pi(it)) it = binding_body(it);
expr const & C = get_app_fn(it);
expr const & C = unwrap_pos(get_app_fn(it));
name ns = get_namespace(p.env());
if (is_constant(C) && !ns.is_anonymous()) {
c_name = const_name(C);
scope.set_name(c_name);
} else if (is_constant(C) && is_app(it) && is_constant(get_app_fn(app_arg(it)))) {
c_name = const_name(get_app_fn(app_arg(it))) + const_name(C);
} else if (is_constant(C) && is_app(it) && is_constant(unwrap_pos(get_app_fn(app_arg(it))))) {
c_name = const_name(unwrap_pos(get_app_fn(app_arg(it)))) + const_name(C);
scope.set_name(c_name);
} else {
p.maybe_throw_error({"failed to synthesize instance name, name should be provided explicitly", c_pos});
@ -172,10 +172,11 @@ void collect_annonymous_inst_implicit(parser const & p, collected_locals & local
while (i > 0) {
--i;
auto const & entry = entries[i];
if (is_local(entry.second) && !locals.contains(entry.second) && is_inst_implicit(local_info(entry.second)) &&
expr l = unwrap_pos(entry.second);
if (is_local(l) && !locals.contains(l) && is_inst_implicit(local_info_p(l)) &&
// remark: remove the following condition condition, if we want to auto inclusion also for non anonymous ones.
is_anonymous_inst_name(entry.first)) {
expr type = local_type(entry.second);
expr type = local_type_p(l);
buffer<expr> C_args;
expr C = get_app_args(type, C_args);
if (!is_const(C))
@ -187,8 +188,8 @@ void collect_annonymous_inst_implicit(parser const & p, collected_locals & local
it2 = ctx.relaxed_whnf(it2);
lean_assert(is_pi(it2));
expr const & d = binding_domain(it2);
if (is_local(C_arg) && is_class_out_param(d)) {
new_locals.insert(C_arg);
if (is_local_p(C_arg) && is_class_out_param(d)) {
new_locals.insert(unwrap_pos(C_arg));
} else {
for_each(C_arg, [&](expr const & e, unsigned) {
if (!ok) return false; // stop
@ -203,7 +204,7 @@ void collect_annonymous_inst_implicit(parser const & p, collected_locals & local
for (auto & l : new_locals.get_collected()) {
locals.insert(l);
}
locals.insert(entry.second);
locals.insert(l);
}
}
}
@ -214,11 +215,11 @@ void sort_locals(buffer<expr> const & locals, parser const & p, buffer<expr> & p
buffer<expr> extra;
name_set explicit_param_names;
for (expr const & p : ps) {
explicit_param_names.insert(local_name(p));
explicit_param_names.insert(local_name_p(p));
}
for (expr const & l : locals) {
// we only copy the locals that are in p's local context
if (p.is_local_decl_user_name(l) && !explicit_param_names.contains(local_name(l)))
if (p.is_local_decl_user_name(l) && !explicit_param_names.contains(local_name_p(l)))
extra.push_back(l);
}
std::sort(extra.begin(), extra.end(), [&](expr const & p1, expr const & p2) {
@ -251,19 +252,7 @@ void update_univ_parameters(parser & p, buffer<name> & lp_names, name_set const
}
expr replace_locals_preserving_pos_info(expr const & e, unsigned sz, expr const * from, expr const * to) {
bool use_cache = false;
return replace_propagating_pos(e, [&](expr const & e, unsigned) {
if (is_local(e)) {
unsigned i = sz;
while (i > 0) {
--i;
if (local_name(from[i]) == local_name(e)) {
return some_expr(copy_pos(e, copy(to[i])));
}
}
}
return none_expr();
}, use_cache);
return replace_locals(e, sz, from, to);
}
expr replace_locals_preserving_pos_info(expr const & e, buffer<expr> const & from, buffer<expr> const & to) {
@ -283,18 +272,19 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
/* Process variables included using the 'include' command */
p.get_include_variables(include_vars);
for (expr const & param : include_vars) {
if (is_local(param)) {
collect_locals_ignoring_tactics(local_type(param), locals);
lp_found = collect_univ_params_ignoring_tactics(local_type(param), lp_found);
locals.insert(param);
expr up = unwrap_pos(param);
if (is_local(up)) {
collect_locals_ignoring_tactics(local_type(up), locals);
lp_found = collect_univ_params_ignoring_tactics(local_type(up), lp_found);
locals.insert(up);
}
}
/* Process explicit parameters */
for (expr const & param : params) {
collect_locals_ignoring_tactics(local_type(param), locals);
lp_found = collect_univ_params_ignoring_tactics(local_type(param), lp_found);
collect_locals_ignoring_tactics(local_type_p(param), locals);
lp_found = collect_univ_params_ignoring_tactics(local_type_p(param), lp_found);
locals.insert(param);
given_params.insert(local_name(param));
given_params.insert(local_name_p(param));
}
/* Process expressions used to define declaration. */
for (expr const & e : all_exprs) {
@ -309,12 +299,12 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
for (unsigned i = 0; i < params.size(); i++) {
expr & param = params[i];
old_params.push_back(param);
expr type = local_type(param);
expr type = local_type_p(param);
expr new_type = replace_locals_preserving_pos_info(type, i, old_params.data(), params.data());
if (!given_params.contains(local_name(param))) {
if (!given_params.contains(local_name_p(param))) {
new_type = copy_pos(type, mk_as_is(new_type));
}
param = copy_pos(param, update_local(param, new_type));
param = copy_pos(param, update_local_p(param, new_type));
}
}
@ -331,9 +321,9 @@ void collect_implicit_locals(parser & p, buffer<name> & lp_names, buffer<expr> &
void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<expr> & new_params) {
for (unsigned i = 0; i < params.size(); i++) {
expr const & param = params[i];
expr type = replace_locals_preserving_pos_info(local_type(param), i, params.data(), new_params.data());
expr type = replace_locals_preserving_pos_info(local_type_p(param), i, params.data(), new_params.data());
expr new_type = elab.elaborate_type(type);
expr new_param = elab.push_local(local_pp_name(param), new_type, local_info(param));
expr new_param = elab.push_local(local_pp_name_p(param), new_type, local_info_p(param));
new_params.push_back(new_param);
}
}
@ -378,11 +368,11 @@ environment add_local_ref(parser & p, environment const & env, name const & c_na
buffer<expr> new_params;
for (unsigned i = 0; i < params.size(); i++) {
expr & param = params[i];
expr type = local_type(param);
expr type = local_type_p(param);
if (is_as_is(type))
type = get_as_is_arg(type);
expr new_type = replace_locals_preserving_pos_info(type, i, params.data(), new_params.data());
new_params.push_back(copy_pos(param, update_local(param, new_type)));
new_params.push_back(copy_pos(param, update_local_p(param, new_type)));
}
expr ref = mk_local_ref(c_real_name, param_names_to_levels(names(lps)), new_params);
return p.add_local_ref(env, c_name, ref);

52
src/frontends/lean/definition_cmds.cpp
View file

@ -126,8 +126,8 @@ static expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<
buffer<name> full_actual_names;
for (expr const & pre_fn : pre_fns) {
// TODO(leo, dhs): make use of attributes
expr fn_type = parse_inner_header(p, local_pp_name(pre_fn)).first;
declaration_name_scope scope2(local_pp_name(pre_fn));
expr fn_type = parse_inner_header(p, local_pp_name_p(pre_fn)).first;
declaration_name_scope scope2(local_pp_name_p(pre_fn));
declaration_name_scope scope3("_main");
full_names.push_back(scope3.get_name());
full_actual_names.push_back(scope3.get_actual_name());
@ -142,7 +142,7 @@ static expr parse_mutual_definition(parser & p, buffer<name> & lp_names, buffer<
}
check_valid_end_of_equations(p);
}
expr fn = mk_local(local_name(pre_fn), local_pp_name(pre_fn), fn_type, mk_rec_info());
expr fn = mk_local(local_name_p(pre_fn), local_pp_name_p(pre_fn), fn_type, mk_rec_info());
fns.push_back(fn);
}
if (p.curr_is_token(get_with_tk()))
@ -266,7 +266,7 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm
return p.env();
bool recover_from_errors = true;
elaborator elab(env, p.get_options(), get_namespace(env) + local_pp_name(fns[0]), metavar_context(), local_context(), recover_from_errors);
elaborator elab(env, p.get_options(), get_namespace(env) + local_pp_name_p(fns[0]), metavar_context(), local_context(), recover_from_errors);
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
val = replace_locals_preserving_pos_info(val, params, new_params);
@ -286,7 +286,7 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm
expr curr_type = head_beta_reduce(elab.infer_type(curr));
finalize_definition(elab, new_params, curr_type, curr, lp_names);
environment env = elab.env();
name c_name = local_name(fns[i]);
name c_name = local_name_p(fns[i]);
name c_real_name;
bool is_abbrev = false;
std::tie(env, c_real_name) = declare_definition(p, env, kind, lp_names, c_name, prv_names[i],
@ -307,7 +307,7 @@ static environment mutual_definition_cmd_core(parser & p, decl_cmd_kind kind, cm
- fn is a local constant with the user name + type
- val is the actual definition
- actual_name for the kernel declaration.
Note that mlocal_pp_name(fn) and actual_name are different for scoped/private declarations.
Note that mlocal_pp_name_p(fn) and actual_name are different for scoped/private declarations.
*/
static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
bool is_example, bool is_instance, bool is_meta, bool is_abbrev) {
@ -321,7 +321,7 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
p.next();
if (is_meta) {
declaration_name_scope scope2("_main");
fn = mk_local(local_name(fn), local_pp_name(fn), local_type(fn), mk_rec_info());
fn = mk_local(local_name_p(fn), local_pp_name_p(fn), local_type_p(fn), mk_rec_info());
p.add_local(fn);
val = p.parse_expr();
/* add fake equation */
@ -336,7 +336,7 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
if (is_abbrev)
throw exception("invalid abbreviation, abbreviations should not be defined using pattern matching");
declaration_name_scope scope2("_main");
fn = mk_local(local_name(fn), local_pp_name(fn), local_type(fn), mk_rec_info());
fn = mk_local(local_name_p(fn), local_pp_name_p(fn), local_type_p(fn), mk_rec_info());
p.add_local(fn);
buffer<expr> eqns;
if (p.curr_is_token(get_period_tk())) {
@ -354,22 +354,22 @@ static std::tuple<expr, expr, name> parse_definition(parser & p, buffer<name> &
} else {
val = p.parser_error_or_expr({"invalid definition, '|' or ':=' expected", p.pos()});
}
collect_implicit_locals(p, lp_names, params, {local_type(fn), val});
collect_implicit_locals(p, lp_names, params, {local_type_p(fn), val});
return std::make_tuple(fn, val, scope2.get_actual_name());
}
static void replace_params(buffer<expr> const & params, buffer<expr> const & new_params, expr & fn, expr & val) {
expr fn_type = replace_locals_preserving_pos_info(local_type(fn), params, new_params);
expr new_fn = update_local(fn, fn_type);
expr fn_type = replace_locals_preserving_pos_info(local_type_p(fn), params, new_params);
expr new_fn = update_local_p(fn, fn_type);
val = replace_locals_preserving_pos_info(val, params, new_params);
val = replace_local_preserving_pos_info(val, fn, new_fn);
fn = new_fn;
}
static expr_pair elaborate_theorem(elaborator & elab, expr const & fn, expr val) {
expr fn_type = elab.elaborate_type(local_type(fn));
expr fn_type = elab.elaborate_type(local_type_p(fn));
elab.ensure_no_unassigned_metavars(fn_type);
expr new_fn = update_local(fn, fn_type);
expr new_fn = update_local_p(fn, fn_type);
val = replace_local_preserving_pos_info(val, fn, new_fn);
return elab.elaborate_with_type(val, mk_as_is(fn_type));
}
@ -377,15 +377,15 @@ static expr_pair elaborate_theorem(elaborator & elab, expr const & fn, expr val)
static expr_pair elaborate_definition_core(elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val) {
// We elaborate `fn` and `val` separately if `fn` is a theorem or its return type
// was specified explicitly
if (kind == decl_cmd_kind::Theorem || !is_placeholder(local_type(fn))) {
if (kind == decl_cmd_kind::Theorem || !is_placeholder(local_type_p(fn))) {
return elaborate_theorem(elab, fn, val);
} else {
return elab.elaborate_with_type(val, local_type(fn));
return elab.elaborate_with_type(val, local_type_p(fn));
}
}
static expr_pair elaborate_definition(parser & p, elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val, pos_info const & pos) {
time_task _("elaboration", p.mk_message(pos, INFORMATION), p.get_options(), local_pp_name(fn));
time_task _("elaboration", p.mk_message(pos, INFORMATION), p.get_options(), local_pp_name_p(fn));
return elaborate_definition_core(elab, kind, fn, val);
}
@ -439,20 +439,20 @@ static expr elaborate_proof(
try {
bool recover_from_errors = true;
elaborator elab(decl_env, opts, get_namespace(decl_env) + local_pp_name(fn), mctx, lctx, recover_from_errors);
elaborator elab(decl_env, opts, get_namespace(decl_env) + local_pp_name_p(fn), mctx, lctx, recover_from_errors);
expr val, type;
{
time_task _("elaboration", message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, INFORMATION),
opts, local_pp_name(fn));
std::tie(val, type) = elab.elaborate_with_type(val0, mk_as_is(local_type(fn)));
opts, local_pp_name_p(fn));
std::tie(val, type) = elab.elaborate_with_type(val0, mk_as_is(local_type_p(fn)));
}
if (is_equations_result(val))
val = get_equations_result(val, 0);
buffer<expr> params; for (auto & e : params_list) params.push_back(e);
finalize_theorem_proof(elab, params, val, finfo);
return inline_new_defs(decl_env, elab.env(), local_pp_name(fn), val);
return inline_new_defs(decl_env, elab.env(), local_pp_name_p(fn), val);
} catch (exception & ex) {
/* Remark: we need the catch to be able to produce correct line information */
message_builder(tc, decl_env, get_global_ios(), file_name, header_pos, ERROR)
@ -480,7 +480,7 @@ static void check_example(environment const & decl_env, options const & opts,
elaborator elab(decl_env, opts, decl_name, mctx, lctx, recover_from_errors);
expr val, type;
std::tie(val, type) = elab.elaborate_with_type(val0, local_type(fn));
std::tie(val, type) = elab.elaborate_with_type(val0, local_type_p(fn));
buffer<expr> params_buf; for (auto & p : params) params_buf.push_back(p);
buffer<name> univ_params_buf; to_buffer(univ_params, univ_params_buf);
finalize_definition(elab, params_buf, type, val, univ_params_buf);
@ -528,7 +528,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
auto begin_pos = p.cmd_pos();
auto end_pos = p.pos();
scope_log_tree lt(logtree().mk_child({}, (get_namespace(env) + local_pp_name(fn)).to_string(),
scope_log_tree lt(logtree().mk_child({}, (get_namespace(env) + local_pp_name_p(fn)).to_string(),
{logtree().get_location().m_file_name, {begin_pos, end_pos}}));
// skip elaboration of definitions during reparsing
@ -536,7 +536,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
return p.env();
bool recover_from_errors = true;
elaborator elab(env, p.get_options(), get_namespace(env) + local_pp_name(fn), metavar_context(), local_context(), recover_from_errors);
elaborator elab(env, p.get_options(), get_namespace(env) + local_pp_name_p(fn), metavar_context(), local_context(), recover_from_errors);
buffer<expr> new_params;
elaborate_params(elab, params, new_params);
elab.freeze_local_instances();
@ -546,13 +546,13 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
expr type;
optional<expr> opt_val;
bool eqns = false;
name c_name = local_name(fn);
name c_name = local_name_p(fn);
pair<environment, name> env_n;
if (kind == decl_cmd_kind::Theorem) {
is_rfl = is_rfl_preexpr(val);
type = elab.elaborate_type(local_type(fn));
type = elab.elaborate_type(local_type_p(fn));
elab.ensure_no_unassigned_metavars(type);
expr new_fn = update_local(fn, type);
expr new_fn = update_local_p(fn, type);
val = replace_local_preserving_pos_info(val, fn, new_fn);
elaborator::theorem_finalization_info thm_finfo;
finalize_theorem_type(elab, new_params, type, lp_names, thm_finfo);

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

@ -240,7 +240,7 @@ bool elaborator::has_synth_sorry(std::initializer_list<expr> && es) {
expr elaborator::mk_sorry(optional<expr> const & expected_type, expr const & ref, bool synthetic) {
auto sorry_type = expected_type ? *expected_type : mk_type_metavar(ref);
return copy_pos(ref, mk_sorry(sorry_type, synthetic));
return mk_sorry(sorry_type, synthetic);
}
expr elaborator::recoverable_error(optional<expr> const & expected_type, expr const & ref, elaborator_exception const & ex) {
@ -253,12 +253,12 @@ level elaborator::mk_univ_metavar() {
return m_ctx.mk_univ_metavar_decl();
}
expr elaborator::mk_metavar(expr const & A, expr const & ref) {
return copy_pos(ref, m_ctx.mk_metavar_decl(m_ctx.lctx(), A));
expr elaborator::mk_metavar(expr const & A, expr const &) {
return m_ctx.mk_metavar_decl(m_ctx.lctx(), A);
}
expr elaborator::mk_metavar(name const & pp_n, expr const & A, expr const & ref) {
return copy_pos(ref, m_ctx.mk_metavar_decl(pp_n, m_ctx.lctx(), A));
expr elaborator::mk_metavar(name const & pp_n, expr const & A, expr const &) {
return m_ctx.mk_metavar_decl(pp_n, m_ctx.lctx(), A);
}
expr elaborator::mk_metavar(optional<expr> const & A, expr const & ref) {
@ -330,8 +330,7 @@ expr elaborator::mk_instance(expr const & C, expr const & ref) {
expr elaborator::instantiate_mvars(expr const & e) {
expr r = m_ctx.instantiate_mvars(e);
if (!get_pos(r))
copy_pos(e, r);
lean_assert(!contains_pos(r));
return r;
}
@ -442,7 +441,7 @@ auto elaborator::use_elim_elab_core(name const & fn) -> optional<elim_info> {
constant_info d = m_env.get(fn);
expr type = d.get_type();
while (is_pi(type)) {
type = instantiate_propagating_pos(binding_body(type), locals.push_local_from_binding(type));
type = instantiate(binding_body(type), locals.push_local_from_binding(type));
}
buffer<expr> C_args;
@ -946,22 +945,26 @@ expr elaborator::visit_const_core(expr const & e) {
/** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
void elaborator::save_identifier_info(expr const & f) {
if (!m_no_info && m_uses_infom && get_pos_info_provider() && (is_constant(f) || is_local(f))) {
if (auto p = get_pos_info_provider()->get_pos_info(f)) {
m_info.add_identifier_info(*p, is_constant(f) ? const_name(f) : local_pp_name(f));
m_info.add_type_info(*p, infer_type(f));
if (!m_no_info && m_uses_infom) {
if (auto p = get_pos(f)) {
expr uf = unwrap_pos(f);
if (is_constant(uf) || is_local(uf)) {
m_info.add_identifier_info(*p, is_constant(uf) ? const_name(uf) : local_pp_name(uf));
m_info.add_type_info(*p, infer_type(uf));
}
}
}
}
expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> const & expected_type, expr const & ref) {
if (is_placeholder(fn)) {
expr ufn = unwrap_pos(fn);
if (is_placeholder(ufn)) {
throw elaborator_exception(ref, "placeholders '_' cannot be used where a function is expected");
}
if (is_field_notation(fn))
if (is_field_notation(ufn))
throw elaborator_exception(ref, "invalid occurrence of field notation");
expr r;
switch (fn.kind()) {
switch (ufn.kind()) {
case expr_kind::BVar:
case expr_kind::Pi:
case expr_kind::MVar:
@ -969,17 +972,17 @@ expr elaborator::visit_function(expr const & fn, bool has_args, optional<expr> c
case expr_kind::Lit:
throw elaborator_exception(ref, "invalid application, function expected");
// The expr_kind::App case can only happen when nary notation is used
case expr_kind::App: r = visit(fn, expected_type); break;
case expr_kind::FVar: r = fn; break;
case expr_kind::Const: r = visit_const_core(fn); break;
case expr_kind::MData: r = visit_mdata(fn, expected_type, true); break;
case expr_kind::Lambda: r = visit_lambda(fn, expected_type); break;
case expr_kind::Let: r = visit_let(fn, expected_type); break;
case expr_kind::App: r = visit(ufn, expected_type); break;
case expr_kind::FVar: r = ufn; break;
case expr_kind::Const: r = visit_const_core(ufn); break;
case expr_kind::MData: r = visit_mdata(ufn, expected_type, true); break;
case expr_kind::Lambda: r = visit_lambda(ufn, expected_type); break;
case expr_kind::Let: r = visit_let(ufn, expected_type); break;
case expr_kind::Proj: throw elaborator_exception(ref, "unexpected occurrence of proj constructor");
case expr_kind::Quote:
throw elaborator_exception(ref, "invalid application, function expected");
}
save_identifier_info(r);
save_identifier_info(copy_pos(fn, r));
if (has_args)
r = ensure_function(r, ref);
return r;
@ -1102,7 +1105,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer<
}
new_args.push_back(new_arg);
postponed_args.push_back(postponed);
type = try_to_pi(instantiate_propagating_pos(binding_body(type), new_arg));
type = try_to_pi(instantiate(binding_body(type), new_arg));
i++;
}
@ -1221,7 +1224,7 @@ optional<expr> elaborator::process_optional_and_auto_params(expr type, expr cons
eta_args.push_back(new_arg);
}
new_args.push_back(new_arg);
type = instantiate_propagating_pos(binding_body(type), new_arg);
type = instantiate(binding_body(type), new_arg);
if (found) {
result_type = type;
sz1 = eta_args.size();
@ -1329,6 +1332,7 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
new_arg = mk_metavar(d, arg_ref);
}
i++;
lean_assert(!get_pos(new_arg));
info.args_mvars.push_back(new_arg);
info.new_args_size.push_back(info.new_args.size());
info.new_instances_size.push_back(info.new_instances.size());
@ -1337,7 +1341,7 @@ void elaborator::first_pass(expr const & fn, buffer<expr> const & args,
}
info.new_args.push_back(new_arg);
/* See comment above at visit_base_app_core */
type_before_whnf = instantiate_propagating_pos(binding_body(type), new_arg);
type_before_whnf = instantiate(binding_body(type), new_arg);
type = whnf(type_before_whnf);
}
type = type_before_whnf;
@ -1503,7 +1507,7 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
}
new_args.push_back(new_arg);
/* See comment above at first type_before_whnf assignment */
type_before_whnf = instantiate_propagating_pos(binding_body(type), new_arg);
type_before_whnf = instantiate(binding_body(type), new_arg);
type = whnf(type_before_whnf);
} else if (i < args.size()) {
bool progress = false;
@ -1672,7 +1676,7 @@ expr elaborator::visit_overloaded_app_core(buffer<expr> const & fns, buffer<expr
optional<expr> const & expected_type, expr const & ref) {
buffer<expr> new_args;
for (expr const & arg : args) {
new_args.push_back(copy_pos(arg, visit(arg, none_expr())));
new_args.push_back(visit(arg, none_expr()));
}
snapshot S(*this);
@ -1887,6 +1891,7 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
bool has_args = !args.empty();
fn = unwrap_pos(fn);
while (is_annotation(fn))
fn = get_annotation_arg(fn);
@ -2007,7 +2012,7 @@ expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type)
if (is_app_of(e, get_scope_trace_name(), 1))
return visit_scope_trace(e, expected_type);
buffer<expr> args;
expr const & fn = get_app_args(e, args);
expr const & fn = unwrap_pos(get_app_args(e, args));
if (is_infix_function(fn)) {
expr infix_fn = get_annotation_arg(fn);
lean_assert(is_lambda(infix_fn));
@ -2087,7 +2092,7 @@ static expr instantiate_rev_locals(expr const & a, unsigned n, expr const * subs
}
return none_expr();
};
return replace_propagating_pos(a, fn);
return replace(a, fn);
}
static expr instantiate_rev_locals(expr const & e, type_context_old::tmp_locals const & locals) {
@ -2107,10 +2112,10 @@ static expr update_equations_fn_type(expr const & eqns, expr const & new_fn_type
expr elaborator::visit_convoy(expr const & e, optional<expr> const & expected_type) {
lean_assert(is_app(e));
lean_assert(is_equations(get_app_fn(e)));
lean_assert(is_equations(unwrap_pos(get_app_fn(e))));
expr const & ref = e;
buffer<expr> args, new_args;
expr const & eqns = get_app_args(e, args);
expr eqns = unwrap_pos(get_app_args(e, args));
lean_assert(equations_num_fns(eqns) == 1);
lean_assert(equations_size(eqns) > 0);
expr fn_type = get_equations_fn_type(eqns);
@ -2144,6 +2149,7 @@ expr elaborator::visit_convoy(expr const & e, optional<expr> const & expected_ty
type_context_old::tmp_locals locals(m_ctx);
expr it = fn_type;
for (unsigned i = 0; i < args.size(); i++) {
it = unwrap_pos(it);
if (!is_pi(it))
throw elaborator_exception(it, "type expected in match-expression");
expr d = instantiate_rev_locals(binding_domain(it), locals);
@ -2166,7 +2172,7 @@ expr elaborator::visit_convoy(expr const & e, optional<expr> const & expected_ty
while (i > 0) {
--i;
new_args[i] = instantiate_mvars(new_args[i]);
new_fn_type = instantiate_propagating_pos(kabstract(m_ctx, new_fn_type, new_args[i]), locals.as_buffer()[i]);
new_fn_type = instantiate(kabstract(m_ctx, new_fn_type, new_args[i]), locals.as_buffer()[i]);
}
new_fn_type = locals.mk_pi(new_fn_type);
} else {
@ -2371,7 +2377,7 @@ class validate_and_collect_lhs_mvars : public replace_visitor {
}
virtual expr visit_let(expr const & e) override {
return visit(instantiate_propagating_pos(let_body(e), let_value(e)));
return visit(instantiate(let_body(e), let_value(e)));
}
virtual expr visit_sort(expr const & e) override {
@ -2474,7 +2480,7 @@ public:
/* Similar to instantiate_mvars, but add an inaccessible pattern annotation around metavariables
whose value has been fixed by type inference. */
static expr instantiate_pattern_mvars(type_context_old & ctx, expr const & lhs) {
return replace_propagating_pos(lhs, [&](expr const & e, unsigned) {
return replace(lhs, [&](expr const & e, unsigned) {
if (is_metavar_decl_ref(e) && ctx.is_assigned(e)) {
expr v = ctx.instantiate_mvars(e);
if (!is_local(v) && !is_metavar(v))
@ -2497,8 +2503,8 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
expr d = instantiate_rev_locals(binding_domain(it), fns);
expr new_d = visit(d, none_expr());
expr ref_d = get_ref_for_child(binding_domain(it), it);
expr fn = copy_pos(binding_domain(it), push_local(fns, binding_name(it), new_d, binding_info(it), ref_d));
save_identifier_info(fn);
expr fn = push_local(fns, binding_name(it), new_d, binding_info(it), ref_d);
save_identifier_info(copy_pos(binding_domain(it), fn));
it = binding_body(it);
}
if (is_no_equation(it)) {
@ -2512,7 +2518,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
while (is_lambda(it)) {
expr type = mk_type_metavar(it);
type_mvars.push_back(type);
expr mvar = copy_pos(binding_domain(it), m_ctx.mk_metavar_decl(binding_name(it), m_ctx.lctx(), type));
expr mvar = m_ctx.mk_metavar_decl(binding_name(it), m_ctx.lctx(), type);
local_mvars.push_back(mvar);
it = binding_body(it);
}
@ -2522,7 +2528,7 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
expr lhs_fn = get_app_fn(lhs);
if (is_explicit_or_partial_explicit(lhs_fn))
lhs_fn = get_explicit_or_partial_explicit_arg(lhs_fn);
if (!is_local(lhs_fn))
if (!is_local_p(lhs_fn))
throw_ill_formed_equation(ref);
expr new_lhs;
{
@ -2638,7 +2644,9 @@ expr elaborator::visit_equations(expr const & e) {
} else {
new_e = copy_pos(e, mk_equations(header, new_eqs.size(), new_eqs.data()));
}
new_e = instantiate_mvars(new_e);
// NOTE: don't call `this.instantiate_mvars`, which checks for position preterm annotations, since equations
// are a mixture of terms and preterms
new_e = m_ctx.instantiate_mvars(new_e);
ensure_no_unassigned_metavars(new_e);
metavar_context mctx = m_ctx.mctx();
expr r = compile_equations(m_env, *this, mctx, m_ctx.lctx(), new_e);
@ -2668,7 +2676,7 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons
type_context_old::tmp_locals locals(m_ctx);
expr t = whnf(s_type);
while (is_pi(t)) {
t = whnf(instantiate_propagating_pos(binding_body(t), locals.push_local_from_binding(t)));
t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
}
if (is_sort(t) && !is_anonymous_field_notation(e)) {
name fname = get_field_notation_field_name(e);
@ -2786,7 +2794,7 @@ public:
/* Predicated variant of `lean::instantiate_mvars`. It does not support universe mvars. */
expr elaborator::instantiate_mvars(expr const & e, std::function<bool(expr const &)> pred) { // NOLINT
return replace_propagating_pos(e, [&](expr const & e) {
return replace(e, [&](expr const & e) {
if (m_ctx.is_mvar(e) && pred(e))
if (auto asn = m_ctx.get_assignment(e))
return some_expr(instantiate_mvars(*asn, pred));
@ -2879,7 +2887,7 @@ class visit_structure_instance_fn {
constant_info decl = m_env.get(const_name(fn));
expr default_val = instantiate_value_univ_params(decl, const_levels(fn));
// clean up 'id' application inserted by `structure_cmd::declare_defaults`
default_val = replace_propagating_pos(default_val, [](expr const & e) {
default_val = replace(default_val, [](expr const & e) {
if (is_app_of(e, get_id_name(), 2)) {
return some_expr(app_arg(e));
}
@ -3005,7 +3013,7 @@ class visit_structure_instance_fn {
}
c_args.push_back(c_arg);
c_type = instantiate_propagating_pos(binding_body(c_type), c_arg);
c_type = instantiate(binding_body(c_type), c_arg);
}
return mk_pair(mk_app(c, c_args), c_type);
}
@ -3218,7 +3226,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional<expr> const & expecte
// antiquotations ~> return `expr`
buffer<expr> locals;
buffer<expr> substs;
s = replace_propagating_pos(s, [&](expr const & t, unsigned) {
s = replace(s, [&](expr const & t, unsigned) {
if (is_antiquote(t)) {
expr local = mk_local(mk_fresh_name(), x.append_after(locals.size() + 1),
mk_expr_placeholder(), mk_binder_info());
@ -3504,12 +3512,12 @@ expr elaborator::visit_lambda(expr const & e, optional<expr> const & expected_ty
}
expr ref_d = get_ref_for_child(binding_domain(it), it);
new_d = ensure_type(new_d, ref_d);
expr l = copy_pos(binding_domain(it), push_local(locals, binding_name(it), new_d, binding_info(it), ref_d));
save_identifier_info(l);
expr l = push_local(locals, binding_name(it), new_d, binding_info(it), ref_d);
save_identifier_info(copy_pos(binding_domain(it), l));
it = binding_body(it);
if (has_expected) {
lean_assert(is_pi(ex));
ex = instantiate_propagating_pos(binding_body(ex), l);
ex = instantiate(binding_body(ex), l);
}
}
expr b = instantiate_rev_locals(it, locals);
@ -3534,8 +3542,8 @@ expr elaborator::visit_pi(expr const & e) {
expr ref_d = get_ref_for_child(binding_domain(it), it);
new_d = ensure_type(new_d, ref_d);
expr ref = binding_domain(it);
expr l = copy_pos(binding_domain(it), push_local(locals, binding_name(it), new_d, binding_info(it), ref));
save_identifier_info(l);
expr l = push_local(locals, binding_name(it), new_d, binding_info(it), ref);
save_identifier_info(copy_pos(binding_domain(it), l));
parent_it = it;
it = binding_body(it);
}
@ -3560,8 +3568,8 @@ expr elaborator::visit_let(expr const & e, optional<expr> const & expected_type)
new_value = instantiate_mvars(new_value);
ensure_no_unassigned_metavars(new_value);
type_context_old::tmp_locals locals(m_ctx);
expr l = copy_pos(let_type(e), push_let(locals, let_name(e), new_type, new_value, ref));
save_identifier_info(l);
expr l = push_let(locals, let_name(e), new_type, new_value, ref);
save_identifier_info(copy_pos(let_type(e), l));
expr body = instantiate_rev_locals(let_body(e), locals);
expr new_body = visit(body, expected_type);
synthesize();
@ -3575,7 +3583,7 @@ expr elaborator::visit_placeholder(expr const & e, optional<expr> const & expect
}
static bool is_have_expr(expr const & e) {
return is_app(e) && is_have_annotation(app_fn(e)) && is_lambda(get_annotation_arg(app_fn(e)));
return is_app(e) && is_have_annotation(unwrap_pos(app_fn(e)));
}
expr elaborator::strict_visit(expr const & e, optional<expr> const & expected_type) {
@ -3588,7 +3596,7 @@ expr elaborator::strict_visit(expr const & e, optional<expr> const & expected_ty
expr elaborator::visit_have_expr(expr const & e, optional<expr> const & expected_type) {
lean_assert(is_have_expr(e));
expr lambda = get_annotation_arg(app_fn(e));
expr lambda = unwrap_pos(get_annotation_arg(app_fn(e)));
expr type = binding_domain(lambda);
expr proof = app_arg(e);
expr new_type = visit(type, none_expr());
@ -3611,7 +3619,7 @@ expr elaborator::visit_suffices_expr(expr const & e, optional<expr> const & expe
lean_assert(is_suffices_annotation(e));
expr body = get_annotation_arg(e);
if (!is_app(body)) throw elaborator_exception(e, "ill-formed suffices expression");
expr fn = app_fn(body);
expr fn = unwrap_pos(app_fn(body));
expr rest = app_arg(body);
if (!is_lambda(fn)) throw elaborator_exception(e, "ill-formed suffices expression");
expr new_fn;
@ -3659,8 +3667,10 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
flet<unsigned> inc_depth(m_depth, m_depth+1);
trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n";
if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";);
return recover_expr_from_exception(expected_type, e, [&] () -> expr {
if (is_placeholder(e)) {
expr e2 = recover_expr_from_exception(expected_type, e, [&] () -> expr {
if (auto p = get_pos(e)) {
return visit(unwrap_pos(e), expected_type);
} else if (is_placeholder(e)) {
return visit_placeholder(e, expected_type);
} else if (is_typed_expr(e)) {
return visit_typed_expr(e);
@ -3689,32 +3699,34 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
}
lean_unreachable();
case expr_kind::MData:
return copy_pos(e, visit_mdata(e, expected_type, false));
return visit_mdata(e, expected_type, false);
case expr_kind::Proj:
throw elaborator_exception(e, "unexpected occurrence of proj constructor");
case expr_kind::Sort:
return copy_pos(e, visit_sort(e));
return visit_sort(e);
case expr_kind::FVar:
return copy_pos(e, visit_local(e, expected_type));
return visit_local(e, expected_type);
case expr_kind::Const:
return copy_pos(e, visit_constant(e, expected_type));
return visit_constant(e, expected_type);
case expr_kind::Lambda:
return copy_pos(e, visit_lambda(e, expected_type));
return visit_lambda(e, expected_type);
case expr_kind::Pi:
return copy_pos(e, visit_pi(e));
return visit_pi(e);
case expr_kind::App:
return copy_pos(e, visit_app(e, expected_type));
return visit_app(e, expected_type);
case expr_kind::Let:
return copy_pos(e, visit_let(e, expected_type));
return visit_let(e, expected_type);
case expr_kind::Quote:
if (is_expr_quote(e))
return copy_pos(e, visit_expr_quote(e, expected_type));
return visit_expr_quote(e, expected_type);
else
return e;
}
lean_unreachable(); // LCOV_EXCL_LINE
}
});
lean_assert(!contains_pos(instantiate_mvars(e2)));
return e2;
}
expr elaborator::get_default_numeral_type() {
@ -3821,6 +3833,7 @@ void elaborator::ensure_no_unassigned_metavars(expr & e) {
// TODO(gabriel): this needs to change e
if (!has_expr_metavar(e)) return;
for_each(e, [&](expr const & e, unsigned) {
lean_assert(!get_pos(e));
if (!has_expr_metavar(e)) return false;
if (is_metavar_decl_ref(e) && !m_ctx.is_assigned(e)) {
tactic_state s = mk_tactic_state_for(e);
@ -3828,7 +3841,7 @@ void elaborator::ensure_no_unassigned_metavars(expr & e) {
auto ty = m_ctx.mctx().get_metavar_decl(e).get_type();
if (!has_synth_sorry(ty))
report_error(s, "context:", "don't know how to synthesize placeholder", e);
m_ctx.assign(e, copy_pos(e, mk_sorry(ty)));
m_ctx.assign(e, mk_sorry(ty));
ensure_no_unassigned_metavars(ty);
auto val = instantiate_mvars(e);
@ -3942,7 +3955,7 @@ struct sanitize_param_names_fn : public replace_visitor {
into regular kernel meta-variables. */
static expr replace_with_simple_metavars(metavar_context mctx, name_map<expr> & cache, expr const & e) {
if (!has_expr_metavar(e)) return e;
return replace_propagating_pos(e, [&](expr const & e, unsigned) {
return replace(e, [&](expr const & e, unsigned) {
if (is_metavar(e)) {
if (auto r = cache.find(mvar_name(e))) {
return some_expr(*r);
@ -4077,7 +4090,7 @@ static optional<expr> resolve_local_name_core(environment const & env, local_con
/* check local_refs */
if (auto ref = get_local_ref(env, id)) {
/* ref may contain local references that have new names at lctx. */
return some_expr(copy_pos(src, replace_propagating_pos(*ref, [&](expr const & e, unsigned) {
return some_expr(copy_pos(src, replace(*ref, [&](expr const & e, unsigned) {
if (is_local(e)) {
if (auto decl = lctx.find_local_decl_from_user_name(local_pp_name(e))) {
return some_expr(decl->mk_ref());

86
src/frontends/lean/inductive_cmds.cpp
View file

@ -66,16 +66,16 @@ static level mk_succn(level const & l, unsigned offset) {
static void convert_params_to_kernel(elaborator & elab, buffer<expr> const & lctx_params, buffer<expr> & kernel_params) {
for (unsigned i = 0; i < lctx_params.size(); ++i) {
expr new_type = replace_locals(elab.infer_type(lctx_params[i]), i, lctx_params.data(), kernel_params.data());
kernel_params.push_back(update_local(lctx_params[i], new_type));
kernel_params.push_back(update_local_p(lctx_params[i], new_type));
}
}
static void replace_params(buffer<expr> const & params, buffer<expr> const & new_params, buffer<expr> const & inds, buffer<expr> const & new_inds,
buffer<expr> const & intro_rules, buffer<expr> & new_intro_rules) {
for (expr const & ir : intro_rules) {
expr new_type = replace_locals(local_type(ir), params, new_params);
expr new_type = replace_locals(local_type_p(ir), params, new_params);
new_type = replace_locals(new_type, inds, new_inds);
new_intro_rules.push_back(update_local(ir, new_type));
new_intro_rules.push_back(update_local_p(ir, new_type));
}
}
@ -141,8 +141,8 @@ class inductive_cmd_fn {
for (unsigned i = 0; i < params.size(); i++) {
expr const & param = params[i];
if (m_p.is_local_decl_user_name(param) &&
!m_p.is_local_variable_user_name(local_pp_name(param))) {
expr const * klocal = m_p.get_local(local_pp_name(param));
!m_p.is_local_variable_user_name(local_pp_name_p(param))) {
expr const * klocal = m_p.get_local(local_pp_name_p(param));
lean_assert(klocal);
params[j] = *klocal;
j++;
@ -186,9 +186,9 @@ class inductive_cmd_fn {
bool has_explicit_level(buffer<buffer<expr> > const & intro_rules) {
for (buffer<expr> const & irs : intro_rules) {
for (expr const & ir : irs) {
name_set ls = collect_univ_params_ignoring_locals(local_type(ir), name_set());
name_set ls = collect_univ_params_ignoring_locals(local_type_p(ir), name_set());
if (!ls.empty()) {
lean_trace(name({"inductive", "lp_names"}), tout() << "explicit universe in '" << local_name(ir) << "': " << local_type(ir) << "\n";);
lean_trace(name({"inductive", "lp_names"}), tout() << "explicit universe in '" << local_name_p(ir) << "': " << local_type_p(ir) << "\n";);
return true;
}
}
@ -203,7 +203,7 @@ class inductive_cmd_fn {
// Create aliases/local refs
levels ctx_levels = collect_local_nonvar_levels(m_p, names(m_lp_names));
for (expr const & ind : inds) {
name d_name = local_name(ind);
name d_name = local_name_p(ind);
name d_short_name(d_name.get_string());
m_env = add_alias(m_p, m_env, false, d_name, ctx_levels, params_only);
name rec_name = mk_rec_name(d_name);
@ -215,7 +215,7 @@ class inductive_cmd_fn {
}
for (buffer<expr> const & irs : intro_rules) {
for (expr const & ir : irs) {
name ir_name = local_name(ir);
name ir_name = local_name_p(ir);
m_env = add_alias(m_p, m_env, true, ir_name, ctx_levels, params_only);
}
}
@ -308,7 +308,7 @@ class inductive_cmd_fn {
lean_assert(m_infer_result_universe);
buffer<level> r_lvls;
for (unsigned i = 0; i < num_intro_rules; i++) {
accumulate_levels(local_type(intro_rules[i]), r_lvls);
accumulate_levels(local_type_p(intro_rules[i]), r_lvls);
}
return mk_result_level(r_lvls);
}
@ -343,7 +343,7 @@ class inductive_cmd_fn {
while (is_pi(ty)) {
expr arg_ty = binding_domain(ty);
for (expr const & ind : inds) {
if (static_cast<bool>(find(arg_ty, [&](expr const & e, unsigned) { return is_mlocal(e) && local_name(e) == local_name(ind); }))) {
if (static_cast<bool>(find(arg_ty, [&](expr const & e, unsigned) { return is_mlocal(e) && local_name_p(e) == local_name_p(ind); }))) {
level nested_level = get_level(ctx, arg_ty);
lean_trace(name({"inductive", "unify"}), tout() << nested_level << " =?= " << resultant_level << "\n";);
if (!ctx.is_def_eq(mk_sort(nested_level), mk_sort(resultant_level))) {
@ -358,7 +358,7 @@ class inductive_cmd_fn {
void check_constant_resultant_universe(expr const & ir, level const & constant_resultant_level) {
type_context_old ctx(m_env);
expr ty = local_type(ir);
expr ty = local_type_p(ir);
unsigned ir_arg = 0;
while (is_pi(ty)) {
ir_arg++;
@ -366,7 +366,7 @@ class inductive_cmd_fn {
level arg_level = get_level(ctx, arg_ty);
if (!(is_geq(constant_resultant_level, arg_level) || is_zero(constant_resultant_level))) {
throw exception(sstream() << "universe level of type_of(arg #" << ir_arg << ") "
<< "of '" << local_name(ir) << "' is too big for the corresponding inductive datatype");
<< "of '" << local_name_p(ir) << "' is too big for the corresponding inductive datatype");
}
expr local = ctx.push_local(binding_name(ty), arg_ty, binding_info(ty));
ty = instantiate(binding_body(ty), local);
@ -379,7 +379,7 @@ class inductive_cmd_fn {
m_p.next();
while (true) {
m_pos = m_p.pos();
name ir_name = local_name(ind) + m_p.check_atomic_id_next("invalid introduction rule, atomic identifier expected");
name ir_name = local_name_p(ind) + m_p.check_atomic_id_next("invalid introduction rule, atomic identifier expected");
if (prepend_ns)
ir_name = get_namespace(m_env) + ir_name;
parser::local_scope S(m_p);
@ -409,7 +409,7 @@ class inductive_cmd_fn {
/** \brief Add a namespace for each inductive datatype */
void add_namespaces(buffer<expr> const & inds) {
for (expr const & ind : inds) {
m_env = add_namespace(m_env, local_name(ind));
m_env = add_namespace(m_env, local_name_p(ind));
}
}
@ -423,11 +423,11 @@ class inductive_cmd_fn {
buffer<expr> & new_params, buffer<expr> & new_inds, buffer<buffer<expr> > & new_intro_rules) {
options opts = m_p.get_options();
bool recover_from_errors = true;
elaborator elab(m_env, opts, local_pp_name(inds[0]), metavar_context(), local_context(), recover_from_errors);
elaborator elab(m_env, opts, local_pp_name_p(inds[0]), metavar_context(), local_context(), recover_from_errors);
buffer<expr> params_no_inds;
for (expr const & p : params) {
if (!std::any_of(inds.begin(), inds.end(), [&](expr const & ind) { return local_name(ind) == local_name(p); }))
if (!std::any_of(inds.begin(), inds.end(), [&](expr const & ind) { return local_name_p(ind) == local_name_p(p); }))
params_no_inds.push_back(p);
}
@ -439,7 +439,7 @@ class inductive_cmd_fn {
level result_level;
bool first = true;
for (expr const & ind : inds) {
expr new_ind_type = local_type(ind);
expr new_ind_type = local_type_p(ind);
if (is_placeholder(new_ind_type))
new_ind_type = mk_sort(mk_level_placeholder());
new_ind_type = elab.elaborate(replace_locals(new_ind_type, params_no_inds, new_params));
@ -459,17 +459,17 @@ class inductive_cmd_fn {
throw_error("mutually inductive types must live in the same universe");
}
}
new_inds.push_back(update_local(ind, new_ind_type));
new_inds.push_back(update_local_p(ind, new_ind_type));
}
for (buffer<expr> const & irs : intro_rules) {
new_intro_rules.emplace_back();
replace_params(params_no_inds, new_params, inds, new_inds, irs, new_intro_rules.back());
for (expr & new_ir : new_intro_rules.back()) {
expr new_ir_type = elab.elaborate(local_type(new_ir));
expr new_ir_type = elab.elaborate(local_type_p(new_ir));
new_ir_type = normalize(new_ir_type);
new_ir = update_local(new_ir, new_ir_type);
lean_trace(name({"inductive", "infer_resultant"}), tout() << "[elaborated ir]: " << local_type(new_ir) << "\n";);
new_ir = update_local_p(new_ir, new_ir_type);
lean_trace(name({"inductive", "infer_resultant"}), tout() << "[elaborated ir]: " << local_type_p(new_ir) << "\n";);
}
}
@ -534,8 +534,8 @@ class inductive_cmd_fn {
lean_trace(name({"inductive", "infer_resultant"}), tout() << "[resultant_level]: " << resultant_level << "\n";);
lean_trace(name({"inductive", "infer_resultant"}), tout() << "[replacement_level]: " << replacement_level << "\n";);
for (unsigned i = offsets[0]; i < offsets[0] + offsets[1]; ++i) {
expr ind_type = replace_u(local_type(all_exprs[i]), replacement_level);
new_inds.push_back(update_local(all_exprs[i], ind_type));
expr ind_type = replace_u(local_type_p(all_exprs[i]), replacement_level);
new_inds.push_back(update_local_p(all_exprs[i], ind_type));
}
} else {
for (unsigned i = offsets[0]; i < offsets[0] + offsets[1]; ++i) {
@ -550,7 +550,7 @@ class inductive_cmd_fn {
// We replace the inds appearing in the types of introduction rules with constants
buffer<expr> c_inds;
for (expr const & ind : inds) {
c_inds.push_back(mk_app(mk_constant(local_name(ind), param_names_to_levels(names(m_lp_names))), new_params));
c_inds.push_back(mk_app(mk_constant(local_name_p(ind), param_names_to_levels(names(m_lp_names))), new_params));
}
unsigned offset = offsets[0] + offsets[1];
@ -559,10 +559,10 @@ class inductive_cmd_fn {
for (unsigned j = 0; j < offsets[i]; ++j) {
expr new_ir = all_exprs[offset+j];
if (m_infer_result_universe) {
new_ir = update_local(new_ir, replace_u(local_type(new_ir), replacement_level));
unify_nested_occurrences(m_ctx, local_type(new_ir), inds, resultant_level);
new_ir = update_local_p(new_ir, replace_u(local_type_p(new_ir), replacement_level));
unify_nested_occurrences(m_ctx, local_type_p(new_ir), inds, resultant_level);
} else if (is_constant) {
unify_nested_occurrences(m_ctx, local_type(new_ir), inds, m_u_meta_assignment);
unify_nested_occurrences(m_ctx, local_type_p(new_ir), inds, m_u_meta_assignment);
}
new_ir = replace_locals(new_ir, offsets[1], all_exprs.data() + offsets[0], c_inds.data());
new_intro_rules.back().push_back(new_ir);
@ -580,7 +580,7 @@ class inductive_cmd_fn {
for (expr const & e : all_exprs) {
lean_trace(name({"inductive", "finalize"}),
tout() << local_name(e) << " (" << local_pp_name(e) << ") : " << local_type(e) << "\n";);
tout() << local_name_p(e) << " (" << local_pp_name_p(e) << ") : " << local_type_p(e) << "\n";);
}
}
@ -593,10 +593,10 @@ class inductive_cmd_fn {
m_explicit_levels = !m_lp_names.empty();
m_mut_attrs.push_back({});
ind = mk_local(get_namespace(m_p.env()) + local_name(ind), local_name(ind), local_type(ind), local_info(ind));
ind = mk_local(get_namespace(m_p.env()) + local_name_p(ind), local_name_p(ind), local_type_p(ind), local_info_p(ind));
lean_trace(name({"inductive", "parse"}),
tout() << local_name(ind) << " : " << local_type(ind) << "\n";);
tout() << local_name_p(ind) << " : " << local_type_p(ind) << "\n";);
m_p.add_local(ind);
m_p.parse_local_notation_decl();
@ -607,11 +607,13 @@ class inductive_cmd_fn {
ind_intro_rules.push_back(ind);
ind_intro_rules.append(intro_rules);
// HACK: without this line, `ind` would be wrapped in an `as_is` annotation
params.push_back(ind);
collect_implicit_locals(m_p, m_lp_names, params, ind_intro_rules);
for (expr const & e : params) {
lean_trace(name({"inductive", "params"}),
tout() << local_name(e) << " (" << local_pp_name(e) << ") : " << local_type(e) << "\n";);
tout() << local_name_p(e) << " (" << local_pp_name_p(e) << ") : " << local_type_p(e) << "\n";);
}
return ind;
@ -628,13 +630,13 @@ class inductive_cmd_fn {
for (expr const & pre_ind : pre_inds) {
m_pos = m_p.pos();
expr ind_type; decl_attributes attrs;
std::tie(ind_type, attrs) = parse_inner_header(m_p, local_pp_name(pre_ind));
std::tie(ind_type, attrs) = parse_inner_header(m_p, local_pp_name_p(pre_ind));
check_attrs(attrs);
m_mut_attrs.push_back(attrs);
lean_trace(name({"inductive", "parse"}), tout() << local_name(pre_ind) << " : " << ind_type << "\n";);
lean_trace(name({"inductive", "parse"}), tout() << local_name_p(pre_ind) << " : " << ind_type << "\n";);
intro_rules.emplace_back();
parse_intro_rules(!params.empty(), pre_ind, intro_rules.back(), true);
expr ind = mk_local(get_namespace(m_p.env()) + local_name(pre_ind), ind_type);
expr ind = mk_local(get_namespace(m_p.env()) + local_name_p(pre_ind), ind_type);
inds.push_back(ind);
}
@ -681,13 +683,13 @@ public:
We are currently using the same doc string for all elements.
*/
if (m_meta_info.m_doc_string)
m_env = add_doc_string(m_env, local_name(ind), *m_meta_info.m_doc_string);
m_env = add_doc_string(m_env, local_name_p(ind), *m_meta_info.m_doc_string);
/* Apply attributes last so that they may access any information on the new decl */
m_env = m_meta_info.m_attrs.apply(m_env, m_p.ios(), local_name(ind));
m_env = m_meta_info.m_attrs.apply(m_env, m_p.ios(), local_name_p(ind));
}
lean_assert(new_inds.size() == m_mut_attrs.size());
for (unsigned i = 0; i < new_inds.size(); ++i)
m_env = m_mut_attrs[i].apply(m_env, m_p.ios(), local_name(new_inds[i]));
m_env = m_mut_attrs[i].apply(m_env, m_p.ios(), local_name_p(new_inds[i]));
}
struct parse_result {
@ -721,12 +723,12 @@ public:
for (unsigned i = 0; i < r.m_inds.size(); i++) {
buffer<constructor> cnstrs;
for (expr const & intro : r.m_intro_rules[i]) {
implicit_infer_kind kind = get_implicit_infer_kind(local_name(intro));
expr type = Pi(r.m_params, local_type(intro));
implicit_infer_kind kind = get_implicit_infer_kind(local_name_p(intro));
expr type = Pi(r.m_params, local_type_p(intro));
type = infer_implicit_params(type, num_params, kind);
cnstrs.push_back(constructor(local_name(intro), type));
cnstrs.push_back(constructor(local_name_p(intro), type));
}
ind_types.push_back(inductive_type(local_name(r.m_inds[i]), Pi(r.m_params, local_type(r.m_inds[i])), constructors(cnstrs)));
ind_types.push_back(inductive_type(local_name_p(r.m_inds[i]), Pi(r.m_params, local_type_p(r.m_inds[i])), constructors(cnstrs)));
}
m_env = m_env.add(mk_inductive_decl(names(m_lp_names), nat(num_params), inductive_types(ind_types), m_meta_info.m_modifiers.m_is_meta));
}

7
src/frontends/lean/local_context_adapter.cpp
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "kernel/find_fn.h"
#include "library/locals.h"
#include "library/pos_info_provider.h"
#include "frontends/lean/local_context_adapter.h"
namespace lean {
@ -35,21 +36,21 @@ local_context_adapter::local_context_adapter(local_expr_decls const & ldecls) {
while (i > 0) {
--i;
pair<name, expr> const & entry = entries[i];
expr const & local = entry.second;
expr const & local = unwrap_pos(entry.second);
if (!is_local(local)) continue;
add_local(local);
}
}
local_context_adapter::local_context_adapter(list<expr> const & lctx) {
lean_assert(std::all_of(lctx.begin(), lctx.end(), is_local));
lean_assert(std::all_of(lctx.begin(), lctx.end(), is_local_p));
lean_assert(m_lctx.empty() && m_locals.empty());
buffer<expr> entries;
to_buffer(lctx, entries);
unsigned i = entries.size();
while (i > 0) {
--i;
add_local(entries[i]);
add_local(unwrap_pos(entries[i]));
}
}

2
src/frontends/lean/parse_table.cpp
View file

@ -489,7 +489,7 @@ static expr expand_pp_pattern(unsigned num, transition const * ts, expr const &
optional<head_index> get_head_index(unsigned num, transition const * ts, expr const & a) {
if (is_simple(num, ts)) {
expr n = expand_pp_pattern(num, ts, a);
expr n = unwrap_pos(expand_pp_pattern(num, ts, a));
if (!is_var(n))
return some(head_index(n));
}

136
src/frontends/lean/parser.cpp
View file

@ -249,15 +249,8 @@ name parser::mk_anonymous_inst_name() {
return n;
}
void parser::erase_pos(expr const & e) {
::lean::erase_pos(e);
}
expr parser::update_pos(expr e, pos_info p) {
return ::lean::save_pos(e, p);
}
expr parser::rec_save_pos(expr const & e, pos_info p) {
return e;
unsigned m = std::numeric_limits<unsigned>::max();
pos_info dummy(m, 0);
for_each(e, [&](expr const & e, unsigned) {
@ -273,45 +266,12 @@ expr parser::rec_save_pos(expr const & e, pos_info p) {
/** \brief Create a copy of \c e, and the position of new expression with p */
expr parser::copy_with_new_pos(expr const & e, pos_info p) {
switch (e.kind()) {
case expr_kind::Sort: case expr_kind::Const: case expr_kind::MVar:
case expr_kind::BVar: case expr_kind::FVar: case expr_kind::Lit:
return save_pos(copy(e), p);
case expr_kind::MData:
return save_pos(::lean::mk_mdata(mdata_data(e), copy_with_new_pos(mdata_expr(e), p)), p);
case expr_kind::Proj:
return save_pos(::lean::mk_proj(proj_idx(e), copy_with_new_pos(proj_expr(e), p)), p);
case expr_kind::App:
return save_pos(::lean::mk_app(copy_with_new_pos(app_fn(e), p),
copy_with_new_pos(app_arg(e), p)),
p);
case expr_kind::Lambda:
return save_pos(::lean::mk_lambda(binding_name(e),
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p),
binding_info(e)),
p);
case expr_kind::Pi:
return save_pos(::lean::mk_pi(binding_name(e),
copy_with_new_pos(binding_domain(e), p),
copy_with_new_pos(binding_body(e), p),
binding_info(e)),
p);
case expr_kind::Let:
return save_pos(::lean::mk_let(let_name(e),
copy_with_new_pos(let_type(e), p),
copy_with_new_pos(let_value(e), p),
copy_with_new_pos(let_body(e), p)),
p);
case expr_kind::Quote:
if (is_pexpr_quote(e)) {
return save_pos(mk_pexpr_quote(copy_with_new_pos(get_pexpr_quote_value(e), p)), p);
} else {
return save_pos(e, p);
}
}
lean_unreachable(); // LCOV_EXCL_LINE
return replace(e, [&](expr const & e, unsigned) {
if (get_pos(e))
return some(save_pos(copy_with_new_pos(unwrap_pos(e), p), p));
else
return none_expr();
});
}
pos_info parser::pos_of(expr const & e, pos_info default_pos) const {
@ -402,8 +362,8 @@ name parser::check_atomic_decl_id_next(char const * msg) {
return id;
}
expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
return save_pos(::lean::mk_app(fn, arg), p);
expr parser::mk_app(expr fn, expr arg, pos_info const &) {
return ::lean::mk_app(fn, arg);
}
expr parser::mk_app(expr fn, buffer<expr> const & args, pos_info const & p) {
@ -485,8 +445,9 @@ void parser::add_local_expr(name const & n, expr const & p, bool is_variable) {
}
m_local_decls.insert(n, p);
if (is_variable) {
lean_assert(is_local(p));
m_variables.insert(local_name(p));
lean_assert(is_local_p(p));
lean_assert(!contains_pos(local_type_p(p)));
m_variables.insert(local_name_p(p));
}
}
@ -510,7 +471,7 @@ environment parser::add_local_ref(environment const & env, name const & n, expr
}
static void check_no_metavars(name const & n, expr const & e) {
lean_assert(is_local(e));
lean_assert(is_local_p(e));
if (has_metavar(e)) {
throw generic_exception(none_expr(), [=](formatter const & fmt) {
format r("failed to add declaration '");
@ -523,23 +484,23 @@ static void check_no_metavars(name const & n, expr const & e) {
}
void parser::add_variable(name const & n, expr const & v) {
lean_assert(is_local(v));
lean_assert(is_local_p(v));
check_no_metavars(n, v);
add_local_expr(n, v, true);
}
void parser::add_parameter(name const & n, expr const & p) {
lean_assert(is_local(p));
lean_assert(is_local_p(p));
check_no_metavars(n, p);
add_local_expr(n, p, false);
m_has_params = true;
}
bool parser::is_local_decl(expr const & l) {
lean_assert(is_local(l));
lean_assert(is_local_p(l));
// TODO(Leo): add a name_set with internal ids if this is a bottleneck
for (pair<name, expr> const & p : m_local_decls.get_entries()) {
if (is_local(p.second) && local_name(p.second) == local_name(l))
if (is_local_p(p.second) && local_name_p(p.second) == local_name_p(l))
return true;
}
return false;
@ -547,7 +508,7 @@ bool parser::is_local_decl(expr const & l) {
bool parser::update_local_binder_info(name const & n, binder_info bi) {
auto it = get_local(n);
if (!it || !is_local(*it)) return false;
if (!it || !is_local_p(*it)) return false;
buffer<pair<name, expr>> entries;
to_buffer(m_local_decls.get_entries(), entries);
@ -565,10 +526,10 @@ bool parser::update_local_binder_info(name const & n, binder_info bi) {
for (unsigned i = idx; i < entries.size(); i++) {
expr const & curr_e = entries[i].second;
expr r = is_local(curr_e) ? local_type(curr_e) : curr_e;
expr r = is_local_p(curr_e) ? local_type_p(curr_e) : curr_e;
if (std::any_of(old_locals.begin(), old_locals.end(), [&](expr const & l) { return depends_on(r, l); })) {
r = replace_locals(r, old_locals, new_locals);
if (is_local(curr_e)) {
if (is_local_p(curr_e)) {
expr new_e = update_local(curr_e, r);
entries[i].second = new_e;
old_locals.push_back(curr_e);
@ -602,7 +563,7 @@ list<expr> parser::locals_to_context() const {
return map_filter<expr>(m_local_decls.get_entries(),
[](pair<name, expr> const & p, expr & out) {
out = p.second;
return is_local(p.second);
return is_local_p(p.second);
});
}
@ -1179,9 +1140,9 @@ void parser::process_postponed(buffer<expr> const & args, bool is_left,
scoped_idx++;
if (is_var(a.get_rec(), 0)) {
if (a.use_lambda_abstraction())
r = Fun(ps_sz, ps.data(), r);
r = Fun_p(ps_sz, ps.data(), r);
else
r = Pi(ps_sz, ps.data(), r);
r = Pi_p(ps_sz, ps.data(), r);
r = rec_save_pos(r, binder_pos);
} else {
expr rec = copy_with_new_pos(a.get_rec(), p);
@ -1190,9 +1151,9 @@ void parser::process_postponed(buffer<expr> const & args, bool is_left,
--i;
expr const & l = ps[i];
if (a.use_lambda_abstraction())
r = Fun(l, r);
r = Fun_p(l, r);
else
r = Pi(l, r);
r = Pi_p(l, r);
r = save_pos(r, binder_pos);
new_args.push_back(r);
r = instantiate_rev(rec, new_args.size(), new_args.data());
@ -1403,7 +1364,7 @@ expr parser::parse_notation(parse_table t, expr * left) {
r = instantiate_rev(r, args.size(), args.data());
}
if (create_lambdas) {
r = rec_save_pos(eta_reduce(Fun(args, r)), p);
r = rec_save_pos(eta_reduce(Fun_p(args, r)), p);
}
cs.push_back(r);
}
@ -1537,7 +1498,7 @@ struct to_pattern_fn {
}
void add_new_local(expr const & l) {
name const & n = local_pp_name(l);
name const & n = local_pp_name_p(l);
if (!n.is_atomic()) {
return m_parser.maybe_throw_error({
"invalid pattern: variable, constructor or constant tagged as pattern expected",
@ -1553,20 +1514,21 @@ struct to_pattern_fn {
}
void collect_new_local(expr const & e) {
name const & n = local_pp_name(e);
name const & n = local_pp_name_p(e);
bool resolve_only = true;
expr new_e = m_parser.id_to_expr(n, m_parser.pos_of(e), resolve_only);
expr unew_e = unwrap_pos(new_e);
if (is_as_atomic(new_e)) {
new_e = get_app_fn(get_as_atomic_arg(new_e));
if (is_explicit(new_e))
new_e = get_explicit_arg(new_e);
}
if (is_constant(new_e) && is_pattern_constant(const_name(new_e))) {
if (is_constant(unew_e) && is_pattern_constant(const_name(unew_e))) {
m_locals_map.insert(n, new_e);
return;
} else if (is_choice(new_e)) {
if (auto r = process_choice(new_e, e)) {
} else if (is_choice(unew_e)) {
if (auto r = process_choice(unew_e, e)) {
m_locals_map.insert(n, *r);
return;
} else {
@ -1601,7 +1563,7 @@ struct to_pattern_fn {
<< "and this kind of overloading is not currently supported in patterns",
m_parser.pos_of(e)});
}
} else if (is_local(e)) {
} else if (is_local_p(e)) {
if (skip_main_fn) {
// do nothing
} else {
@ -1622,6 +1584,8 @@ struct to_pattern_fn {
collect_new_locals(val, false);
} else if (is_annotation(e)) {
collect_new_locals(get_annotation_arg(e), skip_main_fn);
} else if (get_pos(e)) {
collect_new_locals(unwrap_pos(e), skip_main_fn);
} else if (is_constant(e) && is_pattern_constant(const_name(e))) {
// do nothing
} else {
@ -1633,9 +1597,9 @@ struct to_pattern_fn {
}
expr to_expr(expr const & e) {
return replace_propagating_pos(e, [&](expr const & e, unsigned) {
if (is_local(e)) {
if (auto r = m_locals_map.find(local_pp_name(e)))
return replace(e, [&](expr const & e, unsigned) {
if (is_local_p(e)) {
if (auto r = m_locals_map.find(local_pp_name_p(e)))
return some_expr(*r);
else
return some_expr(m_parser.patexpr_to_expr(e));
@ -1679,8 +1643,8 @@ struct to_pattern_fn {
new_args.push_back(visit(get_choice(e, i)));
return mk_choice(new_args.size(), new_args.data());
}
} else if (is_local(e)) {
if (auto r = m_locals_map.find(local_pp_name(e)))
} else if (is_local_p(e)) {
if (auto r = m_locals_map.find(local_pp_name_p(e)))
return *r;
else
return e;
@ -1701,6 +1665,8 @@ struct to_pattern_fn {
return copy_pos(e, mk_structure_instance(info));
} else if (is_annotation(e)) {
return copy_pos(e, mk_annotation(get_annotation_kind(e), visit(get_annotation_arg(e))));
} else if (get_pos(e)) {
return visit(unwrap_pos(e));
} else if (is_constant(e) && is_pattern_constant(const_name(e))) {
return e;
} else {
@ -1740,7 +1706,7 @@ static expr quote(expr const & e) {
return mk_expr_placeholder();
case expr_kind::FVar:
throw elaborator_exception(e, sstream() << "invalid quotation, unexpected local constant '"
<< local_pp_name(e) << "'");
<< local_pp_name_p(e) << "'");
case expr_kind::App:
if (is_metavar_app(e)) {
/* Remark: metavariable applications of the form `?m x1 ... xn` may be introduced
@ -1784,7 +1750,7 @@ static expr elaborate_quote(parser & p, expr e) {
name x("_x");
buffer<expr> locals;
buffer<expr> aqs;
e = replace_propagating_pos(e, [&](expr const & t, unsigned) {
e = replace(e, [&](expr const & t, unsigned) {
if (is_antiquote(t)) {
expr local = mk_local(p.next_name(), x.append_after(locals.size() + 1),
mk_expr_placeholder(), mk_binder_info());
@ -1794,7 +1760,7 @@ static expr elaborate_quote(parser & p, expr e) {
}
return none_expr();
});
e = copy_pos(e, Fun(locals, e));
e = copy_pos(e, Fun_p(locals, e));
metavar_context ctx;
local_context lctx;
@ -1814,7 +1780,7 @@ static expr elaborate_quote(parser & p, expr e) {
expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buffer<expr> & new_locals) {
undef_id_to_local_scope scope(*this);
auto e = replace_propagating_pos(pat_or_expr, [&](expr const & e) {
auto e = replace(pat_or_expr, [&](expr const & e) {
if (is_expr_quote(e)) {
return some_expr(elaborate_quote(*this, e));
} else {
@ -2169,7 +2135,7 @@ expr parser::parse_nud() {
expr e = parse_id();
// if `id` is immediately followed by `@`, parse an as pattern `id@pat`
if (in_pattern() && id.is_atomic() && curr_is_token(get_explicit_tk())) {
lean_assert(is_local(e));
lean_assert(is_local_p(e));
// note: This number is not accurate for an escaped identifier. We should be able to do a better job
// in the new backtracking parser.
auto id_len = utf8_strlen(id.to_string().c_str());
@ -2208,11 +2174,12 @@ expr parser::parse_led(expr left) {
if (is_sort_wo_universe(left) &&
(curr_is_numeral() || curr_is_identifier() || curr_is_token(get_lparen_tk()) || curr_is_token(get_placeholder_tk()))) {
left = get_annotation_arg(left);
level left_l = sort_level(unwrap_pos(left));
level l = parse_level(get_max_prec());
lean_assert(sort_level(left) == mk_level_one() || sort_level(left) == mk_level_zero());
if (sort_level(left) == mk_level_one())
lean_assert(left_l == mk_level_one() || left_l == mk_level_zero());
if (left_l == mk_level_one())
l = mk_succ(l);
return copy_pos(left, update_sort(left, l));
return copy_pos(left, update_sort(unwrap_pos(left), l));
} else {
switch (curr()) {
case token_kind::Keyword:
@ -2618,7 +2585,6 @@ level parser::parser_error_or_level(parser_error && err) {
}
bool parse_commands(environment & env, io_state & ios, char const * fname) {
reset_positions();
// st_task_queue tq;
// scope_global_task_queue scope(&tq);
fs_module_vfs vfs;

10
src/frontends/lean/parser.h
View file

@ -267,8 +267,6 @@ public:
virtual pos_info pos() const override final { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
expr rec_save_pos(expr const & e, pos_info p);
expr rec_save_pos(expr const & e, optional<pos_info> p) { return p ? rec_save_pos(e, *p) : e; }
expr update_pos(expr e, pos_info p);
void erase_pos(expr const & e);
pos_info pos_of(expr const & e, pos_info default_pos) const;
pos_info pos_of(expr const & e) const { return pos_of(e, pos()); }
pos_info cmd_pos() const { return m_last_cmd_pos; }
@ -476,15 +474,15 @@ public:
environment add_local_ref(environment const & env, name const & n, expr const & ref);
void add_variable(name const & n, expr const & p);
void add_parameter(name const & n, expr const & p);
void add_local(expr const & p) { return add_local_expr(local_pp_name(p), p); }
void add_local(expr const & p) { return add_local_expr(local_pp_name_p(p), p); }
bool has_params() const { return m_has_params; }
bool is_local_decl_user_name(expr const & l) const { return is_local(l) && m_local_decls.contains(local_pp_name(l)); }
bool is_local_decl_user_name(expr const & l) const { return is_local_p(l) && m_local_decls.contains(local_pp_name_p(l)); }
bool is_local_decl(expr const & l);
bool is_local_level_variable(name const & n) const { return m_level_variables.contains(n); }
bool is_local_variable(expr const & e) const { return m_variables.contains(local_name(e)); }
bool is_local_variable_user_name(name const & n) const {
if (expr const * d = m_local_decls.find(n))
return is_local(*d) && m_variables.contains(local_name(*d));
return is_local_p(*d) && m_variables.contains(local_name_p(*d));
else
return false;
}
@ -499,7 +497,7 @@ public:
bool is_local_level(name const & n) const { return m_local_level_decls.contains(n); }
/** \brief Position of the local declaration named \c n in the sequence of local decls. */
unsigned get_local_index(name const & n) const;
unsigned get_local_index(expr const & e) const { return get_local_index(local_pp_name(e)); }
unsigned get_local_index(expr const & e) const { return get_local_index(local_pp_name_p(e)); }
/** \brief Return the local parameter named \c n */
expr const * get_local(name const & n) const { return m_local_decls.find(n); }
/** \brief Return local declarations as a list of local constants. */

4
src/frontends/lean/pp.cpp
View file

@ -1228,7 +1228,9 @@ bool pretty_fn::match(level const & p, level const & l) {
}
bool pretty_fn::match(expr const & p, expr const & e, buffer<optional<expr>> & args) {
if (is_explicit(p)) {
if (get_pos(p)) {
return match(unwrap_pos(p), e, args);
} else if (is_explicit(p)) {
return match(get_explicit_arg(p), e, args);
} else if (is_as_atomic(p)) {
return match(get_app_fn(get_as_atomic_arg(p)), e, args);

73
src/frontends/lean/structure_cmd.cpp
View file

@ -251,8 +251,8 @@ struct structure_cmd_fn {
m_local(local), m_default_val(default_val), m_kind(kind), m_infer_kind(infer_kind),
m_has_new_default(default_val && kind == field_kind::new_field) {}
name const & get_name() const { return local_name(m_local); }
expr const & get_type() const { return local_type(m_local); }
name const & get_name() const { return local_name_p(m_local); }
expr const & get_type() const { return local_type_p(m_local); }
};
parser & m_p;
@ -340,7 +340,7 @@ struct structure_cmd_fn {
Returns the structure's name if successful.
*/
name const & check_parent(expr const & parent) {
expr fn = get_app_fn(parent);
expr fn = unwrap_pos(get_app_fn(parent));
if (m_subobjects && is_local_ref(fn))
fn = get_explicit_arg(get_app_fn(get_as_atomic_arg(fn)));
if (!is_constant(fn))
@ -428,18 +428,19 @@ struct structure_cmd_fn {
m_type = m_p.parse_expr();
while (is_annotation(m_type))
m_type = get_annotation_arg(m_type);
if (!is_sort(m_type))
if (!is_sort(unwrap_pos(m_type)))
throw parser_error("invalid 'structure', 'Type' expected", pos);
m_inductive_predicate = is_zero(sort_level(m_type));
level const & l = sort_level(unwrap_pos(m_type));
m_inductive_predicate = is_zero(l);
if (m_inductive_predicate) {
m_infer_result_universe = false;
} else if (is_one_placeholder(sort_level(m_type))) {
} else if (is_one_placeholder(l)) {
m_infer_result_universe = false;
m_type = m_p.save_pos(mk_sort(mk_level_one()), pos);
} else {
m_infer_result_universe = is_placeholder(sort_level(m_type));
m_infer_result_universe = is_placeholder(l);
if (!m_infer_result_universe) {
if (!is_zero(sort_level(m_type)) && !is_not_zero(sort_level(m_type)))
if (!is_zero(l) && !is_not_zero(l))
throw parser_error("invalid universe polymorphic structure declaration, "
"the resultant universe is not Prop (i.e., 0), "
"but it may be Prop for some parameter values "
@ -490,7 +491,7 @@ struct structure_cmd_fn {
return elab(tmp);
} else {
expr new_tmp = elab(mk_arrow(in_header ? parent : mk_as_is(parent), tmp));
parent = copy_pos(parent, expr(binding_domain(new_tmp)));
parent = expr(binding_domain(new_tmp));
if (m_subobjects) {
// immediately register parent field so that we can use it in `mk_parent_expr` below
@ -517,10 +518,10 @@ struct structure_cmd_fn {
}
expr elaborate_local(bool as_is, expr & local, unsigned, expr const & tmp, tele_elab elab) {
expr new_tmp = elab(as_is ? Pi_as_is(local, tmp) : Pi(local, tmp));
expr new_local = update_local(local, binding_domain(new_tmp));
expr new_tmp = elab(as_is ? Pi_as_is(local, tmp) : Pi(local, tmp, m_p));
expr new_local = update_local_p(local, binding_domain(new_tmp));
local = new_local;
return instantiate(binding_body(new_tmp), new_local);
return instantiate(binding_body(new_tmp), unwrap_pos(new_local));
}
/** \brief elaborate parameters and "parent" types */
@ -688,7 +689,7 @@ struct structure_cmd_fn {
if (auto fidx = merge(parent, fname, ftype)) {
fmap.push_back(*fidx);
field = m_fields[*fidx].m_local;
if (local_info(field) != binding_info(intro_type)) {
if (local_info_p(field) != binding_info(intro_type)) {
throw elaborator_exception(parent,
sstream() << "invalid 'structure' header, field '" << fname <<
"' has already been declared with a different binder annotation");
@ -835,9 +836,9 @@ struct structure_cmd_fn {
type = parse_auto_param(m_p, type);
}
}
type = Pi(params, type);
type = Pi(params, type, m_p);
if (default_value_initialized)
default_value = Fun(params, default_value);
default_value = Fun(params, default_value, m_p);
}
if (default_value_initialized && !is_explicit(bi)) {
@ -899,14 +900,14 @@ struct structure_cmd_fn {
expr type = decl.get_type();
auto const & value = decl.m_default_val;
if (value && (!decl.m_has_new_default || is_placeholder(decl.get_type()))) {
new_tmp = elab(mk_let(decl.get_name(), type, *value, abstract(tmp, decl.m_local)));
decl.m_local = update_local(decl.m_local, let_type(new_tmp));
new_tmp = elab(mk_let(decl.get_name(), type, *value, abstract(tmp, unwrap_pos(decl.m_local))));
decl.m_local = update_local_p(decl.m_local, let_type(new_tmp));
decl.m_default_val = let_value(new_tmp);
new_tmp = instantiate(let_body(new_tmp), m_subobjects ? let_value(new_tmp) : decl.m_local);
new_tmp = instantiate(let_body(new_tmp), m_subobjects ? let_value(new_tmp) : unwrap_pos(decl.m_local));
} else if (!value || decl.m_kind == field_kind::new_field) {
new_tmp = elab(Pi(decl.m_local, tmp));
decl.m_local = update_local(decl.m_local, binding_domain(new_tmp));
new_tmp = instantiate(binding_body(new_tmp), decl.m_local);
new_tmp = elab(Pi(decl.m_local, tmp, m_p));
decl.m_local = update_local_p(decl.m_local, binding_domain(new_tmp));
new_tmp = instantiate(binding_body(new_tmp), unwrap_pos(decl.m_local));
} else {
new_tmp = elab(tmp);
}
@ -932,7 +933,7 @@ struct structure_cmd_fn {
expr type = decl.get_type();
expr value = *decl.m_default_val;
expr new_tmp = elab(mk_let(m_p.next_name(), type, value, tmp));
decl.m_local = update_local(decl.m_local, let_type(new_tmp), local_info(decl.m_local));
decl.m_local = update_local_p(decl.m_local, let_type(new_tmp), local_info_p(decl.m_local));
decl.m_default_val = let_value(new_tmp);
return let_body(new_tmp);
}
@ -1018,7 +1019,7 @@ struct structure_cmd_fn {
}
expr mk_structure_type() {
return Pi(m_params, m_type, m_p);
return Pi_p(m_params, m_type);
}
expr mk_structure_type_no_params() {
@ -1031,18 +1032,18 @@ struct structure_cmd_fn {
for (unsigned i = 0; i < m_fields.size(); i++) {
auto const & decl = m_fields[m_fields.size() - 1 - i];
if (decl.m_kind != field_kind::from_parent || !m_subobjects) {
r = abstract(r, decl.m_local);
r = abstract(r, unwrap_pos(decl.m_local));
name n = decl.get_name();
if (decl.m_kind == field_kind::subobject)
n = mk_internal_subobject_field_name(n);
r = mk_pi(n, decl.get_type(), r, local_info(decl.m_local));
r = mk_pi(n, decl.get_type(), r, local_info_p(decl.m_local));
}
}
return r;
}
expr mk_intro_type() {
expr r = Pi(m_params, mk_intro_type_no_params(), m_p);
expr r = Pi_p(m_params, mk_intro_type_no_params());
return infer_implicit_params(r, m_params.size(), m_mk_infer);
}
@ -1092,7 +1093,7 @@ struct structure_cmd_fn {
buffer<implicit_infer_kind> infer_kinds;
for (field_decl const & field : m_fields) {
if (!m_subobjects || field.m_kind != field_kind::from_parent) {
proj_names.push_back(m_name + local_name(field.m_local));
proj_names.push_back(m_name + local_name_p(field.m_local));
infer_kinds.push_back(
field.m_infer_kind != implicit_infer_kind::Implicit ? field.m_infer_kind : m_mk_infer);
}
@ -1104,7 +1105,7 @@ struct structure_cmd_fn {
bool is_param(expr const & local) {
for (auto const & param : m_params) {
if (local_name(param) == local_name(local))
if (local_name_p(param) == local_name_p(local))
return true;
}
return false;
@ -1124,8 +1125,8 @@ struct structure_cmd_fn {
/* Copy params first */
for (expr const & local : used_locals.get_collected()) {
if (is_param(local)) {
if (is_explicit(local_info(local)))
args.push_back(update_local(local, mk_implicit_binder_info()));
if (is_explicit(local_info_p(local)))
args.push_back(update_local_p(local, mk_implicit_binder_info()));
else
args.push_back(local);
}
@ -1133,7 +1134,7 @@ struct structure_cmd_fn {
/* Copy fields it depends on */
for (expr const & local : used_locals.get_collected()) {
if (!is_param(local))
args.push_back(update_local(local, mk_binder_info()));
args.push_back(update_local_p(local, mk_binder_info()));
}
name decl_name = name(m_name + field.get_name(), "_default");
name decl_prv_name;
@ -1144,9 +1145,9 @@ struct structure_cmd_fn {
}
/* TODO(Leo): add helper function for adding definition.
It should unfold_untrusted_macros */
expr decl_type = Pi(args, type);
expr decl_type = Pi_p(args, type);
val = mk_app(m_ctx, get_id_name(), val);
expr decl_value = Fun(args, val);
expr decl_value = Fun_p(args, val);
name_set used_univs;
used_univs = collect_univ_params(decl_value, used_univs);
used_univs = collect_univ_params(decl_type, used_univs);
@ -1246,14 +1247,14 @@ struct structure_cmd_fn {
if (m_meta_info.m_attrs.has_class())
bi = mk_inst_implicit_binder_info();
expr st = mk_local(m_p.next_name(), "s", st_type, bi);
expr coercion_type = infer_implicit(Pi(m_params, Pi(st, parent, m_p), m_p), m_params.size(), true);;
expr coercion_type = infer_implicit(Pi_p(m_params, Pi_p(st, parent)), m_params.size(), true);;
expr coercion_value = parent_intro;
for (unsigned idx : fmap) {
name proj_name = m_name + m_fields[idx].get_name();
expr proj = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), st);
coercion_value = mk_app(coercion_value, proj);
}
coercion_value = Fun(m_params, Fun(st, coercion_value, m_p), m_p);
coercion_value = Fun_p(m_params, Fun_p(st, coercion_value));
name coercion_name = coercion_names[i];
declaration coercion_decl = mk_definition_inferring_meta(m_env, coercion_name, lnames,
coercion_type, coercion_value);
@ -1327,6 +1328,8 @@ struct structure_cmd_fn {
add_ctx_locals();
remove_local_vars(m_p, m_ctx_locals);
m_ctx_levels = collect_local_nonvar_levels(m_p, names(m_level_names));
for (auto & p : m_params)
p = unwrap_pos(p);
declare_inductive_type();
declare_projections();
declare_defaults();

8
src/frontends/lean/util.cpp
View file

@ -230,16 +230,16 @@ expr Pi(expr const & local, expr const & e, parser & p) {
template<bool is_lambda>
static expr mk_binding_as_is(unsigned num, expr const * locals, expr const & b) {
expr r = abstract_propagating_pos(b, num, locals);
expr r = abstract_p(b, num, locals);
unsigned i = num;
while (i > 0) {
--i;
expr const & l = locals[i];
expr t = abstract_propagating_pos(local_type(l), i, locals);
expr t = abstract_p(local_type_p(l), i, locals);
if (is_lambda)
r = mk_lambda(local_pp_name(l), mk_as_is(t), r, local_info(l));
r = mk_lambda(local_pp_name_p(l), mk_as_is(t), r, local_info_p(l));
else
r = mk_pi(local_pp_name(l), mk_as_is(t), r, local_info(l));
r = mk_pi(local_pp_name_p(l), mk_as_is(t), r, local_info_p(l));
}
return r;
}

23
src/library/annotation.cpp
View file

@ -28,28 +28,35 @@ void register_annotation(name const & kind) {
g_annotation_maps->insert(mk_pair(kind, mk_annotation_kvmap(kind)));
}
bool is_annotation(expr const & e) {
return is_mdata(e) && get_name(mdata_data(e), *g_annotation);
optional<expr> is_annotation(expr const & e) {
expr e2 = unwrap_pos(e);
if (is_mdata(e2) && get_name(mdata_data(e2), *g_annotation))
return some_expr(e2);
else
return none_expr();
}
name get_annotation_kind(expr const & e) {
lean_assert(is_annotation(e));
return *get_name(mdata_data(e), *g_annotation);
auto o = is_annotation(e);
lean_assert(o);
return *get_name(mdata_data(*o), *g_annotation);
}
bool is_annotation(expr const & e, name const & kind) {
return is_annotation(e) && get_annotation_kind(e) == kind;
auto o = is_annotation(e);
return o && get_annotation_kind(*o) == kind;
}
expr const & get_annotation_arg(expr const & e) {
lean_assert(is_annotation(e));
return mdata_expr(e);
auto o = is_annotation(e);
lean_assert(o);
return mdata_expr(*o);
}
expr mk_annotation(name const & kind, expr const & e) {
auto it = g_annotation_maps->find(kind);
if (it != g_annotation_maps->end()) {
expr r = copy_pos(e, mk_mdata(it->second, e));
expr r = mk_mdata(it->second, e);
lean_assert(is_annotation(r));
lean_assert(get_annotation_kind(r) == kind);
return r;

2
src/library/annotation.h
View file

@ -21,7 +21,7 @@ void register_annotation(name const & n);
*/
expr mk_annotation(name const & kind, expr const & e);
/** \brief Return true iff \c e was created using #mk_annotation. */
bool is_annotation(expr const & e);
optional<expr> is_annotation(expr const & e);
/** \brief Return true iff \c e was created using #mk_annotation, and has tag \c kind. */
bool is_annotation(expr const & e, name const & kind);
/** \brief Return true iff \c e is of the form (a_1 ... (a_k e') ...)

3
src/library/derive_attribute.cpp
View file

@ -62,7 +62,8 @@ static exprs_attribute const & get_derive_attribute() {
}
static environment derive(environment env, options const & opts, name const & n, exprs const & clss) {
for (auto const & cls : clss) {
for (auto cls : clss) {
cls = unwrap_pos(cls);
auto const & d = env.get(n);
if (!is_constant(cls) || !d.is_definition())
throw exception("don't know how to derive this");

13
src/library/equations_compiler/equations.cpp
View file

@ -63,12 +63,13 @@ expr mk_equation(expr const & lhs, expr const & rhs, bool ignore_if_unused) {
expr mk_no_equation() { return mk_mdata(*g_no_equation, mk_Prop()); }
bool is_equation(expr const & e) {
return is_mdata(e) && get_bool(mdata_data(e), *g_equation_name);
expr e2 = unwrap_pos(e);
return is_mdata(e2) && get_bool(mdata_data(e2), *g_equation_name);
}
bool ignore_equation_if_unused(expr const & e) {
lean_assert(is_equation(e));
return *get_bool(mdata_data(e), *g_equation_name);
return *get_bool(mdata_data(unwrap_pos(e)), *g_equation_name);
}
bool is_lambda_equation(expr const & e) {
@ -78,9 +79,11 @@ bool is_lambda_equation(expr const & e) {
return is_equation(e);
}
expr const & equation_lhs(expr const & e) { lean_assert(is_equation(e)); return app_fn(mdata_expr(e)); }
expr const & equation_rhs(expr const & e) { lean_assert(is_equation(e)); return app_arg(mdata_expr(e)); }
bool is_no_equation(expr const & e) { return is_mdata(e) && get_bool(mdata_data(e), *g_no_equation_name); }
expr const & equation_lhs(expr const & e) { lean_assert(is_equation(e)); return app_fn(mdata_expr(unwrap_pos(e))); }
expr const & equation_rhs(expr const & e) { lean_assert(is_equation(e)); return app_arg(mdata_expr(unwrap_pos(e))); }
bool is_no_equation(expr const & e) {
expr e2 = unwrap_pos(e);
return is_mdata(e2) && get_bool(mdata_data(e2), *g_no_equation_name); }
bool is_lambda_no_equation(expr const & e) {
if (is_lambda(e))

2
src/library/equations_compiler/util.cpp
View file

@ -146,7 +146,7 @@ expr unpack_eqns::repack() {
buffer<expr> new_eqs;
for (buffer<expr> const & fn_eqs : m_eqs) {
for (expr const & eq : fn_eqs) {
new_eqs.push_back(m_locals.ctx().mk_lambda(m_fns, eq));
new_eqs.push_back(m_locals.ctx().mk_lambda(m_fns, unwrap_pos(eq)));
}
}
return update_equations(m_src, new_eqs);

3
src/library/explicit.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "runtime/sstream.h"
#include "library/annotation.h"
#include "library/explicit.h"
#include "library/pos_info_provider.h"
namespace lean {
static name * g_explicit_name = nullptr;
@ -27,7 +28,7 @@ expr const & get_partial_explicit_arg(expr const & e) { lean_assert(is_partial_e
bool is_explicit_or_partial_explicit(expr const & e) { return is_explicit(e) || is_partial_explicit(e); }
expr get_explicit_or_partial_explicit_arg(expr const & e) { lean_assert(is_explicit_or_partial_explicit(e)); return get_annotation_arg(e); }
expr mk_as_is(expr const & e) { return mk_annotation(*g_as_is_name, e); }
expr mk_as_is(expr const & e) { lean_assert(!contains_pos(e)); return mk_annotation(*g_as_is_name, e); }
bool is_as_is(expr const & e) { return is_annotation(e, *g_as_is_name); }
expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); }

1
src/library/head_map.cpp
View file

@ -11,6 +11,7 @@ namespace lean {
head_index::head_index(expr const & e) {
expr f = get_app_fn(e);
while (true) {
f = unwrap_pos(f);
if (is_as_atomic(f))
f = get_app_fn(get_as_atomic_arg(f));
else if (is_explicit(f))

9
src/library/locals.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "kernel/find_fn.h"
#include "library/placeholder.h"
#include "library/locals.h"
#include "library/pos_info_provider.h"
namespace lean {
void collect_univ_params_core(level const & l, name_set & r) {
@ -53,9 +54,9 @@ level_param_names to_level_param_names(name_set const & ls) {
}
void collected_locals::insert(expr const & l) {
if (m_local_names.contains(local_name(l)))
if (m_local_names.contains(local_name_p(l)))
return;
m_local_names.insert(local_name(l));
m_local_names.insert(local_name_p(l));
m_locals.push_back(l);
}
@ -181,12 +182,12 @@ bool depends_on_any(expr const & e, unsigned hs_sz, expr const * hs) {
}
expr replace_locals(expr const & e, unsigned sz, expr const * locals, expr const * terms) {
return instantiate_rev(abstract(e, sz, locals), sz, terms);
return instantiate_rev(abstract_p(e, sz, locals), sz, terms);
}
expr replace_locals(expr const & e, buffer<expr> const & locals, buffer<expr> const & terms) {
lean_assert(locals.size() == terms.size());
lean_assert(std::all_of(locals.begin(), locals.end(), is_local));
lean_assert(std::all_of(locals.begin(), locals.end(), is_local_p));
return replace_locals(e, locals.size(), locals.data(), terms.data());
}
}

15
src/library/placeholder.cpp
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#include "runtime/thread.h"
#include "kernel/find_fn.h"
#include "library/placeholder.h"
#include "library/pos_info_provider.h"
namespace lean {
static name * g_placeholder_one_name = nullptr;
@ -69,17 +70,21 @@ bool is_placeholder(level const & e) { return is_param(e) && is_placeholder(para
bool is_one_placeholder(level const & e) { return is_param(e) && param_id(e) == *g_placeholder_one_name; }
bool is_placeholder(expr const & e) {
return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(local_name(e)));
expr e2 = unwrap_pos(e);
return (is_constant(e2) && is_placeholder(const_name(e2))) || (is_local(e2) && is_placeholder(local_name(e2)));
}
bool is_strict_placeholder(expr const & e) {
return (is_constant(e) && is_strict_placeholder(const_name(e))) || (is_local(e) && is_strict_placeholder(local_name(e)));
expr e2 = unwrap_pos(e);
return (is_constant(e2) && is_strict_placeholder(const_name(e2))) || (is_local(e2) && is_strict_placeholder(local_name(e2)));
}
bool is_explicit_placeholder(expr const & e) {
return (is_constant(e) && is_explicit_placeholder(const_name(e))) || (is_local(e) && is_explicit_placeholder(local_name(e)));
expr e2 = unwrap_pos(e);
return (is_constant(e2) && is_explicit_placeholder(const_name(e2))) || (is_local(e2) && is_explicit_placeholder(local_name(e2)));
}
optional<expr> placeholder_type(expr const & e) {
if (is_local(e) && is_placeholder(e))
return some_expr(local_type(e));
expr e2 = unwrap_pos(e);
if (is_local(e2) && is_placeholder(e2))
return some_expr(local_type(e2));
else
return none_expr();
}

303
src/library/pos_info_provider.cpp
View file

@ -5,46 +5,51 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <vector>
#include "runtime/interrupt.h"
#include "kernel/cache_stack.h"
#include "library/pos_info_provider.h"
#include "kernel/replace_fn.h"
#include "kernel/find_fn.h"
namespace lean {
typedef std::unordered_map<void *, pos_info> pos_table;
const name * g_column_name = nullptr;
const name * g_row_name = nullptr;
static pos_table * g_pos_table;
static mutex * g_pos_table_mutex;
expr save_pos(expr const & e, pos_info const & pos) {
lock_guard<mutex> _(*g_pos_table_mutex);
g_pos_table->insert(mk_pair(e.raw(), pos));
expr unwrap_pos(expr const & e) {
if (get_pos(e)) {
auto const & e2 = mdata_expr(e);
return unwrap_pos(e2);
}
return e;
}
expr copy_pos(expr const & src, expr const & dest) {
lock_guard<mutex> _(*g_pos_table_mutex);
auto it = g_pos_table->find(src.raw());
if (it != g_pos_table->end())
g_pos_table->insert(mk_pair(dest.raw(), it->second));
return dest;
expr save_pos(expr const & e, pos_info const & pos) {
if (is_app(e))
return e;
kvmap m;
m = set_nat(m, *g_column_name, pos.first);
m = set_nat(m, *g_row_name, pos.second);
return mk_mdata(m, unwrap_pos(e));
}
void erase_pos(expr const & e) {
lock_guard<mutex> _(*g_pos_table_mutex);
g_pos_table->erase(e.raw());
expr copy_pos(expr const & src, expr const & dest) {
if (auto pos = get_pos(src))
return save_pos(dest, *pos);
else
return dest;
}
optional<pos_info> get_pos(expr const & e) {
lock_guard<mutex> _(*g_pos_table_mutex);
auto it = g_pos_table->find(e.raw());
if (it != g_pos_table->end())
return optional<pos_info>(it->second);
if (is_mdata(e)) {
kvmap const & m = mdata_data(e);
auto const & column = get_nat(m, *g_column_name);
auto const & row = get_nat(m, *g_row_name);
if (column && row)
return some(mk_pair(column->get_small_value(), row->get_small_value()));
}
return optional<pos_info>();
}
void reset_positions() {
lock_guard<mutex> _(*g_pos_table_mutex);
g_pos_table->clear();
bool contains_pos(expr const & e) {
return !!find(e, [](expr const & e, unsigned) { return get_pos(e); });
}
char const * pos_info_provider::get_file_name() const {
@ -61,232 +66,68 @@ format pos_info_provider::pp(expr const & e) const {
}
void initialize_pos_info_provider() {
g_pos_table = new pos_table();
g_pos_table_mutex = new mutex;
g_column_name = new name("column");
g_row_name = new name("row");
}
void finalize_pos_info_provider() {
delete g_pos_table;
delete g_pos_table_mutex;
delete g_row_name;
delete g_column_name;
}
/* QUICK AND DIRT POSITION PROPAGATION FUNCTIONS */
struct replace_cache2 {
struct entry {
object * m_cell;
unsigned m_offset;
expr m_result;
entry():m_cell(nullptr) {}
};
unsigned m_capacity;
std::vector<entry> m_cache;
std::vector<unsigned> m_used;
replace_cache2(unsigned c):m_capacity(c), m_cache(c) {}
expr * find(expr const & e, unsigned offset) {
unsigned i = hash(hash(e), offset) % m_capacity;
if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset)
return &m_cache[i].m_result;
else
return nullptr;
}
void insert(expr const & e, unsigned offset, expr const & v) {
unsigned i = hash(hash(e), offset) % m_capacity;
if (m_cache[i].m_cell == nullptr)
m_used.push_back(i);
m_cache[i].m_cell = e.raw();
m_cache[i].m_offset = offset;
m_cache[i].m_result = v;
}
void clear() {
for (unsigned i : m_used) {
m_cache[i].m_cell = nullptr;
m_cache[i].m_result = expr();
}
m_used.clear();
}
};
MK_CACHE_STACK(replace_cache2, 1024*8)
class replace_rec_fn2 {
replace_cache2_ref m_cache;
std::function<optional<expr>(expr const &, unsigned)> m_f;
bool m_use_cache;
expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
if (shared)
m_cache->insert(e, offset, r);
return r;
}
expr apply(expr const & e, unsigned offset) {
bool shared = false;
if (m_use_cache && is_shared(e)) {
if (auto r = m_cache->find(e, offset))
return *r;
shared = true;
}
check_system("replace");
if (optional<expr> r = m_f(e, offset)) {
return save_result(e, offset, *r, shared);
} else {
switch (e.kind()) {
case expr_kind::Const: case expr_kind::Sort: case expr_kind::BVar:
case expr_kind::Lit:
return save_result(e, offset, e, shared);
case expr_kind::MVar: {
expr new_t = apply(mvar_type(e), offset);
return save_result(e, offset, copy_pos(e, update_mvar(e, new_t)), shared);
}
case expr_kind::FVar: {
expr new_t = apply(local_type(e), offset);
return save_result(e, offset, copy_pos(e, update_local(e, new_t)), shared);
}
case expr_kind::MData: {
expr new_e = apply(mdata_expr(e), offset);
return save_result(e, offset, copy_pos(e, update_mdata(e, new_e)), shared);
}
case expr_kind::Proj: {
expr new_e = apply(proj_expr(e), offset);
return save_result(e, offset, copy_pos(e, update_proj(e, new_e)), shared);
}
case expr_kind::App: {
expr new_f = apply(app_fn(e), offset);
expr new_a = apply(app_arg(e), offset);
return save_result(e, offset, copy_pos(e, update_app(e, new_f, new_a)), shared);
}
case expr_kind::Pi: case expr_kind::Lambda: {
expr new_d = apply(binding_domain(e), offset);
expr new_b = apply(binding_body(e), offset+1);
return save_result(e, offset, copy_pos(e, update_binding(e, new_d, new_b)), shared);
}
case expr_kind::Let: {
expr new_t = apply(let_type(e), offset);
expr new_v = apply(let_value(e), offset);
expr new_b = apply(let_body(e), offset+1);
return save_result(e, offset, copy_pos(e, update_let(e, new_t, new_v, new_b)), shared);
}
case expr_kind::Quote:
return save_result(e, offset, e, shared);
}
lean_unreachable();
}
}
public:
template<typename F>
replace_rec_fn2(F const & f, bool use_cache):m_f(f), m_use_cache(use_cache) {}
expr operator()(expr const & e) { return apply(e, 0); }
};
expr replace_propagating_pos(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache) {
return replace_rec_fn2(f, use_cache)(e);
}
template<bool rev>
struct instantiate_easy_fn2 {
unsigned n;
expr const * subst;
instantiate_easy_fn2(unsigned _n, expr const * _subst):n(_n), subst(_subst) {}
optional<expr> operator()(expr const & a, bool app) const {
if (!has_loose_bvars(a))
return some_expr(a);
if (is_bvar(a) && bvar_idx(a) < n)
return some_expr(subst[rev ? n - bvar_idx(a).get_small_value() - 1 : bvar_idx(a).get_small_value()]);
if (app && is_app(a))
if (auto new_a = operator()(app_arg(a), false))
if (auto new_f = operator()(app_fn(a), true))
return some_expr(mk_app(*new_f, *new_a));
optional<expr> is_local_p(expr const & e) {
auto e2 = unwrap_pos(e);
if (is_fvar(e2))
return some_expr(e2);
else
return none_expr();
}
};
expr instantiate_propagating_pos(expr const & a, unsigned s, unsigned n, expr const * subst) {
if (
#ifndef LEAN_NO_FREE_VAR_RANGE_OPT
s >= get_loose_bvar_range(a) ||
#endif
n == 0)
return a;
if (s == 0)
if (auto r = instantiate_easy_fn2<false>(n, subst)(a, true))
return *r;
return replace_propagating_pos(a, [=](expr const & m, unsigned offset) -> optional<expr> {
unsigned s1 = s + offset;
if (s1 < s)
return some_expr(m); // overflow, vidx can't be >= max unsigned
#ifndef LEAN_NO_FREE_VAR_RANGE_OPT
if (s1 >= get_loose_bvar_range(m))
return some_expr(m); // expression m does not contain free variables with idx >= s1
#endif
if (is_var(m)) {
nat const & vidx = bvar_idx(m);
if (vidx >= s1) {
unsigned h = s1 + n;
if (h < s1 /* overflow, h is bigger than any vidx */ || vidx < h) {
return some_expr(lift_loose_bvars(subst[vidx.get_small_value() - s1], offset));
} else {
return some_expr(mk_bvar(vidx - nat(n)));
}
}
}
return none_expr();
});
}
name const & local_name_p(expr const & e) { auto o = is_local_p(e); lean_assert(o); return local_name(*o); }
name const & local_pp_name_p(expr const & e) { auto o = is_local_p(e); lean_assert(o); return local_pp_name(*o); }
expr const & local_type_p(expr const & e) { auto o = is_local_p(e); lean_assert(o); return local_type(*o); }
binder_info local_info_p(expr const & e) { auto o = is_local_p(e); lean_assert(o); return local_info(*o); }
expr update_local_p(expr const & e, expr const & new_type) {
return copy_pos(e, update_local(unwrap_pos(e), new_type));
}
expr update_local_p(expr const & e, expr const & new_type, binder_info bi) {
return copy_pos(e, update_local(unwrap_pos(e), new_type, bi));
}
expr update_local_p(expr const & e, binder_info bi) {
return copy_pos(e, update_local(unwrap_pos(e), bi));
}
expr instantiate_propagating_pos(expr const & e, unsigned n, expr const * s) { return instantiate_propagating_pos(e, 0, n, s); }
expr instantiate_propagating_pos(expr const & e, std::initializer_list<expr> const & l) { return instantiate_propagating_pos(e, l.size(), l.begin()); }
expr instantiate_propagating_pos(expr const & e, unsigned i, expr const & s) { return instantiate_propagating_pos(e, i, 1, &s); }
expr instantiate_propagating_pos(expr const & e, expr const & s) { return instantiate_propagating_pos(e, 0, s); }
expr abstract_propagating_pos(expr const & e, unsigned n, expr const * subst) {
lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return !has_loose_bvars(e) && is_local(e); }));
#ifndef LEAN_NO_HAS_LOCAL_OPT
if (!has_local(e))
expr abstract_p(expr const & e, unsigned n, expr const * subst) {
lean_assert(std::all_of(subst, subst+n, [](expr const & e) { return !has_loose_bvars(e) && is_fvar(unwrap_pos(e)); }));
if (!has_fvar(e))
return e;
#endif
return replace_propagating_pos(e, [=](expr const & m, unsigned offset) -> optional<expr> {
#ifndef LEAN_NO_HAS_LOCAL_OPT
if (!has_local(m))
return some_expr(m); // expression m does not contain local constants
#endif
if (is_local(m)) {
unsigned i = n;
while (i > 0) {
--i;
if (local_name(subst[i]) == local_name(m))
return some_expr(mk_bvar(offset + n - i - 1));
}
return none_expr();
return replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
if (!has_fvar(m))
return some_expr(m); // expression m does not contain free variables
if (is_fvar(m)) {
unsigned i = n;
while (i > 0) {
--i;
if (fvar_name(unwrap_pos(subst[i])) == fvar_name(m))
return some_expr(mk_bvar(offset + n - i - 1));
}
return none_expr();
});
}
expr abstract_propagating_pos(expr const & e, name const & l) {
expr dummy = mk_Prop();
expr local = mk_local(l, dummy);
return abstract_propagating_pos(e, 1, &local);
}
return none_expr();
});
}
template<bool is_lambda>
expr mk_binding_p(unsigned num, expr const * locals, expr const & b) {
expr r = abstract_propagating_pos(b, num, locals);
static expr mk_binding_p(unsigned num, expr const * locals, expr const & b) {
expr r = abstract_p(b, num, locals);
unsigned i = num;
while (i > 0) {
--i;
expr const & l = locals[i];
expr t = abstract_propagating_pos(local_type(l), i, locals);
expr t = abstract_p(local_type_p(l), i, locals);
if (is_lambda)
r = mk_lambda(local_pp_name(l), t, r, local_info(l));
r = mk_lambda(local_pp_name_p(l), t, r, local_info_p(l));
else
r = mk_pi(local_pp_name(l), t, r, local_info(l));
r = mk_pi(local_pp_name_p(l), t, r, local_info_p(l));
}
return r;
}

27
src/library/pos_info_provider.h
View file

@ -14,9 +14,9 @@ namespace lean {
/* TEMPORARY HACK for getting position information until we have the new frontend */
expr save_pos(expr const & e, pos_info const & pos);
expr copy_pos(expr const & src, expr const & dest);
void erase_pos(expr const & e);
expr unwrap_pos(expr const & e);
optional<pos_info> get_pos(expr const & e);
void reset_positions();
bool contains_pos(expr const & e);
class pos_info_provider {
public:
@ -44,19 +44,18 @@ public:
void initialize_pos_info_provider();
void finalize_pos_info_provider();
expr replace_propagating_pos(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache = true);
inline expr replace_propagating_pos(expr const & e, std::function<optional<expr>(expr const &)> const & f, bool use_cache = true) {
return replace_propagating_pos(e, [&](expr const & e, unsigned) { return f(e); }, use_cache);
}
expr instantiate_propagating_pos(expr const & a, unsigned s, unsigned n, expr const * subst);
expr instantiate_propagating_pos(expr const & e, unsigned n, expr const * s);
expr instantiate_propagating_pos(expr const & e, std::initializer_list<expr> const & l);
expr instantiate_propagating_pos(expr const & e, unsigned i, expr const & s);
expr instantiate_propagating_pos(expr const & e, expr const & s);
// TEMP: these functions ignore position annotations
expr abstract_propagating_pos(expr const & e, unsigned n, expr const * s);
inline expr abstract_propagating_pos(expr const & e, expr const & s) { return abstract_propagating_pos(e, 1, &s); }
expr abstract_propagating_pos(expr const & e, name const & l);
optional<expr> is_local_p(expr const & e);
name const & local_name_p(expr const & e);
name const & local_pp_name_p(expr const & e);
expr const & local_type_p(expr const & e);
binder_info local_info_p(expr const & e);
expr update_local_p(expr const & e, expr const & new_type);
expr update_local_p(expr const & e, expr const & new_type, binder_info bi);
expr update_local_p(expr const & e, binder_info bi);
expr abstract_p(expr const & e, unsigned n, expr const * subst);
expr Fun_p(unsigned num, expr const * locals, expr const & b);
inline expr Fun_p(expr const & local, expr const & b) { return Fun_p(1, &local, b); }

2
src/library/relation_manager.cpp
View file

@ -18,7 +18,7 @@ namespace lean {
// Check whether e is of the form (f ...) where f is a constant. If it is return f.
static name const & get_fn_const(expr const & e, char const * msg) {
expr const & fn = get_app_fn(e);
if (!is_constant(fn))
if (!is_constant(unwrap_pos(fn)))
throw exception(msg);
return const_name(fn);
}