[info] Hook completion call, fix still some issues with range.

Author: ejgallego

CHANGES.md

@@ -63,6 +63,7 @@
  - new trim command (both in the server and in VSCode) to liberate
    space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
    #348)
+ - completion and notation display (@ejgallego, #41 ???)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

controller/rq_completion.ml

@@ -91,19 +91,43 @@ let get_char_at_point ~(doc : Fleche.Doc.t) ~point =
     None
 
 (* point is a utf char! *)
-let completion ~token:_ ~doc ~point =
+(* let completion ~token:_ ~doc ~point = *)
+
+let build_doc_idents_and_nametab ~token ~doc ~point prefix =
+  let st = Fleche.Info.LC.node ~doc ~point PrevIfEmpty in
+  let st = Option.map Fleche.Doc.Node.state st in
+  let st = Option.default doc.Fleche.Doc.root st in
+  let toc = build_doc_idents ~doc in
+  let open Coq.Protect.E.O in
+  let+ nametab = Fleche.Info.Completion.candidates ~token ~st prefix in
+  let nametab = Option.default [] nametab in
+  let nametab = CList.map (fun label -> mk_completion ~label ()) nametab in
+  toc @ nametab
+
+(* point is a utf-16 charpoint! *)
+let completion ~token ~doc ~point =
   (* Instead of get_char_at_point we should have a CompletionContext.t, to be
      addressed in further completion PRs *)
-  (match get_char_at_point ~doc ~point with
+  match get_char_at_point ~doc ~point with
   | None ->
     let incomplete = true in
     let items = [] in
-    mk_completion_list ~incomplete ~items
+    mk_completion_list ~incomplete ~items |> Result.ok |> Coq.Protect.E.ok
   | Some c ->
-    let incomplete, items =
-      if c = '\\' then (false, unicode_list point)
-      else (true, build_doc_idents ~doc)
+    let open Coq.Protect.E.O in
+    let+ incomplete, items =
+      if c = '\\' then Coq.Protect.E.ok (false, unicode_list point)
+      else
+        (* We want to get the previous *)
+        let point = (fst point, max (snd point - 1) 0) in
+        let prefix = Rq_common.get_id_at_point ~contents:doc.contents ~point in
+        let prefix = Option.default (String.make 1 c) prefix in
+        let+ items = build_doc_idents_and_nametab ~token ~doc ~point prefix in
+        (true, items)
     in
     let res = mk_completion_list ~incomplete ~items in
-    res)
-  |> Result.ok
+    Result.ok res
+
+let completion ~token ~doc ~point =
+  let f () = completion ~token ~doc ~point in
+  Request.R.of_execution ~name:"completion" ~f ()

etc/todo.org

@@ -4,13 +4,16 @@ info.
 
 * Coq LSP Todos
 
+** 0.2
+ - jump to definition
+ - warnings suggestions / fix
+
+** 0.3
  - profit from command refinement
  - lsp server process and coq-lsp-checker client for every document
  - dune integration, auto-build, dap
  - documentation links
- - jump to definition
  - integration with tracing
- - warnings suggestions / fix
  - flags for coq process
  - Implement onsave => compile vo file? [see on-disk cache issues below]
 

fleche/debug.ml

@@ -12,6 +12,9 @@ let send = false || all || lsp
 let read = false || all || lsp
 let lsp_init = false || all || lsp
 
+(* finding tokens from a position *)
+let find = false || all
+
 (* Parsing (this is a bit expensive as it will call the printer *)
 let parsing = false || all
 
@@ -31,4 +34,4 @@ let sched_wakeup = false || all
 let request_delay = true || all
 
 (* Competion *)
-let completion = false || all
+let completion = true || all

fleche/info.ml

@@ -69,6 +69,7 @@ module LineCol : Point with type t = int * int = struct
       if line1 = line && line2 = line then col1 <= col && col < col2
       else (line1 = line && col1 <= col) || (line2 = line && col < col2)
 
+  (* Point is beyond [range] *)
   let gt_range ?range (line, col) =
     match range with
     | None -> false
@@ -172,6 +173,18 @@ module Goals = struct
 end
 
 module Completion = struct
+  let obind f x = Option.bind x f
+
+  (* let find ~doc ~point approx = *)
+  (*   let res = find ~doc ~point approx in *)
+  (*   match res with *)
+  (*   | Some res -> *)
+  (*     Io.Log.trace "info:find" ("found node at " ^ P.to_string point); *)
+  (*     Some res *)
+  (*   | None -> *)
+  (*     Io.Log.trace "info:find" ("failed at " ^ P.to_string point); *)
+  (*     None *)
+
   (* XXX: This belongs in Coq *)
   let pr_extref gr =
     match gr with
@@ -180,13 +193,57 @@ module Completion = struct
 
   (* XXX This may fail when passed "foo." for example, so more sanitizing is
      needed *)
-  let to_qualid p = try Some (Libnames.qualid_of_string p) with _ -> None
+  let remove_dot_if_last p : string =
+    let l = String.length p in
+    if l > 1 then if p.[l - 1] = '.' then String.sub p 0 (l - 1) else p else p
+
+  (* let candidates ~token ~st prefix = *)
+  (*   let ( let* ) = Option.bind in *)
+  (*   Coq.State.in_state ~token ~st prefix ~f:(fun prefix -> *)
+  (*       let* p = to_qualid prefix in *)
+  (*       Nametab.completion_canditates p *)
+  (*       |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x)) *)
+  (*       |> some) *)
+  let to_qualid p =
+    let p = remove_dot_if_last p in
+    try Some (Libnames.qualid_of_string p)
+    with _ ->
+      Io.Log.trace "completion" ("broken qualid_of_string: " ^ p);
+      None
+
+  let completion ~token ~st prefix =
+    Coq.State.in_state ~token ~st prefix ~f:(fun prefix ->
+        to_qualid prefix
+        |> obind (fun p ->
+               Nametab.completion_canditates p
+               |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x))
+               |> List.append
+                    (Notgram_ops.get_defined_notations () |> List.map snd)
+               |> some))
+
+  let _get_id_at_node_point offset range text = Span.find ~offset ~range text
 
