From 7897e21a142f4915634950056f1d5b7f2f8bee81 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 22:55:51 -0800
Subject: [PATCH] feat(frontends/lean/structure_cmd): allow fields to be
 suppresed, but constructor to be provided

---
 src/frontends/lean/parser.cpp        |  4 ++--
 src/frontends/lean/parser.h          |  5 ++++-
 src/frontends/lean/structure_cmd.cpp |  5 +++--
 tests/lean/run/record5.lean          | 18 ++++++++++++++++++
 4 files changed, 27 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/record5.lean

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 139ddb264..21de1da90 100644
--- a/src/frontends/lean/parser.cpp
+++ b/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);
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index d1cb9568d..457f59e93 100644
--- a/src/frontends/lean/parser.h
+++ b/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);
     }
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 572261c12..a96665f22 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/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 {
diff --git a/tests/lean/run/record5.lean b/tests/lean/run/record5.lean
new file mode 100644
index 000000000..6811a2232
--- /dev/null
+++ b/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