fix(lsp): correctness bugs in positions, lookups, and session state

src/common/library.ml

@@ -212,7 +212,7 @@ let path_of_file : (string -> string) -> string -> Path.t =
       match !mapping with
       | None       -> mapping := Some(mp, fp)
       | Some(_, p) ->
-          if String.(length p < length fp) then mapping := Some(mp, p)
+          if String.(length p < length fp) then mapping := Some(mp, fp)
   in
   LibMap.iter f !lib_mappings;
   (* Fail if there is none. *)

src/common/pos.ml

@@ -34,6 +34,13 @@ let cat : pos -> pos -> pos = fun p1 p2 ->
   ; end_col = p2.end_col
   ; end_offset = p2.end_offset }
 
+(** [file_start fname] is a zero-length position at the start of file [fname],
+    used as a fallback for error reporting when no finer position is known. *)
+let file_start : string -> pos = fun fname ->
+  { fname = Some fname
+  ; start_line = 1; start_col = 0; start_offset = 0
+  ; end_line = 1; end_col = 0; end_offset = 0 }
+
 (** [locate ?fname (p1,p2)] converts the pair of Lexing positions [p1,p2] and
     filename [fname] into a {!type:pos}. *)
 let locate : ?fname:string -> Lexing.position * Lexing.position -> pos =

src/lsp/lp_doc.ml

@@ -54,7 +54,7 @@ let buf_get_and_clear buf =
   let res = Buffer.contents buf in
   Buffer.clear buf; res
 
-let process_pstep (pstate,diags,logs) tac nb_subproofs =
+let process_pstep (pstate, diags, logs) tac nb_subproofs =
   let open Pure in
   let tac_loc = Tactic.get_pos tac in
   let hndl_tac_res = handle_tactic pstate tac nb_subproofs in
@@ -63,7 +63,8 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
   | Tac_OK (pstate, qres) ->
     let goals = Some (current_goals pstate) in
     let qres = match qres with None -> "OK" | Some x -> x in
-    pstate, (tac_loc, 4, qres, goals) :: diags, logs
+    let focus_loc = Tactic.get_focus_pos tac in
+    pstate, (focus_loc, 4, qres, goals) :: diags, logs
   | Tac_Error(loc,msg) ->
     let loc = option_default loc tac_loc in
     let goals = Some (current_goals pstate) in
@@ -96,12 +97,13 @@ let process_cmd _file (nodes,st,dg,logs) ast =
   | Cmd_OK (st, qres) ->
     let qres = match qres with None -> "OK" | Some x -> x in
     let nodes = { ast; exec = true; goals = [] } :: nodes in
-    let ok_diag = cmd_loc, 4, qres, None in
+    let ok_diag = Command.get_focus_pos ast, 4, qres, None in
     nodes, st, ok_diag :: dg, logs
-  | Cmd_Proof (pst, tlist, thm_loc, qed_loc) ->
+  | Cmd_Proof (pst, tlist, _thm_loc, qed_loc) ->
     let start_goals = current_goals pst in
     let pst, dg_proof, logs = process_proof pst tlist logs in
-    let dg_proof = (thm_loc, 4, "OK", Some start_goals) :: dg_proof in
+    let dg_proof =
+      (Command.get_focus_pos ast, 4, "OK", Some start_goals) :: dg_proof in
     let goals = get_goals dg_proof in
     let nodes = { ast; exec = true; goals } :: nodes in
     let st, dg_proof, logs =
@@ -148,17 +150,7 @@ let new_doc ~uri ~version ~text =
       let path = String.sub uri 7 (String.length uri - 7) in
       Some(Pure.initial_state path), []
     with Error.Fatal(_pos, msg) ->
