From 69dde320078323bec9f8aed2a1cccf557128f33e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Jan 2020 15:51:54 -0800 Subject: [PATCH] feat: extract macro scopes at `getUnusedName` --- src/Init/Lean/LocalContext.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/LocalContext.lean b/src/Init/Lean/LocalContext.lean index e27bb39d65..46a51a4d57 100644 --- a/src/Init/Lean/LocalContext.lean +++ b/src/Init/Lean/LocalContext.lean @@ -7,6 +7,7 @@ prelude import Init.Data.PersistentArray.Basic import Init.Data.PersistentHashMap.Basic import Init.Lean.Expr +import Init.Lean.Hygiene namespace Lean @@ -149,7 +150,7 @@ lctx.decls.findRev? (fun decl => def usesUserName (lctx : LocalContext) (userName : Name) : Bool := (lctx.findFromUserName? userName).isSome -partial def getUnusedNameAux (lctx : LocalContext) (suggestion : Name) : Nat → Name × Nat +private partial def getUnusedNameAux (lctx : LocalContext) (suggestion : Name) : Nat → Name × Nat | i => let curr := suggestion.appendIndexAfter i; if lctx.usesUserName curr then getUnusedNameAux (i + 1) @@ -157,7 +158,8 @@ partial def getUnusedNameAux (lctx : LocalContext) (suggestion : Name) : Nat → @[export lean_local_ctx_get_unused_name] def getUnusedName (lctx : LocalContext) (suggestion : Name) : Name := -if lctx.usesUserName suggestion then (lctx.getUnusedNameAux suggestion 1).1 +let (suggestion, _) := extractMacroScopes suggestion; +if lctx.usesUserName suggestion then (getUnusedNameAux lctx suggestion 1).1 else suggestion @[export lean_local_ctx_last_decl]