diff --git a/src/common/library.ml b/src/common/library.ml index defb46ce9..01bb6f735 100644 --- a/src/common/library.ml +++ b/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. *) diff --git a/src/common/pos.ml b/src/common/pos.ml index 7996894fe..c3560c7ab 100644 --- a/src/common/pos.ml +++ b/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 = diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 040c86996..809d57ee7 100644 --- a/src/lsp/lp_doc.ml +++ b/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; diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index e6db1697d..db34280ba 100644 --- a/src/lsp/lp_lsp.ml +++ b/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 = diff --git a/src/lsp/lp_lsp.mli b/src/lsp/lp_lsp.mli index 8b8e3041a..e941c9a5f 100644 --- a/src/lsp/lp_lsp.mli +++ b/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. *) diff --git a/src/lsp/lsp_base.ml b/src/lsp/lsp_base.ml index 29c4fb22d..20e06885d 100644 --- a/src/lsp/lsp_base.ml +++ b/src/lsp/lsp_base.ml @@ -10,6 +10,7 @@ (* Status: Very Experimental *) (************************************************************************) +open Lplib open Common open Handle @@ -31,13 +32,27 @@ let mk_reply ~id ~result = let mk_event m p = `Assoc [ "jsonrpc", `String "2.0"; "method", `String m; "params", `Assoc p ] +(* LSP positions are uinteger; clamp defensively to avoid rejection by + strict clients when a synthetic Pos.pos slips through with negative + or zero line/column values. *) +let clamp n = if n < 0 then 0 else n + let mk_range (p : Pos.pos) : J.t = let open Pos in let {start_line=line1; start_col=col1; end_line=line2; end_col=col2; _} = p in - `Assoc ["start", `Assoc ["line", `Int (line1 - 1); "character", `Int col1]; - "end", `Assoc ["line", `Int (line2 - 1); "character", `Int col2]] + `Assoc ["start", `Assoc ["line", `Int (clamp (line1 - 1)); + "character", `Int (clamp col1)]; + "end", `Assoc ["line", `Int (clamp (line2 - 1)); + "character", `Int (clamp col2)]] + +let mk_range_of_interval (r : Range.t) : J.t = + let s = Range.interval_start r and e = Range.interval_end r in + `Assoc ["start", `Assoc ["line", `Int (clamp (Range.line s - 1)); + "character", `Int (clamp (Range.column s))]; + "end", `Assoc ["line", `Int (clamp (Range.line e - 1)); + "character", `Int (clamp (Range.column e))]] let json_of_goal (hyps, concl) = let json_of_hyp (s,t) = `Assoc ["hname", `String s; "htype", `String t] in diff --git a/src/lsp/lsp_base.mli b/src/lsp/lsp_base.mli index c91c081b4..146106a3d 100644 --- a/src/lsp/lsp_base.mli +++ b/src/lsp/lsp_base.mli @@ -10,6 +10,7 @@ (* Status: Very Experimental *) (************************************************************************) +open Lplib open Common open Handle @@ -19,6 +20,8 @@ val std_protocol : bool ref val mk_range : Pos.pos -> J.t +val mk_range_of_interval : Range.t -> J.t + val mk_reply : id:int -> result:J.t -> J.t val mk_diagnostics diff --git a/src/pure/pure.ml b/src/pure/pure.ml index bb18ed3e0..71c56fad9 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -15,6 +15,26 @@ module Util = struct end +(** Make a position spanning [len] characters from the start of [p]. *) +let keyword_pos (p : Pos.pos) (len : int) : Pos.pos = + { p with end_line = p.start_line; end_col = p.start_col + len; + end_offset = p.start_offset + len } + +(** Keyword length for query commands. *) +let query_keyword_len : Syntax.p_query_aux -> int = function + | Syntax.P_query_assert (false, _) -> 6 (* "assert" *) + | Syntax.P_query_assert (true, _) -> 9 (* "assertnot" *) + | Syntax.P_query_normalize _ -> 7 (* "compute" *) + | Syntax.P_query_infer _ -> 4 (* "type" *) + | Syntax.P_query_print _ -> 5 (* "print" *) + | Syntax.P_query_proofterm -> 9 (* "proofterm" *) + | Syntax.P_query_search _ -> 6 (* "search" *) + | Syntax.P_query_flag _ -> 4 (* "flag" *) + | Syntax.P_query_verbose _ -> 7 (* "verbose" *) + | Syntax.P_query_debug _ -> 5 (* "debug" *) + | Syntax.P_query_prover _ -> 6 (* "prover" *) + | Syntax.P_query_prover_timeout _ -> 14 (* "prover_timeout" *) + (** Representation of a single command (abstract). *) module Command = struct type t = Syntax.p_command @@ -23,6 +43,30 @@ module Command = struct let equal_with_pos = (=) let get_pos c = Pos.(c.pos) let print = Util.located Pretty.command + + (** Focused position for OK diagnostics. + For symbol/inductive/opaque: underlines the declared name. + For all other commands: underlines the command keyword. *) + let get_focus_pos (c : t) : Pos.popt = + match c.elt with + | Syntax.P_symbol s -> s.p_sym_nam.pos + | Syntax.P_inductive (_, _, ind :: _) -> + let (name, _, _) = ind.elt in name.pos + | Syntax.P_opaque qid -> qid.pos + | _ -> + let kw_len = match c.elt with + | Syntax.P_rules _ -> 4 (* "rule" *) + | Syntax.P_unif_rule _ -> 9 (* "unif_rule" *) + | Syntax.P_coercion _ -> 11 (* "coerce_rule" *) + | Syntax.P_notation _ -> 8 (* "notation" *) + | Syntax.P_builtin _ -> 7 (* "builtin" *) + | Syntax.P_require _ -> 7 (* "require" *) + | Syntax.P_require_as _ -> 7 (* "require" *) + | Syntax.P_open _ -> 4 (* "open" *) + | Syntax.P_query q -> query_keyword_len q.elt + | _ -> 0 + in + Option.map (fun p -> keyword_pos p kw_len) c.pos end let interval_of_pos : Pos.pos -> Range.t = @@ -48,6 +92,32 @@ module Tactic = struct let equal = Syntax.eq_p_tactic let get_pos t = Pos.(t.pos) let print = Util.located Pretty.tactic + + (** Focused position for OK diagnostics: underlines the tactic keyword. *) + let get_focus_pos (t : t) : Pos.popt = + let kw_len = match t.elt with + | Syntax.P_tac_admit -> 5 (* "admit" *) + | Syntax.P_tac_apply _ -> 5 (* "apply" *) + | Syntax.P_tac_assume _ -> 6 (* "assume" *) + | Syntax.P_tac_change _ -> 6 (* "change" *) + | Syntax.P_tac_eval _ -> 4 (* "eval" *) + | Syntax.P_tac_fail -> 4 (* "fail" *) + | Syntax.P_tac_generalize _ -> 10 (* "generalize" *) + | Syntax.P_tac_have _ -> 4 (* "have" *) + | Syntax.P_tac_induction -> 9 (* "induction" *) + | Syntax.P_tac_refine _ -> 6 (* "refine" *) + | Syntax.P_tac_refl -> 11 (* "reflexivity" *) + | Syntax.P_tac_remove _ -> 6 (* "remove" *) + | Syntax.P_tac_rewrite _ -> 7 (* "rewrite" *) + | Syntax.P_tac_set _ -> 3 (* "set" *) + | Syntax.P_tac_simpl _ -> 8 (* "simplify" *) + | Syntax.P_tac_solve -> 5 (* "solve" *) + | Syntax.P_tac_sym -> 8 (* "symmetry" *) + | Syntax.P_tac_why3 _ -> 4 (* "why3" *) + | Syntax.P_tac_query q -> query_keyword_len q.elt + | _ -> 0 + in + Option.map (fun p -> keyword_pos p kw_len) t.pos end (** Representation of a single proof (abstract). *) @@ -168,7 +238,7 @@ let handle_tactic : proof_state -> Tactic.t -> int -> tactic_result = let qres = Option.map (fun f -> f ()) qres in Tac_OK((Time.save (), ss, ps, finalize, prv, sym_pos), qres) with Fatal(Some p,m) -> - Tac_Error(Some p, Pos.popt_to_string p ^ " " ^ m) + Tac_Error(Some p, m) let end_proof : proof_state -> command_result = fun (_, ss, ps, finalize, _, _) -> @@ -179,6 +249,18 @@ let end_proof : proof_state -> command_result = let get_symbols : state -> Term.sym Extra.StrMap.t = fun (_, ss) -> ss.in_scope +let find_sym : state -> Term.qident Pos.loc -> Term.sym option = + fun (_, ss) qid -> + try Some (Sig_state.find_sym ~prt:true ~prv:true ss qid) + with Fatal _ -> None + +(* [restore_time st] activates the timed state (loaded signatures, library + mappings, ...) captured when [st] was computed. LSP requests must call + this before touching timed globals like [Library.lib_mappings], otherwise + they would observe whichever document was opened most recently. *) +let restore_time : state -> unit = + fun (t, _) -> Time.restore t + (* Equality tests, important for the incremental engine *) (* There are two kind of tests for equality: diff --git a/src/pure/pure.mli b/src/pure/pure.mli index 0ae8a56ee..599074d62 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -10,6 +10,7 @@ module Command : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val get_focus_pos : t -> Pos.popt val print : t Base.pp [@@ocaml.toplevel_printer] end @@ -20,6 +21,7 @@ module Tactic : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val get_focus_pos : t -> Pos.popt val print : t Base.pp [@@ocaml.toplevel_printer] end @@ -86,6 +88,17 @@ val end_proof : proof_state -> command_result [st]. This can be used for displaying the type of symbols. *) val get_symbols : state -> Term.sym Extra.StrMap.t +(** [find_sym st qid] returns the symbol denoted by [qid] in state [st]. + Handles short names in scope, aliased module paths, and fully-qualified + identifiers. Returns [None] if no such symbol is accessible. *) +val find_sym : state -> Term.qident Pos.loc -> Term.sym option + +(** [restore_time st] activates the timed state (loaded signatures, library + mappings, ...) captured when [st] was computed. LSP handlers must call + this before touching timed globals, otherwise they see whichever + document was opened most recently. *) +val restore_time : state -> unit + (** [set_initial_time ()] records the current imperative state as the rollback "time" for the [initial_state] function. This is only useful to initialise or reinitialise the pure interface. *)