Metaprogramming a structure declaration

Stream: Is there code for X?

[Tanner Swett]

Hey everyone! How easy is it to write a macro or elaborator which declares a structure with field names given by the given identifiers? I tried writing

macro "declare_mypoint" name:ident x:ident y:ident : command =>
  `(structure $name where
      $x : Nat
      $y : Nat)

but that's a syntax error after $x.

I actually did manage to write a macro that does it, but I did it by #checking the quotation above (with $x and $y changed to x and y), taking the resulting 50 lines of code, and replacing the parts referring to x and y with expressions that refer to the given identifiers. But my goodness, there must be an easier way.

[Kyle Miller]

Sometimes you need to help antiquotations out with how they're supposed to be interpreted:

macro "declare_mypoint" name:ident x:ident y:ident : command =>
  `(structure $name where
      $x:ident : Nat
      $y:ident : Nat)

[Kyle Miller]

You can do more dynamic things too:

open Lean Parser Command in
macro "declare_mypoint" name:ident xs:ident* : command => do
  let fields ← xs.mapM fun x => `(structExplicitBinder| ($x:ident : Nat))
  let fieldsStx : TSyntax ``structFields ← `(structFields| $fields*)
  `(structure $name where
      $fieldsStx:structFields)

declare_mypoint R2 x y
declare_mypoint R3 x y z

[Tanner Swett]

Dang, I love it!

[Tanner Swett]

Something I'm going to do eventually is write something which takes a description of an algebraic structure, and automatically generates a definition of that structure and homomorphisms on it.

[Tanner Swett]

I also have the reverse question, so to speak. Suppose that I've already written, say,

structure Graph where
  (Vertices Edges : Type)
  (head tail : Vertices → Edges)

Is there an easy way to retrieve the names and types (as expressions) of the fields?

[Kyle Miller]

Do you want to get it from the syntax, or from a pre-existing structure? It's possible to get all the fields of a structure and their types given just the name of the structure.

[Tanner Swett]

From a pre-existing structure.

[Kyle Miller]

open Lean in
elab "#print_structure_fields " c:ident : command => do
  let name ← resolveGlobalConstNoOverload c
  let env ← getEnv
  let some info := getStructureInfo? env name
    | throwErrorAt c "Not a structure"
  logInfo m!"field names: {info.fieldNames}"
  let mut msgs := #[]
  for field in info.fieldInfo do
    let proj := (env.find? field.projFn).get!
    msgs := msgs.push m!"{field.projFn} : {proj.type}"
  logInfo <| MessageData.joinSep msgs.toList "\n"

[Kyle Miller]

It first prints the fields in order, and then it gives the types in alphabetical order

structure MyStruct where
  (n m : Nat)
  (h : n < m)

#print_structure_fields MyStruct
/-
field names: [n, m, h]
MyStruct.h : ∀ (self : MyStruct), self.n < self.m
MyStruct.m : MyStruct → ℕ
MyStruct.n : MyStruct → ℕ
-/

[Tanner Swett]

Very nice! Thank you! I'll see if I can figure out the rest from there.

[Tanner Swett]

I think you just gave me the hard part, so hopefully the rest will be straightforward.

[Kyle Miller]

It looks like you can get the field types in order using a slightly different approach:

open Lean in
elab "#print_structure_fields " c:ident : command => do
  let name ← resolveGlobalConstNoOverload c
  let env ← getEnv
  let some info := getStructureInfo? env name
    | throwErrorAt c "Not a structure"
  logInfo m!"field names: {info.fieldNames}"
  let mut msgs := #[]
  for i in [0:info.fieldNames.size] do
    let some proj := info.getProjFn? i | break
    let proj := (env.find? proj).get!
    msgs := msgs.push m!"{info.fieldNames[i]!} : {proj.type}"
  logInfo <| MessageData.joinSep msgs.toList "\n"

[Shreyas Srinivas]

wait this is possible? I was struggling with this for weeks.

[Shreyas Srinivas]

thanks a lot. What's the right way to cite a thread on zulip like this?

[Kevin Buzzard]

You can make a permalink if the stream is public (and this one is)

[Shreyas Srinivas]

Thanks a lot :)

[Kyle Miller]

I got some of this by looking at the structure pretty printer, unexpandStructureInstance, and then poking around the modules where some of the functions come from.

[Tanner Swett]

I'm in the middle of trying to write a term elaboration cat_alg_info_for which takes the name of a structure and returns some information about it.

I have a structure called Cat_Alg_Info, and for the time being, I just want my elaborator to return @Cat_Alg_Info.mk Name, so I've written:

return (mkAppN (.const ``Cat_Alg_Info.mk [.zero]) #[.const ``Name []])

But instead of writing out a whole expression for the expression, is there something along the following lines I can write?

elab `(@Cat_Alg_Info.mk Name)

