Parser category for instance parameters

Stream: lean4

[Marcus Rossel]

I'm trying to write a macro that generates a type class instance.
What is the correct category to use for the type parameters of the class?

For example, I want to generate:

instance : MyClass Type1 (someComputation .returning).type2 where
  ...

I tried:

open Lean Macro in
macro "generate_instance" first:term second:term : command => do
  ...

But that results in expected term when writing generate_instance Type1 (someComputation .returning).type2.

[Jannis Limperg]

The parser for instance commands is defined like this:

def «instance»       := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix

I found this in Lean/Parser/Command.lean by searching for 'instance'.

[pcpthm]

Alternatively, the parser for a builtin syntax can also be found by the go-to-definition feature https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/structure-like.20custom.20syntax/near/294606430

[Marcus Rossel]

@Jannis Limperg I'm guessing that the relevant part in

def «instance» := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix

... is declSig (which I'm guessing stands for "declaration signature"), right? From its definition:

def declSig := leading_parser many (ppSpace >> (Term.binderIdent <|> Term.bracketedBinder)) >> Term.typeSpec

... I'd take the relevant part to be Term.typeSpec:

def typeSpec := leading_parser " : " >> termParser

... and hence termParser:

def termParser (prec : Nat := 0) : Parser :=
  categoryParser `term prec

But for me that's basically a dead end.
Or does this mean that term is in fact the correct category to use in my example?

[Marcus Rossel]

pcpthm said:

Alternatively, the parser for a builtin syntax can also be found by the go-to-definition feature https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/structure-like.20custom.20syntax/near/294606430

This doesn't seem to work for instance (at least when I tried).

[Jannis Limperg]

Or does this mean that term is in fact the correct category to use in my example?

No, the correct category (parser, actually, but parsers and syntax categories are, I believe, interchangeable here) is declSig. You'll have to lift your term into a declSig, e.g. with something like this:

let sig <- `(declSig| : $first:term)

If you give an #mwe, I can look into the issue in more detail. It usually takes some experimentation for me to get the syntax system to cooperate. ;)

[Marcus Rossel]

@Jannis Limperg Hmm, I don't quite see how to use declSig yet. An MWE would be:

import Lean
open Lean Macro

macro "gen_coe" src:term dst:term : command => do
  `(
    instance : Coe $src $dst where
      coe := sorry
  )

gen_coe Bool (if true then Nat else Int) -- error

[Jannis Limperg]

The error seems to be that Lean parses Bool (if true then Nat else Int) as one term (an ill-typed application). This works:

import Lean
open Lean Macro

macro "gen_coe" "[" src:term "]" "[" dst:term "]" : command =>
  `(
    instance : Coe $src $dst where
      coe := sorry
  )

gen_coe [Bool] [Int]

However, I would recommend that you write $src:term and $dst:term in the body of the macro. Without these annotations, you may get weird errors. (Maybe this is no longer the case with TSyntax.)

[Sebastian Ullrich]

Yes, that issue should no longer be an issue :)

[Sebastian Ullrich]

You can also use src:term:max to make sure it's not parsed as an application

[Marcus Rossel]

Thanks you two!