@@ -70,6 +70,91 @@ def useDiagnosticMsg : MessageData :=
7070 else
7171 pure s! "\n\n Additional diagnostic information may be available using the `set_option { diagnostics.name} true` command."
7272
73+ /-- Name generator that creates user-accessible names. -/
74+ structure DeclNameGenerator where
75+ namePrefix : Name := .anonymous
76+ -- We use a non-nil list instead of changing `namePrefix` as we want to distinguish between
77+ -- numeric components in the original name (e.g. from macro scopes) and ones added by `mkChild`.
78+ private idx : Nat := 1
79+ private parentIdxs : List Nat := .nil
80+ deriving Inhabited
81+
82+ namespace DeclNameGenerator
83+
84+ private def idxs (g : DeclNameGenerator) : List Nat :=
85+ g.idx :: g.parentIdxs
86+
87+ def next (g : DeclNameGenerator) : DeclNameGenerator :=
88+ { g with idx := g.idx + 1 }
89+
90+ /--
91+ Creates a user-accessible unique name of the following structure:
92+ ```
93+ <name prefix>.<infix>_<numeric components>_...
94+ ```
95+ Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other
96+ branching elaboration steps, `mkChild` must be used (automatically done in `wrapAsync*`).
97+ -/
98+ partial def mkUniqueName (env : Environment) (g : DeclNameGenerator) («infix » : Name) :
99+ (Name × DeclNameGenerator) := Id.run do
100+ -- `Name.append` does not allow macro scopes on both operands; as the result of this function is
101+ -- unlikely to be referenced in a macro; the choice doesn't really matter.
102+ let «infix » := if g.namePrefix.hasMacroScopes && infix.hasMacroScopes then infix.eraseMacroScopes else «infix »
103+ let base := g.namePrefix ++ «infix »
104+ let mut g := g
105+ -- NOTE: We only check the current branch and rely on the documented invariant instead because we
106+ -- do not want to block here and because it would not solve the issue for completely separated
107+ -- threads of elaboration such as in Aesop's backtracking search.
108+ while env.containsOnBranch (curr g base) do
109+ g := g.next
110+ return (curr g base, g)
111+ where curr (g : DeclNameGenerator) (base : Name) : Name :=
112+ g.idxs.foldr (fun i n => n.appendIndexAfter i) base
113+
114+ def mkChild (g : DeclNameGenerator) : DeclNameGenerator × DeclNameGenerator :=
115+ ({ g with parentIdxs := g.idx :: g.parentIdxs, idx := 1 },
116+ { g with idx := g.idx + 1 })
117+
118+ end DeclNameGenerator
119+
120+ class MonadDeclNameGenerator (m : Type → Type ) where
121+ getDeclNGen : m DeclNameGenerator
122+ setDeclNGen : DeclNameGenerator → m Unit
123+
124+ export MonadDeclNameGenerator (getDeclNGen setDeclNGen)
125+
126+ instance [MonadLift m n] [MonadDeclNameGenerator m] : MonadDeclNameGenerator n where
127+ getDeclNGen := liftM (getDeclNGen : m _)
128+ setDeclNGen := fun ngen => liftM (setDeclNGen ngen : m _)
129+
130+ /--
131+ Creates a new name for use as an auxiliary declaration that can be assumed to be globally unique.
132+
133+ Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other
134+ branching elaboration steps, `mkChild` must be used (automatically done in `wrapAsync*`).
135+ -/
136+ def mkAuxDeclName [Monad m] [MonadEnv m] [MonadDeclNameGenerator m] (kind : Name := `_aux) : m Name := do
137+ let ngen ← getDeclNGen
138+ let (n, ngen) := ngen.mkUniqueName (← getEnv) («infix » := kind)
139+ setDeclNGen ngen
140+ return n
141+
142+ /--
143+ Adjusts the `namePrefix` of `getDeclNGen` to the given name and resets the nested counter.
144+ -/
145+ def withDeclNameForAuxNaming [Monad m] [MonadFinally m] [MonadDeclNameGenerator m]
146+ (name : Name) (x : m α) : m α := do
147+ let ngen ← getDeclNGen
148+ -- do not reset index if prefix unchanged
149+ if ngen.namePrefix != name then
150+ try
151+ setDeclNGen { namePrefix := name }
152+ x
153+ finally
154+ setDeclNGen ngen
155+ else
156+ x
157+
73158namespace Core
74159
75160builtin_initialize registerTraceClass `Kernel
@@ -93,6 +178,11 @@ structure State where
93178 nextMacroScope : MacroScope := firstFrontendMacroScope + 1
94179 /-- Name generator for producing unique `FVarId`s, `MVarId`s, and `LMVarId`s -/
95180 ngen : NameGenerator := {}
181+ /--
182+ Name generator for creating persistent auxiliary declarations. Separate from `ngen` to keep
183+ numbers smaller and create user-accessible names.
184+ -/
185+ auxDeclNGen : DeclNameGenerator := {}
96186 /-- Trace messages -/
97187 traceState : TraceState := {}
98188 /-- Cache for instantiating universe polymorphic declarations. -/
@@ -197,6 +287,10 @@ instance : MonadNameGenerator CoreM where
197287 getNGen := return (← get).ngen
198288 setNGen ngen := modify fun s => { s with ngen := ngen }
199289
290+ instance : MonadDeclNameGenerator CoreM where
291+ getDeclNGen := return (← get).auxDeclNGen
292+ setDeclNGen ngen := modify fun s => { s with auxDeclNGen := ngen }
293+
200294instance : MonadRecDepth CoreM where
201295 withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
202296 getRecDepth := return (← read).currRecDepth
@@ -220,8 +314,8 @@ instance : Elab.MonadInfoTree CoreM where
220314 modifyInfoState f := modify fun s => { s with infoState := f s.infoState }
221315
222316@[inline] def modifyCache (f : Cache → Cache) : CoreM Unit :=
223- modify fun ⟨env, next, ngen, trace, cache, messages, infoState, snaps⟩ =>
224- ⟨env, next, ngen, trace, f cache, messages, infoState, snaps⟩
317+ modify fun ⟨env, next, ngen, auxDeclNGen, trace, cache, messages, infoState, snaps⟩ =>
318+ ⟨env, next, ngen, auxDeclNGen, trace, f cache, messages, infoState, snaps⟩
225319
226320@[inline] def modifyInstLevelTypeCache (f : InstantiateLevelCache → InstantiateLevelCache) : CoreM Unit :=
227321 modifyCache fun ⟨c₁, c₂⟩ => ⟨f c₁, c₂⟩
@@ -435,7 +529,10 @@ def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CoreM
435529/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state. -/
436530def wrapAsync {α : Type } (act : α → CoreM β) (cancelTk? : Option IO.CancelToken) :
437531 CoreM (α → EIO Exception β) := do
532+ let (childNGen, parentNGen) := (← getDeclNGen).mkChild
533+ setDeclNGen parentNGen
438534 let st ← get
535+ let st := { st with auxDeclNGen := childNGen }
439536 let ctx ← read
440537 let ctx := { ctx with cancelTk? }
441538 let heartbeats := (← IO.getNumHeartbeats) - ctx.initHeartbeats
0 commit comments