[Tanner Swett]

Aha, it looks like this will do it:

  let resultStx ← `(@Cat_Alg_Info.mk Name)
  elabTerm resultStx none

[Kyle Miller]

There's also the Qq library for writing Exprs, vs these quotations for writing Syntax. You can search for instances of q( and Q( in Mathlib for some examples. This would probably be q(@Cat_Alg_Info.mk Name)

[Tanner Swett]

Ah, very nice!

[Tanner Swett]

I don't suppose there's an existing typeclass for types that can be converted into Exprs representing themselves? (Or maybe the quote4 library can do that?)

[Kyle Miller]

That's yet another thing, docs4#Lean.ToExpr.toExpr

[Kyle Miller]

You'll probably want to import Mathlib.Tactic.ToExpr to also get some additional ToExpr instances and a deriving ToExpr handler

[Kyle Miller]

and also by the way, there's docs4#Lean.Quote.quote for turning types into TSyntax `terms that represent themselves.

[Tanner Swett]

Very nice!

Well, I think I'm done for this weekend. I now have a term elaborator which takes the name of a structure and produces a list of the names of its fields.

Some time soon, I'm going to want to make sure that the type of every field is either Type u, or α₁ → ... → αₙ → β, where α₁, ..., αₙ, β are fields whose type is Type u. It looks like maybe the easiest way to do that is going to be to use getProjFnForField? to get the name of each field, and then look up what each projection function returns.

[Shreyas Srinivas]

Is there a list of all syntax categories and what they contain defined inside Lean, Mathlib, Std, etc?

[Notification Bot]

Tanner Swett has marked this topic as resolved.

[Notification Bot]

Shreyas Srinivas has marked this topic as unresolved.

[Jeremy Salwen]

Kyle Miller said:

It looks like you can get the field types in order using a slightly different approach:

open Lean in
elab "#print_structure_fields " c:ident : command => do
  let name ← resolveGlobalConstNoOverload c
  let env ← getEnv
  let some info := getStructureInfo? env name
    | throwErrorAt c "Not a structure"
  logInfo m!"field names: {info.fieldNames}"
  let mut msgs := #[]
  for i in [0:info.fieldNames.size] do
    let some proj := info.getProjFn? i | break
    let proj := (env.find? proj).get!
    msgs := msgs.push m!"{info.fieldNames[i]!} : {proj.type}"
  logInfo <| MessageData.joinSep msgs.toList "\n"

Does getStructureInfo? work here on any structure-like type (i.e. single constructor), or only things that are actually declared structure?

[Kyle Miller]

That's only for actual structures, which I think is necessary because structure-like types don't come with projections, and you might not have names for all the fields.

That said, there's a function for getting some information about structure-like types: https://github.com/leanprover/lean4/blob/a44dd71ad62a1760e32b0e8a12449e560ddcf492/src/Lean/Structure.lean#L195

[Kyle Miller]

structure-like appears to be defined to be single constructor, non-recursive, and no indices.

[Jeremy Salwen]

Kyle Miller said:

That's only for actual structures, which I think is necessary because structure-like types don't come with projections, and you might not have names for all the fields.

That said, there's a function for getting some information about structure-like types: https://github.com/leanprover/lean4/blob/a44dd71ad62a1760e32b0e8a12449e560ddcf492/src/Lean/Structure.lean#L195

If there isn't a name for the field and there isn't a projection, then is there no way to project onto the fields for a structure-like type that isn't a structure?

[Kyle Miller]

You can always define your own projections, like def Foo.x : Foo -> Nat | .mk x y z => x, but as I understand it they won't be handled in exactly the same way as native projections.