[lsp] Jump to definition for non-local definitions

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_...
 ----------------------------------------------------

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

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

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 ()

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)

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

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

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

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

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
 

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.