Change elaboration of `example`

Stream: metaprogramming / tactics

[Christian Merten]

I want example to add a declaration to the environment with an automatically generated name, so that I can access it later for further processing.

For this I tried the following very naive attempt: Essentially it is a macro that replaces example by def with an auto-generated name:

import Batteries
open Lean Elab Command

syntax (name := eExampleS) "eExample" " : "? term:10? " := " term:11 : command

macro_rules
  | `(example := $r) => `(eExample := $r)
  | `(example : $t := $r) => `(eExample : $t := $r)

def newLocalName : CommandElabM Name := do
  let decls ← liftCoreM Batteries.Tactic.Lint.getDeclsInCurrModule
  return s!"name_{(decls.filter fun name ↦ ¬ (name.isInternal)).size}".toName

def eExampleExpander : Syntax → CommandElabM Syntax
  | `(eExample : $t := $r) => do
      `(def $(mkIdent (← newLocalName)) : $t := $r)
  | `(eExample := $r) => do
      `(def $(mkIdent (← newLocalName)) := $r)
  | _ => throwUnsupportedSyntax

@[command_elab eExampleS]
def eExampleElab : CommandElab := adaptExpander eExampleExpander

-- work
example : Nat := 3
example := 3
-- does not work
example (_ : False) : 1 = 1 := rfl

elab "#alldecls" : command => do
  let decls ← liftCoreM Batteries.Tactic.Lint.getDeclsInCurrModule
  logInfo s!"{decls.filter fun name ↦ ¬ (name.isInternal)}"

#alldecls

The issue is that this only works for a small subset of the syntax supported by the example command. Certainly it is possible to extend this to eventually match all possible cases, but I would rather have a more principled solution that uses the example parser directly. I found docs#Lean.Parser.Command.example, but I have no idea how to use this to write a macro / elaborator that does the above.

[Christian Merten]

(side note: I tried to get rid of the additional eExample step with elab_rules, but I could not figure out how to hook eExampleExpander into that.)

[Damiano Testa]

What does this do that theorem does not do? Is it simply giving the declaration a name that you do not know what it is?

[Christian Merten]

The usecase is the following: I am given a file with a bunch of examples (and regular theorems, defs) and I need to inspect all declarations including examples in this file. I could of course do some manual, text-based preprocessing to turn all examples into defs or theorems and then run the inspection, but I would rather just import a file at the top that changes how example elaborates without touching the actual code.

[Christian Merten]

(This depends on my assumption that there is no way to inspect examples, because they don't change the environment. If there is a way to do that directly, without changing the elaboration of example, that would of course be better)

[Damiano Testa]

What kind of inspection do you want to do?

[Damiano Testa]

Also, you can take a look at Mathlib/Tactic/SuppressCompilation.lean to see how suppress_compilation parses examples.

[Christian Merten]

Damiano Testa said:

What kind of inspection do you want to do?

I have a list of pairs of type signatures and a list of allowed axioms and I need to check if the input file contains a declaration for every entry in that list (i.e. a declaration with the given type signature) and if that declaration uses no other axioms besides the allowed axioms.

[Christian Merten]

Damiano Testa said:

Also, you can take a look at Mathlib/Tactic/SuppressCompilation.lean to see how suppress_compilation parses examples.

Ah, thanks! This looks promising. I will report back if I could get it to work from there.

[Christian Merten]

Indeed, copy pasting from Mathlib/Tactic/SuppressCompilation.lean worked:

import Batteries
import Lean

open Lean Elab Command

def newLocalName : CommandElabM Name := do
  let decls ← liftCoreM Batteries.Tactic.Lint.getDeclsInCurrModule
  return s!"name_{(decls.filter fun name ↦ ¬ (name.isInternal)).size}".toName

@[command_elab declaration]
def replaceExampleByDef : CommandElab := fun
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $[noncomputable]? $(unsafe?)?
    $(recKind?)? example $sig:optDeclSig $val:declVal) => do
  let name ← newLocalName
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? noncomputable $(unsafe?)?
    $(recKind?)? def $(mkIdent name) $sig:optDeclSig $val:declVal)
