diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp index 97293e021a..8d8221b50f 100644 --- a/src/frontends/lean/brackets.cpp +++ b/src/frontends/lean/brackets.cpp @@ -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); } diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 7d40e4b2dc..4b7d0abc87 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -128,8 +128,8 @@ static environment redeclare_aliases(environment env, parser & p, pair 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--; } diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 73638be0dc..eeb0f574d9 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -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, expr, expr, optional> 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; diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index a27bde3819..9cb3b75ae1 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -75,13 +75,13 @@ expr parse_single_header(parser & p, declaration_name_scope & scope, buffer 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 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 const & locals, parser const & p, buffer & p buffer 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 & 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 const & from, buffer const & to) { @@ -283,18 +272,19 @@ void collect_implicit_locals(parser & p, buffer & lp_names, buffer & /* 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 & lp_names, buffer & 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 & lp_names, buffer & void elaborate_params(elaborator & elab, buffer const & params, buffer & 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 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); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index fe49a82099..dbe0ef1aea 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -126,8 +126,8 @@ static expr parse_mutual_definition(parser & p, buffer & lp_names, buffer< buffer 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 & 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 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 parse_definition(parser & p, buffer & lp_names, buffer & params, bool is_example, bool is_instance, bool is_meta, bool is_abbrev) { @@ -321,7 +321,7 @@ static std::tuple parse_definition(parser & p, buffer & 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 parse_definition(parser & p, buffer & 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 eqns; if (p.curr_is_token(get_period_tk())) { @@ -354,22 +354,22 @@ static std::tuple parse_definition(parser & p, buffer & } 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 const & params, buffer 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 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 params_buf; for (auto & p : params) params_buf.push_back(p); buffer 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 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 opt_val; bool eqns = false; - name c_name = local_name(fn); + name c_name = local_name_p(fn); pair 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); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0451b5b36d..6b63562596 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -240,7 +240,7 @@ bool elaborator::has_synth_sorry(std::initializer_list && es) { expr elaborator::mk_sorry(optional 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 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 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 { 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 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 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 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 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 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 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 const & fns, buffer const & expected_type, expr const & ref) { buffer 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 const & args, optional const & expected_type) if (is_app_of(e, get_scope_trace_name(), 1)) return visit_scope_trace(e, expected_type); buffer 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 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 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 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 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 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 const & expecte // antiquotations ~> return `expr` buffer locals; buffer 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 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 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 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 const & expected_type) { @@ -3588,7 +3596,7 @@ expr elaborator::strict_visit(expr const & e, optional const & expected_ty expr elaborator::visit_have_expr(expr const & e, optional 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 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 const & expected_type) { flet 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 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 & 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 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()); diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index fc2838df12..908b616e42 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -66,16 +66,16 @@ static level mk_succn(level const & l, unsigned offset) { static void convert_params_to_kernel(elaborator & elab, buffer const & lctx_params, buffer & 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 const & params, buffer const & new_params, buffer const & inds, buffer const & new_inds, buffer const & intro_rules, buffer & 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 > const & intro_rules) { for (buffer 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 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 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(find(arg_ty, [&](expr const & e, unsigned) { return is_mlocal(e) && local_name(e) == local_name(ind); }))) { + if (static_cast(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 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 & new_params, buffer & new_inds, buffer > & 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 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 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 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 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)); } diff --git a/src/frontends/lean/local_context_adapter.cpp b/src/frontends/lean/local_context_adapter.cpp index 2b699bb7d2..eb7c66d4ad 100644 --- a/src/frontends/lean/local_context_adapter.cpp +++ b/src/frontends/lean/local_context_adapter.cpp @@ -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 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 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 entries; to_buffer(lctx, entries); unsigned i = entries.size(); while (i > 0) { --i; - add_local(entries[i]); + add_local(unwrap_pos(entries[i])); } } diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp index 834e12fb61..e827ef234b 100644 --- a/src/frontends/lean/parse_table.cpp +++ b/src/frontends/lean/parse_table.cpp @@ -489,7 +489,7 @@ static expr expand_pp_pattern(unsigned num, transition const * ts, expr const & optional 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)); } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9c06112287..b73356217d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -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::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 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 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> 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 parser::locals_to_context() const { return map_filter(m_local_decls.get_entries(), [](pair 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 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 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 locals; buffer 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 & 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; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 9f84f94064..1add1affda 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -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 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. */ diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 63f3304db1..957e18bfc1 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -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> & 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); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index b69bac0ac0..ba8502176f 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -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 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(); diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 2fc15d9eb1..b15b2f7f44 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -230,16 +230,16 @@ expr Pi(expr const & local, expr const & e, parser & p) { template 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; } diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index 5ed21733c4..333665ac5b 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -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 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; diff --git a/src/library/annotation.h b/src/library/annotation.h index 500d0757a5..b3783fab80 100644 --- a/src/library/annotation.h +++ b/src/library/annotation.h @@ -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 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') ...) diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index f9f7220182..de9cf60535 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -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"); diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index 2b792002d2..5e4cf885fa 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -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)) diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 301f745853..9315727e36 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -146,7 +146,7 @@ expr unpack_eqns::repack() { buffer new_eqs; for (buffer 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); diff --git a/src/library/explicit.cpp b/src/library/explicit.cpp index 00983a25f6..1039635691 100644 --- a/src/library/explicit.cpp +++ b/src/library/explicit.cpp @@ -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); } diff --git a/src/library/head_map.cpp b/src/library/head_map.cpp index 67342146f3..43005cd2b4 100644 --- a/src/library/head_map.cpp +++ b/src/library/head_map.cpp @@ -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)) diff --git a/src/library/locals.cpp b/src/library/locals.cpp index f6f0aa1728..db0644fbd6 100644 --- a/src/library/locals.cpp +++ b/src/library/locals.cpp @@ -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 const & locals, buffer 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()); } } diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 6f12297274..0e435b405a 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -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 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(); } diff --git a/src/library/pos_info_provider.cpp b/src/library/pos_info_provider.cpp index 5ed1c750dd..974a69b54c 100644 --- a/src/library/pos_info_provider.cpp +++ b/src/library/pos_info_provider.cpp @@ -5,46 +5,51 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#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 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 _(*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 _(*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 _(*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 get_pos(expr const & e) { - lock_guard _(*g_pos_table_mutex); - auto it = g_pos_table->find(e.raw()); - if (it != g_pos_table->end()) - return optional(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(); } -void reset_positions() { - lock_guard _(*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 m_cache; - std::vector 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(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 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 - 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(expr const &, unsigned)> const & f, bool use_cache) { - return replace_rec_fn2(f, use_cache)(e); -} - - -template -struct instantiate_easy_fn2 { - unsigned n; - expr const * subst; - instantiate_easy_fn2(unsigned _n, expr const * _subst):n(_n), subst(_subst) {} - optional 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 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(n, subst)(a, true)) - return *r; - return replace_propagating_pos(a, [=](expr const & m, unsigned offset) -> optional { - 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 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 { -#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 { + 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 -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; } diff --git a/src/library/pos_info_provider.h b/src/library/pos_info_provider.h index cdea356eee..9367108dfe 100644 --- a/src/library/pos_info_provider.h +++ b/src/library/pos_info_provider.h @@ -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 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(expr const &, unsigned)> const & f, bool use_cache = true); -inline expr replace_propagating_pos(expr const & e, std::function(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 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 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); } diff --git a/src/library/relation_manager.cpp b/src/library/relation_manager.cpp index f8d679d885..d97375ecd7 100644 --- a/src/library/relation_manager.cpp +++ b/src/library/relation_manager.cpp @@ -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); }