Finding syntax

Stream: general

[Damiano Testa]

I wrote a very naive #find_syntax command, since this comes up every once in a while (e.g. it came up at the last community meeting). You can see below the implementation and the output on searching for ∘.

import Mathlib

namespace Mathlib.FindSyntax

open Lean Elab Command

def extractSymbols : Expr → Array Expr
  | .app a b =>
    let rest := extractSymbols a ++ extractSymbols b
    match a.constName with
      | ``Lean.ParserDescr.symbol | ``Lean.ParserDescr.nonReservedSymbol => rest.push b
      | _ => rest
  | .letE _ a b c _ => extractSymbols a ++ extractSymbols b ++ extractSymbols c
  | .lam _ a b _ => extractSymbols a ++ extractSymbols b
  | .forallE _ a b _ => extractSymbols a ++ extractSymbols b
  | .mdata _ a => extractSymbols a
  | .proj _ _ a => extractSymbols a
  | _ => #[]

def litToString : Expr → String
  | .lit (.natVal v) => s!"{v}"
  | .lit (.strVal v) => v
  | _ => ""

elab "#find_syntax " id:str : command => do
  let prsr : Array Expr := #[.const ``Lean.ParserDescr [], .const ``TrailingParserDescr []]
  let mut hs : Std.HashSet Expr := {}
  let mut symbs : Std.HashSet (Name × Array Expr) := {}
  for (_declName, cinfo) in (← getEnv).constants do
    if prsr.contains cinfo.type && cinfo.hasValue then
      hs := hs.insert cinfo.value!
      let ls := extractSymbols cinfo.value!
      if !cinfo.name.isInternal && !ls.isEmpty then symbs := symbs.insert (cinfo.name, ls)
  let mut msgs := #[]
  for (nm, ar) in symbs.toList do
    let rem : String := " _ ".intercalate (ar.map litToString).toList
    if 2 ≤ (rem.splitOn id.getString).length then
      msgs := msgs.push <| .ofConstName nm ++ m!":\n  '{rem.trim}'\n"
  let uses := msgs.size
  let head := m!"Found {uses} use{if uses == 1 then "" else "s"} \
                among {symbs.size} syntax declarations"
  logInfo <| .joinSep (head::(msgs.push "").toList) "\n---\n\n"

end Mathlib.FindSyntax

#find_syntax "∘"
/-
Found 5 uses among 1455 syntax declarations
---

Function.«term_∘'_»:
  '∘''
---

ContinuousLinearMap.«term_∘L_»:
  '∘L'
---

LinearMap.compNotation:
  '∘ₗ'
---

ProbabilityTheory.«term_∘ₖ_»:
  '∘ₖ'
---

«term_∘_»:
  '∘'
---
-/

[Damiano Testa]

If you find it useful, I can think about how to produce better "usage reports".

[Kyle Miller]

If you use {MessageData.ofConstName nm} you can do "go to definition" on it in the output.

[Damiano Testa]

Ah, that's awesome! I was wondering how to hook into "Go to definition"! I had tried realize...WithInfo to no avail.

[Kyle Miller]

We're looking at making {nm} automatically create "go to definition" links when nm is a constant. (This might be "too convenient" though, since not every name is meant to be a constant...)

[Damiano Testa]

If the doc-strings of realizeGlobalConstant and resolveGlobal... mentioned how to get the "Go to def" behaviour, that would already be great! I had no idea where to look for this, except for hoping that withInfo would magically do it for me.

[Damiano Testa]

I updated the code above and it works great! Btw, I do not know if this is intended or not, but a lot of the term... declaration have default range, so "Go to definition" takes you to the right file, but not to the position of the syntax declaration.

[Damiano Testa]

(I actually exploit this in the duplicated underscore linter, so if this is something requiring a fix, then I'll have to think of a different way of automatically ignoring such declarations in the linter.)

[Damiano Testa]

Rather than leaving it just in Zulip, I PRed it: #17986. Comments are very welcome!