root namespace with idents

Stream: lean4

[Adam Topaz]

Consider the following code snippet:

import Lean
open Lean


macro "foo" s:str : command => do
  let i : Ident := mkIdent (.str .anonymous s.getString)
  `(def $i := (1 : Nat))

macro "bar" s:str : command => do
  let i : Ident := mkIdent ("_root_" ++ s.getString)
  `(def $i := (1 : Nat))

namespace blah

foo "test"
bar "baz"

end blah

#check blah.test
#check baz

This works. What I'm wondering about is how to accomplish the behavior of "bar" similarly to "foo" (i.e. without resorting to manipulating strings with "_root_"). Any pointers?

[Gabriel Ebner]

Are you looking for `_root_ ++ s.getString or .str (.str .anonymous "_root_") s.getString?

[Adam Topaz]

I'm not sure what I'm looking for. I guess at the end of the day I'm wondering if there is a way to get to the root namespace without using "_root_" (or `_root_)

[Mario Carneiro]

not if you are constrained to generate an identifier that goes into def

[Mario Carneiro]

you could just call the underlying API, in which case you can name it whatever you want

[Adam Topaz]

Fair enough. Thanks. Where can I find the underlying API for making defs, structures, etc.?

[Mario Carneiro]

I usually just follow the trail starting at the syntax, to src4#Lean.Elab.Command.elabDeclaration, to src4#Lean.Elab.addPreDefinitions, and finally to src4#Lean.addDecl, depending on how much of the def stuff you want to do

[Mario Carneiro]

addDecl is the kernel interface; in particular it doesn't compile the definition (you need src4#Lean.addAndCompile for that)

[Adam Topaz]

Sorry... I'm a bit slow. What should I do to "follow the trail"?

[Adam Topaz]

My first instinct would be to do something like

#check (`(def a : Nat := 0) : MacroM _)

but I don't see any of the functions you mentioned by doing this.

[Mario Carneiro]

Let's say we want to know what def does.

• My first step is to search the codebase for "def, "def or "def", which usually takes me to the declaration of the syntax, in this case src4#Lean.Parser.Command.def
• This isn't actually a command parser (you can tell because it doesn't have a@[builtinCommandParser] attribute), but if you look for uses in the same file you find src4#Lean.Parser.Command.declaration is the actual command, which has «def» as one of its cases.
• The next step is to find the elab or macro corresponding to this syntax. There are a few ways to do this; I'm still mostly using the old school method of searching for declaration] or «declaration»] looking for the builtinCommandElab for it, but you can also use "Find References" on declaration to get to it. That takes us to src4#Lean.Elab.Command.elabDeclaration
• From there, we just go forward along the function calls looking for where the "real work" is. Declarations are one of the more complicated lean commands, so there is a lot of stuff, but if you imagine you are parsing a def you will try src4#Lean.Elab.Command.elabMutualDef, which calls src4#Lean.Elab.Term.elabMutualDef, which calls src4#Lean.Elab.addPreDefinitions, which calls src4#Lean.Elab.addAndCompileNonRec, which calls a private function that calls src4#Lean.addDecl.

[Adam Topaz]

Thanks Mario! That's very helpful!

[Mario Carneiro]

Actually we can even keep going:

• src4#Lean.addDecl calls src4#Lean.Environment.addDecl, which has an extern "lean_add_decl", so if we want to keep digging we're going to end up in the C++ code.
• Searching for lean_add_decl( yields lean_add_decl, which calls environment::add, which calls environment::add_definition, which calls environment::add (this is a different overload), which calls an extern function lean_environment_add.
• Searching for lean_environment_add leads us back into lean to src4#Lean.Environment.add, because it has an export lean_environment_add declaration on it so that C++ code can call it. That calls src4#Lean.Environment.addAux which inserts into the constants hashmap and now we're really done. (In case you were wondering, the actual kernel typechecker runs in the environment::add_definition step.)