Extend getParamNames

Stream: Is there code for X?

[Yicheng Tao]

I was working on extracting the arg array of a constant. I found the function getParamNames in the library.

/-- Return the parameter names for the given global declaration. -/
def getParamNames (declName : Name) : MetaM (Array Name) := do
  forallTelescopeReducing (← getConstInfo declName).type fun xs _ => do
    xs.mapM fun x => do
      let localDecl ← x.fvarId!.getDecl
      return localDecl.userName

I was trying to make it return not only the userName, but also the type. But the types that depending on local variable appears in the form like _uniq.3 if I simply use localDecl.type.

How to do it correctly?

[Eric Wieser]

Can you un- #xy ?

[Yicheng Tao]

I have the fullname of a constant and an Environment. What I want to get is the arg array of that constant.

E.g.:

theorem test {P Q : Prop} (p : P) : P := p

I have the fullname test and the environment. I want the desired function getParam to return the arg array as #[(P, Prop), (Q, Prop), (p, P)]. The signature of the function would be Name -> Array (String × String).

[Daniel Weber]

If you want to obtain a string you should take a look at docs#Lean.PrettyPrinter.Delaborator.delabConstWithSignature

[Yicheng Tao]

Daniel Weber said:

If you want to obtain a string you should take a look at docs#Lean.PrettyPrinter.Delaborator.delabConstWithSignature

I found doc-gen4 also use delaborator, but it will exceed time limit for some constants. I'm looking for some other way.

[Daniel Weber]

I don't think there are other ways to convert an Expr to a String (assuming you don't want to output the whole expression), perhaps you can find the Syntax where it's defined, but that'll be problematic with variable, local notation, etc.

[Yicheng Tao]

Too bad. I didn't expect it to be that complicated.

[Daniel Weber]

Why does the delaborator time out? Do you have a #mwe?

[Yicheng Tao]

It's hard to extract a #mwe from my code. I was modifying the ExtractData.lean script from LeanDojo. It processes the files in Mathlib one by one. Here is some relevant code:

import Lean
import Lake

namespace DocGen

open Lean Widget Meta
/--
Stores information about a typed name.
-/
structure NameInfo where
  /--
  The name that has this info attached.
  -/
  name  : Name
  /--
  The pretty printed type of this name.
  -/
  type : CodeWithInfos
  deriving Inhabited


/--
An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
-/
structure Arg where
  /--
  The pretty printed binder syntax itself.
  -/
  binder : CodeWithInfos
  /--
  Whether the binder is implicit.
  -/
  implicit : Bool


/--
A base structure for information about a declaration.
-/
structure Info extends NameInfo where
  /--
  The list of arguments to the declaration.
  -/
  args : Array Arg
  deriving Inhabited

/--
Pretty prints a `Lean.Parser.Term.bracketedBinder`.
-/
private def prettyPrintBinder (stx : Syntax) (infos : SubExpr.PosMap Elab.Info) : MetaM Widget.CodeWithInfos := do
  let fmt ← PrettyPrinter.format Parser.Term.bracketedBinder.formatter stx
  let tt := Widget.TaggedText.prettyTagged fmt
  let ctx := {
    env := ← getEnv
    mctx := ← getMCtx
    options := ← getOptions
    currNamespace := ← getCurrNamespace
    openDecls := ← getOpenDecls
    fileMap := default,
    ngen := ← getNGen
  }
  return Widget.tagCodeInfos ctx infos tt

private def prettyPrintTermStx (stx : Term) (infos : SubExpr.PosMap Elab.Info) : MetaM Widget.CodeWithInfos := do
  let fmt ← PrettyPrinter.formatTerm stx
  let tt := Widget.TaggedText.prettyTagged fmt
  let ctx := {
    env := ← getEnv
    mctx := ← getMCtx
    options := ← getOptions
    currNamespace := ← getCurrNamespace
    openDecls := ← getOpenDecls
    fileMap := default,
    ngen := ← getNGen
  }
  return Widget.tagCodeInfos ctx infos tt

def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
  let e := Expr.const v.name (v.levelParams.map mkLevelParam)
  println! s!"{v.name}"
  -- Use the main signature delaborator. We need to run sanitization, parenthesization, and formatting ourselves
  -- to be able to extract the pieces of the signature right before they are formatted
  -- and then format them individually.
  let (sigStx, infos) ← PrettyPrinter.delabCore e (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
  let sigStx := (sanitizeSyntax sigStx).run' { options := (← getOptions) }
  let sigStx ← PrettyPrinter.parenthesize PrettyPrinter.Delaborator.declSigWithId.parenthesizer sigStx
  let `(PrettyPrinter.Delaborator.declSigWithId| $_:term $binders* : $type) := sigStx
    | throwError "signature pretty printer failure for {v.name}"
  let args ← binders.mapM fun binder => do
    let fmt ← prettyPrintBinder binder infos
    return Arg.mk fmt (!binder.isOfKind ``Parser.Term.explicitBinder)
  let type ← prettyPrintTermStx type infos
  return {
    toNameInfo := { name := v.name, type },
    args,
  }
end DocGen

...

/--
Extract premise information from `TermInfo` in `InfoTree`.
-/
private def visitTermInfo (ti : TermInfo) (env : Environment) : TraceM Unit := do
  let some fullName := ti.expr.constName? | return ()
  let fileMap ← getFileMap
  let some const := env.constants.find? fullName | return ()
  let info ← withEnv env $ DocGen.Info.ofConstantVal const.toConstantVal
  let args := info.args.map (fun arg => arg.binder.pretty)
  let type := info.type.pretty
  ...

This is only part of the code. The process visits every term in that file. I just try to print the constant which caused the time out, but I found that it succeeds when be processed individually. I guess the delaborator's time may be accumulated when processing the whole file?

[Yicheng Tao]

I wonder how to set the maxHeartbeats to be higher. The default is 200000 and I failed to set it with set_option.

[Yicheng Tao]

Here is the error message:

uncaught exception: (deterministic) timeout at `delab`, maximum number of heartbeats (200000) has been reached
Use `set_option maxHeartbeats <num>` to set the limit.(invalid MessageData.lazy, missing context)

[Damiano Testa]

What is the error when you try, say set_option maxHeartbeats 0?

[Yicheng Tao]

set_option maxHeartbeats doesn't work. The scripts is a independent file in the project and is ran by using lake env lean --run.

[Yicheng Tao]

It seems that this option should be passed in another way.

[Damiano Testa]

You should place it in the file where you want it to take effect and its effect start from the set_option line.

[Damiano Testa]

You can limit it to the next declaration via set_option ... in <command>.

[Yicheng Tao]

Oh I found the place where I can modify the config.

[Yicheng Tao]

For someone who may be interested:

let (trace, _) ← traceM.run'.toIO {fileName := s!"{path}", fileMap := FileMap.ofString input, maxHeartbeats := 2000000000} {env := env}

[Yicheng Tao]

And it's weird that the 2000000000 here seems to be 2000000 in error message.

[Damiano Testa]

There are two "levels" of heartBeats: an "internal" one that is more fine-grained and a "user-facing" one that is <internal>/10^3.