LSP jump to definition

TODO.md

@@ -1,17 +1,20 @@
 
 ## TODO
 
-- [ ] Inject markdown highlighter into /- -/ comments in vscode
+- [ ] Importing Prelude twice should be an error (currently it causes double hints and breaks auto)
 - [ ] For errors in other files, point to the import
-  - put a try in there and remove exitFailure
 - [x] Unsolved metas should be errors (user metas are fine)
 - [x] Better syntax for forward declared data (so we can distinguish from functions)
 - [ ] maybe allow "Main" module name for any file
+- [ ] Restore "add missing cases" for LSP mode
+- [ ] Case split for LSP mode
+- [ ] Leverage LSP code for web playground
 - [ ] Improve handling of names:
   - We need FC on names in a lot of places
   - [x] FC for duplicate `data`, `record`, `class` name is wrong (points to `data`)
   - [x] FC on bad import should point to the name
   - [x] Current module overrides imports
+  - [ ] Duplicate data constructors point to `data`
   - [ ] Allow Qualified names in surface syntax
   - Don't disambiguate on type for now
 - [x] change "in prefix position" and "trailing operator" errors to do sections
@@ -33,6 +36,8 @@
   - We might get into a situation where solving immediately would have gotten us more progress?
 - [ ] "Failed to unify %var0 and %var1" - get names in there
   - Need fancier `Env` or the index on the type of `Tm`
+  - Or the name on the VVar?
+  - Also we should render %pi, etc more readably (bonus points for _×_)
 - Editor support:
   - [ ] add missing cases should skip indented lines
   - [ ] add missing cases should handle `_::_`

newt-vscode-lsp/src/lsp.ts

@@ -15,6 +15,7 @@ import {
   InitializeParams,
   InitializeResult,
   TextDocumentSyncKind,
+  Location,
 } from "vscode-languageserver/node";
 import { TextDocument } from "vscode-languageserver-textdocument";
 
@@ -69,16 +70,25 @@ connection.onHover((params): Hover | null => {
   const uri = params.textDocument.uri;
   const pos = params.position;
   console.log('HOVER', uri, pos)
-  let value = LSP_hoverInfo(uri, pos.line, pos.character)
-  if (!value) return null
-  console.log('HOVER is ', value)
-  return { contents: { kind: "plaintext", value } };
+  let res = LSP_hoverInfo(uri, pos.line, pos.character)
+  if (!res) return null
+  console.log('HOVER is ', res)
+  return { contents: { kind: "plaintext", value: res.info } };
 });
 
+connection.onDefinition((params): Location | null => {
+  const uri = params.textDocument.uri;
+  const pos = params.position;
+  let value = LSP_hoverInfo(uri, pos.line, pos.character)
+  if (!value) return null;
+  return value.location
+})
+
 connection.onInitialize((_params: InitializeParams): InitializeResult => ({
   capabilities: {
     textDocumentSync: TextDocumentSyncKind.Incremental,
     hoverProvider: true,
+    definitionProvider: true,
   },
 }));
 

newt-vscode-lsp/src/newt.d.ts

@@ -1,5 +1,9 @@
-import { Diagnostic } from "vscode-languageserver";
+import { Diagnostic, Location } from "vscode-languageserver";
 
 export function LSP_updateFile(name: string, content: string): (eta: any) => any;
 export function LSP_checkFile(name: string): Diagnostic[];
-export function LSP_hoverInfo(name: string, row: number, col: number): string|null;
+interface HoverResult {
+    info: string
+    location: Location
+}
+export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult|null;

src/Commands.newt

@@ -24,7 +24,7 @@ decomposeName fn =
 
 -- The cheap version of type at point, find the token, lookup in global context
 -- Later we will either get good FC for entries or scan them all and build a cache.
