feat: structure auto-completion & partial InfoTrees

[mhuisi]

This PR adds auto-completion for the fields of structure instance notation. Specifically, querying the completions via Ctrl+Space in the whitespace of a structure instance notation will now bring up the full list of fields. Whitespace structure completion can be enabled for custom syntax by wrapping the parser for the list of fields in a structInstFields parser.

This PR also makes completions of partial structure fields in the bracketed structure instance notation work again (e.g. completing a in { a }). These were previously broken by the introduction of set notation.

In order to facilitate language server support for ambiguous syntax where all associated elaborators fail, this PR introduces the notion of an InfoTree choice node and an InfoTree PartialTermInfo node. Choice nodes are produced by the elaborator when several overloaded elaborators fail and contain the InfoTrees of each failed elaborator as subtrees. PartialTermInfos are generated when an individual elaborator fails to produce an Expr so that the subtrees produced by that elaborator can be retained as children of that PartialTermInfo.

Since the InfoTree contains more similar CompletionInfos after the introduction of choice nodes, this PR reworks the CompletionInfo selection to be more effective at selecting the best CompletionInfo amongst multiple similar ones.

Finally, this PR splits Completion.lean into several files and fixes #5807.

Breaking changes

• Lean.Elab.withInfoContext' and Lean.Elab.Term.withInfoContext' gained a new parameter mkInfoOnError that is used to produce an InfoTree node when the elaborator x fails. In cases where mkInfo produces a TermInfo using Lean.Elab.Term.mkTermInfo, Lean.Elab.Term.withTermInfoContext' can be used instead of Lean.Elab.Term.withInfoContext'.
• Lean.Elab.Info gained two new alternatives: ofPartialTermInfo and ofChoiceInfo.
• The id field of the fieldId alternative of Lean.Elab.CompletionInfo has been turned into an Option with none representing a full field completion.
• The syntax of structInst and whereStructInst have been adjusted to use the structInstFields parser.

Details of other changes

• Init/Prelude.lean and Init/Meta.lean: Add two new functions getTrailing? and getTrailingTailPos? to work with the trailing whitespace of a SourceInfo / Syntax.
• Lean/Elab/App.lean:
  • Adjust dot completion of a.b.c so that the CompletionInfos for a.b.c reference the syntax a, a.b and a.b.c respectively, instead of all referencing a.b.c. Before, these CompletionInfos were indistinguishable and we only chose the right one by accident.
  • Adjust mergeFailures to produce an InfoTree with an ofChoiceInfo root node and the InfoTrees of all failed elaborators as subtrees instead of throwing them away.
• Lean/Elab/BuiltinTerm.lean: Adjust elabCompletion so that it always produces an identifier CompletionInfo, even when elaborating the left hand side of a dot completion succeeds and we also add a dot CompletionInfo to the InfoTree. With the changes to the CompletionInfo selection in the language server, the language server will now always pick the correct one of these two. Before, we had a special case in the language server dot completion where under certain circumstances we would treat it a dot completion as an identifier completion instead - with this change, this is now not necessary anymore.
• Lean/Elab/MutualDef.lean: Adjust expandWhereStructInst to set reasonable SourceInfos for the produced bracketed structure instance notation. The structure field completion benefits from this SourceInfo.
• Lean/Server/RequestHandling.lean: Adjust handleCompletion so that in the - completion case, we also emit CompletionInfoData. This fixes PANIC at Lean.Lsp.CompletionItem.getFileSource! Lean.Server.CompletionItemData:34:22: no data param on completion item  #5807.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0c190239a5e2d7f99413da0c54a575a0d0353b6 --onto 193b6f2bec332ac0bce33e10856a96163d4be456. (2024-10-25 09:39:39)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0c190239a5e2d7f99413da0c54a575a0d0353b6 --onto 4ee44ceb1d77f16b9b81bc655bc8b318cd6e8c4d. (2024-10-30 09:18:51)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f0c190239a5e2d7f99413da0c54a575a0d0353b6 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-30 15:00:29)
• 💥 Mathlib branch lean-pr-testing-5835 build failed against this PR. (2024-11-18 10:47:45) View Log
• 💥 Mathlib branch lean-pr-testing-5835 build failed against this PR. (2024-11-18 13:17:11) View Log
• ✅ Mathlib branch lean-pr-testing-5835 has successfully built against this PR. (2024-11-18 16:03:19) View Log

[digama0]

Does this work after def foo : MyStruct where and package foo where?

[mhuisi]

Does this work after def foo : MyStruct where and package foo where?

"Yes" to the first question, see the test file: https://github.com/mhuisi/lean4/blob/mhuisi/constructor-field-completion-2/tests/lean/interactive/completionStructureInstance.lean

It doesn't work in the second case because Lake config declarations are a separate command with its own syntax and its own elaborator. For now, whitespace completions are specific to certain syntaxes (before macro expansion).

[digama0]

Does this make it easy to implement the corresponding feature in lake? This has been a long standing feature request.

[mhuisi]

The whitespace completion triggers on the Lean.Parser.Command.whereStructInst parser. I don't know whether it makes sense for Lake to move its config declarations to this parser. (cc @tydeu)

[tydeu]

@mhuisi It don't think using whereStructInst directly is likely viable in Lake. Is there some standard way to emulate this behavior in a different elaborator?

[mhuisi]

@mhuisi It don't think using whereStructInst directly is likely viable in Lake. Is there some standard way to emulate this behavior in a different elaborator?

No, there is not.

[tydeu]

@mhuisi Ah, so this new completion is hardcoded to the parser and is not a matter of creating the right info-tree nodes?

(I guess that is what you meant by "whitespace completions are specific to certain syntax" -- I was not fully sure whether that was simply due to support rather than hardcoding.)

[mhuisi]

@tydeu @digama0 I've adjusted the implementation so that Lake can enable support for whitespace structure completion.