Determining variable binders from syntax

Stream: general

[Michael Rothgang]

Given a variable command, can I determine the inner binder names from a syntax linter? I can get a syntax node of explicitBinder kind, but don't see how to parse out the binder names...

I tried something like the following (minimised):

import Batteries.Tactic.Lint
open Lean Elab Command

def badVariableLinter : Linter where run := withSetOptionIn fun stx ↦ do
    if (← MonadState.get).messages.hasErrors then
      return
    if let Syntax.node _ ``Lean.Parser.Command.variable args := stx then
      let binders := (args.map getBinders).flatten
      if #[``Lean.Parser.Term.implicitBinder, ``Lean.Parser.Term.explicitBinder].contains kind then
        binders.push stx else fargs
      for b in binders do
        -- How to get the list of binder names in b?

More generally, (how) could I obtain the parsed binders from Term.explicitBinder or Term.implicitBinder? If I just print b, the information is there, but I'm missing how to extract it...

Context: I'm trying to write a syntax linter for variable commands which update how a variable is bound and declare new variables at the same time.

[Michael Rothgang]

More generally: is there a way to print the actual syntax for some Lean code? Using something like `Linter.logLint linter.badVariable stx s!"arguments are {args}" pretty-prints the syntax; I would like to see the internal structure.
@Damiano Testa You mentioned some inspect command a few times. Where can I find that? (The API docs don't mention any such method.)

[Michael Rothgang]

@Damiano Testa It seems you tried something similar in #14675, but switched to a different approach? Did you manage to solve the problem I'm worrying about?

[Damiano Testa]

Can you give an example of what you would like? E.g. with

variable (a : Nat) {b c : Int}

you would like a, b, c? Or explicit, implicit, implicit?

[Damiano Testa]

Michael Rothgang said:

Damiano Testa It seems you tried something similar in #14675, but switched to a different approach? Did you manage to solve the problem I'm worrying about?

I simply started with something else, since I wanted to wait for the new variable mechanism before continuing.

I would still like to make "dependent" typeclass variables flagged by a linter, but I was not sure whether the adaptation to the new variable command and this linter would have stepped on each other's toes (and I guess that they would!).

[Damiano Testa]

Michael Rothgang said:

Damiano Testa You mentioned some inspect command a few times. Where can I find that? (The API docs don't mention any such method.)

inspect is a command that I defined to print the tree structure of some syntax. Using dbg_trace stx gives you some idea of what the tree structure looks like.

[Damiano Testa]

Johan suggested upgrading inspect to a clickable interface and PRing it, but I have not gotten around to it.

[Michael Rothgang]

Damiano Testa said:

Can you give an example of what you would like? E.g. with

variable (a : Nat) {b c : Int}

you would like a, b, c? Or explicit, implicit, implicit?

Ultimately, I am interested in a list of items (name, withType): for variable (a) (b : Nat) this would say (a, false), (b, true).

[Michael Rothgang]

FWIW, I asked about this linter and the new variables command - and my impression was that this linter is still desirable.

[Damiano Testa]

Is this close to what you wanted?

import Lean

open Lean

def getNamesWithType (stx : Syntax) : Array (Syntax × Bool) :=
  if #[``Lean.Parser.Term.implicitBinder, ``Lean.Parser.Term.explicitBinder].contains stx.getKind then
    stx[1].getArgs.map (·, stx[2][0] != default)
  else #[]

run_cmd
  let stxs := [← `(bracketedBinder| (a : Nat)), ← `(bracketedBinder| (b c)), ← `(bracketedBinder| {d e f})]
  for stx in stxs do
    logInfo m!"{getNamesWithType stx.raw}"

[Damiano Testa]

Michael Rothgang said:

FWIW, I asked about this linter and the new variables command - and my impression was that this linter is still desirable.

I was thinking of a different linter: the one that I had in mind would complain if you have [Mul R] [Ring R] since Mul is implied by Ring.

[Damiano Testa]

This is the one that you linked to above, I think.

[Michael Rothgang]

Indeed, I was using your PR as inspiration for how to work with variables syntactically.

[Damiano Testa]

Ah, no, the one above is yet another one! The one above, #14675, is one that complains when variable (a : Nat) is available and you type example (a : Nat) ....

[Damiano Testa]

In some sense, that linter tries to maximize the use of the variables in scope. I agree with the sentiment that this is not so great: it is better to be more explicit about assumptions!

[Damiano Testa]

I think that the "implied typeclass" linter does produce better code, but that one will step on the new variable mechanism.

[Damiano Testa]

So, I withheld from developing and adapting mathlib to it until the variable wave washes out.

[Michael Rothgang]

Damiano Testa said:

Is this close to what you wanted?

import Lean

open Lean

def getNamesWithType (stx : Syntax) : Array (Syntax × Bool) :=
  if #[``Lean.Parser.Term.implicitBinder, ``Lean.Parser.Term.explicitBinder].contains stx.getKind then
    stx[1].getArgs.map fun s => (s, stx[2][0] == default)
  else #[]

run_cmd
  let stxs := [← `(bracketedBinder| (a : Nat)), ← `(bracketedBinder| (b c)), ← `(bracketedBinder| {d e f})]
  for stx in stxs do
    logInfo m!"{getNamesWithType stx.raw}"

Yes, it is - thanks a lot! (I actually want to invert the booleans, but that is easy to do.)

[Damiano Testa]

Yes, I noticed it and I have already edited the command above!

[Damiano Testa]

Make sure not to invert them twice! (The original was indeed the opposite of what you wanted.)

[Damiano Testa]

Also, note that (a := 0) is a valid binder and the code above treats it as "no type provided".

[Damiano Testa]

Whether or not this is what you want, I do not know!

[Michael Rothgang]

Damiano Testa said:

Whether or not this is what you want, I do not know!

Good point; I am not sure yet either. I'll think about it!

[Damiano Testa]

Btw, if you want to see a lot of raw binder action, checkout the fully unpolished #15213.

[Kyle Miller]

I don't think you should be parsing binders yourself like this. Take a look at the implementation of variable in docs#Lean.Elab.Command.elabVariable

There's docs#Lean.Elab.Command.getBracketedBinderIds for example to get the ids from each binder. Potentially you could even elaborate the binders using docs#Lean.Elab.Term.elabBinders to get the full list with their types, which includes implicit/explicit/etc.

[Michael Rothgang]

Thanks, that looks really helpful. I'll take a closer look!