Current namespace in declaration elaborator

Stream: metaprogramming / tactics

[Christian Merten]

How do I access the current surrounding namespace of a declaration at elaboration time? For example, in

namespace Foo
def Baz.bla : Nat := 3
end Foo

I would like the output to be Foo. The naive

import Lean

open Lean Elab Command

@[command_elab declaration]
def foo : CommandElab := fun stx => do
  logInfo s!"Namespace in elab: {← getCurrNamespace}"
  elabDeclaration stx

namespace Foo

-- I would like to get `Foo` instead.
/-- info: Namespace in elab: Foo.Baz -/
#guard_msgs in
def Baz.bla : Nat := 3

end Foo

yields Foo.Baz instead. The reason is that before the declaration is elaborated, the macro docs#Lean.Elab.Command.expandNamespacedDeclaration wraps the declaration in a namespace Baz block.

[Edward van de Meent]

i think there isn't really a way to fix this, since it happens after expanding a macro for the syntax you're (presumably?) trying to modify elaboration of.

I think you should check if elaborating an attribute has the same issue (i'm presuming not, since to_additive manages to change namespaces)
Also, let me #xy you need this functionality, just in case

[Christian Merten]

I want to extract the source code for a declaration from a .lean source file while preserving the relevant context, which is in particular the necessary namespace ... commands. The way I am currently doing that is by adding an environment extension that stores the current docs#Lean.Elab.Command.Scope when elaborating the declaration. But this contains the "wrong" namespace in the sense that

namespace {extracted namespace}

-- extracted original source code of declaration

end {extracted namespace}

repeats the Baz (in the Baz.bla example from above).

[Aaron Liu]

do you know about #where

[Aaron Liu]

docs#Lean.Parser.Command.where

[Christian Merten]

Edward van de Meent said:

I think you should check if elaborating an attribute has the same issue (i'm presuming not, since to_additive manages to change namespaces)

It does have the same issue (can't post a nice mwe in the live editor because of initialization).

[Christian Merten]

Aaron Liu said:

do you know about #where

Yes, but I am not sure how that helps: If you look at the source code of docs#Lean.Elab.Command.elabWhere, it also just gets the current docs#Lean.Elab.Command.Scope. So I would need a way to run this just before elaborating the declaration I want to extract.

[Christian Merten]

For the record, I found a hack around this:

import Lean
import Batteries.Tactic.OpenPrivate

open private getDeclName? from Lean.Elab.Declaration

open Lean Elab Command

elab "update_decl_context" decl:ident : command => do
  let scope ← getScope
  let resolvedName : Name := scope.currNamespace ++ decl.getId
  logInfo s!"updating env extension for {resolvedName} in namespace {scope.currNamespace}"

@[macro Lean.Parser.Command.declaration]
def prependUpdateDeclContext : Macro := fun stx => do
  if let some declName := getDeclName? stx then
    `(update_decl_context $(mkIdent (declName))
      $(⟨← expandNamespacedDeclaration stx⟩))
  else
    expandNamespacedDeclaration stx

namespace Foo

/-- info: updating env extension for Foo.Baz.bla in namespace Foo -/
#guard_msgs in
def Baz.bla : Nat := 3

end Foo

The reason I need the update_decl_context helper command is to get access to the environment in my application (to store the scope in an environment extension).
This is also only half the fix, to also still cover unnamespaced declarations, I also had to change the actual command elaborator.