-getHoverInfo : FileSource → List String → Int → Int → M (Maybe String)
+getHoverInfo : FileSource → List String → Int → Int → M (Maybe (String × FC))
 getHoverInfo repo modns row col = do
     mod <- processModule emptyFC repo Nil modns
     -- not necessarily loaded into top... (Maybe push this down into that branch of processModule)
@@ -39,7 +39,7 @@ getHoverInfo repo modns row col = do
 
     -- Lookup the name
     let (Just e) = lookupRaw name top   | _ => pure Nothing
-    pure $ Just "\{show e.name} : \{rpprint Nil e.type}"
+    pure $ Just ("\{show e.name} : \{rpprint Nil e.type}", e.fc)
 
     where
         getTok : List BTok → Maybe String

src/LSP.newt

@@ -79,6 +79,14 @@ updateFile fn src = unsafePerformIO $ do
     -- modifyIORef state [ topContext := ctx ]
     modifyIORef state $ \a => [ topContext := ctx ] a
 
+
+fcToRange : FC → Json
+fcToRange (MkFC uri (MkBounds sr sc er ec)) =
+    JsonObj $ ("start", mkPosition sr sc) :: ("end", mkPosition er (ec + 1)) :: Nil
+    where
+        mkPosition : Int → Int → Json
+        mkPosition l c = JsonObj $ ("line", JsonInt l) :: ("character", JsonInt c) :: Nil
+
 hoverInfo : String → Int → Int → JSObject
 hoverInfo uri line col = unsafePerformIO $ do
     let (base,modns) = decomposeName uri
@@ -87,27 +95,24 @@ hoverInfo uri line col = unsafePerformIO $ do
     if (st.baseDir /= base)
         then resetState base
         else pure MkUnit
-    Right (_, Just msg) <- (getHoverInfo lspFileSource modns line col).runM st.topContext
+    Right (_, Just (msg, fc)) <- (getHoverInfo lspFileSource modns line col).runM st.topContext
         | Right _  => do
             putStrLn $ "Nothing to see here"
             pure $ jsonToJObject JsonNull
         | Left err => do
             putStrLn $ showError "" err
             pure $ jsonToJObject JsonNull
-    pure $ jsonToJObject $ JsonStr msg
+    let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil
+    pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil
 
 errorToDiag : Error -> Json
-errorToDiag (E (MkFC fn (MkBounds sr sc er ec)) msg) =
+errorToDiag (E fc msg) =
   JsonObj
     $  ("severity", JsonInt 1)
-    -- PARSER `$` is winning over `,`, which is not what I'm expecting  Maybe `,` should be special...
-    :: ("range", (JsonObj $ ("start", range sr sc) :: ("end", range er (ec + 1)) :: Nil))
+    :: ("range", fcToRange fc)
     :: ("message", JsonStr msg)
     :: ("source", JsonStr "newt") -- what is this key for?
     :: Nil
-  where
-    range : Int → Int → Json
-    range l c = JsonObj $ ("line", JsonInt l) :: ("character", JsonInt c) :: Nil
 -- These shouldn't escape
 errorToDiag (Postpone fc qn msg) = errorToDiag $ E fc "Postpone \{show qn} \{msg}"
 

src/Lib/Elab.newt

@@ -440,10 +440,8 @@ solve env m sp t = do
         -- let someone else solve this and then check again.
         debug $ \ _ => "CONSTRAINT2 \{show ix} \{show sp} =?= \{show t}"
         addConstraint env m sp t
-      E fc msg => throwError (E fc "\{msg} for \{show ix} \{show sp} =?= \{show t}")
-        -- debug $ \ _ => "CONSTRAINT3 \{show ix} \{show sp} =?= \{show t}"
-        -- debug $ \ _ => "because \{showError "" err}"
-        -- addConstraint env m sp t
+      -- replace with wrapper
+      err => throwError (E (getFC err) "\{errorMsg err} for \{show ix} \{show sp} =?= \{show t}")
         )
 
 unifySpine : Env -> UnifyMode -> Bool -> SnocList Val -> SnocList Val  -> M UnifyResult