From 6ca1768957e2ff2343e7eebec60bd85cc83c2143 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2020 04:39:20 -0700
Subject: [PATCH] fix: optional `:=` in the structure command

---
 src/Lean/Elab/Structure.lean     | 41 ++++++++++++++++++--------------
 src/Lean/Parser/Command.lean     |  2 +-
 tests/lean/run/structNoBody.lean | 27 +++++++++++++++++++++
 3 files changed, 51 insertions(+), 19 deletions(-)
 create mode 100644 tests/lean/run/structNoBody.lean

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 8d58749f2e..905b7125dd 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -16,7 +16,7 @@ open Meta
 
 /- Recall that the `structure command syntax is
 ```
-parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> structFields
+parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> structFields)
 ```
 -/
 
@@ -93,29 +93,34 @@ structure ElabStructResult :=
 private def defaultCtorName := `mk
 
 /-
-The structore constructor syntax is
+The structure constructor syntax is
 ```
 parser! try (declModifiers >> ident >> optional inferMod >> " :: ")
 ```
 -/
 private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM StructCtorView :=
-  let optCtor := structStx[6]
-  if optCtor.isNone then
+  let useDefault :=
     pure { ref := structStx, modifiers := {}, inferMod := false, name := defaultCtorName, declName := structDeclName ++ defaultCtorName }
+  if structStx[5].isNone then
+    useDefault
   else
-    let ctor := optCtor[0]
-    withRef ctor do
-    let ctorModifiers ← elabModifiers ctor[0]
-    checkValidCtorModifier ctorModifiers
-    if ctorModifiers.isPrivate && structModifiers.isPrivate then
-      throwError "invalid 'private' constructor in a 'private' structure"
-    if ctorModifiers.isProtected && structModifiers.isPrivate then
-      throwError "invalid 'protected' constructor in a 'private' structure"
-    let inferMod := !ctor[2].isNone
-    let name := ctor[1].getId
-    let declName := structDeclName ++ name
-    let declName ← applyVisibility ctorModifiers.visibility declName
-    pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }
+    let optCtor := structStx[5][1]
+    if optCtor.isNone then
+      useDefault
+    else
+      let ctor := optCtor[0]
+      withRef ctor do
+      let ctorModifiers ← elabModifiers ctor[0]
+      checkValidCtorModifier ctorModifiers
+      if ctorModifiers.isPrivate && structModifiers.isPrivate then
+        throwError "invalid 'private' constructor in a 'private' structure"
+      if ctorModifiers.isProtected && structModifiers.isPrivate then
+        throwError "invalid 'protected' constructor in a 'private' structure"
+      let inferMod := !ctor[2].isNone
+      let name := ctor[1].getId
+      let declName := structDeclName ++ name
+      let declName ← applyVisibility ctorModifiers.visibility declName
+      pure { ref := ctor, name := name, modifiers := ctorModifiers, inferMod := inferMod, declName := declName }
 
 def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
   if modifiers.isNoncomputable then
@@ -138,7 +143,7 @@ def structFields         := parser! many (structExplicitBinder <|> structImplici
 ```
 -/
 private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
-  let fieldBinders := structStx[7][0].getArgs
+  let fieldBinders := if structStx[5].isNone then #[] else structStx[5][2][0].getArgs
   fieldBinders.foldlM (init := #[]) fun (views : Array StructFieldView) fieldBinder => withRef fieldBinder do
     let k := fieldBinder.getKind
     let binfo ←
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index d1effdbe23..7d39855fa6 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -58,7 +58,7 @@ def structCtor           := parser! «try» (declModifiers true >> ident >> opti
 def structureTk          := parser! "structure "
 def classTk              := parser! "class "
 def «extends»            := parser! " extends " >> sepBy1 termParser ", "
-def «structure»          := parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> " := " >> optional structCtor >> ppDedent structFields
+def «structure»          := parser! (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType >> optional (" := " >> optional structCtor >> ppDedent structFields)
 @[builtinCommandParser] def declaration := parser!
 declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
 
diff --git a/tests/lean/run/structNoBody.lean b/tests/lean/run/structNoBody.lean
new file mode 100644
index 0000000000..56685a59dd
--- /dev/null
+++ b/tests/lean/run/structNoBody.lean
@@ -0,0 +1,27 @@
+#lang lean4
+
+structure A :=
+(x y : Nat)
+
+structure B :=
+(z : Nat)
+
+structure C extends A, B
+
+def f (c : C) :=
+c.x + c.y + c.z
+
+theorem ex1 : f {x := 10, y := 20, z := 30} = 60 :=
+rfl
+
+structure D
+
+def g (d : D) : D :=
+d
+
+theorem ex2 : g {} = {} :=
+rfl
+
+theorem ex3 (d : D) : g d = {} := by
+ cases d
+ exact rfl