[coq] [fleche] Beginnings of Unicode Support

We enforce a stricter separation between `Range.t` and `Loc.t`, with
Flèche not using `Loc.t` anymore, and `Range.t` being in unicode
character positions.

To achieve this we need to convert all the positions coming from Coq.

As we keep a position per sentence, this implies a `O(n)` number of
conversions in total, where `n is the number of sentences; we could
optimize that to be lazy, but it is unlikely to show in profiles as
that is a pretty reasonably `O(.)` factor.

Should fix #193 and #197

TODO:

- more principled conversion on `Coq.Protect
- see what is going on with the loc-independent cache (seems already
  broken in terms of space shifting)?

controller/coq_lsp.ml

@@ -112,8 +112,9 @@ let do_initialize ~params =
   do_client_options coq_lsp_options;
   check_client_version !Fleche.Config.v.client_version;
   let client_capabilities = odict_field "capabilities" params in
-  LIO.trace "init" "client capabilities:";
-  LIO.trace_object "init" (`Assoc client_capabilities);
+  if Fleche.Debug.lsp_init then (
+    LIO.trace "init" "client capabilities:";
+    LIO.trace_object "init" (`Assoc client_capabilities));
   let capabilities =
     [ ("textDocumentSync", `Int 1)
     ; ("documentSymbolProvider", `Bool true)
@@ -231,8 +232,8 @@ let do_position_request ~postpone ~params ~handler =
     match doc.completed with
     | Yes _ -> true
     | Failed loc | Stopped loc ->
-      let proc_line = loc.line_nb_last - 1 in
-      line < proc_line || (line = proc_line && col < loc.ep - loc.bol_pos_last)
+      let proc_line = loc.end_.line in
+      line < proc_line || (line = proc_line && col < loc.end_.character)
   in
   let in_range =
     match version with

controller/doc_manager.ml

@@ -106,8 +106,8 @@ module Handle = struct
         | None -> (handle, Int.Set.empty)
         | Some (id, (req_line, req_col)) ->
           (* XXX: Same code than in doc.ml *)
-          let stop_line = stop_loc.line_nb_last - 1 in
-          let stop_col = stop_loc.ep - stop_loc.bol_pos_last in
+          let stop_line = stop_loc.end_.line in
+          let stop_col = stop_loc.end_.character in
           if
             stop_line > req_line || (stop_line = req_line && stop_col >= req_col)
           then ({ handle with pt_request = None }, Int.Set.singleton id)

controller/requests.ml

@@ -22,16 +22,13 @@ module Util = struct
   let asts_of_doc doc = List.filter_map Fleche.Doc.Node.ast doc.Fleche.Doc.nodes
 end
 
-let mk_syminfo file (name, _path, kind, pos) : Yojson.Safe.t =
+let _mk_syminfo file (name, _path, kind, range) : Yojson.Safe.t =
   `Assoc
     [ ("name", `String name)
     ; ("kind", `Int kind)
     ; (* function *)
       ( "location"
-      , `Assoc
-          [ ("uri", `String file)
-          ; ("range", Lsp.Base.mk_range Fleche.Types.(to_range pos))
-          ] )
+      , `Assoc [ ("uri", `String file); ("range", Lsp.Base.mk_range range) ] )
     ]
 
 let _kind_of_type _tm = 13
@@ -41,17 +38,22 @@ let _kind_of_type _tm = 13
    *) | _ -> 12 (* Function *) *)
 
 let symbols ~(doc : Fleche.Doc.t) =
-  let uri = doc.uri in
-  let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in
-  let ast = Util.asts_of_doc doc in
-  let slist = Coq.Ast.grab_definitions f ast in
-  `List slist
+  ignore doc;
+  (* let uri = doc.uri in *)
+  (* let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in *)
+  (* let ast = Util.asts_of_doc doc in *)
+  (* let slist = Coq.Ast.grab_definitions f ast in *)
+  (* `List slist *)
+  `List []
 
 let hover ~doc ~point =
   let show_loc_info = true in
-  let loc_span = Fleche.Info.LC.loc ~doc ~point Exact in
-  let loc_string =
-    Option.map Coq.Ast.pr_loc loc_span |> Option.default "no ast"
+  let range_span = Fleche.Info.LC.range ~doc ~point Exact in
+  let range_string =
+    let none fmt () = Format.fprintf fmt "no ast" in
+    Format.asprintf "%a"
+      (Format.pp_print_option ~none Fleche.Types.Range.pp)
+      range_span
   in
   let stats = doc.stats in
   let info_string =
@@ -60,17 +62,17 @@ let hover ~doc ~point =
     |> Option.default "no info"
   in
   let hover_string =
-    if show_loc_info then loc_string ^ "\n___\n" ^ info_string else info_string
+    if show_loc_info then range_string ^ "\n___\n" ^ info_string
+    else info_string
   in
   `Assoc
     ([ ( "contents"
        , `Assoc
            [ ("kind", `String "markdown"); ("value", `String hover_string) ] )
      ]
     @ Option.cata
-        (fun loc ->
-          [ ("range", Lsp.Base.mk_range (Fleche.Types.to_range loc)) ])
-        [] loc_span)
+        (fun range -> [ ("range", Lsp.Base.mk_range range) ])
+        [] range_span)
 
 (* Replace by ppx when we can print goals properly in the client *)
 let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t =

coq-lsp.opam

@@ -24,6 +24,7 @@ depends: [
   # lsp dependencies
   "cmdliner"     { >= "1.1.0" }
   "yojson"       { >= "1.7.0" }
+  "camomile"     { >= "1.0.0" }
 
   # Uncomment this for releases
   # "coq"          { >= "8.17" < "8.18"  }

coq/ast.ml

@@ -76,7 +76,7 @@ let grab_definitions f nodes =
 let marshal_in ic : t = Marshal.from_channel ic
 let marshal_out oc v = Marshal.to_channel oc v []
 
-let pr_loc ?(print_file = false) loc =
+let pp_loc ?(print_file = false) fmt loc =
   let open Loc in
   let file =
     if print_file then
@@ -85,7 +85,10 @@ let pr_loc ?(print_file = false) loc =
       | InFile { file; _ } -> "File \"" ^ file ^ "\""
     else "loc"
   in
-  Format.asprintf "%s: line: %d, col: %d -- line: %d, col: %d / {%d-%d}" file
+  Format.fprintf fmt "%s: line: %d, col: %d -- line: %d, col: %d / {%d-%d}" file
     (loc.line_nb - 1) (loc.bp - loc.bol_pos) (loc.line_nb_last - 1)
     (loc.ep - loc.bol_pos_last)
     loc.bp loc.ep
+
+let loc_to_string ?print_file loc =
+  Format.asprintf "%a" (pp_loc ?print_file) loc

coq/ast.mli

@@ -5,8 +5,15 @@ val hash : t -> int
 val compare : t -> t -> int
 val to_coq : t -> Vernacexpr.vernac_control
 val of_coq : Vernacexpr.vernac_control -> t
-val print : t -> Pp.t
 val grab_definitions : (Loc.t -> Names.Id.t -> 'a) -> t list -> 'a list
+
+(** Printing *)
+val print : t -> Pp.t
+
+val pp_loc : ?print_file:bool -> Format.formatter -> Loc.t -> unit
+val loc_to_string : ?print_file:bool -> Loc.t -> string
+
+(** Unused for now *)
 val marshal_in : in_channel -> t
+
 val marshal_out : out_channel -> t -> unit
-val pr_loc : ?print_file:bool -> Loc.t -> string

examples/unicode1.v

@@ -0,0 +1,9 @@
+Axiom P : nat -> Prop.
+Axiom foo : forall {n}, P (S n) -> P n.
+Ltac foo := apply foo.
+Infix "⊆" := lt (at level 10).
+
+Goal forall Γ Δ, Γ ⊆ Δ -> P Γ.
+(* check goal is update after here properly *)
+intros Γ Δ s.
+foo.

fleche/debug.ml

@@ -10,6 +10,7 @@ let cache = false || all
 (* LSP messages: Send and receive *)
 let send = false || all || lsp
 let read = false || all || lsp
+let lsp_init = false || all || lsp
 
 (* Parsing (this is a bit expensive as it will call the printer *)
 let parsing = false || all
@@ -18,7 +19,10 @@ let parsing = false || all
 let scan = false || all
 
 (* Backtraces *)
-let backtraces = false || all
+let backtraces = false || all || true
+
+(* Unicode conversion *)
+let unicode = false || all
 
 (* Sched wakeup *)
 let sched_wakeup = false || all