-      let loc : Pos.pos =
-        {
-          fname = Some(uri);
-          start_line = 0;
-          start_col  = 0;
-          start_offset  = 0;
-          end_line = 0;
-          end_col = 0;
-          end_offset  = 0
-        } in
-      (None, [(1, msg), Some(loc)])
+      (None, [(1, msg), Some (Pos.file_start uri)])
   in
   { uri;
     text;

src/lsp/lp_lsp.ml

@@ -10,7 +10,7 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-open Lplib open Extra
+open Lplib
 open Common
 open Core
 
@@ -59,17 +59,7 @@ let do_check_text ofmt ~doc =
     try
       Lp_doc.check_text ~doc
     with Common.Error.Fatal(_pos, msg) ->
-      let loc : Pos.pos =
-        {
-          fname = Some(doc.uri);
-          start_line = 0;
-          start_col  = 0;
-          start_offset  = 0;
-          end_line = 0;
-          end_col = 0;
-          end_offset  = 0;
-        } in
-      (doc, Lp_doc.mk_error ~doc loc msg)
+      (doc, Lp_doc.mk_error ~doc (Pos.file_start doc.uri) msg)
   in
   Hashtbl.replace doc_table doc.uri doc;
   Hashtbl.replace completed_table doc.uri doc;
@@ -111,7 +101,8 @@ let do_change ofmt params =
 let do_close _ofmt params =
   let document = dict_field "textDocument" params in
   let doc_file = string_field "uri" document in
-  Hashtbl.remove doc_table doc_file
+  Hashtbl.remove doc_table doc_file;
+  Hashtbl.remove completed_table doc_file
 
 let grab_doc params =
   let document = dict_field "textDocument" params in
@@ -132,8 +123,12 @@ let mk_syminfo file (name, _path, kind, pos) : J.t =
   ]
 
 let mk_definfo file pos =
+  let uri =
+    if String.is_prefix "file://" file then file
+    else "file://" ^ file
+  in
   `Assoc [
-      "uri", `String file
+      "uri", `String uri
     ; "range", LSP.mk_range pos
         ]
 
@@ -157,6 +152,7 @@ let do_symbols ofmt ~id params =
     let msg = LSP.mk_reply ~id ~result:`Null in
     LIO.send_json ofmt msg
   | Some ss ->
+    Pure.restore_time ss;
     let sym = Pure.get_symbols ss in
     let sym =
       Extra.StrMap.fold
@@ -230,11 +226,7 @@ let get_node_at_pos doc line pos =
   let open Lp_doc in
   List.find_opt (fun { ast; _ } ->
       let loc = Pure.Command.get_pos ast in
-      let res = in_range ?loc (line,pos) in
-      let ls = Format.asprintf "%B l:%d p:%d / %a"
-                 res line pos Pos.pp loc in
-      LIO.log_error "get_node_at_pos" ("call: "^ls);
-      res
+      in_range ?loc (line,pos)
     ) doc.Lp_doc.nodes
 
 (** [get_first_error doc] returns the first error inferred from doc.logs *)
@@ -272,24 +264,6 @@ let rec get_goals ~doc ~line ~pos =
     | Some (v,_) -> Some v
 
 let get_logs ~doc ~line ~pos : string =
-  (* DEBUG LOG START *)
-  LIO.log_error "get_logs"
-    (Printf.sprintf "%s:%d,%d" doc.Lp_doc.uri line pos);
-  let log_to_str ((sev, log), posopt) =
-    let pos_str =
-      match posopt with
-      | None -> "None"
-      | Some Pos.{start_line; start_col; _} ->
-          Printf.sprintf "(%d, %d)" start_line start_col
-    in
-    let log_str =
-      let len = String.length log in
-      Printf.sprintf "length: %d | %s" len (String.sub log 0 (min 30 len))in
-    Format.asprintf "element(severity:%d): %s -> %s\n " sev pos_str log_str
-  in
-  Lsp_io.log_error "get_logs"
-    (List.fold_left (^) "\n" (List.map log_to_str doc.Lp_doc.logs));
-  (* DEBUG LOG END *)
   let line = line+1 in
   let end_limit =
     match get_first_error doc with
@@ -318,20 +292,15 @@ let do_goals ofmt ~id params =
   let msg = LSP.mk_reply ~id ~result in
   LIO.send_json ofmt msg
 
-let msg_fail hdr msg =
-  LIO.log_error hdr msg;
-  failwith msg
 
