diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 6e7e9b235..8ee292690 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -81,34 +81,34 @@ struct structure_cmd_fn { typedef std::vector field_map; typedef type_modifiers modifiers; - parser & m_p; - environment m_env; - name_generator m_ngen; - type_checker_ptr m_tc; - name m_namespace; - name m_name; - pos_info m_name_pos; - buffer m_level_names; - modifiers m_modifiers; - buffer m_params; - expr m_type; - buffer> m_parent_refs; - buffer m_parents; - buffer m_private_parents; - name m_mk; - name m_mk_short; - pos_info m_mk_pos; - implicit_infer_kind m_mk_infer; - buffer m_fields; - std::vector m_renames; - std::vector m_field_maps; - bool m_infer_result_universe; - bool m_using_explicit_levels; - levels m_ctx_levels; // context levels for creating aliases - buffer m_ctx_locals; // context local constants for creating aliases + parser & m_p; + environment m_env; + name_generator m_ngen; + type_checker_ptr m_tc; + name m_namespace; + name m_name; + pos_info m_name_pos; + buffer m_level_names; + modifiers m_modifiers; + buffer m_params; + expr m_type; + buffer> m_parent_refs; + buffer m_parents; + buffer m_private_parents; + name m_mk; + name m_mk_short; + pos_info m_mk_pos; + implicit_infer_kind m_mk_infer; + buffer m_fields; + std::vector m_renames; + std::vector m_field_maps; + bool m_infer_result_universe; + bool m_using_explicit_levels; + levels m_ctx_levels; // context levels for creating aliases + buffer m_ctx_locals; // context local constants for creating aliases - bool m_gen_eta; - bool m_gen_proj_mk; + bool m_gen_eta; + bool m_gen_proj_mk; structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) { m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false); @@ -479,15 +479,41 @@ struct structure_cmd_fn { } } + void parse_field_block(buffer & new_fields, binder_info const & bi) { + buffer> names; + while (m_p.curr_is_identifier()) { + auto p = m_p.pos(); + names.emplace_back(p, m_p.check_atomic_id_next("invalid field, atomic identifier expected")); + } + if (names.empty()) + throw parser_error("invalid field, identifier expected", m_p.pos()); + + m_p.check_token_next(get_colon_tk(), "invalid field, ':' expected"); + expr type = m_p.parse_expr(); + + for (auto p : names) { + expr local = m_p.save_pos(mk_local(p.second, type, bi), p.first); + m_p.add_local(local); + new_fields.push_back(local); + } + } + /** \brief Parse new fields declared in this structure */ void parse_new_fields(buffer & new_fields) { parser::local_scope scope(m_p); add_locals(); - m_p.parse_optional_binders(new_fields); + while (!m_p.curr_is_command_like()) { + if (m_p.curr_is_identifier()) { + parse_field_block(new_fields, binder_info()); + } else { + binder_info bi = m_p.parse_binder_info(); + parse_field_block(new_fields, bi); + m_p.parse_close_binder_info(bi); + } + } check_new_field_names(new_fields); } - /** \brief Elaborate new fields, and copy them to m_fields */ void elaborate_new_fields(buffer & new_fields) { list ctx = m_p.locals_to_context(); @@ -657,7 +683,7 @@ struct structure_cmd_fn { } void declare_projections() { - m_env = mk_projections(m_env, m_name, m_modifiers.is_class()); + m_env = mk_projections(m_env, m_name, m_mk_infer, m_modifiers.is_class()); for (expr const & field : m_fields) { name field_name = m_name + mlocal_name(field); save_proj_info(field_name); diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 4dbf6364e..c39572c1f 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -273,7 +273,8 @@ static bool is_prop(expr type) { return is_sort(type) && is_zero(sort_level(type)); } -environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { +environment mk_projections(environment const & env, name const & n, buffer const & proj_names, + implicit_infer_kind infer_k, bool inst_implicit) { // Given an inductive datatype C A (where A represent parameters) // intro : Pi A (x_1 : B_1[A]) (x_2 : B_2[A, x_1]) ..., C A // @@ -335,8 +336,7 @@ environment mk_projections(environment const & env, name const & n, buffer rec_args.push_back(major_premise); expr rec_app = mk_app(rec, rec_args); expr proj_type = Pi(proj_args, result_type); - bool strict = true; - proj_type = infer_implicit(proj_type, nparams, strict); + proj_type = infer_implicit_params(proj_type, nparams, infer_k); expr proj_val = Fun(proj_args, rec_app); bool opaque = false; bool use_conv_opt = false; @@ -364,7 +364,8 @@ static name mk_fresh_name(environment const & env, buffer const & names, n } } -environment mk_projections(environment const & env, name const & n, bool inst_implicit) { +environment mk_projections(environment const & env, name const & n, + implicit_infer_kind infer_k, bool inst_implicit) { auto p = get_nparam_intro_rule(env, n); unsigned num_params = p.first; inductive::intro_rule ir = p.second; @@ -377,6 +378,6 @@ environment mk_projections(environment const & env, name const & n, bool inst_im i++; type = binding_body(type); } - return mk_projections(env, n, proj_names, inst_implicit); + return mk_projections(env, n, proj_names, infer_k, inst_implicit); } } diff --git a/src/library/definitional/projection.h b/src/library/definitional/projection.h index 1a1c08338..264df6275 100644 --- a/src/library/definitional/projection.h +++ b/src/library/definitional/projection.h @@ -8,9 +8,20 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { +/** \brief Create projections operators for the structure named \c n. + The procedure assumes \c n is a structure. + + The argument \c infer_k specifies the implicit argument inference strategy used for the + structure parameters. + + If \c inst_implicit == true, then the structure argument of the projection is decorated as + "instance implicit" + [s : n] +*/ environment mk_projections(environment const & env, name const & n, buffer const & proj_names, - bool inst_implicit = false); -environment mk_projections(environment const & env, name const & n, bool inst_implicit = false); + implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false); +environment mk_projections(environment const & env, name const & n, + implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false); /** \brief Return true iff the type named \c S can be viewed as a structure in the given environment. diff --git a/tests/lean/run/struct_infer.lean b/tests/lean/run/struct_infer.lean new file mode 100644 index 000000000..111418096 --- /dev/null +++ b/tests/lean/run/struct_infer.lean @@ -0,0 +1,21 @@ +import data.nat.basic +open nat + +definition associative {A : Type} (op : A → A → A) := ∀a b c, op (op a b) c = op a (op b c) + +structure semigroup [class] (A : Type) := +mk {} :: (mul: A → A → A) (mul_assoc : associative mul) + +definition nat_semigroup [instance] : semigroup nat := +semigroup.mk nat.mul nat.mul.assoc + +example (a b c : nat) : (a * b) * c = a * (b * c) := +semigroup.mul_assoc a b c + +structure semigroup2 (A : Type) := +mk () :: (mul: A → A → A) (mul_assoc : associative mul) + +definition s := semigroup2.mk nat nat.mul nat.mul.assoc + +example (a b c : nat) : (a * b) * c = a * (b * c) := +semigroup2.mul_assoc nat s a b c