From fe1d617ae9eea728f16d00a63f9842a81f473acc Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 20 Sep 2024 18:43:50 +0200 Subject: [PATCH 1/2] feat: jump to definition proof of concept WIP --- flake.lock | 12 ++--- flake.nix | 2 +- language-server/dm/documentManager.ml | 63 ++++++++++++++++++++++++++ language-server/dm/documentManager.mli | 2 + language-server/vscoqtop/lspManager.ml | 17 +++++++ 5 files changed, 89 insertions(+), 7 deletions(-) diff --git a/flake.lock b/flake.lock index 6e2b5ade..1e20e0e7 100644 --- a/flake.lock +++ b/flake.lock @@ -8,17 +8,17 @@ ] }, "locked": { - "lastModified": 1721904741, - "narHash": "sha256-WlJJXr7+m7wBATffAMJu1ZX1/7q4OpzkZh7gxIRcMIc=", - "owner": "coq", + "lastModified": 1726840515, + "narHash": "sha256-HiIz9fO0KX8Y6xgZbdX4sWhSZ2cFokbrfSrzOvhZfGc=", + "owner": "rtetley", "repo": "coq", - "rev": "b42eb84e4422dcf428d46553f002c728f705a6a9", + "rev": "e1030a2c30469ed663f8e7e81613e7ac31649605", "type": "github" }, "original": { - "owner": "coq", + "owner": "rtetley", "repo": "coq", - "rev": "b42eb84e4422dcf428d46553f002c728f705a6a9", + "rev": "e1030a2c30469ed663f8e7e81613e7ac31649605", "type": "github" } }, diff --git a/flake.nix b/flake.nix index fad441e9..c59d79d3 100644 --- a/flake.nix +++ b/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"; }; diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 207869c8..b01edda1 100644 --- a/language-server/dm/documentManager.ml +++ b/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 diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 179d0f5d..81f43d21 100644 --- a/language-server/dm/documentManager.mli +++ b/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 diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index d9e4f4d4..60744cbe 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/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 -> From 40cbed58aca649fc00cd5bc137bc9a0e9ff83633 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 25 Sep 2024 12:23:34 +0200 Subject: [PATCH 2/2] WIP --- language-server/dm/documentManager.ml | 4 +++- language-server/vscoqtop/lspManager.ml | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index b01edda1..7c0cefb5 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -707,7 +707,9 @@ let jump_to_definition st pos = | 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 + 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 diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 60744cbe..56c7570c 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -344,7 +344,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 ();