feat: := private instance syntax

src/Lean/Elab/BuiltinTerm.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Closure
 import Lean.Meta.Diagnostics
 import Lean.Elab.Open
 import Lean.Elab.SetOption
@@ -350,4 +351,16 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
 @[builtin_term_elab Lean.Parser.Term.namedPattern] def elabNamedPatternErr : TermElab := fun stx _ =>
   throwError "`<identifier>@<term>` is a named pattern and can only be used in pattern matching contexts{indentD stx}"
 
+@[builtin_term_elab «privateDecl»] def elabPrivateDecl : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(Parser.Term.privateDecl| private_decl% $e) =>
+    if (← getEnv).isExporting then
+      let name ← mkAuxDeclName `_private
+      withoutExporting do
+        let e ← elabTerm e expectedType?
+        mkAuxDefinitionFor name e
+    else
+      elabTerm e expectedType?
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term

src/Lean/Elab/StructInst.lean

@@ -76,17 +76,20 @@ Structure instance notation makes use of the expected type.
     `(($stxNew : $expected))
 
 private def mkStructInstField (lval : TSyntax ``Parser.Term.structInstLVal) (binders : TSyntaxArray ``Parser.Term.structInstFieldBinder)
-    (type? : Option Term) (val : Term) : MacroM (TSyntax ``Parser.Term.structInstField) := do
+    (type? : Option Term) (isPrivate : Bool) (val : Term) : MacroM (TSyntax ``Parser.Term.structInstField) := do
   let mut val := val
   if let some type := type? then
     val ← `(($val : $type))
+  if isPrivate then
+    val ← `(Parser.Term.privateDecl| private_decl% $val)
   if !binders.isEmpty then
     -- HACK: this produces invalid syntax, but the fun elaborator supports structInstFieldBinder as well
     val ← `(fun $binders* => $val)
   `(Parser.Term.structInstField| $lval := $val)
 
 /--
-Takes an arbitrary `structInstField` and expands it to be a `structInstFieldDef` without any binders or type ascription.
+Takes an arbitrary `structInstField` and expands it to be a `structInstFieldDef` without any
+binders, type ascription, or `private` modifier.
 -/
 private def expandStructInstField (stx : Syntax) : MacroM (Option Syntax) := withRef stx do
   match stx with
@@ -95,17 +98,17 @@ private def expandStructInstField (stx : Syntax) : MacroM (Option Syntax) := wit
     return none
   | `(Parser.Term.structInstField| $lval:structInstLVal $[$binders]* $[: $ty?]? $decl:structInstFieldDecl) =>
     match decl with
-    | `(Parser.Term.structInstFieldDef| := $val) =>
-      mkStructInstField lval binders ty? val
-    | `(Parser.Term.structInstFieldEqns| $alts:matchAlts) =>
+    | `(Parser.Term.structInstFieldDef| := $[private%$privateTk?]? $val) =>
+      mkStructInstField lval binders ty? privateTk?.isSome val
+    | `(Parser.Term.structInstFieldEqns| $[private%$privateTk?]? $alts:matchAlts) =>
       let val ← expandMatchAltsIntoMatch stx alts (useExplicit := false)
-      mkStructInstField lval binders ty? val
+      mkStructInstField lval binders ty? privateTk?.isSome val
     | _ => Macro.throwUnsupported
   | `(Parser.Term.structInstField| $lval:structInstLVal) =>
     -- Abbreviation
     match lval with
     | `(Parser.Term.structInstLVal| $id:ident) =>
-      mkStructInstField lval #[] none id
+      mkStructInstField lval #[] none false id
     | _ =>
       Macro.throwErrorAt lval "unsupported structure instance field abbreviation, expecting identifier"
   | _ => Macro.throwUnsupported
@@ -237,7 +240,7 @@ private def elabModifyOp (stx modifyOp : Syntax) (sourcesView : SourcesView) (ex
     withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
   let rest := modifyOp[0][1]
   if rest.isNone then
-    cont modifyOp[1][2][1]
+    cont modifyOp[1][2][2]
   else
     let s ← `(s)
     let valFirst  := rest[0]
@@ -336,7 +339,7 @@ Converts a `FieldView` back into syntax. Used to construct synthetic structure i
 private def FieldView.toSyntax : FieldView → TSyntax ``Parser.Term.structInstField
   | field =>
     let stx := field.ref
-    let stx := stx.setArg 1 <| stx[1].setArg 2 <| stx[1][2].setArg 1 field.val
+    let stx := stx.setArg 1 <| stx[1].setArg 2 <| stx[1][2].setArg 2 field.val
     match field.lhs with
     | first::rest => stx.setArg 0 <| mkNode ``Parser.Term.structInstLVal #[first.toSyntax true, mkNullNode <| rest.toArray.map (FieldLHS.toSyntax false) ]
     | _ => unreachable!

src/Lean/Linter/MissingDocs.lean

@@ -11,7 +11,7 @@ import Lean.Elab.SetOption
 import Lean.Linter.Util
 
 namespace Lean.Linter