| _ => throwUnsupportedSyntax

example : Nat := 3
example := 3
example (_ : False) : 1 = 1 := rfl

elab "#alldecls" : command => do
  let decls ← liftCoreM Batteries.Tactic.Lint.getDeclsInCurrModule
  logInfo s!"{decls.filter fun name ↦ ¬ (name.isInternal)}"

#alldecls

Thanks again Damiano.

[Damiano Testa]

Looking quickly at the code above, you seem to have made all "new" declarations noncomputable (which is a goal of suppress_compilation), but maybe you want to preserve the same noncomputable flag in your use-case?

[Christian Merten]

Oops, yes that was not intended, this should be correct:

@[command_elab declaration]
def replaceExampleByDef : CommandElab := fun
| `($[$doc?:docComment]? $(attrs?)? $(vis?)? $(noncomputable?)? $(unsafe?)?
    $(recKind?)? example $sig:optDeclSig $val:declVal) => do
  let name ← newLocalName
  elabDeclaration <| ← `($[$doc?:docComment]? $(attrs?)? $(vis?)? $(noncomputable?)? $(unsafe?)?
    $(recKind?)? def $(mkIdent name) $sig:optDeclSig $val:declVal)
| _ => throwUnsupportedSyntax

[Kyle Miller]

Instead of newLocalName, there's mkAuxName `example 1, which will generate a name like example_5, guaranteed to be unused.

[Damiano Testa]

The matching can probably be simplified to

@[command_elab declaration]
def replaceExampleByDef : CommandElab := fun
| `($dms:declModifiers example $sig:optDeclSig $val:declVal) => do
  let name ← newLocalName
  elabDeclaration <| ← `($dms:declModifiers def $(mkIdent name) $sig:optDeclSig $val:declVal)
| _ => throwUnsupportedSyntax

[Christian Merten]

Yes, that works and is quite a bit more readable, thanks. While checking that things still work, I noticed that private declarations (also def) don't show up in my #alldecls command from above, because they are filtered out by ¬ name.isInternal.

Is there a more robust way to query all top level, user accessible declarations of a file, including private ones? Just getDeclsInCurrModule returns many auxiliary declarations.

[Damiano Testa]

Maybe you can look in Batteries/Tactic/OpenPrivate.lean for private? :smile:

[Kyle Miller]

Or maybe use Lean.isPrivateName to unfilter out what's filtered out by isInternal?

[Kyle Miller]

like Lean.isPrivateName n || !n.isInternal

[Christian Merten]

Kyle Miller said:

like Lean.isPrivateName n || !n.isInternal

This is probably good enough for my purposes, but now contains all internal declarations of private declarations, because also _private.foo._cstage1 satisfies Lean.isPrivateName.

[Damiano Testa]

Since you are already redefining the elaboration of some declarations, maybe you can redefine them all (like in suppress_compilation) and, after each declaration has been elaborated append the type signature and axioms to an environment extension.

[Damiano Testa]

After that, the environment extension only contains what you added.

[Christian Merten]

That sounds like a good idea! I'll try it out.

[Kyle Miller]

@Christian Merten Ok, then theres docs#Lean.privateToUserName?

Something like let n' := (Lean.privateToUserName? n).getD n; !n'.isInternal should work better.

[Christian Merten]

That works perfectly, thanks Kyle!

[Christian Merten]

Damiano Testa said:

Since you are already redefining the elaboration of some declarations, maybe you can redefine them all (like in suppress_compilation) and, after each declaration has been elaborated append the type signature and axioms to an environment extension.

I gave this a try. The main issue is that I can't figure out how to properly access the name of the added declaration. Right now I am doing this:

import Lean
import Batteries

open Lean Elab Command Batteries

def Lean.Name.isRelevant (name : Name) : Bool :=
  !((Lean.privateToUserName? name).getD name).isInternal

