From af1d8dd0701186ad3ed4f6ad441d05d877a84917 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 16 May 2025 11:50:43 +0200 Subject: [PATCH] feat: `:= private` instance syntax --- src/Lean/Elab/BuiltinTerm.lean | 13 +++++++++++++ src/Lean/Elab/StructInst.lean | 21 ++++++++++++--------- src/Lean/Linter/MissingDocs.lean | 6 +++--- src/Lean/Parser/Basic.lean | 3 ++- src/Lean/Parser/Term.lean | 8 ++++++-- src/lake/Lake/Config/Meta.lean | 4 ++++ tests/lean/StxQuot.lean.expected.out | 4 ++-- 7 files changed, 42 insertions(+), 17 deletions(-) diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index a25106ed28..1f23675f4f 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/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 "`@` 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 diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index bd103d97f3..dc7897f643 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/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! diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index d59fe2fe73..d156bcf6be 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/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] diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index eb08abab23..f36b5cb79a 100644 --- a/src/Lean/Parser/Basic.lean +++ b/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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 4ef3bcca67..8e12f05a15 100644 --- a/src/Lean/Parser/Term.lean +++ b/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`. diff --git a/src/lake/Lake/Config/Meta.lean b/src/lake/Lake/Config/Meta.lean index 173798b94a..23ada95512 100644 --- a/src/lake/Lake/Config/Meta.lean +++ b/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 diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 99706fff12..4db4a70072 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/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\")))]))"