From cb0284f98e474d329dbfbb833b489959074b2b0e Mon Sep 17 00:00:00 2001 From: Marc Huisinga Date: Tue, 3 Jun 2025 19:26:33 +0200 Subject: [PATCH] feat: signature help (#8511) This PR implements signature help support. When typing a function application, editors with support for signature help will now display a popup that designates the current (remaining) function type. This removes the need to remember the function signature while typing the function application, or having to constantly cycle between hovering over the function identifier and typing the application. In VS Code, the signature help can be triggered manually using `Ctrl+Shift+Space`. ![Demo](https://github.com/user-attachments/assets/d1f6ed79-bb16-4593-8d28-68b1cce5d5dc) ### Other changes - In order to support signature help for the partial syntax `f a <|` or `f a $`, these notations now elaborate as `f a`, not `f a .missing`. - The logic in `delabConstWithSignature` that delaborates parameters is factored out into a function `delabForallParamsWithSignature` so that it can be used for arbitrary `forall`s, not just constants. - The `InfoTree` formatter is adjusted to produce output where it is easier to identify the kind of `Info` in the `InfoTree`. - A bug in `InfoTree.smallestInfo?` is fixed so that it doesn't panic anymore when its predicate `p` does not ensure that both `pos?` and `tailPos?` of the `Info` are present. --- src/Init/Notation.lean | 34 ++- src/Lean/Data/Lsp/Capabilities.lean | 1 + src/Lean/Data/Lsp/LanguageFeatures.lean | 68 ++++++ src/Lean/Elab/InfoTree/Main.lean | 32 +-- src/Lean/Elab/InfoTree/Types.lean | 1 - .../PrettyPrinter/Delaborator/Builtins.lean | 57 +++-- src/Lean/Server/FileSource.lean | 3 + .../Server/FileWorker/RequestHandling.lean | 15 ++ src/Lean/Server/FileWorker/SignatureHelp.lean | 205 ++++++++++++++++++ src/Lean/Server/InfoUtils.lean | 8 +- src/Lean/Server/Watchdog.lean | 3 + tests/lean/binopInfoTree.lean.expected.out | 110 +++++----- tests/lean/interactive/signatureHelp.lean | 144 ++++++++++++ .../signatureHelp.lean.expected.out | 139 ++++++++++++ tests/lean/run/info_trees.lean | 66 +++--- 15 files changed, 755 insertions(+), 131 deletions(-) create mode 100644 src/Lean/Server/FileWorker/SignatureHelp.lean create mode 100644 tests/lean/interactive/signatureHelp.lean create mode 100644 tests/lean/interactive/signatureHelp.lean.expected.out diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index f9247cd26e..c98d3003ba 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -531,8 +531,21 @@ is interpreted as `f (g x)` rather than `(f g) x`. syntax:min term " <| " term:min : term macro_rules - | `($f $args* <| $a) => `($f $args* $a) - | `($f <| $a) => `($f $a) + | `($f $args* <| $a) => + if a.raw.isMissing then + -- Ensures that `$f $args* <|` is elaborated as `$f $args*`, not `$f $args* sorry`. + -- For the latter, the elaborator produces `TermInfo` where the missing argument has already + -- been applied as `sorry`, which inhibits some language server functionality that relies + -- on this `TermInfo` (e.g. signature help). + -- The parser will still produce an error for `$f $args* <|` in this case. + `($f $args*) + else + `($f $args* $a) + | `($f <| $a) => + if a.raw.isMissing then + `($f) + else + `($f $a) /-- Haskell-like pipe operator `|>`. `x |> f` means the same as the same as `f x`, @@ -553,8 +566,21 @@ is interpreted as `f (g x)` rather than `(f g) x`. syntax:min term atomic(" $" ws) term:min : term macro_rules - | `($f $args* $ $a) => `($f $args* $a) - | `($f $ $a) => `($f $a) + | `($f $args* $ $a) => + if a.raw.isMissing then + -- Ensures that `$f $args* $` is elaborated as `$f $args*`, not `$f $args* sorry`. + -- For the latter, the elaborator produces `TermInfo` where the missing argument has already + -- been applied as `sorry`, which inhibits some language server functionality that relies + -- on this `TermInfo` (e.g. signature help). + -- The parser will still produce an error for `$f $args* <|` in this case. + `($f $args*) + else + `($f $args* $a) + | `($f $ $a) => + if a.raw.isMissing then + `($f) + else + `($f $a) @[inherit_doc Subtype] syntax "{ " withoutPosition(ident (" : " term)? " // " term) " }" : term diff --git a/src/Lean/Data/Lsp/Capabilities.lean b/src/Lean/Data/Lsp/Capabilities.lean index 53f3c6ea58..c54a15b328 100644 --- a/src/Lean/Data/Lsp/Capabilities.lean +++ b/src/Lean/Data/Lsp/Capabilities.lean @@ -100,6 +100,7 @@ structure ServerCapabilities where semanticTokensProvider? : Option SemanticTokensOptions := none codeActionProvider? : Option CodeActionOptions := none inlayHintProvider? : Option InlayHintOptions := none + signatureHelpProvider? : Option SignatureHelpOptions := none deriving ToJson, FromJson end Lsp diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index b79a6cce19..8f55fa96e0 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -521,5 +521,73 @@ structure InlayHintOptions extends WorkDoneProgressOptions where resolveProvider? : Option Bool := none deriving FromJson, ToJson +inductive ParameterInformationLabel + | name (name : String) + | range (startUtf16Offset endUtf16Offset : Nat) + +instance : FromJson ParameterInformationLabel where + fromJson? + | .str name => .ok <| .name name + | .arr #[startUtf16OffsetJson, endUtf16OffsetJson] => do + return .range (← fromJson? startUtf16OffsetJson) (← fromJson? endUtf16OffsetJson) + | _ => .error "unexpected JSON for `ParameterInformationLabel`" + +instance : ToJson ParameterInformationLabel where + toJson + | .name name => .str name + | .range startUtf16Offset endUtf16Offset => .arr #[startUtf16Offset, endUtf16Offset] + +structure ParameterInformation where + label : ParameterInformationLabel + documentation? : Option MarkupContent := none + deriving FromJson, ToJson + +structure SignatureInformation where + label : String + documentation? : Option MarkupContent := none + parameters? : Option (Array ParameterInformation) := none + activeParameter? : Option Nat := none + deriving FromJson, ToJson + +structure SignatureHelp where + signatures : Array SignatureInformation + activeSignature? : Option Nat := none + activeParameter? : Option Nat := none + deriving FromJson, ToJson + +inductive SignatureHelpTriggerKind where + | invoked + | triggerCharacter + | contentChange + +instance : FromJson SignatureHelpTriggerKind where + fromJson? + | (1 : Nat) => .ok .invoked + | (2 : Nat) => .ok .triggerCharacter + | (3 : Nat) => .ok .contentChange + | _ => .error "Unexpected JSON in `SignatureHelpTriggerKind`" + +instance : ToJson SignatureHelpTriggerKind where + toJson + | .invoked => 1 + | .triggerCharacter => 2 + | .contentChange => 3 + +structure SignatureHelpContext where + triggerKind : SignatureHelpTriggerKind + triggerCharacter? : Option String := none + isRetrigger : Bool + activeSignatureHelp? : Option SignatureHelp := none + deriving FromJson, ToJson + +structure SignatureHelpParams extends TextDocumentPositionParams, WorkDoneProgressParams where + context? : Option SignatureHelpContext := none + deriving FromJson, ToJson + +structure SignatureHelpOptions extends WorkDoneProgressOptions where + triggerCharacters? : Option (Array String) := none + retriggerCharacters? : Option (Array String) := none + deriving FromJson, ToJson + end Lsp end Lean diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index f6aa869652..7cf83638be 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -72,7 +72,7 @@ def CompletionInfo.lctx : CompletionInfo → LocalContext | _ => .empty def CustomInfo.format : CustomInfo → Format - | i => f!"CustomInfo({i.value.typeName})" + | i => f!"[CustomInfo({i.value.typeName})]" instance : ToFormat CustomInfo := ⟨CustomInfo.format⟩ @@ -155,26 +155,26 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do Meta.ppExpr (← Meta.inferType info.expr) catch _ => pure "" - return f!"{← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}" + return f!"[Term] {← Meta.ppExpr info.expr} {if info.isBinder then "(isBinder := true) " else ""}: {ty} @ {formatElabInfo ctx info.toElabInfo}" def PartialTermInfo.format (ctx : ContextInfo) (info : PartialTermInfo) : Format := - f!"Partial term @ {formatElabInfo ctx info.toElabInfo}" + f!"[PartialTerm] @ {formatElabInfo ctx info.toElabInfo}" def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format := match info with - | .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}" - | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {← ctx.ppSyntax lctx stx} : {expectedType?} @ {formatStxRange ctx info.stx}" - | _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}" + | .dot i (expectedType? := expectedType?) .. => return f!"[Completion-Dot] {← i.format ctx} : {expectedType?}" + | .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[Completion-Id] {← ctx.ppSyntax lctx stx} : {expectedType?} @ {formatStxRange ctx info.stx}" + | _ => return f!"[Completion] {info.stx} @ {formatStxRange ctx info.stx}" def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do - return f!"command @ {formatElabInfo ctx info.toElabInfo}" + return f!"[Command] @ {formatElabInfo ctx info.toElabInfo}" def OptionInfo.format (ctx : ContextInfo) (info : OptionInfo) : IO Format := do - return f!"option {info.optionName} @ {formatStxRange ctx info.stx}" + return f!"[Option] {info.optionName} @ {formatStxRange ctx info.stx}" def FieldInfo.format (ctx : ContextInfo) (info : FieldInfo) : IO Format := do ctx.runMetaM info.lctx do - return f!"{info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}" + return f!"[Field] {info.fieldName} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange ctx info.stx}" def ContextInfo.ppGoals (ctx : ContextInfo) (goals : List MVarId) : IO Format := if goals.isEmpty then @@ -187,31 +187,31 @@ def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do let ctxA := { ctx with mctx := info.mctxAfter } let goalsBefore ← ctxB.ppGoals info.goalsBefore let goalsAfter ← ctxA.ppGoals info.goalsAfter - return f!"Tactic @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}" + return f!"[Tactic] @ {formatElabInfo ctx info.toElabInfo}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}" def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do let stx ← ctx.ppSyntax info.lctx info.stx let output ← ctx.ppSyntax info.lctx info.output - return f!"Macro expansion\n{stx}\n===>\n{output}" + return f!"[MacroExpansion]\n{stx}\n===>\n{output}" def UserWidgetInfo.format (info : UserWidgetInfo) : Format := - f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}" + f!"[UserWidget] {info.id}\n{Std.ToFormat.format <| info.props.run' {}}" def FVarAliasInfo.format (info : FVarAliasInfo) : Format := - f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}" + f!"[FVarAlias] {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}" def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format := - f!"FieldRedecl @ {formatStxRange ctx info.stx}" + f!"[FieldRedecl] @ {formatStxRange ctx info.stx}" def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format := do let loc := if let some loc := info.location? then f!"{loc.module} {loc.range.pos}-{loc.range.endPos}" else "none" - return f!"DelabTermInfo @ {← TermInfo.format ctx info.toTermInfo}\n\ + return f!"[DelabTerm] @ {← TermInfo.format ctx info.toTermInfo}\n\ Location: {loc}\n\ Docstring: {repr info.docString?}\n\ Explicit: {info.explicit}" def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format := - f!"Choice @ {formatElabInfo ctx info.toElabInfo}" + f!"[Choice] @ {formatElabInfo ctx info.toElabInfo}" def Info.format (ctx : ContextInfo) : Info → IO Format | ofTacticInfo i => i.format ctx diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index 8f54b3dc78..0bb6ae2a4d 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -96,7 +96,6 @@ inductive CompletionInfo where | option (stx : Syntax) | endSection (stx : Syntax) (scopeNames : List String) | tactic (stx : Syntax) - -- TODO `import` /-- Info for an option reference (e.g. in `set_option`). -/ structure OptionInfo where diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index fa33de2933..297f826888 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -1411,18 +1411,12 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) private opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw "" /-- -Pretty-prints a constant `c` as `c.{} : `. - -If `universes` is `false`, then the universe level parameters are omitted. +Pretty-prints the parameters of a `forall`. The pretty-printed parameters are passed to +`delabForall` at the end. -/ -partial def delabConstWithSignature (universes : Bool := true) : Delab := do - let e ← getExpr - -- use virtual expression node of arity 2 to separate name and type info - let idStx ← descend e 0 <| - withOptions (pp.universes.set · universes |> (pp.fullNames.set · true)) <| - delabConst - descend (← inferType e) 1 <| - delabParams {} idStx #[] +partial def delabForallParamsWithSignature + (delabForall : (groups : TSyntaxArray ``bracketedBinder) → (type : Term) → DelabM α) : DelabM α := do + delabParams {} #[] where /-- For types in the signature, we want to be sure pi binder types are pretty printed. @@ -1434,7 +1428,7 @@ where Once it reaches a binder with an inaccessible name, or a name that has already been used, the remaining binders appear in pi types after the `:` of the declaration. -/ - delabParams (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) := do + delabParams (bindingNames : NameSet) (groups : TSyntaxArray ``bracketedBinder) := do let e ← getExpr if e.isForall && e.binderInfo.isInstImplicit && e.bindingName!.hasMacroScopes then -- Assumption: this instance can be found by instance search, so it does not need to be named. @@ -1442,14 +1436,14 @@ where -- We could check to see whether the instance appears in the type and avoid omitting the instance name, -- but this would be the usual case. let group ← withBindingDomain do `(bracketedBinderF|[$(← delabTy)]) - withBindingBody e.bindingName! <| delabParams bindingNames idStx (groups.push group) + withBindingBody e.bindingName! <| delabParams bindingNames (groups.push group) else if e.isForall && (!e.isArrow || !(e.bindingName!.hasMacroScopes || bindingNames.contains e.bindingName!)) then - delabParamsAux bindingNames idStx groups #[] + delabParamsAux bindingNames groups #[] else let (opts', e') ← processSpine {} (← readThe SubExpr) withReader (fun ctx => {ctx with optionsPerPos := opts', subExpr := { ctx.subExpr with expr := e' }}) do let type ← delabTy - `(declSigWithId| $idStx:ident $groups* : $type) + delabForall groups type /-- Inner loop for `delabParams`, collecting binders. Invariants: @@ -1457,13 +1451,13 @@ where - It has a name that's not inaccessible. - It has a name that hasn't been used yet. -/ - delabParamsAux (bindingNames : NameSet) (idStx : Ident) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do + delabParamsAux (bindingNames : NameSet) (groups : TSyntaxArray ``bracketedBinder) (curIds : Array Ident) := do let e@(.forallE n d e' i) ← getExpr | unreachable! let n ← if bindingNames.contains n then withFreshMacroScope <| MonadQuotation.addMacroScope n else pure n let bindingNames := bindingNames.insert n if shouldGroupWithNext bindingNames e e' then withBindingBody' n (mkAnnotatedIdent n) fun stxN => - delabParamsAux bindingNames idStx groups (curIds.push stxN) + delabParamsAux bindingNames groups (curIds.push stxN) else /- `mkGroup` constructs binder syntax for the binder names `curIds : Array Ident`, which all have the same type and binder info. @@ -1492,7 +1486,7 @@ where withBindingBody' n (mkAnnotatedIdent n) fun stxN => do let curIds := curIds.push stxN let group ← mkGroup curIds - delabParams bindingNames idStx (groups.push group) + delabParams bindingNames (groups.push group) /- Given the forall `e` with body `e'`, determines if the binder from `e'` (if it is a forall) should be grouped with `e`'s binder. -/ @@ -1528,4 +1522,31 @@ where else return (opts, subExpr.expr) +/-- +Pretty-prints a `forall` similarly to `delabForall`, but explicitly denotes all named parameters. +-/ +partial def delabForallWithSignature : Delab := do + let isProp ← try isProp (← getExpr) catch _ => pure false + delabForallParamsWithSignature fun groups type => do + if groups.isEmpty then + return type + else if isProp && (← getPPOption getPPForalls) then + `(∀ $groups*, $type) + else + groups.foldrM (fun group acc => `(depArrow| $group → $acc)) type + +/-- +Pretty-prints a constant `c` as `c.{} : `. + +If `universes` is `false`, then the universe level parameters are omitted. +-/ +partial def delabConstWithSignature (universes : Bool := true) : Delab := do + let e ← getExpr + -- use virtual expression node of arity 2 to separate name and type info + let idStx ← descend e 0 <| + withOptions (pp.universes.set · universes |> (pp.fullNames.set · true)) <| + delabConst + descend (← inferType e) 1 <| + delabForallParamsWithSignature fun groups type => `(declSigWithId| $idStx:ident $groups* : $type) + end Lean.PrettyPrinter.Delaborator diff --git a/src/Lean/Server/FileSource.lean b/src/Lean/Server/FileSource.lean index 30042a8eb3..243ddc0bef 100644 --- a/src/Lean/Server/FileSource.lean +++ b/src/Lean/Server/FileSource.lean @@ -103,4 +103,7 @@ instance : FileSource CodeActionParams where instance : FileSource InlayHintParams where fileSource p := fileSource p.textDocument +instance : FileSource SignatureHelpParams where + fileSource p := fileSource p.textDocument + end Lean.Lsp diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 8234501426..5a7eca546a 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -8,6 +8,7 @@ prelude import Lean.Server.FileWorker.ExampleHover import Lean.Server.FileWorker.InlayHints import Lean.Server.FileWorker.SemanticHighlighting +import Lean.Server.FileWorker.SignatureHelp import Lean.Server.Completion import Lean.Server.References @@ -562,6 +563,15 @@ partial def handleFoldingRange (_ : FoldingRangeParams) endLine := endP.line kind? := some kind } +def handleSignatureHelp (p : SignatureHelpParams) : RequestM (RequestTask (Option SignatureHelp)) := do + let doc ← readDoc + let text := doc.meta.text + let requestedPos := text.lspPosToUtf8Pos p.position + mapTaskCostly (findCmdDataAtPos doc requestedPos (includeStop := false)) fun cmdData? => do + let some (cmdStx, tree) := cmdData? + | return none + SignatureHelp.findSignatureHelp? text p.context? cmdStx tree requestedPos + partial def handleWaitForDiagnostics (p : WaitForDiagnosticsParams) : RequestM (RequestTask WaitForDiagnostics) := do let rec waitLoop : RequestM EditableDocument := do @@ -627,6 +637,11 @@ builtin_initialize FoldingRangeParams (Array FoldingRange) handleFoldingRange + registerLspRequestHandler + "textDocument/signatureHelp" + SignatureHelpParams + (Option SignatureHelp) + handleSignatureHelp registerLspRequestHandler "$/lean/plainGoal" PlainGoalParams diff --git a/src/Lean/Server/FileWorker/SignatureHelp.lean b/src/Lean/Server/FileWorker/SignatureHelp.lean new file mode 100644 index 0000000000..ca9fd94685 --- /dev/null +++ b/src/Lean/Server/FileWorker/SignatureHelp.lean @@ -0,0 +1,205 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Marc Huisinga +-/ +prelude +import Lean.Server.InfoUtils +import Lean.Data.Lsp +import Init.Data.List.Sort.Basic + +namespace Lean.Server.FileWorker.SignatureHelp + +open Lean + +def determineSignatureHelp (tree : Elab.InfoTree) (appStx : Syntax) + : IO (Option Lsp.SignatureHelp) := do + let some (appCtx, .ofTermInfo appInfo) := tree.smallestInfo? fun + | .ofTermInfo ti => + -- HACK: Use range of syntax to figure out corresponding `TermInfo`. + -- This is necessary because in order to accurately determine which `Syntax` to use, + -- we have to use the original command syntax before macro expansions, + -- whereas the `Syntax` in the `InfoTree` is always from some stage of elaboration. + ti.stx.getRangeWithTrailing? == appStx.getRangeWithTrailing? + | _ => false + | return none + let app := appInfo.expr + let some fmt ← appCtx.runMetaM appInfo.lctx do + let appType ← instantiateMVars <| ← Meta.inferType app + if ! appType.isForall then + return none + let (stx, _) ← PrettyPrinter.delabCore appType + (delab := PrettyPrinter.Delaborator.delabForallWithSignature) + return some <| ← PrettyPrinter.ppTerm ⟨stx⟩ + | return none + return some { + signatures := #[{ label := toString fmt : Lsp.SignatureInformation }] + activeSignature? := some 0 + -- We do not mark the active parameter at all, as this would require retaining parameter indices + -- through the delaborator. + -- However, since we display the signature help using the `TermInfo` of the application, + -- not the function itself, this is not a problem: + -- The parameters keeps reducing as one adds arguments to the function, and the active + -- parameter is then always the first explicit one. + -- This feels very intuitive, so we don't need to thread any additional information + -- through the delaborator for highlighting the active parameter. + activeParameter? := none + } + +inductive CandidateKind where + /-- + Cursor is in the position of the argument to a pipe, like `<|` or `$`. Low precedence. + Ensures that `fun <| otherFun ` yields the signature help of `otherFun`, not `fun`. + -/ + | pipeArg + /-- + Cursor is in the position of the trailing whitespace of some term. Medium precedence. + Ensures that `fun otherFun ` yields the signature help of `fun`, not `otherFun`. + -/ + | termArg + /-- + Cursor is in the position of the argument to a function that already has other arguments applied + to it. High precedence. + -/ + | appArg + +def CandidateKind.prio : CandidateKind → Nat + | .pipeArg => 0 + | .termArg => 1 + | .appArg => 2 + +structure Candidate where + kind : CandidateKind + appStx : Syntax + +inductive SearchControl where + /-- In a syntax stack, keep searching upwards, continuing with the parent of the current term. -/ + | continue + /-- Stop the search through a syntax stack. -/ + | stop + +private def lineCommentPosition? (s : String) : Option String.Pos := Id.run do + let mut it := s.mkIterator + while h : it.hasNext do + let pos := it.pos + let c₁ := it.curr' h + it := it.next' h + if c₁ == '-' then + if h' : it.hasNext then + let c₂ := it.curr' h' + it := it.next' h' + if c₂ == '-' then + return some pos + return none + +private def isPositionInLineComment (text : FileMap) (pos : String.Pos) : Bool := Id.run do + let requestedLineNumber := text.toPosition pos |>.line + let lineStartPos := text.lineStart requestedLineNumber + let lineEndPos := text.lineStart (requestedLineNumber + 1) + let line := text.source.extract lineStartPos lineEndPos + let some lineCommentPos := lineCommentPosition? line + | return false + return pos >= lineStartPos + lineCommentPos + +open CandidateKind in +def findSignatureHelp? (text : FileMap) (ctx? : Option Lsp.SignatureHelpContext) (cmdStx : Syntax) + (tree : Elab.InfoTree) (requestedPos : String.Pos) : IO (Option Lsp.SignatureHelp) := do + -- HACK: Since comments are whitespace, the signature help can trigger on comments. + -- This is especially annoying on end-of-line comments, as the signature help will trigger on + -- every space in the comment. + -- This branch avoids this particular annoyance, but doesn't prevent the signature help from + -- triggering on other comment kinds. + if isPositionInLineComment text requestedPos then + return none + let stack? := cmdStx.findStack? fun stx => Id.run do + let some range := stx.getRangeWithTrailing? (canonicalOnly := true) + | return false + return range.contains requestedPos (includeStop := true) + let some stack := stack? + | return none + let stack := stack.toArray.map (·.1) + let mut candidates : Array Candidate := #[] + for h:i in [0:stack.size] do + let stx := stack[i] + let parent := stack[i+1]?.getD .missing + let (kind?, control) := determineCandidateKind stx parent + if let some kind := kind? then + candidates := candidates.push ⟨kind, stx⟩ + if control matches .stop then + break + -- Uses a stable sort so that we prefer inner candidates over outer candidates. + candidates := candidates.toList.mergeSort (fun c1 c2 => c1.kind.prio >= c2.kind.prio) |>.toArray + -- Look through all candidates until we find a signature help. + -- This helps in cases where the priority puts terms without `TermInfo` or ones that are not + -- applications of a `forall` in front of ones that do. + -- This usually happens when `.termArg` candidates overshadow `.pipeArg` candidates, + -- but the `.termArg` candidates are not semantically valid left-hand sides of applications. + for candidate in candidates do + if let some signatureHelp ← determineSignatureHelp tree candidate.appStx then + return some signatureHelp + return none +where + determineCandidateKind (stx : Syntax) (parent : Syntax) + : Option CandidateKind × SearchControl := Id.run do + let c kind? : Option CandidateKind × SearchControl := (kind?, .continue) + let some tailPos := stx.getTailPos? (canonicalOnly := true) + | return (none, .continue) + -- If the cursor is not in the trailing range of the syntax, then we don't display a signature + -- help. This prevents two undesirable scenarios: + -- - Since for applications `f 0 0 0`, the `InfoTree` only contains `TermInfo` for + -- `f` and `f 0 0 0`, we can't display accurate signature help for the sub-applications + -- `f 0` or `f 0 0`. Hence, we only display the signature help after `f` and `f 0 0 0`, + -- i.e. in the trailing range of the syntax of a candidate. + -- - When the search through the syntax stack passes through a node with more than one child + -- that is not an application, terminating the search if the cursor is on the interior of the + -- syntax ensures that we do not display signature help for functions way outside of the + -- current term that is being edited. + -- We still want to display it for such complex terms if we are in the trailing range of the + -- term since the complex term might produce a function for which we want to display a + -- signature help. + -- If we are ever on the interior of a term, then we will also be on the interior of terms + -- further up in the syntax stack, as these subsume the inner term, and so we terminate + -- the search early in this case. + if requestedPos < tailPos then + return (none, .stop) + let isManualTrigger := ctx?.any (·.triggerKind matches .invoked) + let isRetrigger := ctx?.any (·.isRetrigger) + let isCursorAfterTailPosLine := + (text.toPosition requestedPos).line != (text.toPosition tailPos).line + -- Application arguments are allowed anywhere in the trailing whitespace of a function, + -- e.g. on successive lines, but displaying the signature help in all of those lines + -- can be annoying (e.g. when `#check`ing a function and typing in the lines after it). + -- Hence, we only display the signature help automatically when the cursor is on the same line + -- as the tail position of the syntax, but allow users to display it by manually triggering + -- the signature help (`Ctrl+Shift+Space` in VS Code). We also display it in successive lines + -- if the user never closed it in the meantime, i.e. when the signature help was simply + -- retriggered. + if ! isManualTrigger && ! isRetrigger && isCursorAfterTailPosLine then + return (none, .continue) + if stx matches .ident .. then + match parent with + -- Do not yield a candidate `f` for `_ |>.f `, `_.f ` or `.f `. + -- Since `f` is an `identArg` candidate, has a `TermInfo` of its own and is a subterm of + -- these dot notations, we need to avoid picking its `TermInfo` by accident. + | `($_ |>.$_:ident $_*) => return c none + | `($_.$_:ident) => return c none + | `(.$_:ident) => return c none + | _ => return c termArg + let .node (kind := kind) (args := args) .. := stx + | return c none + -- `nullKind` is usually used for grouping together arguments, so we just skip it until + -- we have more tangible nodes at hand. + if kind == nullKind then + return c none + if kind == ``Parser.Term.app then + return c appArg + match stx with + | `($_ <| $_) => return c pipeArg + | `($_ $ $_) => return c pipeArg + | `($_ |>.$_:ident $_*) => return c pipeArg + | `(.$_:ident) => return c termArg + | `($_.$_:ident) => return c termArg + | _ => + if args.size <= 1 then + return c none + return c termArg diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index b27a7b54f2..fdafbd24ff 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -229,9 +229,9 @@ def Info.occursInOrOnBoundary (i : Info) (hoverPos : String.Pos) : Bool := Id.ru def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) := let ts := t.deepestNodes fun ctx i _ => if p i then some (ctx, i) else none - let infos := ts.map fun (ci, i) => - let diff := i.tailPos?.get! - i.pos?.get! - (diff, ci, i) + let infos := ts.filterMap fun (ci, i) => do + let diff := (← i.tailPos?) - (← i.pos?) + return (diff, ci, i) infos.toArray.getMax? (fun a b => a.1 > b.1) |>.map fun (_, ci, i) => (ci, i) @@ -240,7 +240,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in let results := (← t.visitM (postNode := fun ctx info children results => do let mut results := results.flatMap (·.getD []) if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then - results := results.filter (·.2.info.stx != info.stx[0]) + results := results.filter (·.2.info.stx != info.stx[0]) if omitIdentApps && info.stx.isIdent then -- if an identifier stands for an application (e.g. in the case of a typeclass projection), prefer the application if let .ofTermInfo ti := info then diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 892849761d..2f2fcdf810 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -1440,6 +1440,9 @@ def mkLeanServerCapabilities : ServerCapabilities := { inlayHintProvider? := some { resolveProvider? := false } + signatureHelpProvider? := some { + triggerCharacters? := some #[" "] + } } def initAndRunWatchdogAux : ServerM Unit := do diff --git a/tests/lean/binopInfoTree.lean.expected.out b/tests/lean/binopInfoTree.lean.expected.out index 4872b7485a..cd792ab5d6 100644 --- a/tests/lean/binopInfoTree.lean.expected.out +++ b/tests/lean/binopInfoTree.lean.expected.out @@ -1,12 +1,12 @@ [Elab.info] - • command @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption - • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨3, 0⟩-⟨3, 26⟩ - • option trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩ + • [Command] @ ⟨3, 0⟩-⟨3, 31⟩ @ Lean.Elab.Command.elabSetOption + • [Completion] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨3, 0⟩-⟨3, 26⟩ + • [Option] trace.Elab.info @ ⟨3, 11⟩-⟨3, 26⟩ 1 + 2 + 3 : Nat [Elab.info] - • command @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck - • 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion + • [Command] @ ⟨5, 0⟩-⟨5, 16⟩ @ Lean.Elab.Command.elabCheck + • [Term] 1 + 2 + 3 : Nat @ ⟨5, 7⟩-⟨5, 16⟩ @ «_aux_Init_Notation___macroRules_term_+__2» + • [MacroExpansion] 1 + 2 + 3 -- should propagate through multiple macro expansions @@ -14,67 +14,67 @@ binop% HAdd.hAdd✝ (1 + 2) 3 -- should propagate through multiple macro expansions - • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp - • 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† - • 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion + • [Term] 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† @ Lean.Elab.Term.Op.elabBinOp + • [Term] 1 + 2 + 3 : Nat @ ⟨5, 7⟩†-⟨5, 16⟩† + • [Term] 1 + 2 : Nat @ ⟨5, 7⟩-⟨5, 12⟩ @ «_aux_Init_Notation___macroRules_term_+__2» + • [MacroExpansion] 1 + 2 ===> binop% HAdd.hAdd✝ 1 2 - • 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩† - • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 16⟩† - • [.] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 12⟩† - • 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit - • 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit - • 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit + • [Term] 1 + 2 : Nat @ ⟨5, 7⟩†-⟨5, 12⟩† + • [Completion-Id] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 16⟩† + • [Completion-Id] HAdd.hAdd✝ : none @ ⟨5, 7⟩†-⟨5, 12⟩† + • [Term] 1 : Nat @ ⟨5, 7⟩-⟨5, 8⟩ @ Lean.Elab.Term.elabNumLit + • [Term] 2 : Nat @ ⟨5, 11⟩-⟨5, 12⟩ @ Lean.Elab.Term.elabNumLit + • [Term] 3 : Nat @ ⟨5, 15⟩-⟨5, 16⟩ @ Lean.Elab.Term.elabNumLit fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int [Elab.info] - • command @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck - • fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ - • n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ - • m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ - • Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ - • l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩ - • ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription - • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent - • [.] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩ - • Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ - • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion + • [Command] @ ⟨7, 0⟩-⟨7, 48⟩ @ Lean.Elab.Command.elabCheck + • [Term] fun n m l => ↑n + (↑m + ↑l) : Nat → Nat → Nat → Int @ ⟨7, 7⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabFun + • [Term] Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ + • [Term] Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ + • [Term] n (isBinder := true) : Nat @ ⟨7, 12⟩-⟨7, 13⟩ + • [Term] Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ + • [Term] Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ + • [Term] m (isBinder := true) : Nat @ ⟨7, 14⟩-⟨7, 15⟩ + • [Term] Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] Nat : some Sort.{?_uniq} @ ⟨7, 20⟩-⟨7, 23⟩ + • [Term] Nat : Type @ ⟨7, 20⟩-⟨7, 23⟩ + • [Term] l (isBinder := true) : Nat @ ⟨7, 16⟩-⟨7, 17⟩ + • [Term] ↑n + (↑m + ↑l) : Int @ ⟨7, 28⟩-⟨7, 48⟩ @ Lean.Elab.Term.elabTypeAscription + • [Term] Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] Int : some Sort.{?_uniq} @ ⟨7, 44⟩-⟨7, 47⟩ + • [Term] Int : Type @ ⟨7, 44⟩-⟨7, 47⟩ + • [Term] ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩-⟨7, 41⟩ @ «_aux_Init_Notation___macroRules_term_+__2» + • [MacroExpansion] n + (m +' l) ===> binop% HAdd.hAdd✝ n (m +' l) - • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp - • ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† - • [.] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩† - • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent - • [.] n : none @ ⟨7, 29⟩-⟨7, 30⟩ - • n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ - • ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1» - • Macro expansion + • [Term] ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† @ Lean.Elab.Term.Op.elabBinOp + • [Term] ↑n + (↑m + ↑l) : Int @ ⟨7, 29⟩†-⟨7, 41⟩† + • [Completion-Id] HAdd.hAdd✝ : none @ ⟨7, 29⟩†-⟨7, 41⟩† + • [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] n : none @ ⟨7, 29⟩-⟨7, 30⟩ + • [Term] n : Nat @ ⟨7, 29⟩-⟨7, 30⟩ + • [Term] ↑m + ↑l : Int @ ⟨7, 34⟩-⟨7, 40⟩ @ «_aux_binopInfoTree___macroRules_term_+'__1» + • [MacroExpansion] m +' l ===> m + l - • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2» - • Macro expansion + • [Term] ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† @ «_aux_Init_Notation___macroRules_term_+__2» + • [MacroExpansion] m + l ===> binop% HAdd.hAdd✝ m l - • ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† - • [.] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩† - • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent - • [.] m : none @ ⟨7, 34⟩-⟨7, 35⟩ - • m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ - • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent - • [.] l : none @ ⟨7, 39⟩-⟨7, 40⟩ - • l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ + • [Term] ↑m + ↑l : Int @ ⟨7, 34⟩†-⟨7, 40⟩† + • [Completion-Id] HAdd.hAdd✝ : none @ ⟨7, 34⟩†-⟨7, 40⟩† + • [Term] m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] m : none @ ⟨7, 34⟩-⟨7, 35⟩ + • [Term] m : Nat @ ⟨7, 34⟩-⟨7, 35⟩ + • [Term] l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] l : none @ ⟨7, 39⟩-⟨7, 40⟩ + • [Term] l : Nat @ ⟨7, 39⟩-⟨7, 40⟩ [Elab.info] - • command @ ⟨8, 0⟩-⟨8, 0⟩ @ Lean.Elab.Command.elabEoi + • [Command] @ ⟨8, 0⟩-⟨8, 0⟩ @ Lean.Elab.Command.elabEoi diff --git a/tests/lean/interactive/signatureHelp.lean b/tests/lean/interactive/signatureHelp.lean new file mode 100644 index 0000000000..32c929b2b6 --- /dev/null +++ b/tests/lean/interactive/signatureHelp.lean @@ -0,0 +1,144 @@ +def simpleFun {_ : Type} (a b : Nat) : Nat → Nat → Nat := sorry + +#check simpleFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check simpleFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check simpleFun 0 -- Shortened signature help expected (implicit is skipped) + --^ textDocument/signatureHelp + +#check simpleFun 0 0 -- Shortened signature help without ∀ expected + --^ textDocument/signatureHelp + +#check simpleFun 0 0 0 -- Shortened signature help without ∀ expected + --^ textDocument/signatureHelp + +#check simpleFun 0 0 0 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check simpleFun 0 0 0 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check simpleFun -- No signature help expected in end-of-line comment + --^ textDocument/signatureHelp + +#check simpleFun <| -- Full signature help expected + --^ textDocument/signatureHelp + +#check simpleFun 0 0 0 <| -- Shortened signature help expected + --^ textDocument/signatureHelp + +#check simpleFun 0 <| simpleFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check simpleFun $ -- Full signature help expected + --^ textDocument/signatureHelp + +#check simpleFun 0 0 0 $ -- Shortened signature help expected + --^ textDocument/signatureHelp + +#check simpleFun 0 $ simpleFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check simpleFun ( ) -- No signature help expected + --^ textDocument/signatureHelp + +#check @simpleFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check @simpleFun _ -- Shortened signature help expected (implicit is not skipped) + --^ textDocument/signatureHelp + +#check simpleFun (b := 0) -- Shortened signature help without `b` expected + --^ textDocument/signatureHelp + +#check (simpleFun 0) -- Shortened signature help expected + --^ textDocument/signatureHelp + +#check (simpleFun 0) 0 -- Shortened signature help expected + --^ textDocument/signatureHelp + +def simpleProp (x y : Nat) : x = y → x = y := sorry + +#check simpleProp -- Full signature help with `∀` expected + --^ textDocument/signatureHelp + +#check simpleProp 0 -- Shortened signature help with `∀` expected + --^ textDocument/signatureHelp + +#check simpleProp 0 0 -- Shortened signature help with remaining implication expected + --^ textDocument/signatureHelp + +#check simpleProp 0 0 sorry -- No signature help expected + --^ textDocument/signatureHelp + +def complexFun (f : Nat → Nat → Nat → Nat → Nat) (x : Nat) : Nat := sorry + +#check complexFun simpleFun -- Shortened signature help of `complexFun` expected + --^ textDocument/signatureHelp + +#check complexFun simpleFun 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check complexFun (simpleFun ) -- Signature help of `simpleFun` expected + --^ textDocument/signatureHelp + +structure SomeStructure where + fieldFun (x : Nat) : Nat → Nat + +def SomeStructure.dotFun (s : SomeStructure) (x : Nat) : Nat := sorry + +def SomeStructure.dotIdFun (x : Nat) : SomeStructure := sorry + +variable (s : SomeStructure) (s' : Nat → SomeStructure) + +#check s.fieldFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check s.fieldFun 0 -- Shortened signature help expected + --^ textDocument/signatureHelp + +#check s.fieldFun 0 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check (s' 0).fieldFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check (s' 0).fieldFun 0 -- Shortened signature help expected + --^ textDocument/signatureHelp + +#check s.dotFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check s.dotFun 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check (s' 0).dotFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check (s' 0).dotFun 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check s |>.fieldFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check s |>.fieldFun 0 -- Shortened signature help expected + --^ textDocument/signatureHelp + +#check s |>.fieldFun 0 0 -- No signature help expected + --^ textDocument/signatureHelp + +#check s' 0 |>.fieldFun -- Full signature help expected + --^ textDocument/signatureHelp + +#check s' 0 |>.fieldFun 0 -- Shortened signature help expected + --^ textDocument/signatureHelp + +example : SomeStructure := .dotIdFun -- Full signature help expected + --^ textDocument/signatureHelp + + +example : SomeStructure := .dotIdFun 0 -- No signature help expected + --^ textDocument/signatureHelp diff --git a/tests/lean/interactive/signatureHelp.lean.expected.out b/tests/lean/interactive/signatureHelp.lean.expected.out new file mode 100644 index 0000000000..52760c9dba --- /dev/null +++ b/tests/lean/interactive/signatureHelp.lean.expected.out @@ -0,0 +1,139 @@ +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 2, "character": 16}} +{"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 5, "character": 17}} +{"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 8, "character": 19}} +{"signatures": [{"label": "(b : Nat) → Nat → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 11, "character": 21}} +{"signatures": [{"label": "Nat → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 14, "character": 23}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 17, "character": 25}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 20, "character": 22}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 23, "character": 17}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 26, "character": 20}} +{"signatures": [{"label": "(a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 29, "character": 26}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 32, "character": 32}} +{"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 35, "character": 19}} +{"signatures": [{"label": "(a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 38, "character": 25}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 41, "character": 31}} +{"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 44, "character": 18}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 47, "character": 18}} +{"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 50, "character": 20}} +{"signatures": [{"label": "(a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 53, "character": 26}} +{"signatures": [{"label": "(a : Nat) → Nat → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 56, "character": 21}} +{"signatures": [{"label": "(b : Nat) → Nat → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 59, "character": 23}} +{"signatures": [{"label": "Nat → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 64, "character": 18}} +{"signatures": [{"label": "∀ (x y : Nat), x = y → x = y"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 67, "character": 20}} +{"signatures": [{"label": "∀ (y : Nat), 0 = y → 0 = y"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 70, "character": 22}} +{"signatures": [{"label": "0 = 0 → 0 = 0"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 73, "character": 28}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 78, "character": 28}} +{"signatures": [{"label": "(x : Nat) → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 81, "character": 30}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 84, "character": 29}} +{"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}], + "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 96, "character": 18}} +{"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 99, "character": 20}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 102, "character": 22}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 105, "character": 23}} +{"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 108, "character": 25}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 111, "character": 16}} +{"signatures": [{"label": "(x : Nat) → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 114, "character": 18}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 117, "character": 21}} +{"signatures": [{"label": "(x : Nat) → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 120, "character": 23}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 123, "character": 21}} +{"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 126, "character": 23}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 129, "character": 25}} +null +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 132, "character": 24}} +{"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 135, "character": 26}} +{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 138, "character": 37}} +{"signatures": [{"label": "(x : Nat) → SomeStructure"}], "activeSignature": 0} +{"textDocument": {"uri": "file:///signatureHelp.lean"}, + "position": {"line": 142, "character": 39}} +null diff --git a/tests/lean/run/info_trees.lean b/tests/lean/run/info_trees.lean index 0429c1c26a..cf288dc2eb 100644 --- a/tests/lean/run/info_trees.lean +++ b/tests/lean/run/info_trees.lean @@ -3,78 +3,78 @@ -- it is fine to simply remove the `#guard_msgs` and expected output. /-- -info: • command @ ⟨83, 0⟩-⟨83, 40⟩ @ Lean.Elab.Command.elabDeclaration - • Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩ @ Lean.Elab.Term.elabIdent - • [.] Nat : some Sort.{?_uniq.1} @ ⟨83, 15⟩-⟨83, 18⟩ - • Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩ - • n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩ - • 0 ≤ n : Prop @ ⟨83, 22⟩-⟨83, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2» - • Macro expansion +info: • [Command] @ ⟨83, 0⟩-⟨83, 40⟩ @ Lean.Elab.Command.elabDeclaration + • [Term] Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] Nat : some Sort.{?_uniq.1} @ ⟨83, 15⟩-⟨83, 18⟩ + • [Term] Nat : Type @ ⟨83, 15⟩-⟨83, 18⟩ + • [Term] n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩ + • [Term] 0 ≤ n : Prop @ ⟨83, 22⟩-⟨83, 27⟩ @ «_aux_Init_Notation___macroRules_term_≤__2» + • [MacroExpansion] 0 ≤ n ===> binrel% LE.le✝ 0 n - • 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩† @ Lean.Elab.Term.Op.elabBinRel - • 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩† - • [.] LE.le✝ : none @ ⟨83, 22⟩†-⟨83, 27⟩† - • 0 : Nat @ ⟨83, 22⟩-⟨83, 23⟩ @ Lean.Elab.Term.elabNumLit - • n : Nat @ ⟨83, 26⟩-⟨83, 27⟩ @ Lean.Elab.Term.elabIdent - • [.] n : none @ ⟨83, 26⟩-⟨83, 27⟩ - • n : Nat @ ⟨83, 26⟩-⟨83, 27⟩ - • CustomInfo(Lean.Elab.Term.AsyncBodyInfo) - • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩ - • n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩ - • CustomInfo(Lean.Elab.Term.BodyInfo) - • Tactic @ ⟨83, 31⟩-⟨83, 40⟩ + • [Term] 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩† @ Lean.Elab.Term.Op.elabBinRel + • [Term] 0 ≤ n : Prop @ ⟨83, 22⟩†-⟨83, 27⟩† + • [Completion-Id] LE.le✝ : none @ ⟨83, 22⟩†-⟨83, 27⟩† + • [Term] 0 : Nat @ ⟨83, 22⟩-⟨83, 23⟩ @ Lean.Elab.Term.elabNumLit + • [Term] n : Nat @ ⟨83, 26⟩-⟨83, 27⟩ @ Lean.Elab.Term.elabIdent + • [Completion-Id] n : none @ ⟨83, 26⟩-⟨83, 27⟩ + • [Term] n : Nat @ ⟨83, 26⟩-⟨83, 27⟩ + • [CustomInfo(Lean.Elab.Term.AsyncBodyInfo)] + • [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩ + • [Term] n (isBinder := true) : Nat @ ⟨83, 11⟩-⟨83, 12⟩ + • [CustomInfo(Lean.Elab.Term.BodyInfo)] + • [Tactic] @ ⟨83, 31⟩-⟨83, 40⟩ (Term.byTactic "by" (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]))) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨83, 31⟩-⟨83, 33⟩ + • [Tactic] @ ⟨83, 31⟩-⟨83, 33⟩ "by" before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq + • [Tactic] @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])])) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented + • [Tactic] @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.Tactic.evalTacticSeq1Indented (Tactic.tacticSeq1Indented [(Tactic.exact? "exact?" [])]) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.LibrarySearch.evalExact + • [Tactic] @ ⟨83, 34⟩-⟨83, 40⟩ @ Lean.Elab.LibrarySearch.evalExact (Tactic.exact? "exact?" []) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Tactic @ ⟨83, 34⟩†-⟨83, 40⟩† @ Lean.Elab.Tactic.evalExact + • [Tactic] @ ⟨83, 34⟩†-⟨83, 40⟩† @ Lean.Elab.Tactic.evalExact (Tactic.exact "exact" (Term.app `Nat.zero_le [`n])) before ⏎ n : Nat ⊢ 0 ≤ n after no goals - • Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp - • [.] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.42 @ ⟨1, 0⟩†-⟨1, 0⟩† - • Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩† - • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent - • [.] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩† - • n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† - • CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo) - • UserWidget Lean.Meta.Tactic.TryThis.tryThisWidget + • [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp + • [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.42 @ ⟨1, 0⟩†-⟨1, 0⟩† + • [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩† + • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent + • [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩† + • [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† + • [CustomInfo(Lean.Meta.Tactic.TryThis.TryThisInfo)] + • [UserWidget] Lean.Meta.Tactic.TryThis.tryThisWidget {"suggestions": [{"suggestion": "exact Nat.zero_le n"}], "style": null, "range": {"start": {"line": 82, "character": 34}, "end": {"line": 82, "character": 40}}, "isInline": true, "header": "Try this: "} - • t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩ + • [Term] t (isBinder := true) : ∀ (n : Nat), 0 ≤ n @ ⟨83, 8⟩-⟨83, 9⟩ --- info: Try this: exact Nat.zero_le n -/