From f2b2beefe2e9ab200d23e1c99dc20879eb32e9fa Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 25 Aug 2022 16:23:53 +0000 Subject: [PATCH] feat(frontends/lean/elaborator): backport Lean 4 field notation (#757) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This backports a number of features from the Lean 4 field notation ("dot notation") and fixes a couple of bugs. * Field notation not in a function application position (i.e., `x.f` instead of `x.f a b c`) now uses the general resolution procedure rather than a stripped-down one that is unaware of extended field notation. It also now correctly records its source position and correctly allows local recursive calls to have the recursive argument be after the first. * If `f` is a function, then `f.foo` resolves to `function.foo f` (or more precisely `f` is inserted at the first function argument of `function.foo`). * If `s` is a structure, then `s.foo` is resolved in the following way: * If `foo` is a field of `s`, then it resolves into a projection. (Unchanged.) * If the structure's namespace or one of its ancestor's namespaces contains `foo`, then resolves to that. (Change: now considers ancestors too.) * If the structure's namespace contains `foo` as an alias, then resolves to that. (New, though note it is not fully functional since Lean 3 alias resolution is not as capable as Lean 4's.) * We leave the "insufficient number of arguments" error (deferring Lean 4's lambda synthesis to a potential future PR), but we improve error recovery, making it more likely that users can go-to definition on the field. One breaking change (and a consequence of the first item) is illustrated by the following example: ```lean structure bar := (f : ∀ {m : ℕ}, m = 0) variables (s : bar) #check (s.f : 37 = 0) -- formerly #check (s.f : ∀ {m : ℕ}, m = 0) ``` To get the old behavior, one can generally add lambdas, for example `(λ _, s.f : ∀ {m : ℕ}, m = 0)`. To preserve reverse compatibility, we (temporarily?) add a feature that if the elaborator fails to find an explicit argument corresponding to the structure, it will insert the structure as the first explicit argument. This matches the previous behavior for non-application dot notation (`x.f`). The reason for including this feature is that mathlib has been misusing this type of dot notation for terms with `has_coe_to_fun` instances. It is not currently compatible with Lean 4. (Note that, when paired with the new aliases feature, this feature allows for extension methods.) --- src/frontends/lean/elaborator.cpp | 200 +++++++++++------- src/frontends/lean/elaborator.h | 106 ++++++++-- src/frontends/lean/structure_cmd.cpp | 25 +++ src/frontends/lean/structure_cmd.h | 9 + src/library/attribute_manager.h | 2 +- src/library/constants.cpp | 4 + src/library/constants.h | 1 + src/library/constants.txt | 1 + tests/lean/assertion1.lean.expected.out | 20 +- tests/lean/field_resolution.lean | 136 ++++++++++++ tests/lean/field_resolution.lean.expected.out | 40 ++++ .../interactive/field_info.lean.expected.out | 2 +- 12 files changed, 453 insertions(+), 93 deletions(-) create mode 100644 tests/lean/field_resolution.lean create mode 100644 tests/lean/field_resolution.lean.expected.out diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 6736f9c273..bf6873445f 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1876,41 +1876,85 @@ expr elaborator::visit_app_core(expr fn, buffer const & args, optionalmk_ref()); - proj_type = field_res.m_ldecl->get_type(); - } else { - proj = copy_tag(fn, mk_constant(field_res.get_full_fname())); - proj_type = m_env.get(field_res.get_full_fname()).get_type(); + switch (field_res.m_kind) { + case field_resolution::kind::ProjFn: { + // Projections are handled specially since `s` is inserted at a specific argument, whether + // or not it is explicit. + expr coerced_s = *mk_base_projections(m_env, field_res.get_struct_name(), field_res.get_base_struct_name(), mk_as_is(s)); + expr proj_app = mk_proj_app(m_env, field_res.get_base_struct_name(), field_res.get_field_name(), coerced_s, fn); + expr new_proj = visit_function(proj_app, has_args, has_args ? none_expr() : expected_type, ref); + return visit_base_app(new_proj, arg_mask::Default, args, expected_type, ref); + } + case field_resolution::kind::LocalRec: { + s = mk_as_is(s); + proj = copy_tag(fn, field_res.m_ldecl.mk_ref()); + proj_type = field_res.m_ldecl.get_type(); + break; + } + case field_resolution::kind::Const: { + expr coerced_s = *mk_base_projections(m_env, field_res.get_struct_name(), field_res.get_base_struct_name(), mk_as_is(s)); + s = copy_tag(s, std::move(coerced_s)); + proj = copy_tag(fn, mk_constant(field_res.get_const_name())); + proj_type = m_env.get(field_res.get_full_name()).get_type(); + break; + } + default: lean_unreachable(); } + + expr new_proj = visit_function(proj, has_args, has_args ? none_expr() : expected_type, ref); + + name base_name = field_res.get_base_struct_name(); buffer new_args; - unsigned i = 0; + optional insufficient; + unsigned i = 0; while (is_pi(proj_type)) { if (is_explicit(binding_info(proj_type))) { - if (is_app_of(binding_domain(proj_type), field_res.m_base_S_name)) { + if (is_app_of(binding_domain(proj_type), base_name) + || (is_pi(binding_domain(proj_type)) && base_name == get_function_name())) { /* found s location */ - expr coerced_s = *mk_base_projections(m_env, field_res.m_S_name, field_res.m_base_S_name, mk_as_is(s)); - new_args.push_back(copy_tag(fn, std::move(coerced_s))); + + if (insufficient) { + // We defer reporting this to here to prefer the "does not have explicit argument with type" error + report_or_throw(*insufficient); + } + + new_args.push_back(s); for (; i < args.size(); i++) new_args.push_back(args[i]); - expr new_proj = visit_function(proj, has_args, has_args ? none_expr() : expected_type, ref); - return visit_base_app(new_proj, amask, new_args, expected_type, ref); - } else { - if (i >= args.size()) { - throw elaborator_exception(ref, sstream() << "invalid field notation, insufficient number of arguments for '" - << field_res.get_full_fname() << "'"); - } + + return visit_base_app(new_proj, arg_mask::Default, new_args, expected_type, ref); + } else if (i < args.size()) { new_args.push_back(args[i]); i++; + } else { + if (!insufficient) { + insufficient = elaborator_exception(ref, sstream() << "invalid field notation, insufficient number of arguments for '" + << field_res.get_full_name() << "'"); + } + new_args.push_back(mk_sorry(none_expr(), fn)); } } proj_type = binding_body(proj_type); } - throw elaborator_exception(ref, sstream() << "invalid field notation, function '" - << field_res.get_full_fname() << "' does not have explicit argument with type (" - << field_res.m_base_S_name << " ...)"); + + // If there is no explicit argument of the right type, we try inserting it as the first explicit argument. + // This gives some ability to use dot notation with terms that have a `has_coe_to_fun` instance. + + new_args.clear(); + new_args.push_back(s); + new_args.append(args); + + try { + return visit_base_app(new_proj, arg_mask::Default, new_args, expected_type, ref); + } catch (elaborator_exception & ex) { + throw nested_elaborator_exception(ref, ex, format("invalid field notation, function '") + + format(field_res.get_full_name()) + + format("' does not have explicit argument with type (") + + format(field_res.get_base_struct_name()) + format(" ...)")); + } } else { expr new_fn = visit_function(fn, has_args, has_args ? none_expr() : expected_type, ref); /* Check if we should use a custom elaboration procedure for this application. */ @@ -2685,42 +2729,47 @@ expr elaborator::visit_inaccessible(expr const & e, optional const & expec return copy_tag(e, mk_inaccessible(new_a)); } -elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_type) { - // prefer 'unknown identifier' error when lhs is a constant of non-value type - if (is_field_notation(e)) { - auto lhs = macro_arg(e, 0); - if (is_constant(lhs)) { - type_context_old::tmp_locals locals(m_ctx); - expr t = whnf(s_type); - while (is_pi(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); - throw elaborator_exception(lhs, format("unknown identifier '") + format(const_name(lhs)) + format(".") + - format(fname) + format("'")); - } +elaborator::field_resolution elaborator::resolve_field_notation_aux(expr const & e, expr const & s, expr const & s_type) { + lean_assert(is_field_notation(e)); + + // If it's a function, resolve the field as a declaration in the `function` namespace. + if (is_pi(s_type) && !is_anonymous_field_notation(e)) { + auto fname = get_field_notation_field_name(e); + auto full_fname = get_function_name() + fname; + if (m_env.find(full_fname)) { + return field_resolution_const(get_function_name(), get_function_name(), full_fname); } } - expr I = get_app_fn(s_type); + + expr I = get_app_fn(s_type); + if (!is_constant(I)) { auto pp_fn = mk_pp_ctx(); + // prefer 'unknown identifier' error when lhs (the unelaborated s) is a constant of non-value type + auto lhs = macro_arg(e, 0); + if (!is_anonymous_field_notation(e) && is_constant(lhs)) { + name fname = get_field_notation_field_name(e); + throw elaborator_exception(lhs, format("unknown identifier '") + format(const_name(lhs) + fname) + format("'")); + } throw elaborator_exception(e, format("invalid field notation, type is not of the form (C ...) where C is a constant") + pp_indent(pp_fn, s) + line() + format("has type") + pp_indent(pp_fn, s_type)); } + + auto struct_name = const_name(I); + if (is_anonymous_field_notation(e)) { - if (!is_structure(m_env, const_name(I))) { + if (!is_structure(m_env, struct_name)) { auto pp_fn = mk_pp_ctx(); throw elaborator_exception(e, format("invalid projection, structure expected") + pp_indent(pp_fn, s) + line() + format("has type") + pp_indent(pp_fn, s_type)); } - auto fnames = get_structure_fields(m_env, const_name(I)); + auto fnames = get_structure_fields(m_env, struct_name); unsigned fidx = get_field_notation_field_idx(e); - if (fidx == 0) { + if (fidx == 0) { throw elaborator_exception(e, "invalid projection, index must be greater than 0"); } if (fidx > fnames.size()) { @@ -2731,37 +2780,46 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons line() + format("which has type") + pp_indent(pp_fn, s_type)); } - return const_name(I) + fnames[fidx-1]; + return field_resolution_proj_fn(struct_name, struct_name, fnames[fidx-1]); } else { - name fname = get_field_notation_field_name(e); - // search for "true" fields first, including in parent structures - if (is_structure_like(m_env, const_name(I))) - if (auto p = find_field(m_env, const_name(I), fname)) - return field_resolution(const_name(I), *p, fname); - name full_fname = const_name(I) + fname; - name local_name = full_fname.replace_prefix(get_namespace(env()), {}); - if (auto ldecl = m_ctx.lctx().find_if([&](local_decl const & decl) { - return decl.get_info().is_rec() && decl.get_pp_name() == local_name; - })) { - // projection is recursive call - return field_resolution(full_fname, ldecl); + name fname = get_field_notation_field_name(e); + + // Search for "true" fields first, including in parent structures + if (is_structure_like(m_env, struct_name)) + if (auto p = find_field(m_env, struct_name, fname)) + return field_resolution_proj_fn(*p, struct_name, fname); + + // Check if field notation is being used to make a "local" recursive call. + name full_fname = struct_name + fname; + name local_name = full_fname.replace_prefix(get_namespace(m_env), {}); + if (auto ldecl = m_ctx.lctx().find_if([&](local_decl const & decl) { return decl.get_info().is_rec() && decl.get_pp_name() == local_name; })) { + return field_resolution_local_rec(struct_name, full_fname, *ldecl); } - if (!m_env.find(full_fname)) { - auto pp_fn = mk_pp_ctx(); - throw elaborator_exception(e, format("invalid field notation, '") + format(fname) + format("'") + - format(" is not a valid \"field\" because environment does not contain ") + - format("'") + format(full_fname) + format("'") + - pp_indent(pp_fn, s) + - line() + format("which has type") + - pp_indent(pp_fn, s_type)); + + // Otherwise we search the environment for this "extended" dot notation + + if (auto m = find_method(m_env, struct_name, fname)) { + return field_resolution_const(m->first, struct_name, m->second); + } + + if (auto m = find_method_alias(m_env, struct_name, fname)) { + return field_resolution_const(m->first, m->first, m->second); } - return full_fname; + + auto pp_fn = mk_pp_ctx(); + throw elaborator_exception(e, format("invalid field notation, '") + format(fname) + format("'") + + format(" is not a valid \"field\" because environment does not contain ") + + format("'") + format(struct_name + fname) + format("'") + + pp_indent(pp_fn, s) + + line() + format("which has type") + + pp_indent(pp_fn, s_type)); } } -elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr const & s, expr const & s_type) { +elaborator::field_resolution elaborator::resolve_field_notation(expr const & e, expr const & s, expr const & s_type) { + lean_assert(is_field_notation(e)); try { - return field_to_decl(e, s, s_type); + return resolve_field_notation_aux(e, s, s_type); } catch (elaborator_exception & ex1) { expr new_s_type = s_type; if (auto d = unfold_term(env(), new_s_type)) @@ -2770,7 +2828,7 @@ elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr cons if (new_s_type == s_type) throw; try { - return find_field_fn(e, s, new_s_type); + return resolve_field_notation(e, s, new_s_type); } catch (elaborator_exception & ex2) { throw nested_elaborator_exception(ex2.get_pos(), ex1, ex2.pp()); } @@ -2779,17 +2837,7 @@ elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr cons expr elaborator::visit_field(expr const & e, optional const & expected_type) { lean_assert(is_field_notation(e)); - expr s = visit(macro_arg(e, 0), none_expr()); - expr s_type = head_beta_reduce(instantiate_mvars(infer_type(s))); - auto field_res = find_field_fn(e, s, s_type); - expr proj_app; - if (field_res.m_ldecl) { - proj_app = copy_tag(e, mk_app(field_res.m_ldecl->mk_ref(), mk_as_is(s))); - } else { - expr new_e = *mk_base_projections(m_env, field_res.m_S_name, field_res.m_base_S_name, mk_as_is(s)); - proj_app = mk_proj_app(m_env, field_res.m_base_S_name, field_res.m_fname, new_e, e); - } - return visit(proj_app, expected_type); + return visit_app_core(e, buffer(), expected_type, e); } class reduce_projections_visitor : public replace_visitor { diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 9d40de292c..9e685eab8e 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -246,23 +246,101 @@ class elaborator { expr visit_equation(expr const & eq, unsigned num_fns); expr visit_inaccessible(expr const & e, optional const & expected_type); + /** Field resolution: this is a field projection */ + struct field_resolution_proj_fn { + /** Name of the structure that is the source of the field. Is ancestor of \c m_struct_name + * If this is not equal to \c m_struct_name then we should insert parent projections. */ + name m_base_struct_name; + /** Name of the structure for the expression being projected. */ + name m_struct_name; + /** The field name for the projection */ + name m_field_name; + + field_resolution_proj_fn(name const & base_struct_name, name const & struct_name, name const & field_name): + m_base_struct_name(base_struct_name), m_struct_name(struct_name), m_field_name(field_name) {} + }; + + /** Field resolution: this is a "method" (a.k.a. extended dot notation) */ + struct field_resolution_const { + /** Name of the structure that is the source of the method. Is ancestor of \c m_struct_name + * If this is not equal to \c m_struct_name then we should insert parent projections. */ + name m_base_struct_name; + /** Name of the generalized structure for the expression whose method is being called. */ + name m_struct_name; + /** Name of the constant to use as a function */ + name m_const_name; + + field_resolution_const(name const & base_struct_name, name const & struct_name, name const & const_name): + m_base_struct_name(base_struct_name), m_struct_name(struct_name), m_const_name(const_name) {} + }; + + /** Field resolution: projection is being used to make a "local" recursive call */ + struct field_resolution_local_rec { + /** The generalized structure name for the argument to the call. */ + name m_base_struct_name; + /** The resolved name for the recursive call (for error reporting). */ + name m_full_name; + /** The declaration for the "local" recursive call. */ + local_decl m_ldecl; + + field_resolution_local_rec(name const & base_struct_name, name const & full_name, local_decl const & ldecl): + m_base_struct_name(base_struct_name), m_full_name(full_name), m_ldecl(ldecl) {} + }; + struct field_resolution { - name m_S_name; // structure name of field expression type - name m_base_S_name; // structure name of field - name m_fname; - optional m_ldecl; // projection is a local constant: recursive call - - field_resolution(name const & full_fname, optional ldecl = {}): - m_S_name(full_fname.get_prefix()), m_base_S_name(full_fname.get_prefix()), - m_fname(full_fname.get_string()), m_ldecl(ldecl) {} - field_resolution(const name & S_name, const name & base_S_name, const name & fname): - m_S_name(S_name), m_base_S_name(base_S_name), m_fname(fname) {} - - name get_full_fname() const { return m_base_S_name + m_fname; } + /** `ProjFn`: a field projection. + * `Const`: a "method" (a.k.a. extended dot notation). + * `LocalRec`: a "local" recursive call using field notation. */ + enum class kind { ProjFn, Const, LocalRec }; + + kind m_kind; + /** (All kinds) */ + name m_base_struct_name; + /** (ProjFn and Const) */ + name m_struct_name; + /** (ProjFn) `m_field_name`. + * (Const) `m_const_name`. + * (LocalRec) `m_full_name` (for error reporting). */ + name m_extra; + /** (LocalRec) */ + local_decl m_ldecl; + + field_resolution(field_resolution_proj_fn const & fr_proj_fn): + m_kind(kind::ProjFn), + m_base_struct_name(fr_proj_fn.m_base_struct_name), + m_struct_name(fr_proj_fn.m_struct_name), + m_extra(fr_proj_fn.m_field_name) {} + field_resolution(field_resolution_const const & fr_const): + m_kind(kind::Const), + m_base_struct_name(fr_const.m_base_struct_name), + m_struct_name(fr_const.m_struct_name), + m_extra(fr_const.m_const_name) {} + field_resolution(field_resolution_local_rec const & fr_local_rec): + m_kind(kind::LocalRec), + m_base_struct_name(fr_local_rec.m_base_struct_name), + m_extra(fr_local_rec.m_full_name), + m_ldecl(fr_local_rec.m_ldecl) {} + + name get_base_struct_name() const { return m_base_struct_name; } + name get_struct_name() const { lean_assert(m_kind == kind::ProjFn || m_kind == kind::Const); return m_struct_name; } + name get_field_name() const { lean_assert(m_kind == kind::ProjFn); return m_extra; } + name get_const_name() const { lean_assert(m_kind == kind::Const); return m_extra; } + + /** The function name to use when reporting errors associated to this field resolution. */ + name get_full_name() { + switch (m_kind) { + case kind::ProjFn: return get_base_struct_name() + get_field_name(); + case kind::Const: return get_const_name(); + case kind::LocalRec: return m_extra; + default: lean_unreachable(); + } + } }; - field_resolution field_to_decl(expr const & e, expr const & s, expr const & s_type); - field_resolution find_field_fn(expr const & e, expr const & s, expr const & s_type); + field_resolution resolve_field_notation_aux(expr const & e, expr const & s, expr const & s_type); + /** \c e is the field notation expression, \c s is the elaborated expression, \c s_type is its type */ + field_resolution resolve_field_notation(expr const & e, expr const & s, expr const & s_type); + expr visit_field(expr const & e, optional const & expected_type); expr instantiate_mvars(expr const & e, std::function pred); // NOLINT expr visit_structure_instance(expr const & e, optional expected_type); diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index f421a26f88..3f313848db 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -177,6 +177,31 @@ optional find_field(environment const & env, name const & S_name, name con return {}; } +optional> find_method(environment const & env, name const & struct_name, name const & field_name) { + if (env.find(struct_name + field_name)) + return some(mk_pair(struct_name, struct_name + field_name)); + if (is_structure_like(env, struct_name)) { + for (auto const & p : get_parent_structures(env, struct_name)) { + if (auto m = find_method(env, p, field_name)) + return m; + } + } + return {}; +} + +optional> find_method_alias(environment const & env, name const & struct_name, name const & field_name) { + optional> res = {}; + for (auto const & alias : get_expr_aliases(env, struct_name + field_name)) { + if (alias.drop_prefix() == field_name) { + if (res) { + return {}; + } + res = some(mk_pair(alias.get_prefix(), alias)); + } + } + return res; +} + void get_structure_fields_flattened(environment const & env, name const & structure_name, buffer & full_fnames) { for (auto const & fname : get_structure_fields(env, structure_name)) { full_fnames.push_back(structure_name + fname); diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h index 946da1a89b..32d73b5913 100644 --- a/src/frontends/lean/structure_cmd.h +++ b/src/frontends/lean/structure_cmd.h @@ -27,6 +27,15 @@ optional find_field(environment const & env, name const & S_name, name con optional mk_base_projections(environment const & env, name const & S_name, name const & base_S_name, expr const & e); /** \brief Return an unelaborated expression applying a field projection */ expr mk_proj_app(environment const & env, name const & S_name, name const & fname, expr const & e, expr const & ref = {}); +/** \brief Searches for `struct_name.field_name` in the environment, and if `struct_name` is a structure, + * recursively does the same for its parent structures if the environment contains no such name. + * Returns `(S', n)` where S' is the name of the (generalized) structure and n is the name corresponding to \c field_name */ +optional> find_method(environment const & env, name const & struct_name, name const & field_name); +/** \brief If `struct_name.field_name` is uniquely an alias for `struct_name'.field_name` then + * returns `(struct_name', struct_name'.field_name)`. + * + * Should consider generating an error or warning if there is more than one such alias. */ +optional> find_method_alias(environment const & env, name const & struct_name, name const & field_name); /* Default value support */ optional has_default_value(environment const & env, name const & S_name, name const & fname); diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h index ec5d59f338..891a0e98e6 100644 --- a/src/library/attribute_manager.h +++ b/src/library/attribute_manager.h @@ -260,7 +260,7 @@ struct key_value_data : public attr_data { /** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */ typedef typed_attribute indices_attribute; -/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */ +/** \brief Attribute that represents a single key/value pair. */ typedef typed_attribute key_value_attribute; class user_attribute_ext { diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 12ef730c4d..b7188a0fb8 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -67,6 +67,7 @@ name const * g_forall_congr = nullptr; name const * g_forall_congr_eq = nullptr; name const * g_forall_not_of_not_exists = nullptr; name const * g_format = nullptr; +name const * g_function = nullptr; name const * g_funext = nullptr; name const * g_has_add = nullptr; name const * g_has_add_add = nullptr; @@ -349,6 +350,7 @@ void initialize_constants() { g_forall_congr_eq = new name{"forall_congr_eq"}; g_forall_not_of_not_exists = new name{"forall_not_of_not_exists"}; g_format = new name{"format"}; + g_function = new name{"function"}; g_funext = new name{"funext"}; g_has_add = new name{"has_add"}; g_has_add_add = new name{"has_add", "add"}; @@ -632,6 +634,7 @@ void finalize_constants() { delete g_forall_congr_eq; delete g_forall_not_of_not_exists; delete g_format; + delete g_function; delete g_funext; delete g_has_add; delete g_has_add_add; @@ -914,6 +917,7 @@ name const & get_forall_congr_name() { return *g_forall_congr; } name const & get_forall_congr_eq_name() { return *g_forall_congr_eq; } name const & get_forall_not_of_not_exists_name() { return *g_forall_not_of_not_exists; } name const & get_format_name() { return *g_format; } +name const & get_function_name() { return *g_function; } name const & get_funext_name() { return *g_funext; } name const & get_has_add_name() { return *g_has_add; } name const & get_has_add_add_name() { return *g_has_add_add; } diff --git a/src/library/constants.h b/src/library/constants.h index b5a0861f0e..da2921cad3 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -69,6 +69,7 @@ name const & get_forall_congr_name(); name const & get_forall_congr_eq_name(); name const & get_forall_not_of_not_exists_name(); name const & get_format_name(); +name const & get_function_name(); name const & get_funext_name(); name const & get_has_add_name(); name const & get_has_add_add_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 9605ba8f3d..ad69ff3ffe 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -62,6 +62,7 @@ forall_congr forall_congr_eq forall_not_of_not_exists format +function funext has_add has_add.add diff --git a/tests/lean/assertion1.lean.expected.out b/tests/lean/assertion1.lean.expected.out index 2f31b707b2..4e6c8e58c2 100644 --- a/tests/lean/assertion1.lean.expected.out +++ b/tests/lean/assertion1.lean.expected.out @@ -1 +1,19 @@ -assertion1.lean:37:21: error: invalid field notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...) +assertion1.lean:37:21: error: type mismatch at application + MonoidalCategory.tensorObjects C +term + C +has type + MonoidalCategory : Type (max (u+1) (v+1)) +but is expected to have type + ?m_1.carrier.Obj : Type ? +Additional information: +assertion1.lean:37:21: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message + type mismatch at application + MonoidalCategory.tensorObjects C + term + C + has type + MonoidalCategory : Type (max (u+1) (v+1)) + but is expected to have type + ?m_1.carrier.Obj : Type ? +assertion1.lean:37:21: context: invalid field notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...) diff --git a/tests/lean/field_resolution.lean b/tests/lean/field_resolution.lean new file mode 100644 index 0000000000..ea5bcd42cc --- /dev/null +++ b/tests/lean/field_resolution.lean @@ -0,0 +1,136 @@ +section structures + +structure foo := +(a : ℕ) + +structure bar extends foo := +(b : ℕ) + +def foo.s : foo := {a := 37} +def bar.s : bar := {a := 17, b := 22} + +-- (error) prefer "unknown identifier" +#check foo.c + +-- true fields +#eval foo.s.a +#eval bar.s.a +#eval bar.s.b + +-- anonymous field notation +#eval foo.s.1 +#eval bar.s.1.1 +#eval bar.s.2 + +def foo.inc_a (s : foo) : ℕ := s.a + 1 +def bar.inc_b (s : bar) : ℕ := s.b + 1 + +-- extended dot notation (method resolution) +#eval foo.s.inc_a +#eval bar.s.inc_a +#eval bar.s.inc_b + +def foo.add_a (n : ℕ) (s : foo) : ℕ := s.a + n + +example : foo.s.add_a 1 = foo.s.inc_a := rfl +example : bar.s.add_a 1 = bar.s.inc_a := rfl + +-- (error) insufficient arguments is error (yet could be lambda like in Lean 4) +#check foo.s.add_a +--example : foo.s.add_a = λ n, foo.s.add_a n := rfl +#check bar.s.add_a +--example : bar.s.add_a = λ n, bar.s.add_a n := rfl + +def foo.add_b_of_eq (n : ℕ) {m : ℕ} (h : n = m) (s : foo) : ℕ := s.a + m + +-- (error) insufficient arguments (trickier example for synthesizing lambda) +#check foo.s.add_b_of_eq + +def foo.blah (n : ℕ) : ℕ := n + +-- (error) invalid field notation, no explicit argument of type (foo ...) +#check foo.s.blah 37 +#check bar.s.blah 37 + +structure implicit_test := (f : ∀ {m : ℕ}, m = 0) + +variables (s : implicit_test) +#check (s.f : 37 = 0) -- before #757 would have been (s.f : ∀ {m : ℕ}, m = 0) +#check (λ _, s.f : ∀ {m : ℕ}, m = 0) + +end structures + +section local_constants + +-- Without arguments +def list.double {α : Type*} : list α → list α +| [] := [] +| (x :: xs) := x :: x :: xs.double + +-- With arguments (and list argument after first, fixed in #757) +def list.map' {α β : Type*} : (α → β) → list α → list β +| _ [] := [] +| f (x :: xs) := f x :: xs.map' f + +def list.map'' {α β : Type*} : list α → (α → β) → list β +| [] _ := [] +| (x :: xs) f := f x :: xs.map' f + +end local_constants + +section classes + +class baz (α : Type*) := +(a : α) +(b : ℕ → α) + +-- projection for class instance +example (α : Type*) (I : baz α) : I.a = I.a := rfl +-- projection for class instance with arguments +example (α : Type*) (I : baz α) : I.b 37 = I.b 37 := rfl +-- plain fully qualified name +example (α : Type*) [baz α] : (baz.b 37 : α) = baz.b 37 := rfl + +end classes + +section functions + +lemma function.mt {p q : Prop} (h : p → q) : ¬ q → ¬ p := mt h + +example {p q : Prop} (hnp : ¬ p) (h : q → p) : ¬ q := h.mt hnp + +def function.apply {α β : Type*} (x : α) (f : α → β) : β := f x + +example : (+ 3).apply 1 = 4 := rfl +-- (error) insufficient number of arguments is error (yet could be a lambda like in Lean 4) +#check λ (x : ℕ), (+ x).apply +--example : (λ (x : ℕ), (+ x).apply) = (λ x y, y + x) := rfl +--example : (λ (x : ℕ), (+ x).apply) = (λ (y : ℕ), (+ y).apply) := rfl + +end functions + +section aliases + +def Set (α : Type) := α → Prop +def Set.union {α : Type} (s₁ s₂ : Set α) : Set α := λ a, s₁ a ∨ s₂ a +def FinSet (n : ℕ) := fin n → Prop + +export Set (renaming union → FinSet.union) + +example (x y : FinSet 10) : FinSet 10 := + x.union y -- Works + +end aliases + +section first_arg + +instance (p q : Prop) : has_coe_to_fun (p ↔ q) (λ _, p → q) := ⟨λ h, h.mp⟩ + +structure my_prop (p : Prop) : Prop := (h : p) + +def my_prop.iff {p : Prop} : my_prop p ↔ p := ⟨my_prop.h, λ h, ⟨h⟩⟩ + +-- Use the first explicit argument +example (p : Prop) (h : my_prop p) : p := h.iff + +end first_arg diff --git a/tests/lean/field_resolution.lean.expected.out b/tests/lean/field_resolution.lean.expected.out new file mode 100644 index 0000000000..534e806ab6 --- /dev/null +++ b/tests/lean/field_resolution.lean.expected.out @@ -0,0 +1,40 @@ +field_resolution.lean:13:7: error: unknown identifier 'foo.c' +37 +17 +22 +37 +17 +22 +38 +18 +23 +field_resolution.lean:39:12: error: invalid field notation, insufficient number of arguments for 'foo.add_a' +foo.add_a ⁇ foo.s : ℕ +field_resolution.lean:41:12: error: invalid field notation, insufficient number of arguments for 'foo.add_a' +foo.add_a ⁇ bar.s.to_foo : ℕ +field_resolution.lean:47:12: error: invalid field notation, insufficient number of arguments for 'foo.add_b_of_eq' +foo.add_b_of_eq ⁇ _ foo.s : ℕ +field_resolution.lean:52:12: error: type mismatch at application + foo.blah foo.s +term + foo.s +has type + foo +but is expected to have type + ℕ +Additional information: +field_resolution.lean:52:12: context: invalid field notation, function 'foo.blah' does not have explicit argument with type (foo ...) +field_resolution.lean:53:12: error: type mismatch at application + foo.blah bar.s.to_foo +term + bar.s.to_foo +has type + foo +but is expected to have type + ℕ +Additional information: +field_resolution.lean:53:12: context: invalid field notation, function 'foo.blah' does not have explicit argument with type (foo ...) +s.f : 37 = 0 +λ (_x : ℕ), s.f : ∀ (_x : ℕ), _x = 0 +field_resolution.lean:106:23: error: invalid field notation, insufficient number of arguments for 'function.apply' +λ (x : ℕ), function.apply ⁇ (λ (_x : ℕ), _x + x) : ℕ → ℕ diff --git a/tests/lean/interactive/field_info.lean.expected.out b/tests/lean/interactive/field_info.lean.expected.out index a41f29c66f..8c724a6796 100644 --- a/tests/lean/interactive/field_info.lean.expected.out +++ b/tests/lean/interactive/field_info.lean.expected.out @@ -1,7 +1,7 @@ {"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n n\nwhich has type\n ℕ"}],"response":"all_messages"} {"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n n\nwhich has type\n ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"}],"response":"all_messages"} {"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n n\nwhich has type\n ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"},{"caption":"","file_name":"field_info.lean","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"} -{"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n n\nwhich has type\n ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"},{"caption":"","file_name":"field_info.lean","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"field_info.lean","pos_col":0,"pos_line":12,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n n\nwhich has type\n ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"},{"caption":"","file_name":"field_info.lean","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":12,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"state":"n : ℕ\n⊢ ⁇"},"response":"ok","seq_num":2} {"record":{"full-id":"list.all","source":,"state":"l : list ℕ\n⊢ (ℕ → bool) → bool","type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4}