Defining notations involving indentation?

Stream: lean4

[Tanner Swett]

I'd like to define a notation that behaves similarly to the structure command. If I understand right, it's possible (maybe mandatory?) to have the fields of the structure indented, with the end of the indented block marking the end of the structure.

With the syntax command, is it possible to define something that responds to indentation the same way? (If not, no problem; I'll use braces and semicolons or something.)

[Tanner Swett]

Aha, I think I've figured it out:

syntax "variety_info " (manyIndent(ident ":" term)) : term

This allows me to write stuff like

  def TwoSetsInfo := variety_info
    Set1 : Type
    Set2 : Type

[Tanner Swett]

But now I'm having trouble implementing macro rules for it. What I did manage to get working is this:

syntax "variety_info " (manyIndent(term ":" term)) : term

macro_rules
  | `(variety_info
        $[$name : Type]*) =>
      `(VarietyInfo.mk (sorts := [$[$name],*]))

The above code allows me to write

#check variety_info
  `ThisThing : Type
  `ThatThing : Type

and it comes out as { sorts := [`ThisThing, `ThatThing] } : VarietyInfo. That's _very close_ to what I actually want. What I actually want is to be able to write

#check variety_info
  ThisThing : Type
  ThatThing : Type

My best attempt at getting this working was to write this:

syntax "variety_info " (manyIndent(ident ":" term)) : term

macro_rules
  | `(variety_info
        $[$name : Type]*) =>
      `(VarietyInfo.mk (sorts := [$[`$name],*]))

But I get an error at name on the last line there:

application type mismatch
  Array.map (fun name => Lean.Syntax.node2 info✝ `Lean.Parser.Term.precheckedQuot (Lean.Syntax.atom info✝ "`") name.raw)
    name
argument
  name
has type
  Array (Lean.TSyntax `ident) : Type
but is expected to have type
  Array (Lean.TSyntax `Lean.Parser.Term.quot) : Type

Presumably, writing `$name is not the right way to say "take the identifier bound to $name and make a name literal out of it," but what is?

[Mac Malone]

You are looking for $(quote name) instead of `$name.

[Tanner Swett]

Mac said:

You are looking for $(quote name) instead of `$name.

Many thanks! It looks like that's one half of what I needed—the quote function will convert a Name to a TSyntax `term, and the other half is converting a TSyntax `ident to a Name. So here's the final working code I ended up with:

open Lean (TSyntax quote)

syntax "variety_info " (manyIndent(ident ":" term)) : term

def ident_to_quoted_term (name : TSyntax `ident) : TSyntax `term :=
  match name.raw with
    | .ident _ _ val _ => quote val
    | _ => default

macro_rules
  | `(variety_info
        $[$name : Type]*) =>
      `(VarietyInfo.mk (sorts := [$[$(Array.map ident_to_quoted_term name)],*]))

[Mario Carneiro]

the other half is name.getId