From 586f515470bf61de1db9be52d086028aeabf11be Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 11 Jan 2020 14:43:44 -0500 Subject: [PATCH] fix: global name resolution of macro-introduced idents --- src/Init/Lean/Elab/ResolveName.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Elab/ResolveName.lean b/src/Init/Lean/Elab/ResolveName.lean index bfea04e413..85d44b64c2 100644 --- a/src/Init/Lean/Elab/ResolveName.lean +++ b/src/Init/Lean/Elab/ResolveName.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude +import Init.Lean.Hygiene import Init.Lean.Modifiers import Init.Lean.Elab.Alias @@ -65,8 +66,10 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl → let resolvedIds := if id == openedId then resolvedId :: resolvedIds else resolvedIds; resolveOpenDecls openDecls resolvedIds -private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : List OpenDecl) : Name → List String → List (Name × List String) +private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : List OpenDecl) (scps : List MacroScope) : Name → List String → List (Name × List String) | id@(Name.str p s _), projs => + -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections + let id := addMacroScopes id scps; match resolveUsingNamespace env id ns with | resolvedIds@(_ :: _) => resolvedIds.eraseDups.map $ fun id => (id, projs) | [] => @@ -82,7 +85,9 @@ private def resolveGlobalNameAux (env : Environment) (ns : Name) (openDecls : Li | _, _ => [] def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) := -resolveGlobalNameAux env ns openDecls id [] +-- decode macro scopes from name before recursion +let (id, scps) := extractMacroScopes id; +resolveGlobalNameAux env ns openDecls scps id [] /- Namespace resolution -/