Linter

Suppose a file contains the following commands:

set_option A true in
open B in
set_option C true in
lemma something ‹binders› : ‹concl› := ‹value›

1. Every top-level command of the file gets parsed into its own syntax tree stx : Syntax. In our example, we pretend that the file contains nothing else other than the four lines shown above, which would mean that there is only one top-level command.

   `Command.in`
   ├─ [0] `Command.set_option`
   │      └─ … (4 children)
   ├─ [1] `atom "in"`
   └─ [2] `Command.in`
          └─ … (3 children)
   

   Note that stx[2] corresponds to the syntax tree of all but the first line of code. Also note that stx itself is just the Syntax.node corresponding to the root node of the tree. Syntax.node is defined as one of the possible values of the inductive type Syntax, and each Syntax.node comes with arguments info : SourceInfo, kind : SyntaxNodeKind, and args : Array Syntax (the node's children).

2. Lean calls elabCommandTopLevel stx, which, for our purposes, we can understand as calling elabCommand stx first, and then runLintersAsync stx (many details are omitted here):

   1. elabCommand stx: Since stx.getKind != nullKind, elabCommand calls expandMacroImpl? to check if there is a macro expander defined for stx's kind, and finds expandInCmd. It then runs expandInCmd stx to get stxNew:

      `null`
      ├─ [0] `Command.section`
      │      └─ … (3 children)
      ├─ [1] `Command.set_option`
      │      └─ … (4 children)
      ├─ [2] `Command.InternalSyntax.end_local_scope`
      │      └─ … (2 children)
      ├─ [3] `Command.in`
      │      └─ … (3 children)
      └─ [4] `Command.end`
            └─ … (2 children)
      

      stxNew would correspond to the following source code (written in diff notation to highlight the changes):

      - set_option A true in
      + section
      + set_option A true
      + end_local_scope 1
      open B in
      set_option C true in
      lemma something ‹binders› : ‹concl› := ‹value›
      + end
      

      Note that stxNew[3] = stx[2] remains unexpanded; expansion is performed one layer at a time. After expanding stx to stxNew, elabCommand calls elabCommand stxNew.

      1. elabCommand stxNew: Since stxNew.getKind == nullKind, elabCommand calls stxNew.getArgs.forM elabCommand. And so on. When elabCommand is called on a node for which a specialized elaborator exists, it will call that specialized elaborator. For the node kinds seen above, these specialized elaborators are elabSection, elabSetOption, elabEndLocalScope, and elabEnd (Command.in has no elaborator, but rather just the macro expander expandInCmd). The full tree of stxNew requires many more specialized elaborators still.

   2. runLintersAsync stx: By the time this call runs, stx has been fully processed by the elaborator and macro expander, which may well have modified the command state; in our example, we find that Command.State.env.constants.map₂[`something] now exists, and contains the ConstantInfo corresponding to the (fully elaborated) constant something that we declared. Nonetheless, stx still refers to the original syntax tree that the parser returned at the very beginning.

So generalizeTypeclasses.run has access to the syntax tree of the user's source code pre-elaboration (and thus also pre-expansion), while the command state within which generalizeTypeclasses.run runs also provides it with access to the fully elaborated declaration.

Main definitions

• generalizeTypeclasses: This is the structure that gets registered via initialize addLinter generalizeTypeclasses, and whose run function runs for every top-level command.
• lintTypeclassesFor: The function that computes, verifies, and emits the typeclass weakening suggestions.

def GeneralizationLinter.Frontend.generalizeTypeclasses : Lean.Linter

This is the structure that gets registered via initialize addLinter generalizeTypeclasses, and whose generalizeTypeclasses.run function runs for every top-level command.

For each command that generalizeTypeclasses.run is called on, it figures out whether it should run lintTypeclassesFor and, if so, sets up the DeclSource record that it needs and builds (or fetches from cache) the class graph.

Equations

• One or more equations did not get rendered due to their size.