Get scope *before* some syntax is evaluated

Stream: general

[Michael Rothgang]

I'm writing a linter which inspects variable commands. I'd like to know which variables were in scope before a particular variable command was executed. Is there a way to achieve this?

Simply looking at getScope includes the effect of that command already. (This examples requires two files; probably, one file is also possible with further effort.)

import Batteries.Tactic.Lint
open Lean Elab Command

def badVariableLinter : Linter where run := withSetOptionIn fun stx => do
    -- TODO: how to access the current scope *before* the `variable` command was parsed?
    let previousVariablesOld := ((← getScope).varDecls).map fun var ↦ var.raw
    -- This already prints current variable names...
    dbg_trace previousVariablesOld
    -- Now, the actual linter can do whatever

initialize addLinter badVariableLinter

-- In a new file, importing just this linter and containing "variable (a)", and observe that a is printed.

[Michael Rothgang]

There certainly is a small hack I could use: elaborate a bare section command before stx and using the not-current-anymore scope to compare. I'd be happy to learn about better solutions, though!

[Damiano Testa]

The variables in Scopes (note the plural!) seem to remember each layer already:

import Lean

open Lean Elab Command

/--  `gs i` shows the available `variable`s `i` scopes ago (defaulting to 0 if not given). -/
elab "gs" i:(num)? : command => do
  let sc := (← get).scopes
  let i := (i.getD (← `(num|0))).getNat
  dbg_trace "Number of available scopes: {sc.length}"
  dbg_trace ((sc.getD i default).varDecls.map getBracketedBinderIds).flatten

variable (a0 : Nat)

section
variable (a1 : Nat)

section
variable (a2 : Nat)

section
variable (a3 : Nat)

section
-- try various numbers to see how you "climb up" the variables in scope
gs 2

[Michael Rothgang]

I know! But isn't this basically what I'm saying above? Put differently, using gs n in

import Lean

open Lean Elab Command

/--  `gs i` shows the available `variable`s `i` scopes ago (defaulting to 0 if not given). -/
elab "gs" i:(num)? : command => do
  let sc := (← get).scopes
  let i := (i.getD (← `(num|0))).getNat
  dbg_trace "Number of available scopes: {sc.length}"
  dbg_trace ((sc.getD i default).varDecls.map getBracketedBinderIds).flatten

variable (a0 : Nat)

section

variable (a3 : Nat)
variable (a4 : Nat)

section
-- try various numbers to see how you "climb up" the variables in scope
gs 4

does not distinguish a3 and a4.

[Damiano Testa]

So you are trying to distinguish between variable (a b) and variable a variable b? I.e. if, within a given scope, whether the variables were added in separate variable commands or in the same?

[Michael Rothgang]

The case I'm really interested in is variable {a} variable (a) (two separate commands, the binder type of a is changed in the second one).