From fd9e3d8fe65004911d8a03320443f3b56ff2f870 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 2 Jul 2021 12:49:26 -0700 Subject: [PATCH] chore: add completion test and go-to field type --- src/Lean/Server/Completion.lean | 2 +- .../Server/FileWorker/RequestHandling.lean | 12 ++- tests/lean/interactive/completionOption.lean | 2 + .../completionOption.lean.expected.out | 68 ++++++++++++++++ tests/lean/interactive/goTo.lean | 34 ++++++++ tests/lean/interactive/goTo.lean.expected.out | 81 +++++++++++++++++++ 6 files changed, 195 insertions(+), 4 deletions(-) create mode 100644 tests/lean/interactive/completionOption.lean create mode 100644 tests/lean/interactive/completionOption.lean.expected.out create mode 100644 tests/lean/interactive/goTo.lean create mode 100644 tests/lean/interactive/goTo.lean.expected.out diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 7aca8bdc99..ed1803da9f 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -249,7 +249,7 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) : IO (Option Com let (decls : Std.RBMap _ _ _) ← getOptionDecls let opts ← getOptions let mut items := #[] - for ⟨name, decl⟩ in (decls : Std.RBMap _ _ _) do + for ⟨name, decl⟩ in decls do if partialName.isPrefixOf name || (match partialName, name with | Name.str p₁ s₁ _, Name.str p₂ s₂ _ => p₁ == p₂ && s₁.isPrefixOf s₂ diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 13a0fd4fcf..91955c01a5 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -56,8 +56,9 @@ partial def handleHover (p : HoverParams) return none -inductive GoToKind | declaration | definition | type -deriving DecidableEq +inductive GoToKind + | declaration | definition | type + deriving DecidableEq open Elab GoToKind in partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams) @@ -101,7 +102,12 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams) if let some n := expr.constName? then return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n if let Info.ofFieldInfo fi := i then - if kind ≠ type then + if kind = type then + let expr ← ci.runMetaM i.lctx do + Meta.instantiateMVars (← Meta.inferType fi.val) + if let some n := expr.constName? then + return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n + else return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName -- If other go-tos fail, we try to show the elaborator or parser if let some ei := i.toElabInfo? then diff --git a/tests/lean/interactive/completionOption.lean b/tests/lean/interactive/completionOption.lean new file mode 100644 index 0000000000..c74bb4b343 --- /dev/null +++ b/tests/lean/interactive/completionOption.lean @@ -0,0 +1,2 @@ +set_option pp + --^ textDocument/completion \ No newline at end of file diff --git a/tests/lean/interactive/completionOption.lean.expected.out b/tests/lean/interactive/completionOption.lean.expected.out new file mode 100644 index 0000000000..d4ccca848e --- /dev/null +++ b/tests/lean/interactive/completionOption.lean.expected.out @@ -0,0 +1,68 @@ +{"textDocument": {"uri": "file://completionOption.lean"}, + "position": {"line": 0, "character": 13}} +{"items": + [{"label": "pp.all", + "detail": + "(false), (pretty printer) display coercions, implicit parameters, proof terms, fully qualified names, universe, and disable beta reduction and notations during pretty printing"}, + {"label": "pp.auxDecls", + "detail": + "(false), display auxiliary declarations used to compile recursive functions"}, + {"label": "pp.binder_types", + "detail": + "(false), (pretty printer) display types of lambda and Pi parameters"}, + {"label": "pp.coercions", + "detail": "(true), (pretty printer) hide coercion applications"}, + {"label": "pp.explicit", + "detail": "(false), (pretty printer) display implicit arguments"}, + {"label": "pp.full_names", + "detail": "(false), (pretty printer) display fully qualified names"}, + {"label": "pp.inaccessibleNames", + "detail": "(false), display inaccessible declarations in the local context"}, + {"label": "pp.macroStack", + "detail": "(false), dispaly macro expansion stack"}, + {"label": "pp.motives.all", + "detail": "(false), (pretty printer) print all motives"}, + {"label": "pp.motives.nonConst", + "detail": + "(false), (pretty printer) print all motives that are not constant functions"}, + {"label": "pp.motives.pi", + "detail": "(true), (pretty printer) print all motives that return pi types"}, + {"label": "pp.notation", + "detail": + "(true), (pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)"}, + {"label": "pp.private_names", + "detail": + "(false), (pretty printer) display internal names assigned to private declarations"}, + {"label": "pp.proofs", + "detail": + "(false), (pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder"}, + {"label": "pp.proofs.withType", + "detail": + "(true), (pretty printer) when eliding a proof (see `pp.proofs`), show its type instead"}, + {"label": "pp.raw", + "detail": "(false), (pretty printer) print raw expression/syntax tree"}, + {"label": "pp.raw.maxDepth", + "detail": "(32), (pretty printer) maximum `Syntax` depth for raw printer"}, + {"label": "pp.raw.showInfo", + "detail": + "(false), (pretty printer) print `SourceInfo` metadata with raw printer"}, + {"label": "pp.rawOnError", + "detail": + "(false), (pretty printer) fallback to 'raw' printer when pretty printer fails"}, + {"label": "pp.safe_shadowing", + "detail": + "(true), (pretty printer) allow variable shadowing if there is no collision"}, + {"label": "pp.sanitizeNames", + "detail": + "(true), add suffix '_{}' to shadowed/inaccessible variables when pretty printing"}, + {"label": "pp.structure_instance_type", + "detail": "(false), (pretty printer) display type of structure instances"}, + {"label": "pp.structure_instances", + "detail": + "(true), (pretty printer) display structure instances using the '{ fieldName := fieldValue, ... }' notation or '⟨fieldValue, ... ⟩' if structure is tagged with [pp_using_anonymous_constructor] attribute"}, + {"label": "pp.structure_projections", + "detail": + "(true), (pretty printer) display structure projections using field notation"}, + {"label": "pp.universes", + "detail": "(false), (pretty printer) display universe"}], + "isIncomplete": true} diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean new file mode 100644 index 0000000000..24ce8865f8 --- /dev/null +++ b/tests/lean/interactive/goTo.lean @@ -0,0 +1,34 @@ +import Lean -- needed for go-to elab/syntax + +structure Bar where + +structure Foo where + --v textDocument/definition + foo₁ : Nat + foo₂ : Nat + bar : Bar + +def mkFoo₁ : Foo := { +--v textDocument/definition + foo₁ := 1 +--v textDocument/declaration + foo₂ := 2 +--v textDocument/typeDefinition + bar := ⟨⟩ +} + +--v textDocument/definition +inductive HandWrittenStruct where + | mk (n : Nat) + +--v textDocument/declaration +def HandWrittenStruct.n := fun | mk n => n + +def hws : HandWrittenStruct := { +--v textDocument/definition + n := 3 +} + + --v textDocument/declaration +def mkFoo₂ := mkFoo₁ + diff --git a/tests/lean/interactive/goTo.lean.expected.out b/tests/lean/interactive/goTo.lean.expected.out new file mode 100644 index 0000000000..0bb917064c --- /dev/null +++ b/tests/lean/interactive/goTo.lean.expected.out @@ -0,0 +1,81 @@ +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 6, "character": 9}} +[{"targetUri": "file:///home/wjn/lean4/src/Init/Prelude.lean", + "targetSelectionRange": + {"start": {"line": 341, "character": 10}, + "end": {"line": 341, "character": 13}}, + "targetRange": + {"start": {"line": 341, "character": 0}, + "end": {"line": 343, "character": 24}}, + "originSelectionRange": + {"start": {"line": 6, "character": 9}, "end": {"line": 6, "character": 12}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 12, "character": 2}} +[{"targetUri": "file://goTo.lean", + "targetSelectionRange": + {"start": {"line": 6, "character": 2}, "end": {"line": 6, "character": 6}}, + "targetRange": + {"start": {"line": 6, "character": 2}, "end": {"line": 6, "character": 6}}, + "originSelectionRange": + {"start": {"line": 12, "character": 2}, "end": {"line": 12, "character": 6}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 14, "character": 2}} +[{"targetUri": "file://goTo.lean", + "targetSelectionRange": + {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 6}}, + "targetRange": + {"start": {"line": 7, "character": 2}, "end": {"line": 7, "character": 6}}, + "originSelectionRange": + {"start": {"line": 14, "character": 2}, "end": {"line": 14, "character": 6}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 16, "character": 2}} +[{"targetUri": "file://goTo.lean", + "targetSelectionRange": + {"start": {"line": 2, "character": 10}, "end": {"line": 2, "character": 13}}, + "targetRange": + {"start": {"line": 2, "character": 0}, "end": {"line": 2, "character": 19}}, + "originSelectionRange": + {"start": {"line": 16, "character": 2}, "end": {"line": 16, "character": 5}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 20, "character": 2}} +[{"targetUri": "file:///home/wjn/lean4/src/Lean/Elab/Declaration.lean", + "targetSelectionRange": + {"start": {"line": 140, "character": 4}, + "end": {"line": 140, "character": 19}}, + "targetRange": + {"start": {"line": 140, "character": 0}, + "end": {"line": 161, "character": 41}}, + "originSelectionRange": + {"start": {"line": 20, "character": 0}, + "end": {"line": 21, "character": 16}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 24, "character": 2}} +[{"targetUri": "file:///home/wjn/lean4/src/Lean/Parser/Command.lean", + "targetSelectionRange": + {"start": {"line": 63, "character": 28}, + "end": {"line": 63, "character": 39}}, + "targetRange": + {"start": {"line": 63, "character": 24}, + "end": {"line": 64, "character": 164}}, + "originSelectionRange": + {"start": {"line": 24, "character": 0}, + "end": {"line": 24, "character": 42}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 28, "character": 2}} +[{"targetUri": "file://goTo.lean", + "targetSelectionRange": + {"start": {"line": 24, "character": 4}, "end": {"line": 24, "character": 23}}, + "targetRange": + {"start": {"line": 24, "character": 0}, "end": {"line": 24, "character": 42}}, + "originSelectionRange": + {"start": {"line": 28, "character": 2}, "end": {"line": 28, "character": 3}}}] +{"textDocument": {"uri": "file://goTo.lean"}, + "position": {"line": 32, "character": 14}} +[{"targetUri": "file://goTo.lean", + "targetSelectionRange": + {"start": {"line": 10, "character": 4}, "end": {"line": 10, "character": 10}}, + "targetRange": + {"start": {"line": 10, "character": 0}, "end": {"line": 17, "character": 1}}, + "originSelectionRange": + {"start": {"line": 32, "character": 14}, + "end": {"line": 32, "character": 20}}}]