diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index a7cf96ca55..a216aae91b 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -128,7 +128,7 @@ def addDecl (decl : Declaration) (forceExpose := false) : CoreM Unit := do | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom) | _ => return (← doAdd) - if decl.getTopLevelNames.all isPrivateName then + if decl.getTopLevelNames.all isPrivateName && !(← ResolveName.backward.privateInPublic.getM) then exportedInfo? := none else -- preserve original constant kind in extension if different from exported one diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index abe2a4fa49..d858721c97 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -121,6 +121,9 @@ protected def get? [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : Op protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α := opts.get opt.name opt.defValue +protected def getM [Monad m] [MonadOptions m] [KVMap.Value α] (opt : Lean.Option α) : m α := + return opt.get (← getOptions) + protected def set [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val : α) : Options := opts.set opt.name val diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 0111a90c3f..12048f3018 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1267,7 +1267,9 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N let find? structName' : MetaM (Option (Name × Name)) := do let fullName := privateToUserName structName' ++ fieldName -- We do not want to make use of the current namespace for resolution. - let candidates := ResolveName.resolveGlobalName (← getEnv) Name.anonymous (← getOpenDecls) fullName + let candidates := + (← withTheReader Core.Context ({ · with currNamespace := .anonymous }) do + resolveGlobalName fullName) |>.filter (fun (_, fieldList) => fieldList.isEmpty) |>.map Prod.fst match candidates with @@ -1737,7 +1739,7 @@ where -- Recall that the namespace for private declarations is non-private. let fullName := privateToUserName declName ++ id -- Resolve the name without making use of the current namespace, like in `findMethod?`. - let candidates := ResolveName.resolveGlobalName env Name.anonymous (← getOpenDecls) fullName + let candidates := ResolveName.resolveGlobalName env (← getOptions) Name.anonymous (← getOpenDecls) fullName |>.filter (fun (_, fieldList) => fieldList.isEmpty) |>.map Prod.fst if !candidates.isEmpty then diff --git a/src/Lean/Elab/Open.lean b/src/Lean/Elab/Open.lean index 1008e4d72f..d0832888a1 100644 --- a/src/Lean/Elab/Open.lean +++ b/src/Lean/Elab/Open.lean @@ -33,7 +33,7 @@ instance : MonadResolveName (M (m := m)) where getCurrNamespace := return (← get).currNamespace getOpenDecls := return (← get).openDecls -def resolveId [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do +def resolveId [MonadOptions m] [MonadResolveName m] (ns : Name) (idStx : Syntax) : m Name := do let declName := ns ++ idStx.getId if (← getEnv).contains declName then return declName @@ -48,7 +48,7 @@ Uniquely resolves the identifier `idStx` in the provided namespaces `nss`. If the identifier does not indicate a name in exactly one of the namespaces, an exception is thrown. -/ -def resolveNameUsingNamespacesCore [MonadResolveName m] +def resolveNameUsingNamespacesCore [MonadOptions m] [MonadResolveName m] (nss : List Name) (idStx : Syntax) : m Name := do let mut exs := #[] let mut result := #[] @@ -69,7 +69,7 @@ def resolveNameUsingNamespacesCore [MonadResolveName m] else withRef idStx do throwError "ambiguous identifier `{idStx.getId}`, possible interpretations: {result.map mkConst}" -def elabOpenDecl [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.Command.openDecl) : m (List OpenDecl) := do +def elabOpenDecl [MonadOptions m] [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.Command.openDecl) : m (List OpenDecl) := do StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do match stx with | `(Parser.Command.openDecl| $nss*) => @@ -108,7 +108,7 @@ def elabOpenDecl [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser. | _ => throwUnsupportedSyntax return (← get).openDecls -def resolveNameUsingNamespaces [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name := do +def resolveNameUsingNamespaces [MonadOptions m] [MonadResolveName m] (nss : List Name) (idStx : Ident) : m Name := do StateRefT'.run' (s := { openDecls := (← getOpenDecls), currNamespace := (← getCurrNamespace) }) do resolveNameUsingNamespacesCore (m := M) nss idStx diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index 4627b15bfc..0428f7818a 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -1971,7 +1971,7 @@ where let env ← getEnv -- check for scope errors before trying auto implicits if env.isExporting then - if let [(npriv, _)] ← withEnv (env.setExporting false) <| resolveGlobalName n then + if let [(npriv, _)] ← withEnv (env.setExporting false) <| resolveGlobalName (enableLog := false) n then throwUnknownIdentifierAt (declHint := npriv) stx m!"Unknown identifier `{.ofConstName n}`" if (← read).autoBoundImplicit && !(← read).autoBoundImplicitForbidden n && diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 4b601faa49..a4bd3108b2 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -178,6 +178,7 @@ instance (m n) [MonadLift m n] [MonadQuotation n] [MonadMacroAdapter m] : MonadM def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadLiftT IO m] (x : MacroM α) : m α := do let env ← getEnv + let opts ← getOptions let currNamespace ← getCurrNamespace let openDecls ← getOpenDecls let methods := Macro.mkMethods { @@ -189,7 +190,7 @@ def liftMacroM [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [M hasDecl := fun declName => return env.contains declName getCurrNamespace := return currNamespace resolveNamespace := fun n => return ResolveName.resolveNamespace env currNamespace openDecls n - resolveGlobalName := fun n => return ResolveName.resolveGlobalName env currNamespace openDecls n + resolveGlobalName := fun n => return ResolveName.resolveGlobalName env opts currNamespace openDecls n } match x { methods := methods ref := ← getRef diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index a8b0dc8b0f..c18bfb549d 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -663,7 +663,7 @@ inductive ParserResolution where | alias (p : ParserAliasValue) /-- Resolve the given parser name and return a list of candidates. -/ -def resolveParserNameCore (env : Environment) (currNamespace : Name) +private def resolveParserNameCore (env : Environment) (opts : Options) (currNamespace : Name) (openDecls : List OpenDecl) (ident : Ident) : List ParserResolution := Id.run do let ⟨.ident (val := val) (preresolved := pre) ..⟩ := ident | return [] @@ -684,7 +684,7 @@ def resolveParserNameCore (env : Environment) (currNamespace : Name) if isParserCategory env erased then return [.category erased] - let resolved ← ResolveName.resolveGlobalName env currNamespace openDecls val |>.filterMap fun + let resolved ← ResolveName.resolveGlobalName env opts currNamespace openDecls val |>.filterMap fun | (name, []) => (isParser name).map fun isDescr => .parser name isDescr | _ => none unless resolved.isEmpty do @@ -698,11 +698,11 @@ def resolveParserNameCore (env : Environment) (currNamespace : Name) /-- Resolve the given parser name and return a list of candidates. -/ def ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserResolution := - Parser.resolveParserNameCore ctx.env ctx.currNamespace ctx.openDecls id + Parser.resolveParserNameCore ctx.env ctx.options ctx.currNamespace ctx.openDecls id /-- Resolve the given parser name and return a list of candidates. -/ def resolveParserName (id : Ident) : CoreM (List ParserResolution) := - return resolveParserNameCore (← getEnv) (← getCurrNamespace) (← getOpenDecls) id + return resolveParserNameCore (← getEnv) (← getOptions) (← getCurrNamespace) (← getOpenDecls) id def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do let stack := s.stxStack diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 476b80a46c..05a397e8e6 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -9,6 +9,7 @@ prelude public import Lean.Modifiers public import Lean.Exception public import Lean.Namespace +public import Lean.Log public section @@ -101,11 +102,24 @@ private def containsDeclOrReserved (env : Environment) (declName : Name) : Bool -- avoid blocking from `Environment.contains` if possible env.containsOnBranch declName || isReservedName env declName || env.contains declName -private partial def resolvePrivateName (env : Environment) (declName : Name) : Option Name := do +register_builtin_option backward.privateInPublic : Bool := { + defValue := false + descr := "(module system) Export `private` declarations, allowing for arbitrary access to \ + them while code is being ported to the module system. Such accesses will generate warnings + unless `backward.privateInPublic.warn` is disabled." +} + +register_builtin_option backward.privateInPublic.warn : Bool := { + defValue := true + descr := "(module system) Warn on accesses to `private` declarations that are allowed only by \ + `backward.privateInPublic` being enabled." +} + +private partial def resolvePrivateName (env : Environment) (opts : Options) (declName : Name) : Option Name := do -- No point in checking private names when exporting. This is an optimization but also necessary -- for correct visibility checking while we still carry some private names (e.g. kernel-generated -- from `inductive`) in the public env. - guard !env.isExporting + guard (!env.isExporting || backward.privateInPublic.get opts) if containsDeclOrReserved env (mkPrivateName env declName) then return mkPrivateName env declName -- Under the module system, we assume there are at most a few `import all`s and we can just test @@ -117,27 +131,27 @@ private partial def resolvePrivateName (env : Environment) (declName : Name) : O return n /-- Check whether `ns ++ id` is a valid namespace name and/or there are aliases names `ns ++ id`. -/ -private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name := Id.run do +private def resolveQualifiedName (env : Environment) (opts : Options) (ns : Name) (id : Name) : List Name := Id.run do let resolvedId := ns ++ id -- We ignore protected aliases if `id` is atomic. let resolvedIds := getAliases env resolvedId (skipProtected := id.isAtomic) if !id.isAtomic || !isProtected env resolvedId then if containsDeclOrReserved env resolvedId then return resolvedId :: resolvedIds - else if let some resolvedIdPrv := resolvePrivateName env resolvedId then + else if let some resolvedIdPrv := resolvePrivateName env opts resolvedId then return resolvedIdPrv :: resolvedIds return resolvedIds /-- Check surrounding namespaces -/ -private def resolveUsingNamespace (env : Environment) (id : Name) : Name → List Name +private def resolveUsingNamespace (env : Environment) (opts : Options) (id : Name) : Name → List Name | ns@(.str p _) => - match resolveQualifiedName env ns id with - | [] => resolveUsingNamespace env id p + match resolveQualifiedName env opts ns id with + | [] => resolveUsingNamespace env opts id p | resolvedIds => resolvedIds | _ => [] /-- Check exact name -/ -private def resolveExact (env : Environment) (id : Name) : Option Name := +private def resolveExact (env : Environment) (opts : Options) (id : Name) : Option Name := if id.isAtomic then none else let resolvedId := id.replacePrefix rootNamespace Name.anonymous @@ -145,17 +159,17 @@ private def resolveExact (env : Environment) (id : Name) : Option Name := else -- We also allow `_root_` when accessing private declarations. -- If we change our minds, we should just replace `resolvedId` with `id` - resolvePrivateName env resolvedId + resolvePrivateName env opts resolvedId /-- Check `OpenDecl`s -/ -private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → List Name → List Name +private def resolveOpenDecls (env : Environment) (opts : Options) (id : Name) : List OpenDecl → List Name → List Name | [], resolvedIds => resolvedIds | OpenDecl.simple ns exs :: openDecls, resolvedIds => if exs.contains id then - resolveOpenDecls env id openDecls resolvedIds + resolveOpenDecls env opts id openDecls resolvedIds else - let newResolvedIds := resolveQualifiedName env ns id - resolveOpenDecls env id openDecls (newResolvedIds ++ resolvedIds) + let newResolvedIds := resolveQualifiedName env opts ns id + resolveOpenDecls env opts id openDecls (newResolvedIds ++ resolvedIds) | OpenDecl.explicit openedId resolvedId :: openDecls, resolvedIds => let resolvedIds := if openedId == id then @@ -168,7 +182,7 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → resolvedIds else resolvedIds - resolveOpenDecls env id openDecls resolvedIds + resolveOpenDecls env opts id openDecls resolvedIds /-- Primitive global name resolution procedure. It does not trigger actions associated with reserved names. @@ -177,7 +191,7 @@ containing stating that `foo` is equal to its definition. The action associated automatically proves the theorem. At the macro level, the name is resolved, but the action is not executed. -/ -def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) := +def resolveGlobalName (env : Environment) (opts : Options) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) := -- decode macro scopes from name before recursion let extractionResult := extractMacroScopes id let rec loop (id : Name) (projs : List String) : List (Name × List String) := @@ -185,15 +199,15 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl | .str p s => -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections let id := { extractionResult with name := id }.review - match resolveUsingNamespace env id ns with + match resolveUsingNamespace env opts id ns with | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map fun id => (id, projs) | [] => - match resolveExact env id with + match resolveExact env opts id with | some newId => [(newId, projs)] | none => let resolvedIds := if containsDeclOrReserved env id then [id] else [] - let resolvedIds := if let some idPrv := resolvePrivateName env id then [idPrv] ++ resolvedIds else resolvedIds - let resolvedIds := resolveOpenDecls env id openDecls resolvedIds + let resolvedIds := if let some idPrv := resolvePrivateName env opts id then [idPrv] ++ resolvedIds else resolvedIds + let resolvedIds := resolveOpenDecls env opts id openDecls resolvedIds let resolvedIds := getAliases env id (skipProtected := id.isAtomic) ++ resolvedIds match resolvedIds with | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs) @@ -252,6 +266,15 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where getCurrNamespace := liftM (m:=m) getCurrNamespace getOpenDecls := liftM (m:=m) getOpenDecls +variable [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m] + [MonadError m] + +def checkPrivateInPublic (id : Name) : m Unit := do + if (← getEnv).isExporting && isPrivateName id && (← ResolveName.backward.privateInPublic.warn.getM) then + logWarning m!"Private declaration `{.ofConstName id}` accessed publicly; \ + this is allowed only because the `backward.privateInPublic` option is enabled. \n\n\ + Disable `backward.privateInPublic.warn` to silence this warning." + /-- Given a name `n`, return a list of possible interpretations. Each interpretation is a pair `(declName, fieldList)`, where `declName` @@ -274,22 +297,31 @@ After `open Foo open Boo`, we have - `resolveGlobalName x` => `[(Foo.x, []), (Boo.x, [])]` - `resolveGlobalName x.y` => `[(Foo.x.y, [])]` - `resolveGlobalName x.z.w` => `[(Foo.x, [z, w]), (Boo.x, [z, w])]` + +If `enableLog` is false, this function does not ever log warnings etc, which is useful if it may be +called incidentally or multiple times. -/ -def resolveGlobalName [Monad m] [MonadResolveName m] [MonadEnv m] (id : Name) : m (List (Name × List String)) := do - return ResolveName.resolveGlobalName (← getEnv) (← getCurrNamespace) (← getOpenDecls) id +def resolveGlobalName (id : Name) (enableLog := true) : m (List (Name × List String)) := do + let res := ResolveName.resolveGlobalName (← getEnv) (← getOptions) (← getCurrNamespace) (← getOpenDecls) id + -- `isExporting` is already checked in `checkPrivateInPublic` but should be cheaper than `isPrivateName` + if enableLog && (← getEnv).isExporting then + if let some prv := res.find? (isPrivateName ·.1) then + checkPrivateInPublic prv.1 + + return res /-- Given a namespace name, return a list of possible interpretations. Names extracted from syntax should be passed to `resolveNamespace` instead. -/ -def resolveNamespaceCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Name) (allowEmpty := false) : m (List Name) := do +def resolveNamespaceCore (id : Name) (allowEmpty := false) : m (List Name) := do let nss := ResolveName.resolveNamespace (← getEnv) (← getCurrNamespace) (← getOpenDecls) id if !allowEmpty && nss.isEmpty then throwError s!"unknown namespace `{id}`" return nss /-- Given a namespace identifier, return a list of possible interpretations. -/ -def resolveNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Ident → m (List Name) +def resolveNamespace : Ident → m (List Name) | stx@⟨Syntax.ident _ _ n pre⟩ => do let pre := pre.filterMap fun | .namespace ns => some ns @@ -301,13 +333,13 @@ def resolveNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] | stx => throwErrorAt stx s!"expected identifier" /-- Given a namespace identifier, return the unique interpretation or else fail. -/ -def resolveUniqueNamespace [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Ident) : m Name := do +def resolveUniqueNamespace (id : Ident) : m Name := do match (← resolveNamespace id) with | [ns] => return ns | nss => throwError s!"ambiguous namespace `{id.getId}`, possible interpretations: `{nss}`" /-- Helper function for `resolveGlobalConstCore`. -/ -def filterFieldList [Monad m] [MonadEnv m] [MonadError m] (n : Name) (cs : List (Name × List String)) : m (List Name) := do +def filterFieldList (n : Name) (cs : List (Name × List String)) : m (List Name) := do let cs := cs.filter fun (_, fieldList) => fieldList.isEmpty if cs.isEmpty then throwUnknownConstantAt (← getRef) n return cs.map (·.1) @@ -316,21 +348,21 @@ def filterFieldList [Monad m] [MonadEnv m] [MonadError m] (n : Name) (cs : List Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. For identifiers taken from syntax, use `resolveGlobalConst` instead, which respects preresolved names. -/ -private def resolveGlobalConstCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m (List Name) := do +private def resolveGlobalConstCore (n : Name) : m (List Name) := do let cs ← resolveGlobalName n filterFieldList n cs /-- Helper function for `resolveGlobalConstNoOverloadCore` -/ -def ensureNoOverload [Monad m] [MonadError m] (n : Name) (cs : List Name) : m Name := do +def ensureNoOverload (n : Name) (cs : List Name) : m Name := do match cs with | [c] => pure c | _ => throwError m!"Ambiguous identifier `{n}`; possible interpretations: {cs.map mkConst}" /-- For identifiers taken from syntax, use `resolveGlobalConstNoOverload` instead, which respects preresolved names. -/ -def resolveGlobalConstNoOverloadCore [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (n : Name) : m Name := do +def resolveGlobalConstNoOverloadCore (n : Name) : m Name := do ensureNoOverload n (← resolveGlobalConstCore n) -def preprocessSyntaxAndResolve [Monad m] [MonadError m] (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do +def preprocessSyntaxAndResolve (stx : Syntax) (k : Name → m (List Name)) : m (List Name) := do match stx with | .ident _ _ n pre => do let pre := pre.filterMap fun @@ -367,7 +399,7 @@ After `open Foo open Boo`, we have - `resolveGlobalConst x.y` => `[Foo.x.y]` - `resolveGlobalConst x.z.w` => error: unknown constant -/ -def resolveGlobalConst [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (List Name) := +def resolveGlobalConst (stx : Syntax) : m (List Name) := preprocessSyntaxAndResolve stx resolveGlobalConstCore /-- @@ -375,7 +407,7 @@ Given a list of names produced by `resolveGlobalConst`, throws an error if the l exactly one element. Recall that `resolveGlobalConst` does not return empty lists. -/ -def ensureNonAmbiguous [Monad m] [MonadError m] (id : Syntax) (cs : List Name) : m Name := do +def ensureNonAmbiguous (id : Syntax) (cs : List Name) : m Name := do match cs with | [] => unreachable! | [c] => pure c @@ -404,11 +436,11 @@ After `open Foo open Boo`, we have - `resolveGlobalConstNoOverload x.y` => `Foo.x.y` - `resolveGlobalConstNoOverload x.z.w` => error: unknown constant -/ -def resolveGlobalConstNoOverload [Monad m] [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m Name := do +def resolveGlobalConstNoOverload (id : Syntax) : m Name := do ensureNonAmbiguous id (← resolveGlobalConst id) /-- Resolves the name `n` in the local context. -/ -def resolveLocalName [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n : Name) : m (Option (Expr × List String)) := do +def resolveLocalName [MonadLCtx m] (n : Name) : m (Option (Expr × List String)) := do let lctx ← getLCtx let auxDeclToFullName := (← getLCtx).auxDeclToFullName let currNamespace ← getCurrNamespace @@ -564,7 +596,7 @@ def resolveLocalName [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] ( | .str pre s => let mut globalDeclFoundNext := globalDeclFound unless globalDeclFound do - let r ← resolveGlobalName givenNameView.review + let r ← resolveGlobalName (enableLog := false) givenNameView.review let r := r.filter fun (_, fieldList) => fieldList.isEmpty unless r.isEmpty do globalDeclFoundNext := true @@ -590,8 +622,7 @@ If `n₀` is an accessible name, then the result will be an accessible name. The name `n₀` may be private. -/ -def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] - (n₀ : Name) (fullNames := false) (allowHorizAliases := false) +def unresolveNameGlobal (n₀ : Name) (fullNames := false) (allowHorizAliases := false) (filter : Name → m Bool := fun _ => pure true) : m Name := do if n₀.hasMacroScopes then return n₀ -- `n₁` is the name without any private prefix, and `qn₁?` is a valid fully-qualified name. @@ -604,7 +635,7 @@ def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] else (n₀, some (rootNamespace ++ n₀)) if fullNames then - if let [(potentialMatch, _)] ← resolveGlobalName n₁ then + if let [(potentialMatch, _)] ← resolveGlobalName n₁ (enableLog := false) then if (← pure (potentialMatch == n₀) <&&> filter n₁) then return n₁ if let some qn₁ := qn₁? then @@ -637,7 +668,7 @@ where let mut candidate := Name.anonymous for cmpt in revComponents do candidate := Name.appendCore cmpt candidate - if let [(potentialMatch, _)] ← resolveGlobalName candidate then + if let [(potentialMatch, _)] ← resolveGlobalName (enableLog := false) candidate then if potentialMatch == n₀ then if (← filter candidate) then return some candidate @@ -645,7 +676,7 @@ where /-- Like `Lean.unresolveNameGlobal`, but also ensures that the unresolved name does not conflict with the names of any local declarations. -/ -def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] (n₀ : Name) (fullNames := false) : m Name := +def unresolveNameGlobalAvoidingLocals [MonadLCtx m] (n₀ : Name) (fullNames := false) : m Name := unresolveNameGlobal n₀ (fullNames := fullNames) (filter := fun n => Option.isNone <$> resolveLocalName n) end Lean diff --git a/tests/lean/run/privateInPublic.lean b/tests/lean/run/privateInPublic.lean new file mode 100644 index 0000000000..ece0743d4e --- /dev/null +++ b/tests/lean/run/privateInPublic.lean @@ -0,0 +1,25 @@ +module + +set_option backward.privateInPublic true + +private def fpriv := 1 + +/-- +warning: Private declaration `fpriv` accessed publicly; this is allowed only because the `backward.privateInPublic` option is enabled. ⏎ + +Disable `backward.privateInPublic.warn` to silence this warning. +-/ +#guard_msgs in +@[expose] public def fpub := fpriv + +public structure S + +private def S.fpriv (s : S) := s + +/-- +warning: Private declaration `S.fpriv` accessed publicly; this is allowed only because the `backward.privateInPublic` option is enabled. ⏎ + +Disable `backward.privateInPublic.warn` to silence this warning. +-/ +#guard_msgs in +@[expose] public def fpub2 (s : S) := s.fpriv