Generate structure update expression as part of macro?

Stream: lean4

[Phil Nguyen]

Hi! How can I generate the syntax for updating a field of a large structure (e.g. {s with a := v}) as part of a macro?

For example, given this minimal example:

structure Person where
  name : String
  age : Nat

def foo : Person := {name := "Foo", age := 10}

If I try this macro, I'll get a complaint that ident isn't where structInstLVal is expected:

macro "foo_update" field:ident value:term : term =>
  `({foo with $field := $value})
/-
Application type mismatch: The argument
  field
has type
  TSyntax `ident
but is expected to have type
  TSyntax `Lean.Parser.Term.structInstLVal
in the application
  field.raw
-/

And if I try casting ident to structInstLVal, I'll get an error at the expansion site:

macro "foo_update" field:ident value:term : term => do
  let lhs := TSyntax.mk field.raw
  `({foo with $lhs := $value})

set_option pp.rawOnError true
#check foo_update name "Bar"
/-
unexpected syntax
  [Error pretty printing syntax: parenthesize: uncaught backtrack exception. Falling back to raw printer.]
  (Term.structInst
   "{"
   [[`__src._@.Test.3767781306._hygCtx._hyg.8] "with"]
   (Term.structInstFields [(Term.structInstField `name [[] [] (Term.structInstFieldDef ":=" [] (str "\"Bar\""))])])
   (Term.optEllipsis [])
   []
   "}")
-/

Many thanks!!

[Robin Arnez]

Always try annotating the type when errors occur:

macro "foo_update" field:ident value:term : term =>
  `({foo with $field:ident := $value})

[Phil Nguyen]

Omg thank you so much!!

I didn't think of that because I didn't know what was going on underneath. I thought an ident was not a structInstLVal so I attempted to "unwrap then rewrap" it.

Is this because there's some coercion from ident to structInstLVal that won't kick in without the explicit annotation?

[Robin Arnez]

Well it's because structInstLVal is a node containing a lot of things:

def structInstLVal := leading_parser
  (ident <|> fieldIdx <|> structInstArrayRef) >>
  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)

when parsing, it will take the outermost antiquotation unless specified otherwise, so it expected a syntax for structInstLVal but if you specify ident you force it to instead create a structInstLVal node containing the identifier you provided. In other words, what you specify after the : can determine which part of the syntax will be filled in. For example, you could also specify $field:fieldIdx which would make it instead fill in the fieldIdx part of the structInstLVal syntax and then you'd need to also provide syntax of type fieldIdx.
One common misconception is also that the macro would be able to tell you need an identifier because of type of field - this is not the case since antiquotations are (and need to be) parsed completely before any kind of elaboration, in other words, nothing is known about the types of things at that point. But while parsing the antiquotation it already decided exactly where to put it and what type it should have. That means that if it then turns out to have a different type then it guessed, you'll get an error. Instead, you need to tell it the information that field is an identifier explicitly so it can know that while parsing.

[Phil Nguyen]

Thank you for the thorough explanation!