From 6d51067e0cc2d07bbcc30b6ae30d4c047b4bc50a Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 10 Dec 2024 17:51:42 -0800 Subject: [PATCH] feat: improved `export` command and namespace aliases This PR gives the `export` command the ability to create aliases to namespaces, in addition to its current ability to create aliases to individual declarations. It adds a number of `open`-like variations to the syntax. * `export NS1 ... NSn` makes the current namespace be an alias for the provided namespaces. * `export NS (def1 ... defn)` has the same meaning as before, but if any `NS.defi` is a namespace then the alias also serves as a namespace alias. For example, if one were to do ```lean namespace MyNS export _root_ (Nat) end MyNS ``` then not only is `MyNS.Nat` available as an alias for `Nat`, but additionally `MyNS.Nat.succ` is now an alias for `Nat.succ`. * `export NS hiding def1 ... defn` is like `export NS`, but the given names in `NS` do not get aliases. * `export NS renaming def1 -> def1', ..., defn -> defn'` creates aliases for the given names `def1` through `defn`, but the aliases respectively use the names `def1'` through `defn'`. --- src/Lean/Data/ExportDecl.lean | 32 +++ src/Lean/Elab/BuiltinCommand.lean | 57 +++- src/Lean/Parser/Command.lean | 42 ++- src/Lean/ResolveName.lean | 250 +++++++++++++++--- .../Completion/CompletionCollectors.lean | 59 +++-- stage0/src/stdlib_flags.h | 2 +- tests/lean/run/3031.lean | 2 +- tests/lean/run/export.lean | 125 +++++++++ 8 files changed, 489 insertions(+), 80 deletions(-) create mode 100644 src/Lean/Data/ExportDecl.lean create mode 100644 tests/lean/run/export.lean diff --git a/src/Lean/Data/ExportDecl.lean b/src/Lean/Data/ExportDecl.lean new file mode 100644 index 000000000000..ba69cc7f15eb --- /dev/null +++ b/src/Lean/Data/ExportDecl.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kyle Miller +-/ +prelude +import Init.Meta + +namespace Lean + +/-- +Data for representing `export` commands. +-/ +inductive ExportDecl where + /-- The name `aDeclName` is an alias for the declaration `declName`. -/ + | explicit (aDeclName : Name) (declName : Name) + /-- The namespace `ans` is an alias for the namespace `ns`, + except, if `e` is in `except`, `ans ++ e` is not an alias for `ns ++ e`. + Alias resolution is recursive. `ns` must be a registered namespace. -/ + | namespace (ans ns : Name) (except : List Name) + deriving BEq + +namespace ExportDecl + +instance : ToString ExportDecl := ⟨fun decl => + match decl with + | .explicit adecl decl => toString adecl ++ " → " ++ toString decl + | .namespace ans ns ex => toString ans ++ ".* → " ++ toString ns ++ ".*" ++ (if ex == [] then "" else " hiding " ++ toString ex)⟩ + +end ExportDecl + +end Lean diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index 1175b39ce651..a42dea1404e8 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -128,19 +128,52 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM | Except.ok env => setEnv env | Except.error ex => throwError (ex.toMessageData (← getOptions)) -@[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do - let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax - let nss ← resolveNamespace ns +def elabExportDecl (stx : TSyntax ``Parser.Command.exportDecl) : CommandElabM Unit := do let currNamespace ← getCurrNamespace - if nss == [currNamespace] then throwError "invalid 'export', self export" - let mut aliases := #[] - for idStx in ids do - let id := idStx.getId - let declName ← resolveNameUsingNamespaces nss idStx - if (← getInfoState).enabled then - addConstInfo idStx declName - aliases := aliases.push (currNamespace ++ id, declName) - modify fun s => { s with env := aliases.foldl (init := s.env) fun env p => addAlias env p.1 p.2 } + match stx with + | `(Parser.Command.exportDecl| $nss*) => + for ns in nss do + let ns ← resolveUniqueNamespace ns + modifyEnv fun env => addNamespaceAlias env currNamespace ns [] + | `(Parser.Command.exportDecl| $ns ($ids*)) => + let nss ← resolveNamespace ns + let mut aliases := #[] + for idStx in ids do + let declName ← resolveNameUsingNamespaces nss idStx + if (← getInfoState).enabled then + addConstInfo idStx declName + let aDeclName := currNamespace ++ idStx.getId + if aDeclName == declName then + throwErrorAt idStx "invalid 'export', self export" + aliases := aliases.push (aDeclName, declName) + addAliases aliases + | `(Parser.Command.exportDecl| $ns hiding $ids*) => + let ns ← resolveUniqueNamespace ns + for id in ids do + let declName ← resolveNameUsingNamespaces [ns] id + if (← getInfoState).enabled then + addConstInfo id declName + let except := ids.map (·.getId) |>.toList + modifyEnv fun env => addNamespaceAlias env currNamespace ns except + | `(Parser.Command.exportDecl| $ns renaming $[$froms -> $tos],*) => + let ns ← resolveUniqueNamespace ns + let mut aliases := #[] + for «from» in froms, to in tos do + let declName ← resolveNameUsingNamespaces [ns] «from» + if (← getInfoState).enabled then + addConstInfo «from» declName + addConstInfo to declName + let aDeclName := currNamespace ++ to.getId + aliases := aliases.push (aDeclName, declName) + addAliases aliases + | _ => throwUnsupportedSyntax +where + addAliases (aliases : Array (Name × Name)) : CommandElabM Unit := + modifyEnv fun env => aliases.foldl (init := env) fun env p => addAlias env p.1 p.2 + +@[builtin_command_elab «export»] def elabExport : CommandElab := fun stx => do + let decl : TSyntax ``Parser.Command.exportDecl := ⟨stx[1]⟩ + elabExportDecl decl @[builtin_command_elab «open»] def elabOpen : CommandElab | `(open $decl:openDecl) => do diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 73a94a5b0fae..9a23f33d31ff 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -539,12 +539,44 @@ def eraseAttr := leading_parser "attribute " >> "[" >> withoutPosition (sepBy1 (eraseAttr <|> Term.attrInstance) ", ") >> "]" >> many1 (ppSpace >> ident) -/-- Adds names from other namespaces to the current namespace. +def exportHiding := leading_parser + ppSpace >> atomic (ident >> " hiding") >> many1 (ppSpace >> checkColGt >> ident) +def exportRenamingItem := leading_parser + ident >> unicodeSymbol " → " " -> " >> checkColGt >> ident +def exportRenaming := leading_parser + ppSpace >> atomic (ident >> " renaming ") >> sepBy1 exportRenamingItem ", " +def exportOnly := leading_parser + ppSpace >> atomic (ident >> " (") >> many1 ident >> ")" +def exportNamespace := leading_parser + many1 (ppSpace >> checkColGt >> ident) +/-- `exportDecl` is the body of an `export` declaration (see `export`) -/ +@[builtin_doc] def exportDecl := + withAntiquot (mkAntiquot "exportDecl" `Lean.Parser.Command.exportDecl (isPseudoKind := true)) <| + exportHiding <|> exportRenaming <|> exportOnly <|> exportNamespace +/-- +Adds aliases into the current namespaces for names from other namespaces. + +There are two kinds of aliases: +* Name aliases make a name `aDecl` refer to another name `dDecl`. +* Namespace aliases make all names in a namespace `ans` refer to names in another namespace `ns`. + +The `export` command be used in a few different ways: + +* `export NS₁ … NSₙ` makes the current namespace be an alias for the namespaces `NS₁`, …, `NSₙ`. + If the current namespace is `A` and `NSᵢ.x` exists, then this causes `A.x` to be an alias for `NSᵢ.x`. + +* `export NS hiding def₁ … defₙ` makes the current namespace be an alias for the namespace `NS` + like in `export NS`, but none of the `NS.defᵢ` names are aliased. + +* `export NS (def₁ … defₙ)` creates aliases for the names `NS.def₁`, …, `NS.defₙ` in the current namespace. + If the current namespace is `A`, then `A.defᵢ` refers to whatever `NS.defᵢ` resolves to. -The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`: +* `export NS renaming def₁ → def₁', …, defₙ → defₙ'` is like `export NS (def₁ … defₙ)` but it enables + naming the aliases; `A.defᵢ'` refers to whatever `NS.defᵢ` resolves to. -- visible in the current namespace without prefix `Some.Namespace`, like `open`, and -- visible from outside the current namespace `N` as `N.name₁` and `N.name₂`. +Aliases make names visible in the current namespace without a prefix (like `open`). +The only rule for `protected` declarations is that when resolving an atomic identifier, +only non-`protected` declarations are considered. ## Examples @@ -564,7 +596,7 @@ end Evening.Sky ``` -/ @[builtin_command_parser] def «export» := leading_parser - "export " >> ident >> " (" >> many1 ident >> ")" + withPosition ("export " >> exportDecl) @[builtin_command_parser] def «import» := leading_parser "import" -- not a real command, only for error messages def openHiding := leading_parser diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index a5167193d9fa..bc96b2eea08a 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -5,13 +5,18 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude import Lean.Data.OpenDecl +import Lean.Data.ExportDecl import Lean.Hygiene import Lean.Modifiers import Lean.Exception +/-! +# Name resolution +-/ + namespace Lean /-! -Reserved names. +### Reserved names. We use reserved names for automatically generated theorems (e.g., equational theorems). Automation may register new reserved name predicates. @@ -48,49 +53,225 @@ def isReservedName (env : Environment) (name : Name) : Bool := reservedNamePredicatesExt.getState env |>.any (· env name) /-! - We use aliases to implement the `export (+)` command. - An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`. +### Aliases + +The `export` command creates *aliases*, which are like "symbolic links" in the name hierarchy. +An `export A (x)` from within the namespace `B` produces an alias `B.x ~> y`, where `y` is what the name `A.x` resolves to. +An `export A` from within the namespace `B` produces a family of aliases `B.* ~> A.*`. +Alias resolution is recursive. + +Abstract description: "`m` is an alias for `n`" is a relation on names. +1. If `n₁` is an alias for `n₂` and `n₂` is an alias for `n₃` then `n₁` is an alias for `n₃`. +2. Given `ExportDecl.explicit aDecl dDecl`, then `aDecl` is an alias for `dDecl`. + Futhermore, if `dDecl` is a namepace then the rule for `ExportDecl.namespace aDecl dDecl []` also applies. +3. Given `ExportDecl.namespace ans ns except`, then for all names `m` not in `except`, + if `m = Name.str m' id`, `ns ++ m'` is a namespace, and `ans ++ m` is not a private name, + then `ans ++ m` is an alias for `ns ++ m`. + +For a name `m`, we say "alias `m` resolves to `n`" if `m` maps to `n` and `n` is a declaration or a reserved name. +**The result of `resolveAlias m`** is a list containing every `n` such that alias `m` resolves to `n`. +The condition that `ExportDecl.namespace` only resolves names whose prefix is a namespace ensures that we can implement +this with a (terminating!) efficient algorithm, since this ensures the problem is equivalent to a graph search on a finite graph. + +The difference between the behavior of `ExportDecl.explict ans ns` and `ExportDecl.namespace ans ns []` is that the +first one additionally makes `ans` an alias for `ns` if `ns` is a declaration. The second does not — it only causes names +appearing inside `ns` to be aliased inside `ans`. -/ -abbrev AliasState := SMap Name (List Name) -abbrev AliasEntry := Name × Name +/-- +Data for exporting a namespace into another namespace. Represents a single `ExportDecl.namespace` entry. +The `fwd` parameter represents whether this is for the forward map or the reverse map in `AliasState`. +-/ +structure NamespaceAlias (fwd : Bool) where + /-- If `fwd`, then the namespace that's been exported. Otherwise, the destination namespace for the export. -/ + ns : Name + /-- The names that are not exported. For each `e` in `except`, `ns ++ e` is not exported. -/ + except : List Name + deriving BEq, Inhabited -def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState := - match s.find? e.1 with - | none => s.insert e.1 [e.2] - | some es => if es.contains e.2 then s else s.insert e.1 (e.2 :: es) +/-- +The main state for aliases. `AliasStateMaps true` is the forward direction, and `AliasStateMaps false` is the reverse direction. +Each determines the other, but in `AliasState` we have both for efficient lookups. +-/ +structure AliasStateMaps (fwd : Bool) where + /-- Map from aliases to the declarations they could refer to. + An `ExportDecl.explicit a b` entry is represented as `b ∈ aliases[a]` (if forward mode) or `a ∈ aliases[b]` (if backward mode). -/ + aliases : SMap Name (List Name) := {} + /-- Map from namespaces to the namespaces exported to it. + An `ExportDecl.namespace a b except` entry is represented as `{ns := b, except} ∈ namespaceAliases[a]` (if forward mode) + or `{ns := a, except} ∈ namespaceAliases[b]` (if backward mode). -/ + namespaceAliases : SMap Name (List (NamespaceAlias fwd)) := {} + deriving Inhabited + +def AliasStateMaps.addExplicit (s : AliasStateMaps fwd) (aDeclName declName : Name) : AliasStateMaps fwd := + let (key, value) := if fwd then (aDeclName, declName) else (declName, aDeclName) + let { aliases, namespaceAliases } := s + let aliases := + if let some decls := aliases.find? key then + if decls.contains declName then aliases else aliases.insert key (value :: decls) + else + aliases.insert key [value] + { aliases, namespaceAliases } + +def AliasStateMaps.addNamespace (s : AliasStateMaps fwd) (ans ns : Name) (except : List Name) : AliasStateMaps fwd := + let (key, value) := if fwd then (ans, ns) else (ns, ans) + let { aliases, namespaceAliases } := s + let nsAlias : NamespaceAlias fwd := { ns := value, except } + let namespaceAliases := + if let some decls := namespaceAliases.find? key then + if decls.contains nsAlias then namespaceAliases else namespaceAliases.insert key (nsAlias :: decls) + else + namespaceAliases.insert key [nsAlias] + { aliases, namespaceAliases } + +def AliasStateMaps.switch : AliasStateMaps fwd → AliasStateMaps fwd + | { aliases, namespaceAliases } => { aliases := aliases.switch, namespaceAliases := namespaceAliases.switch } -builtin_initialize aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState ← +/-- +Applies `f` to all relevant alias entries for the name `a`. +In `fwd` mode, this means finding all `.explicit a' _` entries with `a'` a prefix of `a` (or equal to `a`) +and all `.namespace ns _ _` entries with `ns` a prefix of `a`. +Otherwise, in reverse mode, this means doing it with `.explicit _ a'` and `.namespace _ ns _` instead. +Does not do any processing of `.namespace` exceptions, and does not do any checking of the namespace rules. +-/ +def AliasStateMaps.forMatchingM [Monad m] (s : AliasStateMaps fwd) (a : Name) (f : ExportDecl → m Unit) : m Unit := do + if let some decls := s.aliases.find? a then + decls.forM (fun val => f (mkExplicit a val)) + if let .str ns _ := a then + visitNS ns +where + mkExplicit (key val : Name) : ExportDecl := + if fwd then .explicit key val else .explicit val key + mkNamespace (key val : Name) (except : List Name) : ExportDecl := + if fwd then .namespace key val except else .namespace val key except + visitNS (ns : Name) : m Unit := do + match ns with + | .str ns' _ | .num ns' _ => visitNS ns' + | .anonymous => pure () + if let some decls := s.aliases.find? ns then + decls.forM fun val => f (mkExplicit ns val) + if let some decls := s.namespaceAliases.find? ns then + decls.forM fun decl => f (mkNamespace ns decl.ns decl.except) + +structure AliasState where + /-- Alias maps, forward direction. Maps aliases to what they are aliases to. For resolving aliases. -/ + fwd : AliasStateMaps true := {} + /-- Alias maps, reverse direction. Maps names to their aliases. For 'unresolving'. -/ + rev : AliasStateMaps false := {} + deriving Inhabited + +def AliasState.switch : AliasState → AliasState + | { fwd, rev } => { fwd := fwd.switch, rev := rev.switch } + +private def addExportDecl (s : AliasState) (e : ExportDecl) : AliasState := + let { fwd, rev } := s + match e with + | .explicit aDecl dDecl => + { fwd := fwd.addExplicit aDecl dDecl + rev := rev.addExplicit aDecl dDecl } + | .namespace ans ns except => + { fwd := fwd.addNamespace ans ns except + rev := rev.addNamespace ans ns except } + +builtin_initialize aliasExtension : SimplePersistentEnvExtension ExportDecl AliasState ← registerSimplePersistentEnvExtension { - addEntryFn := addAliasEntry, - addImportedFn := fun es => mkStateFromImportedEntries addAliasEntry {} es |>.switch + addEntryFn := addExportDecl, + addImportedFn := fun es => mkStateFromImportedEntries addExportDecl {} es |>.switch } -/-- Add alias `a` for `e` -/ -@[export lean_add_alias] def addAlias (env : Environment) (a : Name) (e : Name) : Environment := - aliasExtension.addEntry env (a, e) +/-- +Adds an alias `aDeclName` that refers to `declName`. (Creates an `ExportDecl.explicit` entry). +-/ +@[export lean_add_alias] def addAlias (env : Environment) (aDeclName : Name) (declName : Name) : Environment := + aliasExtension.addEntry env (.explicit aDeclName declName) + +/-- +Makes `ans.f` resolve to `ns.f` if `ns.f` exists as either a declaration or an alias +and `f` is not in the `except` list. (Creates an `ExportDecl.namespace` entry). +-/ +def addNamespaceAlias (env : Environment) (ans : Name) (ns : Name) (except : List Name) : Environment := + aliasExtension.addEntry env (.namespace ans ns except) def getAliasState (env : Environment) : AliasState := aliasExtension.getState env /-- - Retrieve aliases for `a`. If `skipProtected` is `true`, then the resulting list only includes - declarations that are not marked as `protected`. +Implementation of procedure to resolve the alias `a`. +The `List Name` state for aliases visited is used to prevent infinite loops, +which can be caused by `.namespace` exports re-exporting aliases. -/ -def getAliases (env : Environment) (a : Name) (skipProtected : Bool) : List Name := - match aliasExtension.getState env |>.find? a with - | none => [] - | some es => - if skipProtected then - es.filter (!isProtected env ·) - else - es +private partial def resolveAliasAux (env : Environment) (a : Name) (skipProtected : Bool) : + StateM (List Name × List Name) Unit := do + unless (← get).1.contains a do + modify fun (aliases, declNames) => (a :: aliases, declNames) + let visitDecl (dDecl : Name) : StateM (List Name × List Name) Unit := do + if (env.contains dDecl && (!skipProtected || !isProtected env dDecl)) + || (isReservedName env dDecl && !skipProtected) then + modify fun (aliases, declNames) => (aliases, dDecl :: declNames) + resolveAliasAux env dDecl skipProtected + let visitIfNamespace (decl : Name) : StateM (List Name × List Name) Unit := do + if decl.isStr && env.isNamespace decl.getPrefix then + visitDecl decl + let isPriv := isPrivateName a + getAliasState env |>.fwd.forMatchingM a fun edecl => do + match edecl with + | .explicit aDecl dDecl => + if aDecl == a then + visitDecl dDecl + else if !isPriv then + visitIfNamespace (a.replacePrefix aDecl dDecl) + | .namespace ans ns except => + if !isPriv then + let m := a.replacePrefix ans .anonymous + unless except.contains m do + visitIfNamespace (Name.appendCore ns m) --- slower, but only used in the pretty printer -def getRevAliases (env : Environment) (e : Name) : List Name := - (aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) [] +/-- +Retrieve declarations that `a` is an alias for. +If `skipProtected` is `true`, then the resulting list only includes declarations that are not marked as `protected`. +-/ +def resolveAlias (env : Environment) (a : Name) (skipProtected : Bool) : List Name := + resolveAliasAux env a skipProtected |>.run ([], []) |>.2.2 + +/-- +Implementation of procedure to find all aliases of the declaration `d`. +The `List Name` state for declarations is to prevent infinite loops. +-/ +private partial def unresolveAliasesAux (env : Environment) (d : Name) (skipAtomic : Bool) (allowHorizAliases : Bool) : + StateM (List Name × List Name) Unit := + unless (← get).2.contains d do + modify fun (aliases, declNames) => (aliases, d :: declNames) + let visitDecl (aDecl : Name) : StateM (List Name × List Name) Unit := do + if (!skipAtomic || !aDecl.isAtomic) && (allowHorizAliases || aDecl.getPrefix.isPrefixOf d) then + modify fun (aliases, declNames) => (aDecl :: aliases, declNames) + unresolveAliasesAux env aDecl skipAtomic allowHorizAliases + let visitNamespace (aDecl : Name) : StateM (List Name × List Name) Unit := do + if d.isStr && env.isNamespace d.getPrefix && !isPrivateName aDecl then + visitDecl aDecl + getAliasState env |>.rev.forMatchingM d fun edecl => do + match edecl with + | .explicit aDecl dDecl => + if dDecl == d then + visitDecl aDecl + else + visitNamespace (d.replacePrefix dDecl aDecl) + | .namespace ans ns except => + let m := d.replacePrefix ns .anonymous + unless except.contains m do + visitNamespace (Name.appendCore ans m) + +/-- +Retrieve all aliases of the declaration `declName`. + +If `skipAtomic` is true, then aliases that are atomic names are not returned. +This option is parallel to `Lean.getAliases`'s `skipProtected`, which is used in `Lean.ResolveName.resolveQualifiedName`. + +For `allowHorizAliases`, see the docstring for `Lean.unresolveNameGlobal`. +-/ +def unresolveAliases (env : Environment) (declName : Name) (skipAtomic := false) (allowHorizAliases := true) : List Name := + unresolveAliasesAux env declName (skipAtomic := skipAtomic) (allowHorizAliases := allowHorizAliases) |>.run ([], []) |>.2.1 -/-! # Global name resolution -/ +/-! ### Global name resolution -/ namespace ResolveName private def containsDeclOrReserved (env : Environment) (declName : Name) : Bool := @@ -100,7 +281,7 @@ private def containsDeclOrReserved (env : Environment) (declName : Name) : Bool private def resolveQualifiedName (env : Environment) (ns : Name) (id : Name) : List Name := let resolvedId := ns ++ id -- We ignore protected aliases if `id` is atomic. - let resolvedIds := getAliases env resolvedId (skipProtected := id.isAtomic) + let resolvedIds := resolveAlias env resolvedId (skipProtected := id.isAtomic) if (containsDeclOrReserved env resolvedId && (!id.isAtomic || !isProtected env resolvedId)) then resolvedId :: resolvedIds else @@ -178,14 +359,14 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl let idPrv := mkPrivateName env id let resolvedIds := if containsDeclOrReserved env idPrv then [idPrv] ++ resolvedIds else resolvedIds let resolvedIds := resolveOpenDecls env id openDecls resolvedIds - let resolvedIds := getAliases env id (skipProtected := id.isAtomic) ++ resolvedIds + let resolvedIds := resolveAlias env id (skipProtected := id.isAtomic) ++ resolvedIds match resolvedIds with | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs) | [] => loop p (s::projs) | _ => [] loop extractionResult.name [] -/-! # Namespace resolution -/ +/-! ### Namespace resolution -/ def resolveNamespaceUsingScope? (env : Environment) (n : Name) (ns : Name) : Option Name := match ns with @@ -411,7 +592,10 @@ def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name match (← resolveGlobalName n₀) with | [(potentialMatch, _)] => if (privateToUserName? potentialMatch).getD potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀ | _ => return n₀ -- if can't resolve, return the original - let mut initialNames := (getRevAliases (← getEnv) n₀).toArray + let env ← getEnv + -- In `Lean.ResolveName.resolveQualifiedName`, if a name is atomic it's not allowed to refer to a protected declaration, + -- so here we conversely omit atomic aliases if the declaration is protected. + let mut initialNames := (unresolveAliases env n₀ (allowHorizAliases := allowHorizAliases) (skipAtomic := isProtected env n₀)).toArray unless allowHorizAliases do initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₀.getPrefix initialNames := initialNames.push (rootNamespace ++ n₀) diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 8fb4cffc03ef..6ca385be06ae 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -369,6 +369,7 @@ private def idCompletionCore addUnresolvedCompletionItem localDecl.userName (.fvar localDecl.fvarId) (kind := CompletionItemKind.variable) score -- search for matches in the environment let env ← getEnv + let eligibleHeaderDecls ← getEligibleHeaderDecls env forEligibleDeclsM fun declName c => do let bestMatch? ← (·.2) <$> StateT.run (s := none) do let matchUsingNamespace (ns : Name) : StateT (Option (Name × Float)) M Unit := do @@ -400,19 +401,35 @@ private def idCompletionCore matchUsingNamespace Name.anonymous if let some (bestLabel, bestScore) := bestMatch? then addUnresolvedCompletionItem bestLabel (.const declName) (← getCompletionKindForDecl c) bestScore - let matchAlias (ns : Name) (alias : Name) : Option Float := - -- Recall that aliases may not be atomic and include the namespace where they were created. - if ns.isPrefixOf alias then - let alias := alias.replacePrefix ns Name.anonymous - matchAtomic id alias danglingDot - else - none - let eligibleHeaderDecls ← getEligibleHeaderDecls env - -- Auxiliary function for `alias` - let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do - declNames.forM fun declName => do - if allowCompletion eligibleHeaderDecls env declName then - addUnresolvedCompletionItemForDecl (.mkSimple alias.getString!) declName score + -- Aliases for declName. Name resolution only allows atomic aliases if the declaration isn't protected. + unresolveAliases env declName (skipAtomic := isProtected env declName) |>.forM fun alias => do + let matchAlias (ns : Name) (alias : Name) : Option Float := + -- Recall that aliases might not be atomic, and they can include the namespace where they were created. + if ns.isPrefixOf alias then + let alias := alias.replacePrefix ns Name.anonymous + matchAtomic id alias danglingDot + else + none + -- Auxiliary function for `alias` + let addAlias (alias : Name) (declName : Name) (score : Float) : M Unit := do + if allowCompletion eligibleHeaderDecls env declName then + addUnresolvedCompletionItemForDecl (.mkSimple alias.getString!) declName score + -- Use current namespace + let rec searchAlias (ns : Name) : M Unit := do + if let some score := matchAlias ns alias then + addAlias alias declName score + else + match ns with + | Name.str p .. => searchAlias p + | _ => return () + searchAlias ctx.currNamespace + -- Use open namespaces for aliases + for openDecl in ctx.openDecls do + match openDecl with + | OpenDecl.explicit .. => pure () + | OpenDecl.simple ns _ => + if let some score := matchAlias ns alias then + addAlias alias declName score -- search explicitly open `ids` for openDecl in ctx.openDecls do match openDecl with @@ -420,21 +437,7 @@ private def idCompletionCore if allowCompletion eligibleHeaderDecls env resolvedId then if let some score := matchAtomic id openedId danglingDot then addUnresolvedCompletionItemForDecl (.mkSimple openedId.getString!) resolvedId score - | OpenDecl.simple ns _ => - getAliasState env |>.forM fun alias declNames => do - if let some score := matchAlias ns alias then - addAlias alias declNames score - -- search for aliases - getAliasState env |>.forM fun alias declNames => do - -- use current namespace - let rec searchAlias (ns : Name) : M Unit := do - if let some score := matchAlias ns alias then - addAlias alias declNames score - else - match ns with - | Name.str p .. => searchAlias p - | _ => return () - searchAlias ctx.currNamespace + | OpenDecl.simple .. => pure () -- Used by aliases (see above) -- Search keywords if !danglingDot then if let .str .anonymous s := id then diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index b647d85f376c..a3d118fd9f11 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -9,7 +9,7 @@ options get_default_options() { opts = opts.update({"debug", "proofAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/lean/run/3031.lean b/tests/lean/run/3031.lean index d9956916e528..f3001213c856 100644 --- a/tests/lean/run/3031.lean +++ b/tests/lean/run/3031.lean @@ -43,7 +43,7 @@ def Common'.String.c (s : String) : Nat := 0 export Common (String.c) export Common' (String.c) /-- -error: invalid field notation 'c', the name 'String.c' is ambiguous, possible interpretations: 'Common'.String.c', 'Common.String.c' +error: invalid field notation 'c', the name 'String.c' is ambiguous, possible interpretations: 'Common.String.c', 'Common'.String.c' -/ #guard_msgs in #eval "".c diff --git a/tests/lean/run/export.lean b/tests/lean/run/export.lean new file mode 100644 index 000000000000..326869441a3d --- /dev/null +++ b/tests/lean/run/export.lean @@ -0,0 +1,125 @@ +/-! +# Tests for the `export` command +-/ + +/-! +Explicit export +-/ +def A.x : Bool := true +namespace B +export A (x) + +/-- info: A.x : Bool -/ +#guard_msgs in #check x +/-- info: x : Bool -/ +#guard_msgs in #check (x) +end B + +/-- info: A.x : Bool -/ +#guard_msgs in #check B.x +/-- info: A.x : Bool -/ +#guard_msgs in #check (B.x) + + +/-! +Namespace export +-/ +namespace C +export A + +/-- info: A.x : Bool -/ +#guard_msgs in #check x +/-- info: x : Bool -/ +#guard_msgs in #check (x) +end C + +/-- info: A.x : Bool -/ +#guard_msgs in #check C.x +/-- info: A.x : Bool -/ +#guard_msgs in #check (C.x) + + +/-! +Renaming +-/ +namespace D +export A renaming x → y + +/-- info: A.x : Bool -/ +#guard_msgs in #check y +/-- info: A.x : Bool -/ +#guard_msgs in #check (y) +end D + +/-- info: A.x : Bool -/ +#guard_msgs in #check D.y +/-- info: A.x : Bool -/ +#guard_msgs in #check (D.y) + + +/-! +Hiding +-/ +def A.n : Nat := 0 +namespace E +export A hiding x + +/-- error: unknown identifier 'x' -/ +#guard_msgs in #check x +/-- info: A.n : Nat -/ +#guard_msgs in #check n +end E + +/-- error: unknown identifier 'E.x' -/ +#guard_msgs in #check E.x +/-- info: A.n : Nat -/ +#guard_msgs in #check E.n + + +/-! +Protected export, atomic names don't resolve, but they still are accessible with `F.p` for example. +-/ +protected def A.p : Bool := true +namespace F +export A (p) +/-- error: unknown identifier 'p' -/ +#guard_msgs in #check p +/-- info: A.p : Bool -/ +#guard_msgs in #check F.p +end F +/-- info: A.p : Bool -/ +#guard_msgs in #check F.p + +/-! +Exporting an inductive type +-/ + +inductive Foo where + | cons + +export Foo + +/-- info: Foo.cons : Foo -/ +#guard_msgs in #check cons +/-- error: unknown identifier 'recOn' -/ +#guard_msgs in #check recOn + +namespace G +export Foo +end G +/-- info: Foo.recOn.{u} {motive : Foo → Sort u} (t : Foo) (cons : motive cons) : motive t -/ +#guard_msgs in #check G.recOn + + +/-! +Exporting a name, it also exports it as a namespace. +-/ + +inductive A.Ty where + | mk + +namespace H +export A (Ty) +end H +/-- info: A.Ty.mk : A.Ty -/ +#guard_msgs in #check H.Ty.mk