[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;
we do this in a principled way, but the whole business is often
delicate.

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.

Fixes #193 , fixes #197 .

CHANGES.md

@@ -1,9 +1,10 @@
-# coq-lsp 0.1.4:
-----------------------
+# coq-lsp 0.1.4: View
+---------------------
 
  - Support for OCaml 4.11 (@ejgallego, #184)
  - The keybinding alt+enter in VSCode is now correctly scoped
    (@artagnon, #188)
+ - Support Unicode files (@ejgallego, #200, fixes #193, fixes #197)
 
 # coq-lsp 0.1.3: Event
 ----------------------

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/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

@@ -3,10 +3,20 @@ type t
 val loc : t -> Loc.t option
 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
+
+(** Internal, will go away once the [Lang.t] interface is ready *)
+val to_coq : t -> Vernacexpr.vernac_control
+
+val of_coq : Vernacexpr.vernac_control -> t

coq/init.mli

@@ -33,4 +33,4 @@ val doc_init :
      root_state:State.t
   -> workspace:Workspace.t
   -> libname:Names.DirPath.t
-  -> State.t Protect.E.t
+  -> (State.t, Loc.t) Protect.E.t

coq/interp.ml

@@ -19,7 +19,7 @@ module Info = struct
   type 'a t = { res : 'a }
 end
 
-type 'a interp_result = 'a Info.t Protect.E.t
+type 'a interp_result = ('a Info.t, Loc.t) Protect.E.t
 
 let coq_interp ~st cmd =
   let st = State.to_coq st in

coq/interp.mli

@@ -19,6 +19,6 @@ module Info : sig
   type 'a t = { res : 'a }
 end
 
-type 'a interp_result = 'a Info.t Protect.E.t
+type 'a interp_result = ('a Info.t, Loc.t) Protect.E.t
 
 val interp : st:State.t -> Ast.t -> State.t interp_result

coq/message.ml

@@ -1,4 +1,4 @@
 (** Messages from Coq *)
-type t = Loc.t option * int * Pp.t
+type 'l t = 'l option * int * Pp.t
 
 type coq = Feedback.feedback

coq/message.mli

@@ -1,4 +1,4 @@
 (** Messages from Coq *)
-type t = Loc.t option * int * Pp.t
+type 'l t = 'l option * int * Pp.t
 
 type coq = Feedback.feedback

coq/parsing.mli

@@ -5,5 +5,5 @@ module Parsable : sig
   val loc : t -> Loc.t
 end
 
-val parse : st:State.t -> Parsable.t -> Ast.t option Protect.E.t
+val parse : st:State.t -> Parsable.t -> (Ast.t option, Loc.t) Protect.E.t
 val discard_to_dot : Parsable.t -> unit

coq/print.mli

@@ -3,4 +3,4 @@ val pr_letype_env :
   -> Environ.env
   -> Evd.evar_map
   -> EConstr.t
-  -> Pp.t Protect.E.t
+  -> (Pp.t, Loc.t) Protect.E.t

coq/protect.ml

@@ -1,18 +1,18 @@
 module Error = struct
-  type payload = Loc.t option * Pp.t
+  type 'l payload = 'l option * Pp.t
 
-  type t =
-    | User of payload
-    | Anomaly of payload
+  type 'l t =
+    | User of 'l payload
+    | Anomaly of 'l payload
 
   let map ~f = function
     | User e -> User (f e)
     | Anomaly e -> Anomaly (f e)
 end
 
 module R = struct
