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/b42eb84e4422dcf428d46553f002c728f705a6a9"; }; # Should be kept in sync with PIN_COQ in CI workflow
+    coq-master = { url = "github:rtetley/coq/e1030a2c30469ed663f8e7e81613e7ac31649605"; }; # Should be kept in sync with PIN_COQ in CI workflow
     coq-master.inputs.nixpkgs.follows = "nixpkgs";
 
   };

language-server/dm/documentManager.ml

@@ -658,6 +658,69 @@ let hover st pos =
         hover_of_sentence st loc pattern (Document.find_next_qed st.document loc)
     | _ -> None
 
+    (* match loc.Loc.fname with
+    | Loc.ToplevelInput | InFile  { dirpath = None } -> Loc.pr loc
+    | InFile { dirpath = Some dp } ->
+      let f = Loadpath.locate_absolute_library @@ Libnames.dirpath_of_string dp in
+      let f = match f with
+        | Ok f ->
+          let f =  Filename.remove_extension f ^ ".v" in
+          if Sys.file_exists f
+          then str "File " ++ qstring f
+          else str "Library " ++ qstring dp
+        | Error _ -> str "Library " ++ qstring dp
+      in
+      (f ++
+       str", line " ++ int loc.line_nb ++ str", characters " ++
+       int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos)) *)
+
+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 ^ "\"");
+    match st.observe_id with
+    | None -> log "jumpToDef in continuous mode currently not supported"; None
+    | Some Top -> log "jumpToDef with no context"; None
+    | Some (Id id) ->
+      match Document.get_sentence st.document id with
+      | None -> log "jumpToDef: observe_id does not exist"; None
+      | Some { stop } ->
+        let o_pos = RawDocument.position_of_loc raw_doc stop in
+        match get_context st o_pos with
+        | None -> log "No context found"; None
+        | Some _ ->
+          match parse_entry st loc (Pcoq.Prim.smart_global) pattern with
+          | { v = AN qid } -> 
+            begin match Nametab.locate qid with
+              | ConstRef x -> begin match Declare.get_loc x 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 range = RawDocument.range_of_loc raw_doc loc in
+                              Some (range, f)
+                            else
+                              None
+                            )
+                          | Error _ -> None
+                        end
+                  end
+                end
+              | _ -> None
+            end
+          | _ -> None
+
+
 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

@@ -121,6 +121,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,string) Result.t
 
 val locate : state -> Position.t -> pattern:string -> (pp, string) Result.t

language-server/vscoqtop/lspManager.ml

@@ -155,10 +155,12 @@ let do_initialize id params =
   let completionProvider = CompletionOptions.create ~resolveProvider:false () in
   let documentSymbolProvider = `Bool true in
   let hoverProvider = `Bool true in
+  let definitionProvider = `Bool true in
   let capabilities = ServerCapabilities.create
     ~textDocumentSync
     ~completionProvider
     ~hoverProvider
+    ~definitionProvider
     ~documentSymbolProvider
   ()
   in
@@ -358,6 +360,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"
@@ -585,6 +600,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 ->