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 -/