@[command_elab declaration]
def appendDeclInfoDemo : CommandElab := fun
| `($dms:declModifiers example $sig:optDeclSig $val:declVal) => do
  let declName ← mkAuxName `example 1
  elabDeclaration <| ← `($dms:declModifiers def $(mkIdent declName) $sig:optDeclSig $val:declVal)
  logInfo s!"added {declName}"
| stx => do
  let allDeclsBefore := (← liftCoreM <| Tactic.Lint.getDeclsInCurrModule).filter Name.isRelevant
  elabDeclaration stx
  let allDeclsAfter := (← liftCoreM <| Tactic.Lint.getDeclsInCurrModule).filter Name.isRelevant
  let newDecls := allDeclsAfter.filter (fun x ↦ x ∉ allDeclsBefore)
  let declName : Name := newDecls.toList.head!
  logInfo s!"added {declName}"

def foo (_ : False) : Nat := 3
example : Nat := 3

This seems to work, but is certainly not very robust. Is there a better way?

[Damiano Testa]

Here is a possible alternative approach:

import Lean
import Batteries

open Lean Elab Command Batteries

def Lean.Name.isRelevant (name : Name) : Bool :=
  !((Lean.privateToUserName? name).getD name).isInternal

partial
def scanInfoTree : InfoTree → NameSet
  | .context (.parentDeclCtx i) t => (scanInfoTree t).insert i
  | .context _ t => scanInfoTree t
  | .node _ ts => ts.foldl (·.union <| scanInfoTree ·) ∅
  | .hole .. => ∅

def getAllNames (ts : PersistentArray InfoTree) : NameSet :=
  ts.map scanInfoTree |>.foldl .union ∅

@[command_elab declaration]
def appendDeclInfoDemo : CommandElab := fun
| `($dms:declModifiers example $sig:optDeclSig $val:declVal) => do
  let declName ← mkAuxName `example 1
  elabDeclaration <| ← `($dms:declModifiers def $(mkIdent declName) $sig:optDeclSig $val:declVal)
  let ts ← getInfoTrees
  dbg_trace "Using `InfoTree`s: {(getAllNames ts).toArray}"
  logInfo s!"added {declName}"
| stx => do
  let allDeclsBefore := (← liftCoreM <| Tactic.Lint.getDeclsInCurrModule).filter Name.isRelevant
  elabDeclaration stx
  let ts ← getInfoTrees
  dbg_trace "Using `InfoTree`s: {(getAllNames ts).toArray}"
  let allDeclsAfter := (← liftCoreM <| Tactic.Lint.getDeclsInCurrModule).filter Name.isRelevant
  let newDecls := allDeclsAfter.filter (fun x ↦ x ∉ allDeclsBefore)
  let declName : Name := newDecls.toList.head!
  logInfo s!"added {declName}"

def foo (_ : False) : Nat := 3

example : True := trivial

namespace X
example : True := trivial
end X

namespace Y
instance : ToString Nat where toString _ := ""
end Y

namespace _root_
theorem _root_.InRoot : True := trivial
theorem InRoot : True := trivial -- panic!
end _root_

[Damiano Testa]

I have not seen an example where the NameSet that getAllNames returns consists of more than a single name, but I honestly do not understand InfoTrees enough to know whether this is just me not trying hard enough or whether it is a structural property.

[Damiano Testa]

If you can guarantee that the NameSet consists of a single name, then you can avoid traversing all of the InfoTree and simply return the first (non-anonymous?) name that it finds.

[Damiano Testa]

It also just occurred to me that the above will ignore entirely mutual definitions: I do not know if this is something that is relevant in your use-case or not.

[Christian Merten]

Thanks, that looks quite a bit better, although I understand less what is going on :) Do I understand correctly that the (or one of the) PartialContextInfos will be of the form .parentDeclCtx parentDecl where parentDecl is the name of the added declaration? I am surprised by the fact that this information leaks out of the call to elabDeclaration.

[Christian Merten]

Damiano Testa said:

It also just occurred to me that the above will ignore entirely mutual definitions: I do not know if this is something that is relevant in your use-case or not.

For now, ignoring mutual defs is fine for my use case.

[Damiano Testa]

Christian Merten said:

Thanks, that looks quite a bit better, although I understand less what is going on :smile: Do I understand correctly that the (or one of the) PartialContextInfos will be of the form .parentDeclCtx parentDecl where parentDecl is the name of the added declaration? I am surprised by the fact that this information leaks out of the call to elabDeclaration.

I think that this is correct, but I am not entirely sure. My vague understanding is that a parentDecl in PartialContextInfo contains the name of the declaration that is currently being elaborated. I would hope that such a node is always present when you are elaborating a declaration!

[Christian Merten]

So elabDeclaration is updating the info tree with this information somewhere?

[Damiano Testa]

I think that everything that elaborates anything is expected to update the infotrees. I even think that if it does not, then it might be considered a bug!

[Damiano Testa]

The information that is stored in the infotrees is used, I think, by the hover information and if you hover over the name of a declaration, you see it's fully-qualified name. This suggests to me that some node of the infotree will contain that information.

[Damiano Testa]

I have a conjecture that any information that you may want to extract from lean code you can extract from the infotrees.

[Christian Merten]

Damiano Testa said:

I think that everything that elaborates anything is expected to update the infotrees. I even think that if it does not, then it might be considered a bug!

But this is up to the implementation of the specific elaborator and not automatically done by the elab or @[command_elab] infrastructure, right? Moving your

  let ts ← getInfoTrees
  dbg_trace "Using `InfoTree`s: {(getAllNames ts).toArray}"

before elabDeclaration yields an empty output.

[Damiano Testa]

Ah, yes, I probably expressed myself badly: you should expect the infotrees to be updated by elabDeclaration (or rather some of the inner elabXXX that elabDeclaration calls. There, I was piggy-backing the infotrees that elabDeclaration updated. Until you call elabDeclaration the infotrees for the declaration have not yet been created.

[Damiano Testa]

elabDeclaration also takes care of updating the environment, which is what you were exploiting in your code: you were storing the declarations before elaboration and comparing them to the ones after.

[Damiano Testa]

In the "after" world, besides the change in the environment, there are also infotrees to play with.

[Damiano Testa]

When I talked about it being a bug not updating the infotrees, I meant that the low-level elabXXX should do that for you, not that you should be doing that yourself.

[Damiano Testa]

(Also, do not take what I said too literally, since a lot about infotrees is obscure to me!)

[Christian Merten]

Thanks for the explanations, Damiano. That makes it a lot clearer.

[Christian Merten]

Kyle Miller said:

Instead of newLocalName, there's mkAuxName `example 1, which will generate a name like example_5, guaranteed to be unused.

This does not seem to interact well with namespaces, for example:

import Lean

open Lean Elab Command

@[command_elab declaration]
def replaceExampleByDef : CommandElab := fun
| `($dms:declModifiers example $sig:optDeclSig $val:declVal) => do
  let name ← mkAuxName `example 1
  elabDeclaration <| ← `($dms:declModifiers def $(mkIdent name) $sig:optDeclSig $val:declVal)
| _ => throwUnsupportedSyntax

namespace Foo

example : True := sorry
/--
error: 'Foo.example_1' has already been declared
-/
#guard_msgs in
example : True := sorry

end Foo

How do I make mkAuxName namespace aware? My guess is that the check here does not first resolve the namespace of candidate, hence it sees that example_1 does not exist, so it returns that name, which is then added as Foo.example_1 by elabDeclaration.
(For now, I just went back to my naive newLocalName, but I would like to know how to do it properly)

[Kyle Miller]

If you do let name ← `_root_ ++ mkAuxName `example 1, I think it should work. That would have it always go into the root namespace.

Or, you could do something like

let baseName := (<- getCurrNamespace) ++ `example
let name <- mkAuxName (`_root_ ++ baseName) 1

if you want it to be inside the namespace.

[Christian Merten]

You probably meant let name := `_root_ ++ (← mkAuxName `example 1) which works, thanks! The second one fails with the same error as above, though.

[Kyle Miller]

Yes, that was a mistake!

[Kyle Miller]

The second one should be

let baseName := (<- getCurrNamespace) ++ `example
let name := `_root_ ++ (<- mkAuxName baseName 1)

[Christian Merten]

Thanks!