-open Elab.Command Parser.Command
+open Elab.Command Parser Command
 open Parser.Term hiding «set_option»
 
 register_builtin_option linter.missingDocs : Bool := {
@@ -120,7 +120,7 @@ def hasInheritDoc (attrs : Syntax) : Bool :=
     attr[1][0].getId.eraseMacroScopes == `inherit_doc
 
 def declModifiersPubNoDoc (mods : Syntax) : Bool :=
-  mods[2][0].getKind != ``«private» && mods[0].isNone && !hasInheritDoc mods[1]
+  mods[2][0].getKind != ``Command.private && mods[0].isNone && !hasInheritDoc mods[1]
 
 def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
   if k == ``«abbrev» then lintNamed id "public abbrev"
@@ -134,7 +134,7 @@ def lintDeclHead (k : SyntaxNodeKind) (id : Syntax) : CommandElabM Unit := do
 @[builtin_missing_docs_handler declaration]
 def checkDecl : SimpleHandler := fun stx => do
   let head := stx[0]; let rest := stx[1]
-  if head[2][0].getKind == ``«private» then return -- not private
+  if head[2][0].getKind == ``Command.private then return -- not private
   let k := rest.getKind
   if declModifiersPubNoDoc head then -- no doc string
     lintDeclHead k rest[1][0]

src/Lean/Parser/Basic.lean

@@ -1477,7 +1477,8 @@ that the `else` is not less indented than the `if` it matches with.
 
 This parser has arity 0 - it does not capture anything. -/
 @[builtin_doc] def checkColGe (errorMsg : String := "checkColGe") : Parser where
-  fn := checkColGeFn errorMsg
+  fn   := checkColGeFn errorMsg
+  info := epsilonInfo
 
 def checkColGtFn (errorMsg : String) : ParserFn := fun c s =>
   match c.savedPos? with

src/Lean/Parser/Term.lean

@@ -522,10 +522,10 @@ The structure type can be specified if not inferable:
 
 @[builtin_structInstFieldDecl_parser]
 def structInstFieldDef := leading_parser
-  " := " >> termParser
+  " := " >> optional "private" >> termParser
 @[builtin_structInstFieldDecl_parser]
 def structInstFieldEqns := leading_parser
-  matchAlts
+  optional "private" >> matchAlts
 
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
@@ -879,6 +879,10 @@ In particular, it is like a unary operation with a fixed parameter `b`, where on
 /-- A macro which evaluates to the name of the currently elaborating declaration. -/
 @[builtin_term_parser] def declName := leading_parser "decl_name%"
 
+/-- `private_decl% e` elaborates `e` in a private context and wraps the result in a helper `def`. -/
+@[builtin_term_parser] def «privateDecl» :=
+  leading_parser "private_decl% " >> termParser maxPrec
+
 /--
 * `with_decl_name% id e` elaborates `e` in a context while changing the effective
   declaration name to `id`.

src/lake/Lake/Config/Meta.lean

@@ -83,6 +83,10 @@ private structure FieldMetadata where
   cmds : Array Command := #[]
   fields : Term := Unhygienic.run `(Array.empty)
 
+-- We automatically disable the following option for `macro`s but the subsequent `def`s both contain
+-- quotations and are called only by `macro`s, so we disable the option for them manually.
+set_option internal.parseQuotWithCurrentStage false
+
 private def mkConfigAuxDecls
   (structId : Ident) (structTy : Term) (views : Array FieldView)
 : MacroM (Array Command) := do

tests/lean/StxQuot.lean.expected.out

@@ -32,8 +32,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "`a._@.UnhygienicMain._hyg.1"
 "(Term.explicitUniv `a._@.UnhygienicMain._hyg.1 \".{\" [(num \"0\")] \"}\")"
 "#[(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" (num \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (num \"2\"))]"
-"(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n  [(Term.structInstField\n    (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 [])\n    [[] [] (Term.structInstFieldDef \":=\" `a._@.UnhygienicMain._hyg.1)])])\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
-"(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n  [(Term.structInstField\n    (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 [])\n    [[] [] (Term.structInstFieldDef \":=\" `a._@.UnhygienicMain._hyg.1)])])\n (Term.optEllipsis [])\n []\n \"}\")"
+"(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n  [(Term.structInstField\n    (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 [])\n    [[] [] (Term.structInstFieldDef \":=\" [] `a._@.UnhygienicMain._hyg.1)])])\n (Term.optEllipsis [])\n [\":\" `a._@.UnhygienicMain._hyg.1]\n \"}\")"
+"(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n  [(Term.structInstField\n    (Term.structInstLVal `a._@.UnhygienicMain._hyg.1 [])\n    [[] [] (Term.structInstFieldDef \":=\" [] `a._@.UnhygienicMain._hyg.1)])])\n (Term.optEllipsis [])\n []\n \"}\")"
 "(Command.section (Command.sectionHeader [] []) \"section\" [])"
 "(Command.section (Command.sectionHeader [] []) \"section\" [`foo._@.UnhygienicMain._hyg.1])"
 "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n    \"=>\"\n    («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))"