Merge pull request #911 from coq/jump-to-def

feat: jump to definition proof of concept

flake.nix

@@ -4,7 +4,7 @@
   inputs = {
     flake-utils.url = "github:numtide/flake-utils";
 
-    coq-master = { url = "github:coq/coq/668dc3ca9735a2b008f5ce52c14969af59cc24e1"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:coq/coq/d6dd8a618cbf628a6580c9a42db0cf5f44606bea"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };

language-server/dm/documentManager.ml

@@ -749,6 +749,48 @@ let hover st pos =
   let lconstr = Procq.Constr.lconstr
 [%%endif]
 
+
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+let jump_to_definition _  _ = None
+[%%else]
+let jump_to_definition st pos =
+  let raw_doc = Document.raw_document st.document in
+  let loc = RawDocument.loc_of_position raw_doc pos in
+  let opattern = RawDocument.word_at_position raw_doc pos in
+  match opattern with
+  | None -> log "jumpToDef: no word found at cursor"; None
+  | Some pattern ->
+    log ("jumpToDef: found word at cursor: \"" ^ pattern ^ "\"");
+    try
+    let qid = parse_entry st loc (Procq.Prim.qualid) pattern in
+      let ref = Nametab.locate_extended qid in
+        match Nametab.cci_src_loc ref with
+          | None -> None
+          | Some loc ->
+            begin match loc.Loc.fname with
+              | Loc.ToplevelInput | InFile  { dirpath = None } -> None
+              | InFile { dirpath = Some dp } ->
+                  let f = Loadpath.locate_absolute_library @@ Libnames.dirpath_of_string dp in
+                  begin match f with
+                    | Ok f ->
+                      let f =  Filename.remove_extension f ^ ".v" in
+                      (if Sys.file_exists f then
+                        let b_pos = Position.create ~character:(loc.bp - loc.bol_pos) ~line:(loc.line_nb - 1) in
+                        let e_pos = Position.create ~character:(loc.ep - loc.bol_pos) ~line:(loc.line_nb - 1) in
+                        let range = Range.create ~end_:b_pos ~start:e_pos in
+                        Some (range, f)
+                      else
+                        None
+                      )
+                    | Error _ -> None
+                  end
+            end
+        with e ->
+          let e, info = Exninfo.capture e in
+          log (Pp.string_of_ppcmds @@ CErrors.iprint (e, info)); None
+
+[%%endif]
+
 let check st pos ~pattern =
   let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
   match get_context st pos with

language-server/dm/documentManager.mli

@@ -132,6 +132,8 @@ val hover : state -> Position.t -> MarkupContent.t option
     if None, the position did not have a word,
     if Some, an Ok/Error result is returned. *)
 
+val jump_to_definition : state -> Position.t -> (Range.t * string) option
+
 val check : state -> Position.t -> pattern:string -> (pp,error) Result.t
 
 val locate : state -> Position.t -> pattern:string -> (pp, error) Result.t

language-server/vscoqtop/lspManager.ml

@@ -153,10 +153,12 @@ let do_initialize id params =
   let completionProvider = CompletionOptions.create ~resolveProvider:false () in
   let documentSymbolProvider = `DocumentSymbolOptions (DocumentSymbolOptions.create ~workDoneProgress:true ()) in
   let hoverProvider = `Bool true in
+  let definitionProvider = `Bool true in
   let capabilities = ServerCapabilities.create
     ~textDocumentSync
     ~completionProvider
     ~hoverProvider
+    ~definitionProvider
     ~documentSymbolProvider
   ()
   in
@@ -367,7 +369,7 @@ let textDocumentDidClose params =
   let Lsp.Types.DidCloseTextDocumentParams.{ textDocument } = params in
   let path = DocumentUri.to_path textDocument.uri in
   begin match Hashtbl.find_opt states path with
-  | None -> assert false
+  | None -> log @@ "[textDocumentDidClose] closed document with no state"
   | Some { st } -> replace_state path st false
   end;
   consider_purge_invisible_tabs ();
@@ -383,6 +385,19 @@ let textDocumentHover id params =
     | Some contents -> Ok (Some (Hover.create ~contents:(`MarkupContent contents) ()))
     | _ -> Ok None (* FIXME handle error case properly *)
 
+let textDocumentDefinition params =
+  let Lsp.Types.DefinitionParams.{ textDocument; position } = params in
+  match Hashtbl.find_opt states (DocumentUri.to_path textDocument.uri) with
+  | None -> log @@ "[textDocumentDefinition] ignoring event on non existing document"; Ok None (* FIXME handle error case properly *)
+  | Some { st } -> 
+    match Dm.DocumentManager.jump_to_definition st position with
+    | None -> log @@ "[textDocumentDefinition] could not find symbol location"; Ok None (* FIXME handle error case properly *)
+    | Some (range, uri) ->
+      let uri = DocumentUri.of_path uri in
+      let location = Location.create ~range:range ~uri:uri in
+      Ok (Some (`Location [location]))
+
+
 let progress_hook uri () =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log @@ "ignoring non existent document"
@@ -548,6 +563,8 @@ let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a,
     do_shutdown id ()
   | TextDocumentCompletion params ->
     textDocumentCompletion id params
+  | TextDocumentDefinition params ->
+    textDocumentDefinition params, []
   | TextDocumentHover params ->
     textDocumentHover id params, []
   | DocumentSymbol params ->