Use a ConstructorVal in syntax as a constructor

Stream: lean4

[Thomas Murrills]

Given a ConstructorVal, as you might get from getStructureCtor, how do you use it within syntax?

For example, the Lean metaprogramming book includes a mini project (page 70, end of the Elaboration section) which uses a custom getCtors. This yields the Names of the constructors. The defined elaboration function then checks if there's exactly one constructor, calls it ctor, then uses it in `($(mkIdent ctor) $args*) as syntax (which elabTerm is then called on).

If instead we get a ConstructorVal from getStructureCtor, we don't seem to be able to extract the name of the constructor itself to use in the same way. While I could just use/reimplement the custom getCtors to get things working, I became curious as to how ConstructorVals were used and what they were for. How would you do something analogous `($(mkIdent ctor) $args*)?

And, bonus question: are there any robustness concerns with using mkIdent on a constructor name? Is there a better way to do term elaboration than by following the pattern given in the mini project, or is this generally safe?

[Henrik Böving]

Sure you can easily get the name of the constructor from a ConstructorVal it extends docs4#Lean.ConstantVal which has a name field you can just use.

[Thomas Murrills]

Oh! I straight-up missed that extends while reading the code. Whoops, thanks. :)

So, shifting to the bonus question: is using a Name with mkIdent to create syntax which is then re-elaborated a robust pattern for term elaboration in general? Is this the standard way to do term elaboration?

[Mario Carneiro]

If you use mkIdent alone, no it is not robust to shadowing:

macro "foo" : term => pure (mkIdent ``some)

namespace Foo
def Option.some := 1

#check foo -- prints `Foo.Option.some`

However if you use mkCIdent it will "preresolve" the name, so it will resolve as intended:

macro "foo" : term => pure (mkCIdent ``some)

namespace Foo
def Option.some := 1

#check foo -- prints `_root_.Option.some`

[Thomas Murrills]

oh, perfect! Thanks! :)