chore: cleaner structure/class syntax

@Kha I implemented the syntax for structure/class that we discussed this morning.
It is much cleaner. See new tests at `struct2.lean`.
I updated the documentation to use it.

doc/functions.md

@@ -26,9 +26,9 @@ the function body is `x + 1`, and the return value is of type `Nat`.
 The following example defines the factorial recursive function using pattern matching.
 ```lean
 def fact x :=
- match x with
- | 0   => 1
- | n+1 => (n+1) * fact n
+  match x with
+  | 0   => 1
+  | n+1 => (n+1) * fact n
 
 #eval fact 100
 ```

doc/lean3changes.md

@@ -24,8 +24,8 @@ In Lean 4, one can easily create new notation that abbreviates commonly used idi
 def Prod.str : Nat × Nat → String :=
   fun (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")"
 
-structure Point :=
-  (x y z : Nat)
+structure Point where
+  x y z : Nat
 
 def Point.addX : Point → Point → Nat :=
   fun { x := a, .. } { x := b, .. } =>  a+b
@@ -173,7 +173,7 @@ example (x y : α) : g x y = fun (c : α) => x + y + c := rfl
 In Lean 4, we can use `..` to provide missing explicit arguments as `_`.
 This feature combined with named arguments is useful for writing patterns. Here is an example:
 ```lean
-inductive Term
+inductive Term where
   | var    (name : String)
   | num    (val : Nat)
   | add    (fn : Term) (arg : Term)

doc/stringinterp.md

@@ -41,9 +41,9 @@ def vals := [1, 2, 3]
 You can define a `ToString` instance for your own datatypes.
 
 ```lean
-structure Person :=
-  (name : String)
-  (age  : Nat)
+structure Person where
+  name : String
+  age  : Nat
 
 instance : ToString Person where
   toString : Person -> String

doc/tour.md

@@ -84,7 +84,7 @@ theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=
 
 -- An enumerated type is a special case of inductive type in Lean
 -- The following command creates a new type `Weekday`
-inductive Weekday :=
+inductive Weekday where
   | sunday    : Weekday
   | monday    : Weekday
   | tuesday   : Weekday

src/Lean/Elab/Structure.lean

@@ -135,15 +135,20 @@ def checkValidFieldModifier (modifiers : Modifiers) : CommandElabM Unit := do
 
 /-
 ```
-def structExplicitBinder := parser! try (declModifiers >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
-def structImplicitBinder := parser! try (declModifiers >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
-def structInstBinder     := parser! try (declModifiers >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
+def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
+def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
+def structInstBinder     := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
+def structSimpleBinder   := parser! atomic (declModifiers true >> many1 ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
 def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
 ```
 -/
 private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (structDeclName : Name) : CommandElabM (Array StructFieldView) :=
   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 mut fieldBinder := fieldBinder
+    if fieldBinder.getKind == `Lean.Parser.Command.structSimpleBinder then
+      fieldBinder := Syntax.node `Lean.Parser.Command.structExplicitBinder
+        #[ fieldBinder[0], mkAtomFrom fieldBinder "(", fieldBinder[1], fieldBinder[2], fieldBinder[3], fieldBinder[4], mkAtomFrom fieldBinder ")" ]
     let k := fieldBinder.getKind
     let binfo ←
       if k == `Lean.Parser.Command.structExplicitBinder then pure BinderInfo.default
@@ -178,12 +183,12 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str
         throwError! "invalid field name '{name}', identifiers starting with '_' are reserved to the system"
       let declName := structDeclName ++ name
       let declName ← applyVisibility fieldModifiers.visibility declName
-      pure $ views.push {
+      return views.push {
         ref        := ident,
         modifiers  := fieldModifiers,
         binderInfo := binfo,
         inferMod   := inferMod,
-         declName   := declName,
+        declName   := declName,
         name       := name,
         binders    := binders,
         type?      := type?,

src/Lean/Parser/Command.lean

@@ -47,17 +47,20 @@ def «axiom»          := parser! "axiom " >> declId >> declSig
 def «example»        := parser! "example " >> declSig >> declVal
 def inferMod         := parser! atomic ("{" >> "}")
 def ctor             := parser! "\n| " >> declModifiers true >> ident >> optional inferMod >> optDeclSig
-def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> optional ":=" >> many ctor
-def classInductive   := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional ":=" >> many ctor
+def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
+def classInductive   := parser! atomic (group ("class " >> "inductive ")) >> declId >> optDeclSig >> optional (":=" <|> "where") >> many ctor
 def structExplicitBinder := parser! atomic (declModifiers true >> "(") >> many1 ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
 def structImplicitBinder := parser! atomic (declModifiers true >> "{") >> many1 ident >> optional inferMod >> declSig >> "}"
 def structInstBinder     := parser! atomic (declModifiers true >> "[") >> many1 ident >> optional inferMod >> declSig >> "]"
-def structFields         := parser! many (ppLine >> (structExplicitBinder <|> structImplicitBinder <|> structInstBinder))
+def structSimpleBinder   := parser! atomic (declModifiers true >> many1 ident) >> optional inferMod >> optDeclSig >> optional Term.binderDefault
+def structFields         := parser! manyIndent (ppLine >> checkColGe >>(structExplicitBinder <|> structImplicitBinder <|> structInstBinder <|> structSimpleBinder))
 def structCtor           := parser! atomic (declModifiers true >> ident >> optional inferMod >> " :: ")
 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 (" := " >> optional structCtor >> structFields)
+def «structure»          := parser!
+    (structureTk <|> classTk) >> declId >> many Term.bracketedBinder >> optional «extends» >> Term.optType
+    >> optional ((" := " <|> " where ") >> optional structCtor >> structFields)
 @[builtinCommandParser] def declaration := parser!
 declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
 

tests/lean/run/struct2.lean

@@ -1,6 +1,4 @@
-
-
-universe u
+universes u v w
 
 structure A (α : Type u) :=
 (f : (β : Type u) → α → β → α)
@@ -14,3 +12,52 @@ structure B (α : Type u) extends A α :=
 #check B.f._default
 
 #check { x := 10 : B Nat}
+
+namespace New
+
+structure A (α : Type u) where
+  f : (β : Type u) → α → β → α
+
+structure B (α : Type u) extends A α where
+  x : Nat
+  f := fun β a b => a
+
+#check B.f._default
+
+#check { x := 10 : B Nat }
+
+structure Data where
+  index?   : Option Nat := none
+  lowlink? : Option Nat := none
+  onStack  : Bool       := false
+
+structure State (α : Type) where
+  stack     : List α := []
+  nextIndex : Nat := 0
+  data      : Array Data := #[]
+  sccs      : List (List α) := []
+
+inductive Format where
+  | nil                 : Format
+  | line                : Format
+  | text                : String → Format
+  | nest (indent : Int) : Format → Format
+  | append              : Format → Format → Format
+  | group               : Format → Format
+
+class MonadControl (m : Type u → Type v) (n : Type u → Type w) where
+  stM          : Type u → Type u
+  liftWith {α} : (({β : Type u} → n β → m (stM β)) → m α) → n α
+  restoreM {α} : m (stM α) → n α
+
+instance : MonadControl m (ReaderT ρ m) where
+  stM        := id
+  liftWith f := fun ctx => f fun x => x ctx
+  restoreM x := fun ctx => x
+
+instance [Monad m] : MonadControl m (StateT σ m) where
+  stM α := α × σ
+  liftWith f := do let s ← get; liftM (f (fun x => x.run s))
+  restoreM x := do let (a, s) ← liftM x; set s; pure a
+
+end New