feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided

src/frontends/lean/parser.cpp

@@ -832,12 +832,12 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentr
 }
 
 local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries,
-                                        bool & last_block_delimited) {
+                                        bool & last_block_delimited, bool allow_empty) {
     flet<environment> save(m_env, m_env); // save environment
     local_expr_decls::mk_scope scope(m_local_decls);
     unsigned old_sz = r.size();
     parse_binders_core(r, nentries, last_block_delimited);
-    if (old_sz == r.size())
+    if (!allow_empty && old_sz == r.size())
         throw_invalid_open_binder(pos());
     return local_environment(m_env);
 }

src/frontends/lean/parser.h

@@ -185,7 +185,7 @@ class parser {
     expr parse_binder_core(binder_info const & bi);
     void parse_binder_block(buffer<expr> & r, binder_info const & bi);
     void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited);
-    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited);
+    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, bool allow_empty = false);
     bool parse_local_notation_decl(buffer<notation_entry> * entries);
 
     friend environment section_cmd(parser & p);
@@ -328,6 +328,9 @@ public:
     local_environment parse_binders(buffer<expr> & r) {
         bool tmp; return parse_binders(r, nullptr, tmp);
     }
+    local_environment parse_optional_binders(buffer<expr> & r) {
+        bool tmp; return parse_binders(r, nullptr, tmp, true);
+    }
     local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> & nentries) {
         bool tmp; return parse_binders(r, &nentries, tmp);
     }

src/frontends/lean/structure_cmd.cpp

@@ -416,7 +416,7 @@ struct structure_cmd_fn {
     void parse_new_fields(buffer<expr> & new_fields) {
         parser::local_scope scope(m_p);
         add_locals();
-        m_p.parse_binders(new_fields);
+        m_p.parse_optional_binders(new_fields);
         check_new_field_names(new_fields);
     }
 
@@ -704,7 +704,8 @@ struct structure_cmd_fn {
                 m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected");
                 m_mk = m_name + m_mk;
                 m_mk_infer = parse_implicit_infer_modifier(m_p);
-                m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");
+                if (!m_p.curr_is_command_like())
+                    m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");
             }
             process_new_fields();
         } else {

tests/lean/run/record5.lean

@@ -0,0 +1,18 @@
+import logic data.unit
+
+structure point (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+structure point2 (A : Type) (B : Type) extends point A B :=
+make
+
+check point2.make
+
+structure point3 extends point num num, point2 num num renaming x→y y→z
+
+check point3.mk
+
+set_option pp.coercions true
+
+theorem tst : point3.mk 1 2 3 = point2.make 2 3 :=
+rfl