Delaboration of constants in function applications #911
Conversation
This was the It would be cool if we had tests for that (like |
|
The first place where they were dropped was in automatically generated delaborators for syntax that was defined using |
hargoniX
force-pushed
the
const-delab
branch
from
54c1c34
to
22d803c
Compare
| @@ -90,6 +90,11 @@ register_builtin_option pp.safeShadowing : Bool := { | |||
| group := "pp" | |||
| descr := "(pretty printer) allow variable shadowing if there is no collision" | |||
| } | |||
| register_builtin_option pp.tagSymbols : Bool := { | |||
There was a problem hiding this comment.
The name here is a bit misleading, the option does not only affect symbols (which I associate with +, etc.) but any head symbol (such as f in f a b). The terminology isn't great, we have lots of things that are called symbols.
There was a problem hiding this comment.
Maybe tagAllFunctions ?
There was a problem hiding this comment.
The All seems redundant. How about tagAppFns, in reference to Expr.getAppFn?
There was a problem hiding this comment.
Would also be good to have a comment that if the constant is not part of an application, the tagging is unconditionally done by delabFor.
|
nit: you shouldn't capitalize the first word in commit messages |
Add an option called pp.tagSymbols which, if set, makes the delaborator add term information to all symbols it can during delaboration. This option is disabled per default because it would break the LSP server's hovering behaviour. It is however useful when for example automatically generating interactive documentation.
Previously automatically generated delaborators for syntax declared with the notation (and derived) keywords would silently drop information during delaboration.
hargoniX
force-pushed
the
const-delab
branch
3 times, most recently
from
36ff74a
to
1ee2d89
Compare
src/Lean/Elab/Notation.lean
Outdated
| `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] | ||
| aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun | ||
| | `($$(_):ident $args*) => `($pat) | ||
| | _ => throw ()) | ||
| | `($$fun_ref:ident $args*) => withRef fun_ref `($pat) |
There was a problem hiding this comment.
That doesn't match our naming convention, let's go with just f? Same below. And mind the indentation.
There was a problem hiding this comment.
By the way, the why I was missing yesterday is that the quotation uses the reference as the source location of any newly introduced identifiers, which in this case is the function head.
| @@ -90,6 +90,11 @@ register_builtin_option pp.safeShadowing : Bool := { | |||
| group := "pp" | |||
| descr := "(pretty printer) allow variable shadowing if there is no collision" | |||
| } | |||
| register_builtin_option pp.tagSymbols : Bool := { | |||
There was a problem hiding this comment.
The All seems redundant. How about tagAppFns, in reference to Expr.getAppFn?
| @@ -90,6 +90,11 @@ register_builtin_option pp.safeShadowing : Bool := { | |||
| group := "pp" | |||
| descr := "(pretty printer) allow variable shadowing if there is no collision" | |||
| } | |||
| register_builtin_option pp.tagSymbols : Bool := { | |||
There was a problem hiding this comment.
Would also be good to have a comment that if the constant is not part of an application, the tagging is unconditionally done by delabFor.
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
The ppNotationCode.lean test failed because the output of the notation elaborator changed (purposely), adapt it to the new output.
hargoniX
force-pushed
the
const-delab
branch
from
1ee2d89
to
4c47942
Compare
| | `($$(_):ident) => `($pat) | ||
| | _ => throw ()) | ||
| | `($$f:ident) => withRef f `($pat) | ||
| | _ => throw ()) | ||
| | _ => failure |
There was a problem hiding this comment.
Now I'm unsure with the indentation here, is this correct? Should it be further to the left? Is there some written down style guide for this?
|
Merged manually |
As described in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Function.20application.20delaboration it would be nice to be able to (optionally) add info tags to the syntactic node representing the function in a function application, instead of just the entire function application, for automatic documentation generation purposes. However this would break the LSP's hovering behavior so this feature is disabled per default. Furthermore this PR fixes a few bugs along the delaboration/formatting pipeline which dropped the generated information at two places.