feat: closes #415

src/Lean/Elab/StructInst.lean

@@ -17,7 +17,7 @@ open Meta
   Structure instances are of the form:
 
       "{" >> optional (atomic (termParser >> " with "))
-          >> manyIndent (group (structInstField >> optional ", "))
+          >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
           >> optEllipsis
           >> optional (" : " >> termParser)
           >> " }"
@@ -94,32 +94,35 @@ private def getStructSource (stx : Syntax) : TermElabM Source :=
 -/
 private def isModifyOp? (stx : Syntax) : TermElabM (Option Syntax) := do
   let s? ← stx[2].getArgs.foldlM (init := none) fun s? p =>
-    /- p is of the form `(group (structInstField >> optional ", "))` -/
+    /- p is of the form `(group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))` -/
     let arg := p[0]
-    /- Remark: the syntax for `structInstField` is
-       ```
-       def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
-       def structInstField  := leading_parser structInstLVal >> " := " >> termParser
-       ```
-    -/
-    let lval := arg[0]
-    let k    := lval[0].getKind
-    if k == ``Lean.Parser.Term.structInstArrayRef then
-      match s? with
-      | none   => pure (some arg)
-      | some s =>
-        if s.getKind == ``Lean.Parser.Term.structInstArrayRef then
-          throwErrorAt arg "invalid \{...} notation, at most one `[..]` at a given level"
-        else
-          throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level"
+    if arg.getKind == ``Lean.Parser.Term.structInstField then
+      /- Remark: the syntax for `structInstField` is
+         ```
+         def structInstLVal   := leading_parser (ident <|> numLit <|> structInstArrayRef) >> many (group ("." >> (ident <|> numLit)) <|> structInstArrayRef)
+         def structInstField  := leading_parser structInstLVal >> " := " >> termParser
+         ```
+      -/
+      let lval := arg[0]
+      let k    := lval[0].getKind
+      if k == ``Lean.Parser.Term.structInstArrayRef then
+        match s? with
+        | none   => pure (some arg)
+        | some s =>
+          if s.getKind == ``Lean.Parser.Term.structInstArrayRef then
+            throwErrorAt arg "invalid \{...} notation, at most one `[..]` at a given level"
+          else
+            throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level"
+      else
+        match s? with
+        | none   => pure (some arg)
+        | some s =>
+          if s.getKind == ``Lean.Parser.Term.structInstArrayRef then
+            throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level"
+          else
+            pure s?
     else
-      match s? with
-      | none   => pure (some arg)
-      | some s =>
-        if s.getKind == ``Lean.Parser.Term.structInstArrayRef then
-          throwErrorAt arg "invalid \{...} notation, can't mix field and `[..]` at a given level"
-        else
-          pure s?
+      pure s?
   match s? with
   | none   => pure none
   | some s => if s[0][0].getKind == ``Lean.Parser.Term.structInstArrayRef then pure s? else pure none
@@ -281,7 +284,7 @@ def Field.toSyntax : Field Struct → Syntax
     | first::rest => stx.setArg 0 <| mkNullNode #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
     | _ => unreachable!
 
-private def toFieldLHS (stx : Syntax) : Except String FieldLHS :=
+private def toFieldLHS (stx : Syntax) : MacroM FieldLHS :=
   if stx.getKind == ``Lean.Parser.Term.structInstArrayRef then
     return FieldLHS.modifyOp stx stx[1]
   else
@@ -291,19 +294,25 @@ private def toFieldLHS (stx : Syntax) : Except String FieldLHS :=
       return FieldLHS.fieldName stx stx.getId.eraseMacroScopes
     else match stx.isFieldIdx? with
       | some idx => return FieldLHS.fieldIndex stx idx
-      | none     => throw "unexpected structure syntax"
+      | none     => Macro.throwError "unexpected structure syntax"
 
-private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : Except String Struct := do
+private def mkStructView (stx : Syntax) (structName : Name) (source : Source) : MacroM Struct := do
   /- Recall that `stx` is of the form
      ```
      leading_parser "{" >> optional (atomic (termParser >> " with "))
-                 >> manyIndent (group (structInstField >> optional ", "))
+                 >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
                  >> optional ".."
                  >> optional (" : " >> termParser)
                  >> " }"
      ```
   -/