+  let debug_completion cat msg =
+    if Debug.completion then Io.Log.trace ("completion: " ^ cat) msg
+
+  let pr_completion_res = function
+    | None -> "no results"
+    | Some res -> string_of_int (List.length res) ^ " results"
+
+  (* This is still buggy for the case that find doesn't work (i.e. no ast) *)
+  (* let candidates ~st ~point:_ () = *)
   let candidates ~token ~st prefix =
-    let ( let* ) = Option.bind in
-    Coq.State.in_state ~token ~st prefix ~f:(fun prefix ->
-        let* p = to_qualid prefix in
-        Nametab.completion_canditates p
-        |> List.map (fun x -> Pp.string_of_ppcmds (pr_extref x))
-        |> some)
+    (* we do exact matching for... *)
+    (* let range = node.Doc.Node.range in *)
+    (* let text = doc.Doc.contents.text in *)
+    (* let span = Span.make ~contents:doc.Doc.contents ~loc in *)
+    (* let offset = P.to_offset point text in *)
+    (* debug_completion "offset" (string_of_int offset); *)
+    (* let prefix = get_id_at_node_point offset range text in *)
+    (* let prefix = "" in *)
+    debug_completion "prefix" prefix;
+    let open Coq.Protect.E.O in
+    let+ res = completion ~token ~st prefix in
+    debug_completion "n results" (pr_completion_res res);
+    res
 end

fleche/span.ml

@@ -0,0 +1,50 @@
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2022 Inria           -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+(* Status: Experimental                                                 *)
+(************************************************************************)
+
+type t =
+  { range : Lang.Range.t
+  ; contents : String.t
+  }
+
+let make ~contents ~range = { range; contents }
+
+let delim c =
+  match c with
+  | '\n' | ' ' -> true
+  | _ -> false
+
+let rec find_backwards_delim offset lower text =
+  if offset = lower then offset
+  else if delim text.[offset - 1] then offset
+  else find_backwards_delim (offset - 1) lower text
+
+let rec id_at_point acc offset upper text =
+  if delim text.[offset] || offset + 1 = upper then acc
+  else id_at_point (text.[offset] :: acc) (offset + 1) upper text
+
+let id_at_point offset upper text =
+  let id = id_at_point [] offset upper text |> List.rev in
+  let len = List.length id in
+  String.init len (List.nth id)
+
+let debug_find cat msg =
+  if Debug.find then Io.Log.trace ("Span.find: " ^ cat) msg
+
+let find ~offset ~(range : Lang.Range.t) text =
+  let lower = range.start.offset in
+  let upper = range.end_.offset in
+  debug_find "lower / upper" (string_of_int lower ^ "/" ^ string_of_int upper);
+  debug_find "text length" (string_of_int (String.length text));
+  let rtext = String.sub text lower (upper - lower) in
+  debug_find "ranged" rtext;
+  debug_find "char at off" (String.make 1 text.[offset]);
+  debug_find "initial offset" (string_of_int offset);
+  let offset = find_backwards_delim offset lower text in
+  debug_find "span.find, base offset" (string_of_int offset);
+  id_at_point offset upper text

fleche/span.mli

@@ -0,0 +1,34 @@
+(************************************************************************)
+(* Coq Language Server Protocol                                         *)
+(* Copyright 2019 MINES ParisTech -- Dual License LGPL 2.1 / GPL3+      *)
+(* Copyright 2022 Inria           -- Dual License LGPL 2.1 / GPL3+      *)
+(* Written by: Emilio J. Gallego Arias                                  *)
+(************************************************************************)
+(* Status: Experimental                                                 *)
+(************************************************************************)
+
+type t =
+  { range : Lang.Range.t
+  ; contents : String.t
+  }
+
+val make : contents:String.t -> range:Lang.Range.t -> t
+
+(** [find ~offset ~range text] finds an identifier at offset, offset is
+    absolutely positioned *)
+val find : offset:int -> range:Lang.Range.t -> string -> string
+
+(** TODO:
+
+    - We want some kind of tokenization for the span, two kinds of spans, with
+      AST, and without *)
+
+(** Focused text span on a range / XXX same structure than caching *)
+
+(**
+  type context =
+    | Parsed of { span : t; node : Doc.node }
+    (** [span] corresponding to [node]  *)
+    | Text of { span : t; prev : Doc.node }
+    (** Independent [span], [prev] node for help *)
+*)