-let get_symbol : Range.point ->
-('a * 'b) RangeMap.t -> ('b * Range.t) option
+let get_symbol : Range.point -> 'a RangeMap.t -> ('a * Range.t) option
 = fun pos doc ->
 
   let open RangeMap in
 
   match (find pos doc) with
   | None -> None
-  | Some(interval, (_, token)) -> Some (token, interval)
-
+  | Some(interval, value) -> Some (value, interval)
 
 let do_definition ofmt ~id params =
 
@@ -341,122 +310,55 @@ let do_definition ofmt ~id params =
     let msg = LSP.mk_reply ~id ~result:`Null in
     LIO.send_json ofmt msg
   | Some ss ->
+    Pure.restore_time ss;
     let ln, pos = get_textPosition params in
 
-    (* Lines send by the client start at 0 *)
+    (* Lines sent by the client start at 0 *)
     let pt = Range.make_point (ln + 1) pos in
-    let sym_target =
-      match get_symbol pt doc.map with
-      | None -> "No symbol found"
-      | Some(token, _) -> token
-    in
-
-    (*Some printing in the log*)
-    LIO.log_error "token map" (RangeMap.to_string snd doc.map);
-    LIO.log_error "do_definition" sym_target;
-
-    let sym = Pure.get_symbols ss in
-    let map_pp : string =
-      Extra.StrMap.bindings sym
-      |> List.map (fun (key, sym) ->
-          Format.asprintf "{%s} / %s: @[%a@]"
-            key sym.Term.sym_name Pos.pp sym.sym_pos)
-      |> String.concat "\n"
-    in
-    LIO.log_error "symbol map" map_pp;
-
     let sym_info =
-      match StrMap.find_opt sym_target sym with
+      match get_symbol pt doc.map with
       | None -> `Null
-      | Some s ->
-        match s.sym_pos with
+      | Some (qid, _) ->
+        match Pure.find_sym ss (Pos.none qid) with
         | None -> `Null
-        | Some pos ->
-        (* A JSON with the path towards the definition of the term
-          and its position is returned
-          /!\ : extension is fixed, only works for .lp files *)
-          mk_definfo
-            Library.(file_of_path s.Term.sym_path ^ lp_src_extension) pos
+        | Some s when s.Term.sym_path = Sign.Ghost.path -> `Null
+        | Some s ->
+          let file =
+            Library.(file_of_path s.Term.sym_path ^ lp_src_extension) in
+          let pos = Option.get (Pos.file_start file) s.sym_pos in
+          mk_definfo file pos
     in
     let msg = LSP.mk_reply ~id ~result:sym_info in
     LIO.send_json ofmt msg
 
 let hover_symInfo ofmt ~id params =
-
   let _, _, doc = grab_doc params in
   let ln, pos = get_textPosition params in
-
-  (* Positions sent by the client are one line late *)
   let pt = Range.make_point (ln + 1) pos in
-  LIO.log_error "searched point" (Range.point_to_string pt);
-
-  (* The hovered token and its start/finish positions are stored *)
-  let sym_target, interval  =
-  match get_symbol pt doc.map with
-    | None ->
-      "No symbol found", (Range.make_interval pt pt)
-    (* VSCode highlights the token properly if the interval is extended to the
-       character next to it. This might be handled differently in other
-       editors in the future, but it is the most practical solution for
-       now. *)
-    | Some(token, range) ->
-      token, (Range.translate range 0 1)
-  in
 
-  (* Some printing in the log *)
-  (* LIO.log_error "token map" (RangeMap.to_string snd doc.map);
-
-  LIO.log_error "hoverSymInfo" sym_target;
-  LIO.log_error "hoverSymInfo" (Range.interval_to_string interval); *)
+  let send_null () =
+    LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null)
+  in
 
   try