-  type 'a t =
-    | Completed of ('a, Error.t) result
+  type ('a, 'l) t =
+    | Completed of ('a, 'l Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
 
   let map ~f = function
@@ -22,7 +22,8 @@ module R = struct
 
   let map_error ~f = function
     | Completed (Error e) -> Completed (Error (Error.map ~f e))
-    | res -> res
+    | Completed (Ok r) -> Completed (Ok r)
+    | Interrupted -> Interrupted
 
   let map_loc ~f =
     let f (loc, msg) = (Option.map f loc, msg) in
@@ -44,9 +45,9 @@ let eval_exn ~f x =
     else R.Completed (Error (User (loc, msg)))
 
 module E = struct
-  type 'a t =
-    { r : 'a R.t
-    ; feedback : Message.t list
+  type ('a, 'l) t =
+    { r : ('a, 'l) R.t
+    ; feedback : 'l Message.t list
     }
 
   let map ~f { r; feedback } = { r = R.map ~f r; feedback }
@@ -56,7 +57,7 @@ module E = struct
     { r = R.map_loc ~f r; feedback = List.map (map_message ~f) feedback }
 end
 
-let fb_queue : Message.t list ref = ref []
+let fb_queue : Loc.t Message.t list ref = ref []
 
 (* Eval with reified exceptions and feedback *)
 let eval ~f x =

coq/protect.mli

@@ -4,40 +4,42 @@
 
     As of today this includes feedback and exceptions. *)
 module Error : sig
-  type payload = Loc.t option * Pp.t
+  type 'l payload = 'l option * Pp.t
 
-  type t = private
-    | User of payload
-    | Anomaly of payload
+  type 'l t = private
+    | User of 'l payload
+    | Anomaly of 'l payload
 end
 
 module R : sig
-  type 'a t = private
-    | Completed of ('a, Error.t) result
+  type ('a, 'l) t = private
+    | Completed of ('a, 'l Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
 
-  val map : f:('a -> 'b) -> 'a t -> 'b t
-  val map_error : f:(Error.payload -> Error.payload) -> 'a t -> 'a t
+  val map : f:('a -> 'b) -> ('a, 'l) t -> ('b, 'l) t
+
+  val map_error :
+    f:('l Error.payload -> 'm Error.payload) -> ('a, 'l) t -> ('a, 'm) t
 
   (** Update the loc stored in the result, this is used by our cache-aware
       location *)
-  val map_loc : f:(Loc.t -> Loc.t) -> 'a t -> 'a t
+  val map_loc : f:('l -> 'm) -> ('a, 'l) t -> ('a, 'm) t
 end
 
 module E : sig
-  type 'a t =
-    { r : 'a R.t
-    ; feedback : Message.t list
+  type ('a, 'l) t =
+    { r : ('a, 'l) R.t
+    ; feedback : 'l Message.t list
     }
 
-  val map : f:('a -> 'b) -> 'a t -> 'b t
-  val map_loc : f:(Loc.t -> Loc.t) -> 'a t -> 'a t
+  val map : f:('a -> 'b) -> ('a, 'l) t -> ('b, 'l) t
+  val map_loc : f:('l -> 'm) -> ('a, 'l) t -> ('a, 'm) t
 end
 
 (** Must be hooked to allow [Protect] to capture the feedback. *)
-val fb_queue : Message.t list ref
+val fb_queue : Loc.t Message.t list ref
 
 (** Eval a function and reify the exceptions. Note [f] _must_ be pure, as in
     case of anomaly [f] may be re-executed with debug options. Beware, not
     thread-safe! *)
-val eval : f:('i -> 'o) -> 'i -> 'o E.t
+val eval : f:('i -> 'o) -> 'i -> ('o, Loc.t) E.t

coq/state.mli

@@ -17,16 +17,17 @@ val lemmas : st:t -> Proof.t option
 
 (** Execute a command in state [st]. Unfortunately this can produce anomalies as
     Coq state setting is imperative, so we need to wrap it in protect. *)
-val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b Protect.E.t
+val in_state : st:t -> f:('a -> 'b) -> 'a -> ('b, Loc.t) Protect.E.t
 
 (** Drop the proofs from the state *)
 val drop_proofs : st:t -> t
 
 (** Admit an ongoing proof *)
 val admit : st:t -> t
 
-(* Extra *)
+(** Extra / interanl *)
 val marshal_in : in_channel -> t
+
 val marshal_out : out_channel -> t -> unit
 val of_coq : Vernacstate.t -> t
 val to_coq : t -> Vernacstate.t

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 updated after the intros 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