-  let fieldsStx := stx[2].getArgs.map (·[0])
+  let fieldsStx ← stx[2].getArgs.mapM fun stx =>
+    let stx := stx[0]
+    if stx.getKind == ``Lean.Parser.Term.structInstField then
+      return stx
+    else
+      let id := stx[0]
+      `(Lean.Parser.Term.structInstField| $id:ident := $id:ident)
   let fields ← fieldsStx.toList.mapM fun fieldStx => do
     let val   := fieldStx[2]
     let first ← toFieldLHS fieldStx[0][0]
@@ -788,14 +797,12 @@ private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (sour
   let (structName, structType) ← getStructName stx expectedType? source
   unless isStructureLike (← getEnv) structName do
     throwError "invalid \{...} notation, structure type expected{indentExpr structType}"
-  match mkStructView stx structName source with
-  | Except.error ex  => throwError ex
-  | Except.ok struct =>
-    let struct ← expandStruct struct
-    trace[Elab.struct] "{struct}"
-    let (r, struct) ← elabStruct struct expectedType?
-    DefaultFields.propagate struct
-    pure r
+  let struct ← liftMacroM <| mkStructView stx structName source
+  let struct ← expandStruct struct
+  trace[Elab.struct] "{struct}"
+  let (r, struct) ← elabStruct struct expectedType?
+  DefaultFields.propagate struct
+  return r
 
 @[builtinTermElab structInst] def elabStructInst : TermElab := fun stx expectedType? => do
   match (← expandNonAtomicExplicitSource stx) with

src/Lean/Parser/Term.lean

@@ -81,9 +81,10 @@ def sufficesDecl := leading_parser optIdent >> termParser >> (fromTerm <|> byTac
 def structInstArrayRef := leading_parser "[" >> termParser >>"]"
 def structInstLVal   := leading_parser (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
 def structInstField  := ppGroup $ leading_parser structInstLVal >> " := " >> termParser
+def structInstFieldAbbrev := leading_parser atomic (ident >> notFollowedBy ("." <|> ":=" <|> symbol "[") "invalid field abbreviation") -- `x` is an abbreviation for `x := x`
 def optEllipsis      := leading_parser optional ".."
 @[builtinTermParser] def structInst := leading_parser "{" >> ppHardSpace >> optional (atomic (termParser >> " with "))
-  >> manyIndent (group (structInstField >> optional ", "))
+  >> manyIndent (group ((structInstFieldAbbrev <|> structInstField) >> optional ", "))
   >> optEllipsis
   >> optional (" : " >> termParser) >> " }"
 def typeSpec := leading_parser " : " >> termParser

tests/lean/415.lean

@@ -0,0 +1,39 @@
+structure Point where
+  x : Nat
+  y : Nat
+
+def f (x : Nat) : Point :=
+  let y := x + 1
+  { x, y }
+
+theorem ex1 : f x = { x, y := x + 1 } :=
+  rfl
+
+def g (p : Point) : Nat :=
+  p.x + p.y
+
+def Set (α : Type u) : Type u :=
+  α → Prop
+
+def Set.empty : Set α :=
+  fun a => False
+
+def Set.insert (s : Set α) (a : α) : Set α :=
+  fun x => x = a ∨ s a
+
+syntax (name := finSet) "{" term,* "}" : term
+
+macro_rules (kind := finSet)
+  | `({ $as,* }) => do
+     as.getElems.foldlM (init := ← `(Set.empty)) fun s a => `(Set.insert $s $a)
+
+#check { 1, 2, 3 }
+
+#check fun x y => g {x, y}
+
+#check fun x y : Nat => {x, y}
+
+#check fun x y : Nat => {x, y : Point}
+
+theorem ex2 (x y : Nat) : { x, y } = (Set.empty.insert x |>.insert y) :=
+  rfl

tests/lean/415.lean.expected.out

@@ -0,0 +1,4 @@
+Set.insert (Set.insert (Set.insert Set.empty 1) 2) 3 : Set Nat
+fun (x y : Nat) => g { x := x, y := y } : Nat → Nat → Nat
+fun (x y : Nat) => Set.insert (Set.insert Set.empty x) y : Nat → Nat → Set Nat
+fun (x y : Nat) => { x := x, y := y } : Nat → Nat → Point