-    (* The information about the tokens is stored *)
-    let sym =
-      match doc.final with
-      | Some ss -> Pure.get_symbols ss
-      | None    -> raise (Error.fatal_no_pos("Root state is missing
-      probably because new_doc has raised exception")) in
-
-    (* The start/finish positions are used to hover the full qualified term,
-      not just the token *)
-    let start = Range.interval_start interval
-    and finish = Range.interval_end interval in
-
-    (* FIXME: types and typed conversion should take care of this *)
-    let sl, sc, fl, fc =
-      (Range.line start - 1),
-      (Range.column start - 1),
-      (Range.line finish - 1),
-      (Range.column finish - 1)
-    in
-
-    let s = `Assoc["line", `Int sl; "character", `Int sc] in
-    let f = `Assoc["line", `Int fl; "character", `Int fc] in
-    let range = `Assoc["start", s; "end", f] in
-
-    let map_pp : string =
-      Extra.StrMap.bindings sym
-      |> List.map (fun (key, sym) ->
-          Format.asprintf "{%s} / %s: @[%a@]"
-            key sym.Term.sym_name Pos.pp sym.sym_pos)
-      |> String.concat "\n"
-    in
-    LIO.log_error "symbol map" map_pp;
-
-    let sym_found =
-      match StrMap.find_opt sym_target sym with
-      | None -> msg_fail "hover_SymInfo" "Sym not found"
-      | Some sym -> sym
-    in
-    let sym_type = Format.asprintf "%a" Core.Print.sym_type sym_found in
-    let result : J.t =
-      `Assoc [ "contents", `String sym_type; "range", range ] in
-    let msg = LSP.mk_reply ~id ~result in
-    LIO.send_json ofmt msg
-
-  with _ ->
-    let msg = LSP.mk_reply ~id ~result:`Null in
-    LIO.send_json ofmt msg
+    let ss = match doc.final with
+      | Some ss -> ss
+      | None -> raise (Error.fatal_no_pos "Root state is missing") in
+    Pure.restore_time ss;
+
+    match get_symbol pt doc.map with
+    | None -> send_null ()
+    | Some (qid, range) ->
+      match Pure.find_sym ss (Pos.none qid) with
+      | None -> send_null ()
+      | Some sym_found ->
+        let sym_type = Format.asprintf "%a" Core.Print.sym_type sym_found in
+        let result = `Assoc [ "contents", `String sym_type
+                            ; "range", LSP.mk_range_of_interval range ] in
+        LIO.send_json ofmt (LSP.mk_reply ~id ~result)
+  with e ->
+    LIO.log_error "hover_symInfo" (Printexc.to_string e);
+    send_null ()
 
 let protect_dispatch p f x =
   try f x
@@ -488,10 +390,12 @@ let dispatch_message ofmt dict =
       (do_symbols ofmt ~id) params
 
   | "textDocument/hover" ->
-    hover_symInfo ofmt ~id params
+    (try hover_symInfo ofmt ~id params
+     with _ -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null))
 
   | "textDocument/definition" ->
-    do_definition ofmt ~id params
+    (try do_definition ofmt ~id params
+     with _ -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null))
 
   | "proof/goals" ->
     do_goals ofmt ~id params
@@ -528,13 +432,12 @@ let process_input ofmt (com : J.t) =
     let bt = Printexc.get_backtrace () in
     LIO.log_error "[BT]" bt;
     LIO.log_error "process_input" (Printexc.to_string exn);
-    (*Send an "empty" answer with Null goals when exception occurs*)
-    let id     = oint_field "id" (U.to_assoc com) in
-    let goals = None in
-    let logs = "" in
-    let result = LSP.json_of_goals goals ~logs in
-    let msg = LSP.mk_reply ~id ~result in
-    LIO.send_json ofmt msg
+    (* Send a null reply so the client doesn't hang *)
+    let id = oint_field "id" (U.to_assoc com) in
+    if id <> 0 then begin
+      let msg = LSP.mk_reply ~id ~result:`Null in
+      LIO.send_json ofmt msg
+    end
 
 let main std log_file =
 

src/lsp/lp_lsp.mli

@@ -13,3 +13,4 @@
 val default_log_file : string
 
 val main : bool -> string -> unit
+(** [main standard_lsp log_file] starts the LSP server. *)