max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: refine resolveNamespace

Browse source 
see issue #1224
This commit is contained in:
Leonardo de Moura 2022-06-17 09:17:14 -07:00
parent f0e2696ec8
commit e985eb2b8a
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/ResolveName.lean
View file

@ -131,9 +131,9 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
/- Namespace resolution -/
def resolveNamespaceUsingScope (env : Environment) (n : Name) : Name → List Name
| Name.anonymous => if env.isNamespace n then [n] else []
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then (ns ++ n) :: resolveNamespaceUsingScope env n p else resolveNamespaceUsingScope env n p
def resolveNamespaceUsingScope? (env : Environment) (n : Name) : Name → Option Name
| Name.anonymous => if env.isNamespace n then some n else none
| ns@(Name.str p _ _) => if env.isNamespace (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScope? env n p
| _ => unreachable!
def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → List Name
@ -145,14 +145,17 @@ def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDec
Given a name `id` try to find namespaces it may refer to. The resolution procedure works as follows
1- If `id` is in the scope of `namespace` commands the namespace `s_1. ... . s_n`,
then include `s_1 . ... . s_i ++ n` if it is the name of an existing namespace.
then we include `s_1 . ... . s_i ++ n` in the result if it is the name of an existing namespace.
We search "backwards", and include at most one of the in the list of resulting namespaces.
2- If `id` is the extact name of an existing namespace, then include `id`
3- Finally, for each command `open N`, include in the result `N ++ n` if it is the name of an existing namespace.
We only consider simple `open` commands. -/
def resolveNamespace (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List Name :=
resolveNamespaceUsingScope env id ns ++ resolveNamespaceUsingOpenDecls env id openDecls
match resolveNamespaceUsingScope? env id ns with
| some ns => ns :: resolveNamespaceUsingOpenDecls env id openDecls
| none => resolveNamespaceUsingOpenDecls env id openDecls
end ResolveName