Dot notation in syntax antiquotations

Stream: lean4

[Adam Topaz]

I'm looking for some advice regarding dot notation inside of an antiquotation. I can't seem to get it to work (albeit I only tried naive things). For example, how would I go about getting the second command to work similarly to the first command (modulo namespaces):

macro "c0" s:ident t:ident r:ident : command =>
  `(structure $s where ($t : Nat)
    namespace $s
    def $r := $t
    end $s)

macro "c1" s:ident t:ident r:ident : command =>
  `(structure $s where ($t : Nat)
    def $r := $s.$t)

c0 foo bar baz
#check foo.baz

c1 foo' bar' baz' -- fails

[Mario Carneiro]

dot notation directly on identifiers is lexed as a single identifier, so you have to combine the idents yourself:

import Lean
open Lean

macro "c0" s:ident t:ident r:ident : command =>
  `(structure $s where ($t : Nat)
    namespace $s
    def $r := $t
    end $s)

macro "c1" s:ident t:ident r:ident : command =>
  let s_t := mkIdentFrom (mkNullNode #[s, t]) (s.getId ++ t.getId)
  `(structure $s where ($t : Nat)
    def $r := $s_t)

c0 foo bar baz
#print foo.baz
-- def foo.baz : foo → Nat :=
-- foo.bar

c1 foo' bar' baz'
#print baz'
-- def baz' : foo' → Nat :=
-- foo'.bar'

[Adam Topaz]

Ah! I see. Thanks Mario!

[Mario Carneiro]

In fact, in this case you aren't actually using dot notation. The error you get in the original version is what you get if you force dot notation use, similar to writing (foo).bar or foo |>.bar, which fails because foo is a type / namespace, not an expression whose type is in an appropriate namespace

[Adam Topaz]

Yeah, I figured out that much... but had no idea what to try instead :)

[Adam Topaz]

One more question: What's the purpose of mkIdentFrom and mkNullNode? The following works as well -- is it equivalent?

macro "c1" s:ident t:ident r:ident : command =>
  let s_t := mkIdent (s.getId ++ t.getId)
  `(structure $s where ($t : Nat)
    def $r := $s_t)

c1 foo bar baz
#print baz

[Mario Carneiro]

it annotates the synthesized identifier s_t with the span of foo bar in the original call to c1

[Mario Carneiro]

so for example if there was a type error when elaborating the def you would see a red underline on that span

[Adam Topaz]

Ah interesting! Thanks!

[Mario Carneiro]

import Lean
open Lean

macro "c1" s:ident t:ident r:ident : command =>
  let s_t := mkIdentFrom (mkNullNode #[s, t]) (s.getId ++ t.getId)
  `(structure $s where ($t : Nat)
    def $r : Nat := $s_t)

c1 foo' bar' baz'
-- ^^^^^^^^^ type mismatch, bla bla

[Mario Carneiro]

of course it's a design question where exactly you want to put those underlines for any given macro