From ca43608aa01da6f08ffb135227fe54bd8d9beb9b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Aug 2025 18:06:21 +0200 Subject: [PATCH] feat: allow combining `private/public` and `protected` --- src/Lean/Elab/DeclModifiers.lean | 42 +++++++++---------- src/Lean/Elab/Inductive.lean | 2 +- src/Lean/Elab/MutualInductive.lean | 4 +- src/Lean/Elab/Structure.lean | 23 +++++----- src/Lean/Linter/UnusedVariables.lean | 2 +- src/Lean/Parser/Command.lean | 8 ++-- src/lake/Lake/Load/Toml.lean | 7 ++++ tests/lean/StxQuot.lean.expected.out | 8 ++-- .../partialSyntaxTraces.lean.expected.out | 2 +- tests/lean/run/ctorFieldVisibilityHints.lean | 2 +- 10 files changed, 52 insertions(+), 48 deletions(-) diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index 1fa38a458f..e059383130 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -49,26 +49,21 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadFina addInfo declName throwError "a non-private declaration '{.ofConstName declName true}' has already been declared" -/-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/ +/-- Declaration visibility modifier. That is, whether a declaration is public or private or inherits its visibility from the outer scope. -/ inductive Visibility where - | regular | «protected» | «private» | «public» + | regular | «private» | «public» deriving Inhabited instance : ToString Visibility where toString | .regular => "regular" | .private => "private" - | .protected => "protected" | .public => "public" def Visibility.isPrivate : Visibility → Bool | .private => true | _ => false -def Visibility.isProtected : Visibility → Bool - | .protected => true - | _ => false - def Visibility.isPublic : Visibility → Bool | .public => true | _ => false @@ -92,6 +87,7 @@ structure Modifiers where stx : TSyntax ``Parser.Command.declModifiers := ⟨.missing⟩ docString? : Option (TSyntax ``Parser.Command.docComment) := none visibility : Visibility := Visibility.regular + isProtected : Bool := false computeKind : ComputeKind := .regular recKind : RecKind := RecKind.default isUnsafe : Bool := false @@ -99,7 +95,6 @@ structure Modifiers where deriving Inhabited def Modifiers.isPrivate (m : Modifiers) : Bool := m.visibility.isPrivate -def Modifiers.isProtected (m : Modifiers) : Bool := m.visibility.isProtected def Modifiers.isPublic (m : Modifiers) : Bool := m.visibility.isPublic def Modifiers.isInferredPublic (env : Environment) (m : Modifiers) : Bool := m.visibility.isInferredPublic env @@ -147,8 +142,8 @@ instance : ToFormat Modifiers := ⟨fun m => ++ (match m.visibility with | .regular => [] | .private => [f!"private"] - | .protected => [f!"protected"] | .public => [f!"public"]) + ++ (if m.isProtected then [f!"protected"] else []) ++ (match m.computeKind with | .regular => [] | .meta => [f!"meta"] | .noncomputable => [f!"noncomputable"]) ++ (match m.recKind with | RecKind.partial => [f!"partial"] | RecKind.nonrec => [f!"nonrec"] | _ => []) ++ (if m.isUnsafe then [f!"unsafe"] else []) @@ -176,18 +171,19 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers : let docCommentStx := stx.raw[0] let attrsStx := stx.raw[1] let visibilityStx := stx.raw[2] + let protectedStx := stx.raw[3] let computeKind := - if stx.raw[3].isNone then + if stx.raw[4].isNone then .regular - else if stx.raw[3][0].getKind == ``Parser.Command.meta then + else if stx.raw[4][0].getKind == ``Parser.Command.meta then .meta else .noncomputable - let unsafeStx := stx.raw[4] + let unsafeStx := stx.raw[5] let recKind := - if stx.raw[5].isNone then + if stx.raw[6].isNone then RecKind.default - else if stx.raw[5][0].getKind == ``Parser.Command.partial then + else if stx.raw[6][0].getKind == ``Parser.Command.partial then RecKind.partial else RecKind.nonrec @@ -197,14 +193,14 @@ def elabModifiers (stx : TSyntax ``Parser.Command.declModifiers) : m Modifiers : | some v => match v with | `(Parser.Command.visibility| private) => pure .private - | `(Parser.Command.visibility| protected) => pure .protected | `(Parser.Command.visibility| public) => pure .public | _ => throwErrorAt v "unexpected visibility modifier" + let isProtected := !protectedStx.isNone let attrs ← match attrsStx.getOptional? with | none => pure #[] | some attrs => elabDeclAttrs attrs return { - stx, docString?, visibility, computeKind, recKind, attrs, + stx, docString?, visibility, isProtected, computeKind, recKind, attrs, isUnsafe := !unsafeStx.isNone } @@ -213,12 +209,12 @@ Ensure the function has not already been declared, and apply the given visibilit If `private`, return the updated name using our internal encoding for private names. If `protected`, register `declName` as protected in the environment. -/ -def applyVisibility (visibility : Visibility) (declName : Name) : m Name := do +def applyVisibility (modifiers : Modifiers) (declName : Name) : m Name := do let mut declName := declName - if !visibility.isInferredPublic (← getEnv) then + if !modifiers.visibility.isInferredPublic (← getEnv) then declName := mkPrivateName (← getEnv) declName checkNotAlreadyDeclared declName - if visibility matches .protected then + if modifiers.isProtected then modifyEnv fun env => addProtected env declName pure declName @@ -246,16 +242,16 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) shortName := Name.mkSimple s currNamespace := p.replacePrefix `_root_ Name.anonymous checkIfShadowingStructureField declName - let declName ← applyVisibility modifiers.visibility declName - match modifiers.visibility with - | Visibility.protected => + let declName ← applyVisibility modifiers declName + if modifiers.isProtected then match currNamespace with | .str _ s => return (declName, Name.mkSimple s ++ shortName) | _ => if shortName.isAtomic then throwError "protected declarations must be in a namespace" return (declName, shortName) - | _ => return (declName, shortName) + else + return (declName, shortName) /-- `declId` is of the form diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index a2ff71dc52..b833521b02 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -60,7 +60,7 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Term checkValidCtorModifier ctorModifiers let ctorName := ctor.getIdAt 3 let ctorName := declName ++ ctorName - let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers.visibility ctorName + let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName let (binders, type?) := expandOptDeclSig ctor[4] addDocString' ctorName ctorModifiers.docString? addDeclarationRangesFromSyntax ctorName ctor ctor[3] diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 6f9724a84d..43e10702f5 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -1021,8 +1021,8 @@ private def applyComputedFields (indViews : Array InductiveView) : CommandElabM for {ref, fieldId, type, matchAlts, modifiers, ..} in indView.computedFields do computedFieldDefs := computedFieldDefs.push <| ← do let modifiers ← match modifiers with - | `(Lean.Parser.Command.declModifiersT| $[$doc:docComment]? $[$attrs:attributes]? $[$vis]? $[noncomputable]?) => - `(Lean.Parser.Command.declModifiersT| $[$doc]? $[$attrs]? $[$vis]? noncomputable) + | `(Lean.Parser.Command.declModifiersT| $[$doc:docComment]? $[$attrs:attributes]? $[$vis]? $[protected%$protectedTk]? $[noncomputable]?) => + `(Lean.Parser.Command.declModifiersT| $[$doc]? $[$attrs]? $[$vis]? $[protected%$protectedTk]? noncomputable) | _ => do withRef modifiers do logError "Unsupported modifiers for computed field" `(Parser.Command.declModifiersT| noncomputable) diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 37ba3179b9..845479ce71 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -233,11 +233,12 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc (forcePrivate : Bool) : TermElabM CtorView := do let useDefault := do let visibility := if forcePrivate then .private else .regular + let modifiers := { (default : Modifiers) with visibility } let declName := structDeclName ++ defaultCtorName - let declName ← applyVisibility visibility declName + let declName ← applyVisibility modifiers declName let ref := structStx[1].mkSynthetic addDeclarationRangesFromSyntax declName ref - pure { ref, declId := ref, modifiers := { (default : Modifiers) with visibility }, declName } + pure { ref, declId := ref, modifiers, declName } if structStx[4].isNone then useDefault else @@ -273,7 +274,7 @@ private def expandCtor (structStx : Syntax) (structModifiers : Modifiers) (struc throwError m!"Constructor must be `private` because one or more of this structure's fields are `private`" ++ hint let name := ctor[1].getId let declName := structDeclName ++ name - let declName ← applyVisibility ctorModifiers.visibility declName + let declName ← applyVisibility ctorModifiers declName -- `binders` is type parameter binder overrides; this will be validated when the constructor is created in `Structure.mkCtor`. let binders := ctor[2] addDocString' declName ctorModifiers.docString? @@ -379,7 +380,7 @@ private def expandFields (structStx : Syntax) (structModifiers : Modifiers) (str unless name.isAtomic do throwErrorAt ident "Invalid field name `{name.eraseMacroScopes}`: Field names must be atomic" let declName := structDeclName ++ name - let declName ← applyVisibility fieldModifiers.visibility declName + let declName ← applyVisibility fieldModifiers declName addDocString' declName fieldModifiers.docString? return views.push { ref := ident @@ -611,13 +612,11 @@ private def getFieldDefault? (structName : Name) (params : Array Expr) (fieldNam else return none -private def toVisibility (fieldInfo : StructureFieldInfo) : CoreM Visibility := do - if isProtected (← getEnv) fieldInfo.projFn then - return Visibility.protected - else if isPrivateName fieldInfo.projFn then - return Visibility.private - else - return Visibility.regular +private def toModifiers (fieldInfo : StructureFieldInfo) : CoreM Modifiers := do + return { + isProtected := isProtected (← getEnv) fieldInfo.projFn + visibility := if isPrivateName fieldInfo.projFn then .private else .regular + } mutual @@ -654,7 +653,7 @@ private partial def withStructField (view : StructView) (sourceStructNames : Lis its default value is overridden, otherwise the `declName` is irrelevant, except to ensure a declaration is not already declared. -/ let mut declName := view.declName ++ fieldName if inSubobject?.isNone then - declName ← applyVisibility (← toVisibility fieldInfo) declName + declName ← applyVisibility (← toModifiers fieldInfo) declName -- No need to validate links because this docstring was already added to the environment previously addDocStringCore' declName (← findDocString? (← getEnv) fieldInfo.projFn) addDeclarationRangesFromSyntax declName (← getRef) diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index 2814729668..5cea440259 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -232,7 +232,7 @@ builtin_initialize addBuiltinUnusedVariablesIgnoreFn (fun _ stack _ => stx.isOfKind ``Lean.Parser.Command.optDeclSig || stx.isOfKind ``Lean.Parser.Command.declSig) && (stack[5]? |>.any fun (stx, _) => match stx[0] with - | `(Lean.Parser.Command.declModifiersT| $[$_:docComment]? @[$[$attrs:attr],*] $[$vis]? $[noncomputable]?) => + | `(Lean.Parser.Command.declModifiersT| $[$_:docComment]? @[$[$attrs:attr],*] $[$vis]? $[protected]? $[noncomputable]?) => attrs.any (fun attr => attr.raw.isOfKind ``Parser.Attr.extern || attr matches `(attr| implemented_by $_)) | _ => false)) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 1fa98c756c..493eeb530c 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -62,11 +62,11 @@ def namedPrio := leading_parser def optNamedPrio := optional namedPrio def «private» := leading_parser "private " -def «protected» := leading_parser "protected " def «public» := leading_parser "public " def visibility := withAntiquot (mkAntiquot "visibility" decl_name% (isPseudoKind := true)) <| - «private» <|> «protected» <|> «public» + «private» <|> «public» +def «protected» := leading_parser "protected " def «meta» := leading_parser "meta " def «noncomputable» := leading_parser "noncomputable " def «unsafe» := leading_parser "unsafe " @@ -76,7 +76,8 @@ def «nonrec» := leading_parser "nonrec " /-- `declModifiers` is the collection of modifiers on a declaration: * a doc comment `/-- ... -/` * a list of attributes `@[attr1, attr2]` -* a visibility specifier, `private`, `protected`, or `public` +* a visibility specifier, `private` or `public` +* `protected` * `noncomputable` * `unsafe` * `partial` or `nonrec` @@ -90,6 +91,7 @@ such as inductive constructors, structure projections, and `let rec` / `where` d optional docComment >> optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >> optional visibility >> + optional «protected» >> optional («meta» <|> «noncomputable») >> optional «unsafe» >> optional («partial» <|> «nonrec») diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 47aa332c18..b393a30172 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -347,6 +347,12 @@ instance : DecodeToml Dependency := ⟨fun v => do Dependency.decodeToml (← v. /-! ## Package & Target Configuration Decoders -/ +section +-- We automatically disable the following option for `macro`s but the subsequent `def` both contains +-- a quotation and is called only by `macro`s, so we disable the option for it manually. Note that +-- we can't use `in` as it is parsed as a single command and so the option would not influence the +-- parser. +set_option internal.parseQuotWithCurrentStage false private def genDecodeToml (cmds : Array Command) (tyName : Name) [info : ConfigInfo tyName] (takesName : Bool) @@ -366,6 +372,7 @@ private def genDecodeToml let instId ← mkIdentFromRef <| `_root_ ++ tyName.str "instDecodeToml" let cmds ← cmds.push <$> `(instance $instId:ident : DecodeToml $ty := ⟨decodeTableValue $decId⟩) return cmds +end local macro "gen_toml_decoders%" : command => do let cmds := #[] diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index 084fa32053..2443f5b965 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -8,8 +8,8 @@ StxQuot.lean:8:12-8:13: error: unexpected token ')'; expected identifier or term "(«term_+_» (num \"1\") \"+\" (num \"1\"))" StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] [] \"=>\" `a._@.UnhygienicMain._hyg.1))" -"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))" -"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n []))]" +"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))" +"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n []))]" "`Nat.one._@.UnhygienicMain._hyg.1" "`Nat.one._@.UnhygienicMain._hyg.1" "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])" @@ -18,8 +18,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)" "(«term_+_» (num \"2\") \"+\" (num \"1\"))" "(«term_+_» («term_+_» (num \"1\") \"+\" (num \"2\")) \"+\" (num \"1\"))" -"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))" -"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))]" +"(Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))" +"[(Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"2\") (Termination.suffix [] []) [])\n []))\n (Command.declaration\n (Command.declModifiers [] [] [] [] [] [] [])\n (Command.definition\n \"def\"\n (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n (Command.optDeclSig [] [])\n (Command.declValSimple \":=\" (num \"1\") (Termination.suffix [] []) [])\n []))]" "0" 0 1 diff --git a/tests/lean/partialSyntaxTraces.lean.expected.out b/tests/lean/partialSyntaxTraces.lean.expected.out index d49f0e8928..652a1cc599 100644 --- a/tests/lean/partialSyntaxTraces.lean.expected.out +++ b/tests/lean/partialSyntaxTraces.lean.expected.out @@ -1,6 +1,6 @@ partialSyntaxTraces.lean:6:0: error: unexpected end of input; expected ':=', 'where' or '|' [Elab.command] [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.] (Command.declaration - (Command.declModifiers [] [] [] [] [] []) + (Command.declModifiers [] [] [] [] [] [] []) (Command.definition "def" (Command.declId `f []) (Command.optDeclSig [] []) (Command.whereStructInst ))) [Elab.command] diff --git a/tests/lean/run/ctorFieldVisibilityHints.lean b/tests/lean/run/ctorFieldVisibilityHints.lean index 7061b13661..776b611eab 100644 --- a/tests/lean/run/ctorFieldVisibilityHints.lean +++ b/tests/lean/run/ctorFieldVisibilityHints.lean @@ -10,7 +10,7 @@ necessary correction is reasonably unambiguous. error: Constructor must be `private` because one or more of this structure's fields are `private` Hint: Mark constructor as `private` - p̵r̵o̵t̵e̵c̵t̵e̵d̵p̲r̲i̲v̲a̲t̲e̲ mk :: + p̲r̲i̲v̲a̲t̲e̲ ̲protected mk :: -/ #guard_msgs in structure Foo where