diff --git a/CHANGES.md b/CHANGES.md index 002ba362..ae9e5819 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -21,6 +21,11 @@ #755, cc: #722, #725) - [hover] Show input howto for unicode characters on hover (@ejgallego, Léo Stefanesco, #756) + - [lsp] [definition] Support for jump to definition across workspace + files. The location information is obtained from `.glob` files, so + it is often not perfect. (@ejgallego, #762, fixes #317) + - [lsp] [hover] Show full name and provenance of identifiers + (@ejgallego, #762) # coq-lsp 0.1.10: Hasta el 40 de Mayo _en effect_... ---------------------------------------------------- diff --git a/controller/rq_common.ml b/controller/rq_common.ml index a8e1c9ba..8a18a4c8 100644 --- a/controller/rq_common.ml +++ b/controller/rq_common.ml @@ -96,3 +96,60 @@ let get_uchar_at_point ~prev ~contents ~point = else None in get_char_at_point_gen ~prev ~get ~contents ~point + +module CoqModule = struct + type t = + { dp : Names.DirPath.t + ; source : string + ; vo : string + ; uri : Lang.LUri.File.t + } + + let uri { uri; _ } = uri + let source { source; _ } = source + + let make dp = + match Loadpath.locate_absolute_library dp with + | Ok vo -> + Fleche.Io.Log.trace "rq_definition" "File Found"; + let source = Filename.remove_extension vo ^ ".v" in + let source = Str.replace_first (Str.regexp "_build/default/") "" source in + let uri = Lang.LUri.of_string ("file://" ^ source) in + let uri = Lang.LUri.File.of_uri uri |> Result.get_ok in + Ok { dp; source; vo; uri } + | Error err -> + Fleche.Io.Log.trace "rq_definition" "File Not Found :("; + (* Debug? *) + Error err + + let offset_to_range source (bp, ep) = + let text = + Coq.Compat.Ocaml_414.In_channel.(with_open_text source input_all) + in + let rec count (lines, char) cur goal = + if cur >= goal then (lines, char) + else + match text.[cur] with + | '\n' -> count (lines + 1, 0) (cur + 1) goal + | _ -> count (lines, char + 1) (cur + 1) goal + in + (* XXX UTF-8 / 16 adjust *) + let bline, bchar = count (0, 0) 0 bp in + let eline, echar = count (bline, bchar) bp ep in + let start = Lang.Point.{ line = bline; character = bchar; offset = bp } in + let end_ = Lang.Point.{ line = eline; character = echar; offset = ep } in + Lang.Range.{ start; end_ } + + let find { vo; source; _ } name = + let glob = Filename.remove_extension vo ^ ".glob" in + match Coq.Glob.open_file glob with + | Error err -> + Fleche.Io.Log.trace "rq_definition:open_file" ("Error: " ^ err); + Error err + | Ok g -> ( + match Coq.Glob.get_info g name with + | Some { offset; _ } -> Ok (Some (offset_to_range source offset)) + | None -> + Fleche.Io.Log.trace "rq_definition:get_info" "Not found"; + Ok None) +end diff --git a/controller/rq_common.mli b/controller/rq_common.mli index 75ac2447..4a9a22a7 100644 --- a/controller/rq_common.mli +++ b/controller/rq_common.mli @@ -20,3 +20,13 @@ val get_uchar_at_point : -> contents:Fleche.Contents.t -> point:int * int -> (Uchar.t * string) option + +module CoqModule : sig + type t + + (* Lookup module as needed *) + val make : Names.DirPath.t -> (t, Loadpath.Error.t) Result.t + val uri : t -> Lang.LUri.File.t + val source : t -> string + val find : t -> string -> (Lang.Range.t option, string) Result.t +end diff --git a/controller/rq_definition.ml b/controller/rq_definition.ml index fe7d28cc..131602c0 100644 --- a/controller/rq_definition.ml +++ b/controller/rq_definition.ml @@ -5,17 +5,80 @@ (* Written by: Emilio J. Gallego Arias *) (************************************************************************) -let request ~token:_ ~(doc : Fleche.Doc.t) ~point = +let get_from_toc ~doc id_at_point = + let { Fleche.Doc.toc; _ } = doc in + Fleche.Io.Log.trace "rq_definition" "get_from_toc"; + match CString.Map.find_opt id_at_point toc with + | Some node -> + let uri = doc.uri in + let range = node.range in + Some Lsp.Core.Location.{ uri; range } + | None -> None + +let lp_to_string = function + | Loadpath.Error.LibNotFound -> "library not found" + | Loadpath.Error.LibUnmappedDir -> "unmapped library" + +let err_code = -32803 + +let locate_extended qid = + try Some (Nametab.locate_extended qid) with Not_found -> None + +let find_name_in dp name = + match Rq_common.CoqModule.make dp with + | Error err -> Error (err_code, lp_to_string err) + | Ok mod_ -> ( + let uri = Rq_common.CoqModule.uri mod_ in + match Rq_common.CoqModule.find mod_ name with + | Error err -> Error (err_code, err) + | Ok range -> + Ok (Option.map (fun range -> Lsp.Core.Location.{ uri; range }) range)) + +let get_from_file id_at_point = + Fleche.Io.Log.trace "rq_definition" "get_from_file"; + let qid = Libnames.qualid_of_string id_at_point in + match locate_extended qid with + | Some (TrueGlobal (ConstRef cr)) -> + Fleche.Io.Log.trace "rq_definition" "TrueGlobal Found"; + let dp = Names.Constant.modpath cr |> Names.ModPath.dp in + let name = Names.Constant.to_string cr in + find_name_in dp name + | Some (TrueGlobal (IndRef (ind, _idx))) -> + let dp = Names.MutInd.modpath ind |> Names.ModPath.dp in + let name = Names.MutInd.to_string ind in + find_name_in dp name + | Some (Abbrev _abbrev) -> + (* Needs improved .glob parsing *) + Ok None + | _ -> + Fleche.Io.Log.trace "rq_definition" "No TrueGlobal Found"; + Ok None + +let get_from_file ~token ~st id_at_point = + let f = get_from_file in + Coq.State.in_state ~token ~st ~f id_at_point + +let request ~token ~(doc : Fleche.Doc.t) ~point = let { Fleche.Doc.contents; _ } = doc in + let ok s = Coq.Protect.E.ok (Result.Ok s) in + let idp = Rq_common.get_id_at_point ~contents ~point in Option.cata - (fun id_at_point -> - let { Fleche.Doc.toc; _ } = doc in - match CString.Map.find_opt id_at_point toc with - | Some node -> - let uri = doc.uri in - let range = node.range in - Lsp.Core.Location.({ uri; range } |> to_yojson) - | None -> `Null) - `Null - (Rq_common.get_id_at_point ~contents ~point) - |> Result.ok + (fun idp -> + match get_from_toc ~doc idp with + | Some loc -> ok (Some loc) + | None -> + let approx = Fleche.Info.PrevIfEmpty in + Fleche.Info.LC.node ~doc ~point approx + |> Option.cata + (fun node -> + let st = Fleche.Doc.Node.state node in + get_from_file ~token ~st idp) + (ok None)) + (ok None) idp + |> Coq.Protect.E.map + ~f:(Result.map (Option.cata Lsp.Core.Location.to_yojson `Null)) + +let request ~token ~doc ~point = + let name = "textDocument/definition" in + let f () = request ~token ~doc ~point in + Request.R.of_execution ~name ~f () diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml index 7386e957..00abe072 100644 --- a/controller/rq_hover.ml +++ b/controller/rq_hover.ml @@ -12,7 +12,7 @@ let build_ind_type mip = Inductive.type_of_inductive mip type id_info = | Notation of Pp.t - | Def of Pp.t + | Def of (Pp.t * Names.Constant.t option * string option) let info_of_ind env sigma ((sp, i) : Names.Ind.t) = let mib = Environ.lookup_mind sp env in @@ -37,7 +37,7 @@ let info_of_ind env sigma ((sp, i) : Names.Ind.t) = (Impargs.implicits_of_global (Names.GlobRef.IndRef (sp, i))) in let impargs = List.map Impargs.binding_kind_of_status impargs in - Def (Printer.pr_ltype_env ~impargs env_params sigma arity) + Def (Printer.pr_ltype_env ~impargs env_params sigma arity, None, None) let type_of_constant cb = cb.Declarations.const_type @@ -53,7 +53,12 @@ let info_of_const env sigma cr = (Impargs.implicits_of_global (Names.GlobRef.ConstRef cr)) in let impargs = List.map Impargs.binding_kind_of_status impargs in - Def (Printer.pr_ltype_env env sigma ~impargs typ) + let typ = Printer.pr_ltype_env env sigma ~impargs typ in + let dp = Names.Constant.modpath cr |> Names.ModPath.dp in + let source = + Rq_common.CoqModule.(make dp |> Result.to_option |> Option.map source) + in + Def (typ, Some cr, source) let info_of_var env vr = let vdef = Environ.lookup_named vr env in @@ -70,7 +75,7 @@ let info_of_constructor env cr = in ctype -let print_type env sigma x = Def (Printer.pr_ltype_env env sigma x) +let print_type env sigma x = Def (Printer.pr_ltype_env env sigma x, None, None) let info_of_id env sigma id = let qid = Libnames.qualid_of_string id in @@ -114,10 +119,22 @@ let info_of_id_at_point ~token ~node id = let st = node.Fleche.Doc.Node.state in Coq.State.in_state ~token ~st ~f:(info_of_id ~st) id +let pp_cr fmt = function + | None -> () + | Some cr -> + Format.fprintf fmt " - **full path**: `%a`@\n" Pp.pp_with + (Names.Constant.print cr) + +let pp_file fmt = function + | None -> () + | Some file -> Format.fprintf fmt " - **in file**: `%s`" file + let pp_typ id = function - | Def typ -> + | Def (typ, cr, file) -> let typ = Pp.string_of_ppcmds typ in - Format.(asprintf "```coq\n%s : %s\n```" id typ) + Format.( + asprintf "@[```coq\n%s : %s@\n```@\n@[%a@]@[%a@]@]" id typ pp_cr cr + pp_file file) | Notation nt -> let nt = Pp.string_of_ppcmds nt in Format.(asprintf "```coq\n%s\n```" nt) diff --git a/coq/compat.ml b/coq/compat.ml index ea4561c3..bec4f452 100644 --- a/coq/compat.ml +++ b/coq/compat.ml @@ -120,3 +120,12 @@ let format_to_file ~file ~f x = Out_channel.with_open_bin file (fun oc -> let of_fmt = Format.formatter_of_out_channel oc in Format.fprintf of_fmt "@[%a@]%!" f x) + +module Option = struct + include Stdlib.Option + + module O = struct + let ( let+ ) r f = map f r + let ( let* ) r f = bind r f + end +end diff --git a/coq/compat.mli b/coq/compat.mli index fc56a00c..b3eeb5e0 100644 --- a/coq/compat.mli +++ b/coq/compat.mli @@ -35,3 +35,12 @@ module Result : sig -> ('r, 'e) Result.t -> unit end + +module Option : sig + include module type of Stdlib.Option + + module O : sig + val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t + val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t + end +end diff --git a/coq/glob.ml b/coq/glob.ml index 6c9eb714..054e72aa 100644 --- a/coq/glob.ml +++ b/coq/glob.ml @@ -184,7 +184,4 @@ let open_file file = Compat.Ocaml_414.In_channel.with_open_text file (Coq.read_glob (Some vfile)) else Error (Format.asprintf "Cannot open file: %s" file) -let get_info map name = - match DefMap.find_opt name map with - | Some info -> Ok info - | None -> Error (Format.asprintf "definition %s not found in glob table" name) +let get_info map name = DefMap.find_opt name map diff --git a/coq/glob.mli b/coq/glob.mli index 83376443..742a2564 100644 --- a/coq/glob.mli +++ b/coq/glob.mli @@ -18,6 +18,7 @@ (* Glob file that was read and parsed successfully *) type t +(* Input is a .glob file *) val open_file : string -> (t, string) Result.t module Info : sig @@ -27,4 +28,4 @@ module Info : sig } end -val get_info : t -> string -> (Info.t, string) Result.t +val get_info : t -> string -> Info.t option diff --git a/etc/doc/PROTOCOL.md b/etc/doc/PROTOCOL.md index 8da3b04c..e802371d 100644 --- a/etc/doc/PROTOCOL.md +++ b/etc/doc/PROTOCOL.md @@ -19,41 +19,41 @@ https://github.com/microsoft/language-server-protocol/issues/1414 If a feature doesn't appear here it usually means it is not planned in the short term: -| Method | Support | Notes | -|---------------------------------------|---------|------------------------------------------------------------| -| `initialize` | Partial | We don't obey the advertised client capabilities | -| `client/registerCapability` | No | Not planned ATM | -| `$/setTrace` | Yes | | -| `$/logTrace` | Yes | | -| `window/logMessage` | Yes | | -|---------------------------------------|---------|------------------------------------------------------------| -| `textDocument/didOpen` | Yes | We can't reuse Memo tables yet | -| `textDocument/didChange` | Yes | We only support `TextDocumentSyncKind.Full` for now | -| `textDocument/didClose` | Partial | We'd likely want to save a `.vo` file on close if possible | -| `textDocument/didSave` | Partial | Undergoing behavior refinement | -|---------------------------------------|---------|------------------------------------------------------------| -| `notebookDocument/didOpen` | No | Planned | -|---------------------------------------|---------|------------------------------------------------------------| -| `textDocument/declaration` | No | Planned, blocked on upstream issues | -| `textDocument/definition` | Partial | Working only locally on files for now | -| `textDocument/references` | No | Planned, blocked on upstream issues | -| `textDocument/hover` | Yes | Shows stats and type info of identifiers at point | -| `textDocument/codeLens` | No | | -| `textDocument/foldingRange` | No | | -| `textDocument/documentSymbol` | Yes | Sections and modules missing (#322) | -| `textDocument/semanticTokens` | No | Planned | -| `textDocument/inlineValue` | No | Planned | -| `textDocument/inlayHint` | No | Planned | -| `textDocument/completion` | Partial | Needs more work locally and upstream (#50) | -| `textDocument/publishDiagnostics` | Yes | | -| `textDocument/diagnostic` | No | Planned, issue #49 | -| `textDocument/codeAction` | No | Planned | -| `textDocument/selectionRange` | Partial | Selection for a point is its span; no parents | -|---------------------------------------|---------|------------------------------------------------------------| -| `workspace/workspaceFolders` | Yes | Each folder should have a `_CoqProject` file at the root. | -| `workspace/didChangeWorkspaceFolders` | Yes | | -| `workspace/didChangeConfiguration` | Yes (*) | We still do a client -> server push, instead of pull | -|---------------------------------------|---------|------------------------------------------------------------| +| Method | Support | Notes | +|---------------------------------------|---------|---------------------------------------------------------------| +| `initialize` | Partial | We don't obey the advertised client capabilities | +| `client/registerCapability` | No | Not planned ATM | +| `$/setTrace` | Yes | | +| `$/logTrace` | Yes | | +| `window/logMessage` | Yes | | +|---------------------------------------|---------|---------------------------------------------------------------| +| `textDocument/didOpen` | Yes | We can't reuse Memo tables yet | +| `textDocument/didChange` | Yes | We only support `TextDocumentSyncKind.Full` for now | +| `textDocument/didClose` | Partial | We'd likely want to save a `.vo` file on close if possible | +| `textDocument/didSave` | Partial | Undergoing behavior refinement | +|---------------------------------------|---------|---------------------------------------------------------------| +| `notebookDocument/didOpen` | No | Planned | +|---------------------------------------|---------|---------------------------------------------------------------| +| `textDocument/declaration` | No | Planned, blocked on upstream issues | +| `textDocument/definition` | Yes (*) | Uses .glob information which is often incomplete | +| `textDocument/references` | No | Planned, blocked on upstream issues | +| `textDocument/hover` | Yes | Shows stats and type info of identifiers at point, extensible | +| `textDocument/codeLens` | No | | +| `textDocument/foldingRange` | No | | +| `textDocument/documentSymbol` | Yes | Sections and modules missing (#322) | +| `textDocument/semanticTokens` | No | Planned | +| `textDocument/inlineValue` | No | Planned | +| `textDocument/inlayHint` | No | Planned | +| `textDocument/completion` | Partial | Needs more work locally and upstream (#50) | +| `textDocument/publishDiagnostics` | Yes | | +| `textDocument/diagnostic` | No | Planned, issue #49 | +| `textDocument/codeAction` | No | Planned | +| `textDocument/selectionRange` | Partial | Selection for a point is its span; no parents | +|---------------------------------------|---------|---------------------------------------------------------------| +| `workspace/workspaceFolders` | Yes | Each folder should have a `_CoqProject` file at the root. | +| `workspace/didChangeWorkspaceFolders` | Yes | | +| `workspace/didChangeConfiguration` | Yes (*) | We still do a client -> server push, instead of pull | +|---------------------------------------|---------|---------------------------------------------------------------| ### URIs accepted by coq-lsp diff --git a/examples/Pff.v b/examples/Pff.v index e058003b..252b89f3 100644 --- a/examples/Pff.v +++ b/examples/Pff.v @@ -11,6 +11,8 @@ Require Export List. Require Export PeanoNat. Require Import Psatz. +Set Warnings "-deprecated". + (* Compatibility workaround, remove once requiring Coq >= 8.16 *) Module Import Compat. diff --git a/petanque/agent.ml b/petanque/agent.ml index dcb846a8..b72774c2 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -237,8 +237,10 @@ end let info_of ~glob ~name = let open Coq.Compat.Result.O in let* g = Memo.open_file glob in - let+ { Coq.Glob.Info.kind; offset } = Coq.Glob.get_info g name in - (kind, offset) + Ok + (Option.map + (fun { Coq.Glob.Info.kind; offset } -> (kind, offset)) + (Coq.Glob.get_info g name)) let raw_of ~file ~offset = match offset with @@ -254,7 +256,12 @@ let to_premise (p : Coq.Library_file.Entry.t) : Premise.t = let file = Filename.(remove_extension file ^ ".v") in let glob = Filename.(remove_extension file ^ ".glob") in let range = Error "not implemented yet" in - let kind, offset = info_of ~glob ~name |> Coq.Compat.Result.split in + let kind, offset = + match info_of ~glob ~name with + | Ok None -> (Error "not in glob table", Error "not in glob table") + | Error err -> (Error err, Error err) + | Ok (Some (kind, offset)) -> (Ok kind, Ok offset) + in let raw_text = raw_of ~file ~offset in { full_name = name; file; kind; range; offset; raw_text }