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

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
 

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
@@ -119,7 +120,7 @@ module type S = sig
   val goals : (approx, Coq.Goals.reified_pp) query
   val messages : (approx, Doc.Node.Message.t list) query
   val info : (approx, Doc.Node.Info.t) query
-  val completion : (string, string list) query
+  val completion : (unit, string list) query
 end
 
 let some x = Some x
@@ -191,6 +192,16 @@ module Make (P : Point) : S with module P := P = struct
   let info ~doc ~point approx =
     find ~doc ~point approx |> Option.map Doc.Node.info
 
+  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
@@ -199,17 +210,52 @@ module Make (P : Point) : S with module P := P = 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 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 ~doc ~point prefix =
-    find ~doc ~point Exact
+  let completion ~node prefix =
+    in_state ~st:node.Doc.Node.state 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 completion ~doc ~point () =
+    (* state for the completion *)
+    find ~doc ~point Prev
     |> obind (fun node ->
-           in_state ~st:node.Doc.Node.state 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))
-                      |> 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
+           debug_completion "prefix" prefix;
+           let res = completion ~node prefix in
+           debug_completion "n results" (pr_completion_res res);
+           res)
 end
 
 module LC = Make (LineCol)

fleche/info.mli

@@ -50,7 +50,7 @@ module type S = sig
   val goals : (approx, Coq.Goals.reified_pp) query
   val messages : (approx, Doc.Node.Message.t list) query
   val info : (approx, Doc.Node.Info.t) query
-  val completion : (string, string list) query
+  val completion : (unit, string list) query
 end
 
 module LC : S with module P := LineCol

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,32 @@
+(************************************************************************)
+(* 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 *)
+*)