From 4d9e95d11da4b3d1c4d93f32779394df9adc0230 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 19:01:00 +0200 Subject: [PATCH 01/14] parser: map a bare open to P_open again A bare open (not preceded by require) was parsed as require open since the LL(1) parser rework (#1441), silently loading not yet required modules instead of failing, and pretty-printing back as require open. --- CHANGES.md | 3 +++ src/parsing/lpParser.ml | 16 ++++++++++------ tests/KO/open_not_required.lp | 3 +++ 3 files changed, 16 insertions(+), 6 deletions(-) create mode 100644 tests/KO/open_not_required.lp diff --git a/CHANGES.md b/CHANGES.md index 783f6da8e..16574018e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -36,6 +36,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). ### Fixed +- A bare `open` (not preceded by `require`) was parsed as `require open` + since the parser rework, silently loading not yet required modules + instead of failing. - Convertibility test of non-linear higher-order pattern variables in rule LHS. - Syntactical errors in Dedukti export. - Weak head normal form test. diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 3bdd29d4c..9f953b0ed 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -433,11 +433,15 @@ let term_id (lb:'token lexbuf): p_term = (* commands *) -let open_ (priv:bool) (lb:'token lexbuf) : p_command_aux = +(* [req] tells whether the command starts with the [require] keyword: + [require [private] open] loads the modules and opens them + ([P_require]), while a bare [[private] open] only opens modules + that are already loaded ([P_open]). *) +let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux = if log_enabled() then log "%s" __FUNCTION__; consume OPEN lb; let ps = nelist path_tks path lb in - P_require(Some priv,ps) + if req then P_require(Some priv,ps) else P_open(priv,ps) let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = if log_enabled() then log "%s" __FUNCTION__; @@ -520,7 +524,7 @@ and command (lb:'token lexbuf) : p_command = end | [{elt=P_expo Term.Privat;_}] -> begin match current_token lb with - | OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb) + | OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ false true lb) | SYMBOL -> extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb) | L_PAREN @@ -546,10 +550,10 @@ and command (lb:'token lexbuf) : p_command = begin match current_token lb with | OPEN -> - extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb) + extend_pos lb (*__FUNCTION__*) pos1 (open_ true false lb) | PRIVATE -> consume_token lb; - extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb) + extend_pos lb (*__FUNCTION__*) pos1 (open_ true true lb) | QID _ -> let ps = nelist path_tks path lb in begin @@ -570,7 +574,7 @@ and command (lb:'token lexbuf) : p_command = | _ -> expected lb "" [OPEN;PRIVATE;QID[]] end | OPEN -> - extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb) + extend_pos lb (*__FUNCTION__*) pos1 (open_ false false lb) | SYMBOL -> extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb) | L_PAREN diff --git a/tests/KO/open_not_required.lp b/tests/KO/open_not_required.lp new file mode 100644 index 000000000..dfc4496a9 --- /dev/null +++ b/tests/KO/open_not_required.lp @@ -0,0 +1,3 @@ +// A bare [open] does not load modules: the module must have been +// required first (with [require] or [require open]). +open tests.OK.boolean; From 070c614ead4b6a81ca3381a01186d37ec7bbd664 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Wed, 8 Jul 2026 15:32:10 +0200 Subject: [PATCH 02/14] LSP: success hints on the ";" of commands and the keyword of tactics The severity-4 "OK" diagnostic of a command or tactic previously spanned the whole command or tactic, so the success underline covered symbol bodies, rule right-hand sides and whole proofs. Instead: - A command's hint is shown on its terminating ";". The command's recorded position stops one character before it (the parser's extend_pos), so lp_doc derives the ";" position from it (at_semicolon). - Symbol declarations always create proof data, so their "OK" went through the proof path and landed on the symbol name. The initial goals stay anchored at the symbol (for the goals panel), but the visible hint now goes on the ";". - A tactic's hint is shown on its leading keyword (Syntax.tactic_keyword, exposed as Pure.Tactic.keyword), since a tactic's end is ill-defined once it has subproofs. These diagnostics also anchor the goals panel, whose lookup (closest_before) only reads the start of each position, which does not move. Also rename the lp_doc node field "ast" to "cmd". --- CHANGES.md | 4 ++++ src/lsp/lp_doc.ml | 53 ++++++++++++++++++++++++++++++++++--------- src/lsp/lp_lsp.ml | 4 ++-- src/parsing/syntax.ml | 49 +++++++++++++++++++++++++++++++++++++++ src/pure/pure.ml | 1 + src/pure/pure.mli | 2 ++ 6 files changed, 100 insertions(+), 13 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 16574018e..6d59bd962 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,6 +52,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/). duplicated directory component. - LSP server: go-to-definition and hover on qualified identifiers, and session state leaking between open documents. +- LSP server: the success ("OK") diagnostic of a command is now shown on its + terminating ";", and that of a tactic on its leading keyword, instead of + underlining the whole command or tactic (symbol body, rule right-hand + side, proof, etc.). ## 3.0.0 (2025-07-16) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index d7f0f87c4..a8a1d46f3 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -22,7 +22,7 @@ module LSP = Lsp_base let lp_logger = Buffer.create 100 type doc_node = - { ast : Pure.Command.t + { cmd : Pure.Command.t ; exec : bool (*; tactics : Proof.Tactic.t list*) ; goals : (Goal.info list * Pos.popt) list @@ -54,6 +54,16 @@ let buf_get_and_clear buf = let res = Buffer.contents buf in Buffer.clear buf; res +(* [at_keyword p kw] is the sub-position of [p] covering only its leading + keyword [kw] (keywords are ASCII, so their column width is their string + length). *) +let at_keyword : Pos.popt -> string -> Pos.popt = fun p kw -> + match p with + | None -> None + | Some p -> + Pos.(Some { p with end_line = p.start_line + ; end_col = p.start_col + String.length kw }) + let process_pstep (pstate,diags,logs) tac nb_subproofs = let open Pure in let tac_loc = Tactic.get_pos tac in @@ -63,7 +73,14 @@ 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 + (* Show the success hint on the tactic's leading keyword only. This + tuple also anchors the goals panel (see [get_goals]), whose lookup + reads the start of the position: the start must not move. *) + let hint_loc = match Tactic.keyword tac with + | Some kw -> at_keyword tac_loc kw + | None -> tac_loc + in + pstate, (hint_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 @@ -83,27 +100,41 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -let process_cmd _file (nodes,st,dg,logs) ast = +(* A command's recorded position ends one character before its terminating + ";" (the parser's [extend_pos] stops at the start of the following token). + [at_semicolon p] returns the position of that ";", where success ("OK") + hints are shown so that they do not underline the whole command. *) +let at_semicolon : Pos.popt -> Pos.popt = function + | None -> None + | Some p -> + Pos.(Some { p with start_line = p.end_line; start_col = p.end_col + 1 + ; end_line = p.end_line; end_col = p.end_col + 2 }) + +let process_cmd _file (nodes,st,dg,logs) cmd = let open Pure in (* let open Timed in *) (* XXX: Capture output *) (* Console.out_fmt := lp_fmt; * Console.err_fmt := lp_fmt; *) - let cmd_loc = Command.get_pos ast in - let hndl_cmd_res = handle_command st ast in + let cmd_loc = Command.get_pos cmd in + let hndl_cmd_res = handle_command st cmd in let logs = ((3, buf_get_and_clear lp_logger), cmd_loc) :: logs in match hndl_cmd_res with | 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 nodes = { cmd; exec = true; goals = [] } :: nodes in + (* Show the success hint on the terminating ";", not the whole command. *) + let ok_diag = at_semicolon cmd_loc, 4, qres, None in nodes, st, ok_diag :: dg, logs | 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 goals = get_goals dg_proof in - let nodes = { ast; exec = true; goals } :: nodes in + (* Initial goals stay anchored at the symbol, for the goals panel. *) + let goals = + get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in + let nodes = { cmd; exec = true; goals } :: nodes in + (* Visible success hint on the terminating ";", not on the symbol name. *) + let dg_proof = (at_semicolon cmd_loc, 4, "OK", None) :: dg_proof in let st, dg_proof, logs = match end_proof pst with | Cmd_OK (st, qres) -> @@ -123,7 +154,7 @@ let process_cmd _file (nodes,st,dg,logs) ast = nodes, st, dg_proof @ dg, logs | Cmd_Error(loc, msg) -> - let nodes = { ast; exec = false; goals = [] } :: nodes in + let nodes = { cmd; exec = false; goals = [] } :: nodes in let cmd_loc, loc, diag, log = match cmd_loc, loc with | Some l, Some Some l' -> if l.fname = l'.fname then diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 22d76b2f6..a9b0847bc 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -222,8 +222,8 @@ let in_range ?loc (line, pos) = 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 + List.find_opt (fun { cmd; _ } -> + let loc = Pure.Command.get_pos cmd in in_range ?loc (line,pos) ) doc.Lp_doc.nodes diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index be3357f14..b21f3c213 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -298,6 +298,55 @@ and p_tactic = p_tactic_aux loc (** [is_destructive t] says whether tactic [t] changes the current goal. *) let is_destructive {elt;_} = match elt with P_tac_have _ -> false | _ -> true +(** [query_keyword q] returns the keyword introducing query [q]. *) +let query_keyword : p_query -> string = fun {elt;_} -> + match elt with + | P_query_verbose _ -> "verbose" + | P_query_debug _ -> "debug" + | P_query_flag _ -> "flag" + | P_query_assert(true,_) -> "assertnot" + | P_query_assert(false,_) -> "assert" + | P_query_infer _ -> "type" + | P_query_normalize _ -> "compute" + | P_query_prover _ -> "prover" + | P_query_prover_timeout _ -> "prover_timeout" + | P_query_print _ -> "print" + | P_query_proofterm -> "proofterm" + | P_query_search _ -> "search" + +(** [tactic_keyword t] returns the keyword introducing tactic [t], or + [None] for tactics that no single keyword introduces (not produced by + the LP parser). *) +let tactic_keyword : p_tactic -> string option = fun {elt;_} -> + match elt with + | P_tac_admit -> Some "admit" + | P_tac_and _ -> None + | P_tac_all_hyps _ -> Some "all_hyps" + | P_tac_apply _ -> Some "apply" + | P_tac_assume _ -> Some "assume" + | P_tac_assumption -> Some "assumption" + | P_tac_change _ -> Some "change" + | P_tac_eval _ -> Some "eval" + | P_tac_fail -> Some "fail" + | P_tac_first_hyp _ -> Some "first_hyp" + | P_tac_focus _ -> Some "focus" + | P_tac_generalize _ -> Some "generalize" + | P_tac_have _ -> Some "have" + | P_tac_induction -> Some "induction" + | P_tac_orelse _ -> Some "orelse" + | P_tac_query q -> Some (query_keyword q) + | P_tac_refine _ -> Some "refine" + | P_tac_refl -> Some "reflexivity" + | P_tac_remove _ -> Some "remove" + | P_tac_repeat _ -> Some "repeat" + | P_tac_rewrite _ -> Some "rewrite" + | P_tac_set _ -> Some "set" + | P_tac_simpl _ -> Some "simplify" + | P_tac_solve -> Some "solve" + | P_tac_sym -> Some "symmetry" + | P_tac_try _ -> Some "try" + | P_tac_why3 _ -> Some "why3" + (** Parser-level representation of a proof. *) type p_subproof = p_proofstep list diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 2efd2f992..ad0dca261 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -47,6 +47,7 @@ module Tactic = struct type t = Syntax.p_tactic let equal = Syntax.eq_p_tactic let get_pos t = Pos.(t.pos) + let keyword = Syntax.tactic_keyword let print = Util.located Pretty.tactic end diff --git a/src/pure/pure.mli b/src/pure/pure.mli index b865e9f71..f8bc60bcf 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -20,6 +20,8 @@ module Tactic : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val keyword : t -> string option + (** Keyword introducing the tactic, if a single keyword does. *) val print : t Base.pp [@@ocaml.toplevel_printer] end From b490ace893c5019229efe4df30ba3d2b2770c7b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 11:46:54 +0200 Subject: [PATCH 03/14] LSP: review fixes for success hint positions Set the character offsets of hint positions consistently with their columns (at_keyword left end_offset at the end of the whole tactic, at_semicolon did not update offsets at all). Handle a ";" at the beginning of a line: the parser's extend_pos does not back up at column 0, so a command position with end_col = 0 cannot distinguish a ";" at column 0 from one at column 1 (the hint used to underline column 1, one character past a line-initial ";"). Cover both columns in that case. --- src/lsp/lp_doc.ml | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index a8a1d46f3..27b492362 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -55,14 +55,15 @@ let buf_get_and_clear buf = Buffer.clear buf; res (* [at_keyword p kw] is the sub-position of [p] covering only its leading - keyword [kw] (keywords are ASCII, so their column width is their string - length). *) + keyword [kw] (keywords are ASCII, so their string length is their width + both in columns and in character offsets). *) let at_keyword : Pos.popt -> string -> Pos.popt = fun p kw -> match p with | None -> None | Some p -> Pos.(Some { p with end_line = p.start_line - ; end_col = p.start_col + String.length kw }) + ; end_col = p.start_col + String.length kw + ; end_offset = p.start_offset + String.length kw }) let process_pstep (pstate,diags,logs) tac nb_subproofs = let open Pure in @@ -100,15 +101,30 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -(* A command's recorded position ends one character before its terminating - ";" (the parser's [extend_pos] stops at the start of the following token). - [at_semicolon p] returns the position of that ";", where success ("OK") - hints are shown so that they do not underline the whole command. *) +(* [at_semicolon p] is the position of the ";" terminating a command whose + position is [p]. Success ("OK") hints are shown there so that they do + not underline the whole command. Position ends are exclusive (as in the + LSP ranges they are mapped to), so the position of the one-character + ";" ends one column after it. The parser's [extend_pos] ends [p] one + character before the ";", except when the ";" is at column 0, where it + does not back up over the newline: a ";" at column 0 and one at column + 1 both yield [end_col = 0] (with [end_offset] the offset of column 0), + so in that case the returned position covers both columns. *) let at_semicolon : Pos.popt -> Pos.popt = function | None -> None | Some p -> - Pos.(Some { p with start_line = p.end_line; start_col = p.end_col + 1 - ; end_line = p.end_line; end_col = p.end_col + 2 }) + Pos.( + if p.end_col = 0 then + Some { p with start_line = p.end_line; start_col = 0 + ; start_offset = p.end_offset + ; end_col = 2 + ; end_offset = p.end_offset + 2 } + else + Some { p with start_line = p.end_line + ; start_col = p.end_col + 1 + ; start_offset = p.end_offset + 1 + ; end_col = p.end_col + 2 + ; end_offset = p.end_offset + 2 }) let process_cmd _file (nodes,st,dg,logs) cmd = let open Pure in From 1e2e768c4c802f273670c2f88dadbfaed526f303 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 13:50:01 +0200 Subject: [PATCH 04/14] LSP: show command success hints on the introducing keyword Show the "OK" hint of a command on its keyword ("symbol", "rule", "require", ...) rather than on the terminating ";". The keyword of a symbol, inductive or open command is not always at the command's start (modifiers or parameters may precede it), so the parser records the keyword position in the AST for these three constructors. For the other commands, Syntax.command_keyword_pos computes it as a prefix of the command's position. Tactics use the same mechanism (tactic_keyword_pos); at_keyword and at_semicolon disappear from lp_doc, replaced by Pos.prefix. --- CHANGES.md | 6 ++-- src/cli/lambdapi.ml | 3 +- src/common/pos.ml | 10 +++++++ src/export/coq.ml | 6 ++-- src/export/lean.ml | 6 ++-- src/export/rawdk.ml | 2 +- src/handle/command.ml | 8 +++--- src/lsp/lp_doc.ml | 51 ++++------------------------------ src/parsing/dkParser.mly | 4 ++- src/parsing/lpParser.ml | 23 ++++++++++------ src/parsing/parser.ml | 2 +- src/parsing/pretty.ml | 10 +++---- src/parsing/syntax.ml | 59 ++++++++++++++++++++++++++++++++-------- src/pure/pure.ml | 3 +- src/pure/pure.mli | 9 ++++-- 15 files changed, 112 insertions(+), 90 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 6d59bd962..2b1b61b39 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,9 +52,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). duplicated directory component. - LSP server: go-to-definition and hover on qualified identifiers, and session state leaking between open documents. -- LSP server: the success ("OK") diagnostic of a command is now shown on its - terminating ";", and that of a tactic on its leading keyword, instead of - underlining the whole command or tactic (symbol body, rule right-hand +- LSP server: the success ("OK") diagnostic of a command or tactic is now + shown on its introducing keyword ("symbol", "rule", "assume", …), instead + of underlining the whole command or tactic (symbol body, rule right-hand side, proof, etc.). ## 3.0.0 (2025-07-16) diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index fac04645c..0ed9822ea 100644 --- a/src/cli/lambdapi.ml +++ b/src/cli/lambdapi.ml @@ -28,7 +28,8 @@ let sig_state_of_require l : Sig_state.sig_state = Handle.Command.handle Compile.compile ss (Pos.none (Parsing.Syntax.P_require - (Some false, [Pos.none (Parsing.Parser.path_of_string req)])))) + (Some false, + [Pos.none (Parsing.Parser.path_of_string req)])))) Core.Sig_state.dummy l let search_cmd cfg rules require s dbpath_opt = diff --git a/src/common/pos.ml b/src/common/pos.ml index 395777779..754df1d53 100644 --- a/src/common/pos.ml +++ b/src/common/pos.ml @@ -111,6 +111,16 @@ let cat : popt -> popt -> popt = fun p1 p2 -> | None, Some p -> Some p | None, None -> None +(** [prefix n p] is the sub-position of [p] covering only its first [n] + characters, which are assumed to lie on the first line of [p] and to be + ASCII (so that [n] is both a column count and a character count). *) +let prefix : int -> popt -> popt = fun n p -> + match p with + | None -> None + | Some p -> Some { p with end_line = p.start_line + ; end_col = p.start_col + n + ; end_offset = p.start_offset + n } + (** [shift k p] returns a position that is [k] characters after [p]. *) let shift : int -> popt -> popt = fun k p -> match p with diff --git a/src/export/coq.ml b/src/export/coq.ml index 6defb5ba5..c9d438918 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -114,9 +114,9 @@ and typopt oc t = Option.iter (prefix " : " term oc) t let command oc {elt; pos} = begin match elt with - | P_open(true,ps) -> + | P_open(_,true,ps) -> string oc "Import "; list path " " oc ps; string oc ".\n" - | P_open(false,ps) -> + | P_open(_,false,ps) -> string oc "Export "; list path " " oc ps; string oc ".\n" | P_require (None, ps) -> string oc "Require "; list path " " oc ps; string oc ".\n" @@ -129,7 +129,7 @@ let command oc {elt; pos} = string oc "Module "; ident oc i; string oc " := "; path oc p; string oc ".\n" | P_symbol - { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_prf=_; p_sym_def } -> if not (is_mapped p_sym_nam.elt) then begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with diff --git a/src/export/lean.ml b/src/export/lean.ml index 6aebe4d46..cb00be6ca 100644 --- a/src/export/lean.ml +++ b/src/export/lean.ml @@ -140,7 +140,7 @@ let openings = ref [] let command oc {elt; pos} = begin match elt with - | P_open(_,ps) -> List.iter (open_mod oc) ps + | P_open(_,_,ps) -> List.iter (open_mod oc) ps | P_require(b,ps) -> List.iter (req_mod oc) ps; begin @@ -149,8 +149,8 @@ let command oc {elt; pos} = | _ -> () (*FIXME?*) end | P_require_as(p,i) -> Stt.alias := StrMap.add i.elt p.elt !Stt.alias - | P_symbol { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; - p_sym_prf=_; p_sym_def } -> + | P_symbol { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ; + p_sym_trm; p_sym_prf=_; p_sym_def } -> if not (is_mapped p_sym_nam.elt) then begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with | true, Some t, _, Some a when List.exists is_lem p_sym_mod -> diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml index b9b917e67..174d7f04e 100644 --- a/src/export/rawdk.ml +++ b/src/export/rawdk.ml @@ -198,7 +198,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) -> | P_query q -> query ppf q | P_require(None,ps) -> List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.mident elt) ps - | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg; p_sym_typ; + | P_symbol{p_sym_mod; p_sym_kw=_; p_sym_nam=n; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_prf=None; p_sym_def=_;} -> let ms = partition_modifiers p_sym_mod in begin match get_ac_typ pos ms p_sym_arg p_sym_typ with diff --git a/src/handle/command.ml b/src/handle/command.ml index d0a10f141..0ce0f2d8f 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -249,7 +249,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = | P_require(bo,ps) -> (List.fold_left (handle_require compile bo) ss ps, None, None) | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None) - | P_open(b,ps) -> (List.fold_left (handle_open b) ss ps, None, None) + | P_open(_,b,ps) -> (List.fold_left (handle_open b) ss ps, None, None) | P_rules(rs) -> (* Scope rules, and check that they preserve typing. Return the list of rules [srs] and also a [map] mapping every symbol defined by a rule @@ -344,7 +344,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = Console.out 2 (Color.gre "coercion %a") sym_rule r; (ss, None, None) - | P_inductive(ms, params, p_ind_list) -> + | P_inductive(_, ms, params, p_ind_list) -> (* Check modifiers. *) let (prop, expo, mstrat, opaq) = handle_modifiers ms in if prop <> Defin then @@ -446,8 +446,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = rec_sym_list; (ss, None, None) - | P_symbol {p_sym_mod;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf; - p_sym_def} -> + | P_symbol {p_sym_mod;p_sym_kw=_;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm; + p_sym_prf;p_sym_def} -> (* We check that the identifier is not already used. *) let {elt=id; _} = p_sym_nam in if Sign.mem ss.signature id then diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 27b492362..11449acaa 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -54,17 +54,6 @@ let buf_get_and_clear buf = let res = Buffer.contents buf in Buffer.clear buf; res -(* [at_keyword p kw] is the sub-position of [p] covering only its leading - keyword [kw] (keywords are ASCII, so their string length is their width - both in columns and in character offsets). *) -let at_keyword : Pos.popt -> string -> Pos.popt = fun p kw -> - match p with - | None -> None - | Some p -> - Pos.(Some { p with end_line = p.start_line - ; end_col = p.start_col + String.length kw - ; end_offset = p.start_offset + String.length kw }) - let process_pstep (pstate,diags,logs) tac nb_subproofs = let open Pure in let tac_loc = Tactic.get_pos tac in @@ -77,11 +66,7 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs = (* Show the success hint on the tactic's leading keyword only. This tuple also anchors the goals panel (see [get_goals]), whose lookup reads the start of the position: the start must not move. *) - let hint_loc = match Tactic.keyword tac with - | Some kw -> at_keyword tac_loc kw - | None -> tac_loc - in - pstate, (hint_loc, 4, qres, goals) :: diags, logs + pstate, (Tactic.keyword_pos tac, 4, qres, goals) :: diags, logs | Tac_Error(loc,msg) -> let loc = option_default loc tac_loc in let goals = Some (current_goals pstate) in @@ -101,31 +86,6 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -(* [at_semicolon p] is the position of the ";" terminating a command whose - position is [p]. Success ("OK") hints are shown there so that they do - not underline the whole command. Position ends are exclusive (as in the - LSP ranges they are mapped to), so the position of the one-character - ";" ends one column after it. The parser's [extend_pos] ends [p] one - character before the ";", except when the ";" is at column 0, where it - does not back up over the newline: a ";" at column 0 and one at column - 1 both yield [end_col = 0] (with [end_offset] the offset of column 0), - so in that case the returned position covers both columns. *) -let at_semicolon : Pos.popt -> Pos.popt = function - | None -> None - | Some p -> - Pos.( - if p.end_col = 0 then - Some { p with start_line = p.end_line; start_col = 0 - ; start_offset = p.end_offset - ; end_col = 2 - ; end_offset = p.end_offset + 2 } - else - Some { p with start_line = p.end_line - ; start_col = p.end_col + 1 - ; start_offset = p.end_offset + 1 - ; end_col = p.end_col + 2 - ; end_offset = p.end_offset + 2 }) - let process_cmd _file (nodes,st,dg,logs) cmd = let open Pure in (* let open Timed in *) @@ -139,8 +99,8 @@ let process_cmd _file (nodes,st,dg,logs) cmd = | Cmd_OK (st, qres) -> let qres = match qres with None -> "OK" | Some x -> x in let nodes = { cmd; exec = true; goals = [] } :: nodes in - (* Show the success hint on the terminating ";", not the whole command. *) - let ok_diag = at_semicolon cmd_loc, 4, qres, None in + (* Show the success hint on the command's introducing keyword only. *) + let ok_diag = Command.keyword_pos cmd, 4, qres, None in nodes, st, ok_diag :: dg, logs | Cmd_Proof (pst, tlist, thm_loc, qed_loc) -> let start_goals = current_goals pst in @@ -149,8 +109,9 @@ let process_cmd _file (nodes,st,dg,logs) cmd = let goals = get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in let nodes = { cmd; exec = true; goals } :: nodes in - (* Visible success hint on the terminating ";", not on the symbol name. *) - let dg_proof = (at_semicolon cmd_loc, 4, "OK", None) :: dg_proof in + (* Visible success hint on the "symbol" keyword, not on the symbol + name. *) + let dg_proof = (Command.keyword_pos cmd, 4, "OK", None) :: dg_proof in let st, dg_proof, logs = match end_proof pst with | Cmd_OK (st, qres) -> diff --git a/src/parsing/dkParser.mly b/src/parsing/dkParser.mly index 8e5e867b6..9d34eb0e0 100644 --- a/src/parsing/dkParser.mly +++ b/src/parsing/dkParser.mly @@ -49,6 +49,7 @@ let symbol lps p_sym_mod i ps p_sym_typ p_sym_trm = make_pos lps (P_symbol { p_sym_mod + ; p_sym_kw = None (* Dedukti has no "symbol" keyword. *) ; p_sym_nam = p_ident i ; p_sym_arg = List.map (fun (i,t) -> params i (Some t)) ps ; p_sym_typ @@ -77,7 +78,8 @@ let query lps q = make_pos lps (P_query q) - let require (lps,id) = make_pos lps (P_require(None,[make_pos lps [id]])) + let require (lps,id) = + make_pos lps (P_require(None,[make_pos lps [id]])) let arrow lps a b = make_pos lps (P_Arro (a, b)) let binary lps a = arrow lps a (arrow lps a a) diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 9f953b0ed..828401bb8 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -436,15 +436,20 @@ let term_id (lb:'token lexbuf): p_term = (* [req] tells whether the command starts with the [require] keyword: [require [private] open] loads the modules and opens them ([P_require]), while a bare [[private] open] only opens modules - that are already loaded ([P_open]). *) + that are already loaded ([P_open]). For a bare open, the position + of the "open" keyword is recorded in the AST (a "private" modifier, + like modifiers of symbol declarations, is not part of the + keyword). *) let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux = if log_enabled() then log "%s" __FUNCTION__; + let kw_pos = Some(locate (current_pos lb)) in consume OPEN lb; let ps = nelist path_tks path lb in - if req then P_require(Some priv,ps) else P_open(priv,ps) + if req then P_require(Some priv,ps) else P_open(kw_pos,priv,ps) let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = if log_enabled() then log "%s" __FUNCTION__; + let p_sym_kw = Some(locate (current_pos lb)) in consume SYMBOL lb; let p_sym_nam = uid lb in let p_sym_arg = list params_tks params lb in @@ -460,7 +465,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_prf = Some (proof lb) in let p_sym_def = false in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm=None; p_sym_def; p_sym_prf} in P_symbol(sym) | ASSIGN -> @@ -468,7 +473,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_trm, p_sym_prf = term_proof lb in let p_sym_def = true in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_def; p_sym_prf} in P_symbol(sym) | SEMICOLON -> @@ -476,7 +481,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_def = false in let p_sym_prf = None in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_def; p_sym_prf} in P_symbol(sym) | _ -> @@ -488,7 +493,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_def = true in let p_sym_typ = None in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_def; p_sym_prf} in P_symbol(sym) | _ -> @@ -501,10 +506,11 @@ and inductive_cmd (p_sym_mod:p_modifier list) (lb:'token lexbuf) let xs = list params_tks params lb in match current_token lb with | INDUCTIVE -> + let kw_pos = Some(locate (current_pos lb)) in consume INDUCTIVE lb; let i = inductive lb in let is = list [WITH] (prefix WITH inductive) lb in - P_inductive(p_sym_mod,xs,i::is) + P_inductive(kw_pos,p_sym_mod,xs,i::is) | _ -> expected lb "" [L_PAREN;L_SQ_BRACKET;INDUCTIVE] and command (lb:'token lexbuf) : p_command = @@ -569,7 +575,8 @@ and command (lb:'token lexbuf) : p_command = extend_pos lb (*__FUNCTION__*) pos1 (P_require_as(p,i)) | _ -> set_expected_tokens lb [AS] ; - extend_pos lb (*__FUNCTION__*) pos1 (P_require(None,ps)) + extend_pos lb (*__FUNCTION__*) pos1 + (P_require(None,ps)) end | _ -> expected lb "" [OPEN;PRIVATE;QID[]] end diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml index dcc83fa18..be2d65fa8 100644 --- a/src/parsing/parser.ml +++ b/src/parsing/parser.ml @@ -75,7 +75,7 @@ module Dk : PARSER with type lexbuf := Lexing.lexbuf = struct parse_lexbuf None entry lb let command = - let r = ref (Pos.none (P_open(false,[]))) in + let r = ref (Pos.none (P_open(None,false,[]))) in fun (lb:lexbuf): p_command -> Debug.(record_time Parsing (fun () -> r := DkParser.line DkLexer.token lb)); !r diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 6a1b790f0..f120de2f5 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -367,16 +367,16 @@ let proof : (p_proof * p_proof_end) pp = fun ppf (p, pe) -> let command : p_command pp = fun ppf { elt; _ } -> begin match elt with | P_builtin (s, qid) -> out ppf "@[builtin \"%s\"@ ≔ %a@]" s qident qid - | P_inductive (_, _, []) -> assert false (* not possible *) - | P_inductive (ms, xs, i :: il) -> + | P_inductive (_, _, _, []) -> assert false (* not possible *) + | P_inductive (_, ms, xs, i :: il) -> let with_ind ppf i = out ppf "@,%a" (inductive "with") i in out ppf "@[@[%a%a@]%a%a@]" modifiers ms (List.pp params " ") xs (inductive "inductive") i (List.pp with_ind "") il | P_notation (qid, n) -> out ppf "notation %a %a" qident qid (Print.notation string) n - | P_open(false,ps) -> out ppf "open %a" (List.pp path " ") ps - | P_open(true,ps) -> out ppf "private open %a" (List.pp path " ") ps + | P_open(_,false,ps) -> out ppf "open %a" (List.pp path " ") ps + | P_open(_,true,ps) -> out ppf "private open %a" (List.pp path " ") ps | P_query q -> query ppf q | P_require (None, ps) -> out ppf "require %a" (List.pp path " ") ps | P_require (Some false, ps) -> @@ -389,7 +389,7 @@ let command : p_command pp = fun ppf { elt; _ } -> let with_rule ppf r = out ppf "@.%a" (rule "with") r in rule "rule" ppf r; List.iter (with_rule ppf) rs | P_symbol - { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_prf; p_sym_def } -> begin out ppf "@[@[<2>%asymbol %a%a%a%a%a@]%a@]" diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index b21f3c213..91fa648e9 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -347,6 +347,14 @@ let tactic_keyword : p_tactic -> string option = fun {elt;_} -> | P_tac_try _ -> Some "try" | P_tac_why3 _ -> Some "why3" +(** [tactic_keyword_pos t] returns the position of the keyword introducing + tactic [t], or the position of the whole of [t] when no single keyword + does. *) +let tactic_keyword_pos : p_tactic -> Pos.popt = fun ({pos;_} as t) -> + match tactic_keyword t with + | Some kw -> Pos.prefix (String.length kw) pos + | None -> pos + (** Parser-level representation of a proof. *) type p_subproof = p_proofstep list @@ -386,6 +394,7 @@ let is_priv {elt; _} = match elt with P_expo Privat -> true | _ -> false (** Parser-level representation of symbol declarations. *) type p_symbol = { p_sym_mod : p_modifier list (** modifiers *) + ; p_sym_kw : Pos.popt (** position of the "symbol" keyword *) ; p_sym_nam : p_ident (** symbol name *) ; p_sym_arg : p_params list (** arguments before ":" *) ; p_sym_typ : p_term option (** symbol type *) @@ -397,10 +406,12 @@ type p_symbol = type p_command_aux = | P_require of (*private?*)bool (*open?*)option * p_path list | P_require_as of p_path * p_ident - | P_open of (*private?*)bool * p_path list + | P_open of (*"open" keyword position*)Pos.popt + * (*private?*)bool * p_path list | P_symbol of p_symbol | P_rules of p_rule list - | P_inductive of p_modifier list * p_params list * p_inductive list + | P_inductive of (*"inductive" keyword position*)Pos.popt + * p_modifier list * p_params list * p_inductive list | P_builtin of string * p_qident | P_notation of p_qident * string Term.notation | P_unif_rule of p_rule @@ -411,6 +422,29 @@ type p_command_aux = (** Parser-level representation of a single (located) command. *) type p_command = p_command_aux loc +(** [command_keyword_pos c] returns the position of the keyword introducing + command [c] ("symbol", "rule", "require", …). Symbol, inductive and + open commands record it in the AST, as modifiers or parameters may + precede their keyword; for the other commands it is a prefix of the + position of [c]. When no position was recorded (e.g. on Dedukti input), + the position of the whole of [c] is returned instead. *) +let command_keyword_pos : p_command -> Pos.popt = fun {elt; pos} -> + let prefix kw = Pos.prefix (String.length kw) pos in + match elt with + | P_open(kw,_,_) + | P_inductive(kw,_,_,_) + | P_symbol{p_sym_kw=kw;_} -> + (match kw with Some _ -> kw | None -> pos) + | P_require _ + | P_require_as _ -> prefix "require" + | P_rules _ -> prefix "rule" + | P_builtin _ -> prefix "builtin" + | P_notation _ -> prefix "notation" + | P_unif_rule _ -> prefix "unif_rule" + | P_coercion _ -> prefix "coerce_rule" + | P_query q -> prefix (query_keyword q) + | P_opaque _ -> prefix "opaque" + (** Top level AST returned by the parser. *) type ast = p_command Stream.t @@ -542,12 +576,12 @@ let eq_p_sym_prf : (p_proof * p_proof_end) eq = fun (p1, pe1) (p2, pe2) -> pe1.elt = pe2.elt && eq_p_proof p1 p2 let eq_p_symbol : p_symbol eq = fun - { p_sym_mod=p_sym_mod1; p_sym_nam=p_sym_nam1; p_sym_arg=p_sym_arg1; - p_sym_typ=p_sym_typ1; p_sym_trm=p_sym_trm1; p_sym_prf=p_sym_prf1; - p_sym_def=p_sym_def1} - { p_sym_mod=p_sym_mod2; p_sym_nam=p_sym_nam2; p_sym_arg=p_sym_arg2; - p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2; p_sym_prf=p_sym_prf2; - p_sym_def=p_sym_def2} -> + { p_sym_mod=p_sym_mod1; p_sym_kw=_; p_sym_nam=p_sym_nam1; + p_sym_arg=p_sym_arg1; p_sym_typ=p_sym_typ1; p_sym_trm=p_sym_trm1; + p_sym_prf=p_sym_prf1; p_sym_def=p_sym_def1} + { p_sym_mod=p_sym_mod2; p_sym_kw=_; p_sym_nam=p_sym_nam2; + p_sym_arg=p_sym_arg2; p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2; + p_sym_prf=p_sym_prf2; p_sym_def=p_sym_def2} -> List.eq eq_p_modifier p_sym_mod1 p_sym_mod2 && eq_p_ident p_sym_nam1 p_sym_nam2 && List.eq eq_p_params p_sym_arg1 p_sym_arg2 @@ -560,13 +594,14 @@ let eq_p_symbol : p_symbol eq = fun are compared up to source code positions. *) let eq_p_command : p_command eq = fun {elt=c1;_} {elt=c2;_} -> match c1, c2 with - | P_require(b1,l1), P_require(b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2 - | P_open(b1,l1), P_open(b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2 + | P_require(b1,l1), P_require(b2,l2) -> + b1 = b2 && List.eq eq_p_path l1 l2 + | P_open(_,b1,l1), P_open(_,b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2 | P_require_as(m1,i1), P_require_as(m2,i2) -> eq_p_path m1 m2 && eq_p_ident i1 i2 | P_symbol s1, P_symbol s2 -> eq_p_symbol s1 s2 | P_rules(r1), P_rules(r2) -> List.eq eq_p_rule r1 r2 - | P_inductive(m1,xs1,l1), P_inductive(m2,xs2,l2) -> + | P_inductive(_,m1,xs1,l1), P_inductive(_,m2,xs2,l2) -> m1 = m2 && List.eq eq_p_params xs1 xs2 && List.eq eq_p_inductive l1 l2 | P_builtin(s1,q1), P_builtin(s2,q2) -> s1 = s2 && eq_p_qident q1 q2 @@ -766,7 +801,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = | P_coercion r | P_unif_rule r -> fold_rule a r | P_rules rs -> List.fold_left fold_rule a rs - | P_inductive (_, xs, ind_list) -> + | P_inductive (_, _, xs, ind_list) -> let vs, a = List.fold_left fold_args (StrSet.empty, a) xs in List.fold_left (fold_inductive_vars vs) a ind_list | P_symbol {p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;_} -> diff --git a/src/pure/pure.ml b/src/pure/pure.ml index ad0dca261..422cd26e3 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -22,6 +22,7 @@ module Command = struct (* TODO: Fixme not to use generic equality *) let equal_with_pos = (=) let get_pos c = Pos.(c.pos) + let keyword_pos = Syntax.command_keyword_pos let print = Util.located Pretty.command end @@ -47,7 +48,7 @@ module Tactic = struct type t = Syntax.p_tactic let equal = Syntax.eq_p_tactic let get_pos t = Pos.(t.pos) - let keyword = Syntax.tactic_keyword + let keyword_pos = Syntax.tactic_keyword_pos let print = Util.located Pretty.tactic end diff --git a/src/pure/pure.mli b/src/pure/pure.mli index f8bc60bcf..0634f3c7f 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -10,6 +10,10 @@ module Command : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val keyword_pos : t -> Pos.popt + (** Position of the keyword introducing the command ("symbol", "rule", + "require", …), which is not always at its start: modifiers or + parameters may precede it. *) val print : t Base.pp [@@ocaml.toplevel_printer] end @@ -20,8 +24,9 @@ module Tactic : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt - val keyword : t -> string option - (** Keyword introducing the tactic, if a single keyword does. *) + val keyword_pos : t -> Pos.popt + (** Position of the keyword introducing the tactic, or of the whole + tactic when no single keyword does. *) val print : t Base.pp [@@ocaml.toplevel_printer] end From d194bc4cfa7f2867b0244251d81cd649975ace0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Wed, 8 Jul 2026 19:05:38 +0200 Subject: [PATCH 05/14] LSP groundwork: expose command AST, module-path ranges, printer state Additions to the pure/parsing API for the LSP server: - Syntax.fold_paths and Pure.path_rangemap map the source ranges of require/open module paths; Lp_doc stores this path range map alongside the identifier range map - Pure.Command.get_elt exposes the parser-level command shape so clients can pattern-match on declaration forms (outlines) - Pure.set_print_state installs a document's signature state in the printer for correctly qualified output --- src/lsp/lp_doc.ml | 5 ++++- src/parsing/syntax.ml | 12 ++++++++++++ src/pure/pure.ml | 18 ++++++++++++++++++ src/pure/pure.mli | 12 ++++++++++++ 4 files changed, 46 insertions(+), 1 deletion(-) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 11449acaa..0c4be484c 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -42,6 +42,7 @@ type t = { (* severity is same as LSP specifications : https://git.io/JiGAB *) logs : ((int * string) * Pos.popt) list; (*((severity, message), location)*) map : Core.Term.qident RangeMap.t; + path_map : Common.Path.t RangeMap.t; } let option_default o1 d = @@ -166,6 +167,7 @@ let new_doc ~uri ~version ~text = nodes = []; logs = logs; map = RangeMap.empty; + path_map = RangeMap.empty; } (* XXX: Save on close. *) @@ -208,5 +210,6 @@ let check_text ~doc = | Some(pos,msg) -> logs @ [((1, msg), Some pos)], diags @ [pos,1,msg,None] in let map = Pure.rangemap cmds in - let doc = { doc with nodes; final=Some(final); map; logs } in + let path_map = Pure.path_rangemap cmds in + let doc = { doc with nodes; final=Some(final); map; path_map; logs } in doc, LSP.mk_diagnostics ~uri ~version diags diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 91fa648e9..79f0ff271 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -815,3 +815,15 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = in List.fold_left fold_command + +(** [fold_paths f a ast] applies [f] to every module path occurring in + [require], [require … as …], or [open] commands. Used by the LSP to + offer go-to-definition on module names. *) +let fold_paths : ('a -> p_path -> 'a) -> 'a -> p_command list -> 'a = + fun f -> + List.fold_left (fun a {elt; _} -> + match elt with + | P_require (_, paths) + | P_open (_, _, paths) -> List.fold_left f a paths + | P_require_as (path, _) -> f a path + | _ -> a) diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 422cd26e3..c8042406e 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -22,6 +22,7 @@ module Command = struct (* TODO: Fixme not to use generic equality *) let equal_with_pos = (=) let get_pos c = Pos.(c.pos) + let get_elt (c : t) : Syntax.p_command_aux = c.Pos.elt let keyword_pos = Syntax.command_keyword_pos let print = Util.located Pretty.command end @@ -43,6 +44,16 @@ let rangemap : Command.t list -> Term.qident RangeMap.t = in Syntax.fold_idents f RangeMap.empty +(** Document module-path range map: positions of paths appearing in + [require]/[open] commands, mapped to the path they denote. *) +let path_rangemap : Command.t list -> Common.Path.t RangeMap.t = + let f map ({elt; pos} : Syntax.p_path) = + match pos with + | Some pos -> RangeMap.add (interval_of_pos pos) elt map + | None -> map + in + Syntax.fold_paths f RangeMap.empty + (** Representation of a single tactic (abstract). *) module Tactic = struct type t = Syntax.p_tactic @@ -196,6 +207,13 @@ let find_sym : state -> Term.qident -> Term.sym option = let restore_time : state -> unit = fun (t, _) -> Time.restore t +(** [set_print_state st] installs [st] as the printer's signature state + so that subsequent [Print.sym_type] / [Print.term] calls produce + correctly qualified output. *) +let set_print_state : state -> unit = fun (time, ss) -> + Time.restore time; + Print.sig_state := ss + (* 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 0634f3c7f..840aa639f 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -10,6 +10,9 @@ module Command : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val get_elt : t -> Parsing.Syntax.p_command_aux + (** Expose the parser-level command shape so clients (LSP, MCP, …) + can pattern-match on declaration forms (e.g. to build outlines). *) val keyword_pos : t -> Pos.popt (** Position of the keyword introducing the command ("symbol", "rule", "require", …), which is not always at its start: modifiers or @@ -19,6 +22,10 @@ end val rangemap : Command.t list -> Term.qident RangeMap.t +(** [path_rangemap cmds] maps source ranges of module paths appearing in + [require]/[open] commands to the paths they denote. *) +val path_rangemap : Command.t list -> Common.Path.t RangeMap.t + (** Abstract representation of a tactic (proof item). *) module Tactic : sig type t @@ -104,6 +111,11 @@ val find_sym : state -> Term.qident -> Term.sym option document was opened most recently. *) val restore_time : state -> unit +(** [set_print_state st] installs [st] as the printer's signature state + so that subsequent [Print.sym_type] / [Print.term] calls produce + correctly qualified output. *) +val set_print_state : 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. *) From e4329bef23489132d871476f58b269cc28b29aac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:16:57 +0200 Subject: [PATCH 06/14] LSP: robust message framing and JSON-RPC replies - read header lines up to the blank separator, accepting Content-Length in any position (clients may send Content-Type too) - keep request ids verbatim (JSON-RPC ids are numbers or strings, including 0) and echo them back as-is; key the crash-recovery null reply on the presence of the id field - reply MethodNotFound (-32601) to unknown request methods so clients do not wait forever; unknown notifications are logged and dropped - didChange: apply all content changes of a message, then re-check once --- src/lsp/lp_lsp.ml | 51 ++++++++++++++++++++++++++------------------ src/lsp/lsp_base.ml | 11 +++++++++- src/lsp/lsp_base.mli | 8 ++++++- src/lsp/lsp_io.ml | 36 +++++++++++++++++-------------- 4 files changed, 67 insertions(+), 39 deletions(-) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index a9b0847bc..eb281ac3a 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -24,8 +24,6 @@ let list_field name dict = U.to_list List.(assoc name dict) let string_field name dict = U.to_string List.(assoc name dict) (* Conditionals *) -let oint_field name dict = - Option.map_default U.to_int 0 List.(assoc_opt name dict) let odict_field name dict = Option.get [] U.(to_option to_assoc (Option.get `Null List.(assoc_opt name dict))) @@ -66,13 +64,6 @@ let do_check_text ofmt ~doc = Hashtbl.replace completed_table doc.uri doc; LIO.send_json ofmt @@ diags -let do_change ofmt ~doc change = - let open Lp_doc in - LIO.log_error "checking file" - (doc.uri ^ " / version: " ^ (string_of_int doc.version)); - let doc = { doc with text = string_field "text" change; } in - do_check_text ofmt ~doc - let do_open ofmt params = let document = dict_field "textDocument" params in let uri, version, text = @@ -95,9 +86,18 @@ let do_change ofmt params = string_field "uri" document, int_field "version" document in let changes = List.map U.to_assoc @@ list_field "contentChanges" params in + LIO.log_error "checking file" + (uri ^ " / version: " ^ (string_of_int version)); let doc = Hashtbl.find doc_table uri in let doc = { doc with Lp_doc.version; } in - List.iter (do_change ofmt ~doc) changes + (* With full-document sync each change carries the whole new text; + the fold applies them all, then a single re-check runs. *) + let doc = + List.fold_left + (fun (doc : Lp_doc.t) change -> + { doc with text = string_field "text" change }) + doc changes in + do_check_text ofmt ~doc let do_close _ofmt params = let document = dict_field "textDocument" params in @@ -379,7 +379,9 @@ let protect_dispatch p f x = theading model there is not a lot of difference yet; something to think for the future. *) let dispatch_message ofmt dict = - let id = oint_field "id" dict in + (* The "id" member is kept verbatim (JSON-RPC ids may be numbers or + strings) and echoed back as-is in replies. *) + let id = Option.get `Null (List.assoc_opt "id" dict) in let params = odict_field "params" dict in match string_field "method" dict with (* Requests *) @@ -423,11 +425,18 @@ let dispatch_message ofmt dict = exit 0 (* NOOPs *) - | "initialized" - | "workspace/didChangeWatchedModule" -> + | "initialized" -> () | msg -> - LIO.log_error "no_handler" msg + (* Requests carry an id; notifications don't. For requests we must + reply with JSON-RPC MethodNotFound so the client doesn't wait + forever. Notifications get logged and dropped, matching the + spec's "no response" rule. *) + LIO.log_error "no_handler" msg; + if List.mem_assoc "id" dict then + LIO.send_json ofmt + (LSP.mk_error_reply ~id ~code:(-32601) + ~msg:("Method not found: " ^ msg)) let process_input ofmt (com : J.t) = try dispatch_message ofmt (U.to_assoc com) @@ -438,12 +447,13 @@ 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 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 + (* Send a null reply so the client doesn't hang. Requests carry an + "id" field; note that id 0 is a valid request id (Zed numbers + its first request 0), so key on the field's presence. *) + let dict = U.to_assoc com in + match List.assoc_opt "id" dict with + | Some id -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null) + | None -> () let main std log_file = @@ -467,7 +477,6 @@ let main std log_file = LIO.log_object "read" com; process_input oc com; F.pp_print_flush lp_fmt (); - (* flush lp_oc ;*) loop () in try loop () diff --git a/src/lsp/lsp_base.ml b/src/lsp/lsp_base.ml index 32cab663e..d3739c441 100644 --- a/src/lsp/lsp_base.ml +++ b/src/lsp/lsp_base.ml @@ -26,8 +26,17 @@ let _parse_uri str = let l = String.length str - 7 in String.(sub str 7 l) +(* [id] is the request's "id" member verbatim: JSON-RPC allows numbers + AND strings, and a reply must echo back exactly what came in. *) let mk_reply ~id ~result = - `Assoc [ "jsonrpc", `String "2.0"; "id", `Int id; "result", result ] + `Assoc [ "jsonrpc", `String "2.0"; "id", (id:J.t); "result", result ] + +(* JSON-RPC error reply. Codes follow the JSON-RPC 2.0 spec (see also + LSP §error-codes): -32601 MethodNotFound is the one we reach for. *) +let mk_error_reply ~id ~code ~msg = + `Assoc [ "jsonrpc", `String "2.0"; + "id", (id:J.t); + "error", `Assoc ["code", `Int code; "message", `String msg] ] let mk_event m p = `Assoc [ "jsonrpc", `String "2.0"; "method", `String m; "params", `Assoc p ] diff --git a/src/lsp/lsp_base.mli b/src/lsp/lsp_base.mli index 146106a3d..e0f8b71c7 100644 --- a/src/lsp/lsp_base.mli +++ b/src/lsp/lsp_base.mli @@ -22,7 +22,13 @@ 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_reply : id:J.t -> result:J.t -> J.t +(** [id] is the request's "id" member verbatim — JSON-RPC ids may be + numbers or strings, and replies must echo them back unchanged. *) + +val mk_error_reply : id:J.t -> code:int -> msg:string -> J.t +(** JSON-RPC error reply. Codes follow the JSON-RPC 2.0 spec; [-32601] + is [MethodNotFound]. *) val mk_diagnostics : uri:string diff --git a/src/lsp/lsp_io.ml b/src/lsp/lsp_io.ml index fdac5d310..fefb03c58 100644 --- a/src/lsp/lsp_io.ml +++ b/src/lsp/lsp_io.ml @@ -24,28 +24,32 @@ let log_object hdr obj = exception ReadError of string let read_request ic = - let cl = input_line ic in - let sin = Scanf.Scanning.from_string cl in try - let raw_obj = - Scanf.bscanf sin "Content-Length: %d\r" (fun size -> - let buf = Bytes.create size in - (* Consume the second \r\n *) - let _ = input_line ic in - really_input ic buf 0 size; - Bytes.to_string buf - ) in - J.from_string raw_obj + (* Read header lines up to the empty "\r\n" separator, taking the + size from whichever one is [Content-Length] (a client may also + send e.g. [Content-Type], in any order). [input_line] strips + the '\n'; a trailing '\r' remains. *) + let rec content_length acc = + match input_line ic with + | "" | "\r" -> acc + | line -> + let acc = + try Scanf.sscanf line "Content-Length: %d" (fun n -> Some n) + with Scanf.Scan_failure _ | Failure _ -> acc + in + content_length acc + in + match content_length None with + | None -> raise (ReadError "missing Content-Length header") + | Some size -> + let buf = Bytes.create size in + really_input ic buf 0 size; + J.from_string (Bytes.to_string buf) with - (* if the end of input is encountered while some more characters are needed - to read the current conversion specification. *) | End_of_file -> raise (ReadError "EOF") - (* if the input does not match the format. *) | Scanf.Scan_failure msg - (* if a conversion to a number is not possible. *) | Failure msg - (* if the format string is invalid. *) | Invalid_argument msg -> raise (ReadError msg) From dc8d492530bc3182a3a503ff01643f9ebdf6b0bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:17:15 +0200 Subject: [PATCH 07/14] LSP: initialize reads workspace folders and client capabilities MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - apply the workspace's lambdapi.pkg before the first document opens, from rootUri (pre-3.6 clients) and workspaceFolders, deduplicated — clients typically send both for the same directory; a package-config failure is logged, never fatal (the client would kill the server and retry in a loop) - record snippetSupport, hierarchicalDocumentSymbolSupport and the completion documentationFormat, for the handlers that gate on them --- src/lsp/lp_lsp.ml | 94 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 93 insertions(+), 1 deletion(-) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index eb281ac3a..ec2410937 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -31,8 +31,100 @@ let odict_field name dict = module LIO = Lsp_io module LSP = Lsp_base +(* Walk a nested path of object keys; return the leaf or [None] if any + segment is missing / has the wrong shape. *) +let json_path (j : J.t) (keys : string list) : J.t option = + List.fold_left + (fun j k -> + match j with + | Some (`Assoc fields) -> List.assoc_opt k fields + | _ -> None) + (Some j) keys + +(** [path_of_file_uri uri] strips the [file://] scheme and percent-decodes + the remainder. Returns [None] when [uri] is not a [file:] URI. *) +let path_of_file_uri (uri : string) : string option = + if String.is_prefix "file://" uri then + Some (Uri.pct_decode (String.sub uri 7 (String.length uri - 7))) + else None + +(* Client capabilities we gate features on, read from the [initialize] + request. *) + +(* [textDocument.completion.completionItem.snippetSupport]: snippet + syntax allowed in completion [insertText]. *) +let snippet_support = ref false + +(* [textDocument.documentSymbol.hierarchicalDocumentSymbolSupport]: + hierarchical [DocumentSymbol[]] responses understood; when false, + fall back to flat [SymbolInformation[]]. *) +let hierarchical_symbols = ref false + +(* [textDocument.completion.completionItem.documentationFormat] + includes "markdown": completion docs may be sent as markdown + [MarkupContent] (plain strings render literally otherwise). *) +let markdown_completion_docs = ref false + (* Request Handling: The client expects a reply *) -let do_initialize ofmt ~id _params = +let do_initialize ofmt ~id params = + (* Read clientCapabilities for features we gate on client support. *) + let client_caps = + Option.get `Null (List.assoc_opt "capabilities" params) in + let cap_bool path = + match json_path client_caps path with + | Some (`Bool b) -> b + | _ -> false + in + snippet_support := + cap_bool + ["textDocument"; "completion"; "completionItem"; "snippetSupport"]; + hierarchical_symbols := + cap_bool + ["textDocument"; "documentSymbol"; + "hierarchicalDocumentSymbolSupport"]; + markdown_completion_docs := + (match json_path client_caps + ["textDocument"; "completion"; "completionItem"; + "documentationFormat"] + with + | Some (`List fmts) -> List.mem (`String "markdown") fmts + | _ -> false); + (* Apply the workspace's [lambdapi.pkg] (if any) so module mappings + are live before the first document is opened. [rootUri] is the + pre-3.6 field; [workspaceFolders] is the current one — clients + typically send BOTH for the same directory, so deduplicate. And a + failure (e.g. "module path already mapped") must never abort + [initialize] — the client would kill the server and retry in a + loop; per-file [Package.apply_config] still runs on every open. *) + let apply_folder uri = + match path_of_file_uri uri with + | Some p -> + (try + LIO.log_error "initialize" ("applying package config at " ^ p); + Parsing.Package.apply_config p + with e -> + LIO.log_error "initialize" + ("package config skipped: " ^ Printexc.to_string e)) + | None -> () + in + let root_folders = + match List.assoc_opt "rootUri" params with + | Some (`String uri) -> [uri] + | _ -> [] + in + let ws_folders = + match List.assoc_opt "workspaceFolders" params with + | Some (`List folders) -> + List.filter_map + (fun f -> + match json_path f ["uri"] with + | Some (`String uri) -> Some uri + | _ -> None) + folders + | _ -> [] + in + List.iter apply_folder + (List.sort_uniq Stdlib.compare (root_folders @ ws_folders)); let msg = LSP.mk_reply ~id ~result:( `Assoc ["capabilities", `Assoc [ From 5ebb4b4cfa6bdf78a3ab7a3b0a18ad416e879627 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:17:31 +0200 Subject: [PATCH 08/14] LSP: hierarchical document symbols - when the client supports it, answer documentSymbol with a DocumentSymbol[] tree built from the parsed AST: symbol declarations, and inductive types with their constructors as children; the flat SymbolInformation[] list remains the fallback - drop the kind classification: no LSP SymbolKind matches lambdapi's notions (axiom, constructor, definable symbol, theorem, ...), so every symbol reports the least surprising kind, Function --- src/lsp/lp_lsp.ml | 103 ++++++++++++++++++++++++++++++++++------------ 1 file changed, 76 insertions(+), 27 deletions(-) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index ec2410937..3827f8212 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -222,18 +222,62 @@ let mk_definfo file pos = ; "range", LSP.mk_range pos ] -let kind_of_type tm = - let open Term in - let open Timed in - let is_undef = - Option.is_None !(tm.sym_def) && List.length !(tm.sym_rules) = 0 in - match !(tm.sym_type) with - | Vari _ -> - 13 (* Variable *) - | Type | Kind | Symb _ | _ when is_undef -> - 14 (* Constant *) - | _ -> - 12 (* Function *) +(* No LSP SymbolKind matches lambdapi's notions (axiom, constructor, + definable symbol, theorem, …), so we do not classify: every symbol + is reported as Function, the least surprising icon. (SymbolKind is + a mandatory field; completions simply omit their optional one.) *) +let symbol_kind = 12 (* Function *) + +let mk_document_symbol ?(children=[]) ~name ~kind ~range ~selection_range () + : J.t = + `Assoc [ + "name", `String name; + "kind", `Int kind; + "range", range; + "selectionRange", selection_range; + "children", `List children; + ] + +(** Build hierarchical [DocumentSymbol[]] from the parsed AST. Only + declarations that introduce user-visible symbols are emitted: + [symbol] (Function) and [inductive] (Enum with constructors as + EnumMember children). Require/open, rules, builtins, queries, + notations, etc. are skipped. *) +let document_symbols_of_nodes (nodes : Lp_doc.doc_node list) : J.t list = + let open Parsing.Syntax in + let range_or_fallback (p : Pos.popt) (fallback : J.t) = + match p with Some p -> LSP.mk_range p | None -> fallback + in + (* [nodes] is stored in reverse (head = most recent); restore + top-to-bottom order for the outline. *) + List.concat_map (fun ({ cmd; _ } : Lp_doc.doc_node) -> + match Pure.Command.get_pos cmd with + | None -> [] + | Some cmd_pos -> + let cmd_range = LSP.mk_range cmd_pos in + match Pure.Command.get_elt cmd with + | P_symbol s -> + let sel = range_or_fallback s.p_sym_nam.pos cmd_range in + [ mk_document_symbol + ~name:s.p_sym_nam.elt ~kind:symbol_kind + ~range:cmd_range ~selection_range:sel () ] + | P_inductive (_, _, _, inds) -> + List.map (fun (ind : p_inductive) -> + let (iname, _, cons) = ind.Pos.elt in + let ind_range = range_or_fallback ind.Pos.pos cmd_range in + let sel = range_or_fallback iname.pos ind_range in + let children = List.map (fun (cname, _ctyp) -> + let crange = range_or_fallback cname.Pos.pos ind_range in + mk_document_symbol + ~name:cname.Pos.elt ~kind:22 (* EnumMember *) + ~range:crange ~selection_range:crange () + ) cons in + mk_document_symbol + ~name:iname.elt ~kind:10 (* Enum *) + ~range:ind_range ~selection_range:sel ~children () + ) inds + | _ -> [] + ) (List.rev nodes) let do_symbols ofmt ~id params = let file, _, doc = grab_doc params in @@ -242,21 +286,26 @@ 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 - (fun _ s l -> - let open Term in - (* LIO.log_error "sym" - ( s.sym_name ^ " | " - ^ Format.asprintf "%a" term !(s.sym_type)); *) - Option.map_default - (fun p -> mk_syminfo file - (s.sym_name, s.sym_path, kind_of_type s, p) :: l) l s.sym_pos) - sym [] in - let msg = LSP.mk_reply ~id ~result:(`List sym) in - LIO.send_json ofmt msg + let result = + if !hierarchical_symbols then + (* Built from the parsed AST alone; no signature state needed. *) + `List (document_symbols_of_nodes doc.Lp_doc.nodes) + else + let () = Pure.restore_time ss in + let sym = Pure.get_symbols ss in + let syms = + Extra.StrMap.fold + (fun _ s l -> + let open Term in + Option.map_default + (fun p -> + mk_syminfo file + (s.sym_name, s.sym_path, symbol_kind, p) :: l) + l s.sym_pos) + sym [] in + `List syms + in + LIO.send_json ofmt (LSP.mk_reply ~id ~result) let get_docTextPosition params = From 62a09314843b930f80e279ca10c02f38a17351c4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:17:47 +0200 Subject: [PATCH 09/14] LSP: go-to-definition on module paths, with in-scope fallback - the module paths of require/open commands jump to the start of that module's file (via the path range map added with the groundwork) - when the identifier map has no resolvable entry at the cursor, look up the raw token under the cursor (code-point aware) in the in-scope symbol table: definition keeps working in mid-edit text and in code past a parse error --- src/lsp/lp_lsp.ml | 88 ++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 75 insertions(+), 13 deletions(-) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 3827f8212..35b566aaa 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -368,6 +368,44 @@ let get_node_at_pos doc line pos = in_range ?loc (line,pos) ) doc.Lp_doc.nodes +(* Identifier-ish token at the (0-based) [line]/[col] of [doc]'s text: + the maximal run of non-delimiter code points around the cursor. + Columns are counted in code points, matching the position handling + in the rest of the server. Being text-based, it also works in + regions the checker never reached (mid-edit text, code past a + parse error). *) +(* Byte offset of each code point of [str], with the total length as + a final sentinel. *) +let codepoint_offsets (str : string) : int array = + let offs = ref [] and i = ref 0 in + let n = String.length str in + while !i < n do + offs := !i :: !offs; + i := !i + Uchar.utf_decode_length (String.get_utf_8_uchar str !i) + done; + Array.of_list (List.rev (n :: !offs)) + +let token_at_pos (doc : Lp_doc.t) line col : string option = + match List.nth_opt (String.split_on_char '\n' doc.Lp_doc.text) line with + | None -> None + | Some str -> + let offs = codepoint_offsets str in + let ncp = Array.length offs - 1 in + (* Delimiters are ASCII; a multi-byte code point (first byte + [>= '\x80']) always belongs to a token. *) + let is_delim k = + match str.[offs.(k)] with + | ' ' | '\t' | '\r' | '(' | ')' | '[' | ']' | '{' | '}' + | ';' | ',' | '"' | '.' | ':' | '@' -> true + | _ -> false + in + if col < 0 || col >= ncp || is_delim col then None + else + let s = ref col and e = ref col in + while !s > 0 && not (is_delim (!s - 1)) do decr s done; + while !e + 1 < ncp && not (is_delim (!e + 1)) do incr e done; + Some (String.sub str offs.(!s) (offs.(!e + 1) - offs.(!s))) + (** [get_first_error doc] returns the first error inferred from doc.logs *) let get_first_error doc = List.fold_left (fun acc b -> @@ -454,23 +492,47 @@ let do_definition ofmt ~id params = (* Lines sent by the client start at 0 *) let pt = Range.make_point (ln + 1) pos in + (* Ghost symbols (internal symbols used e.g. for unification rules + and string literals) have no user-facing definition site one + could jump to. *) + let definfo_of_sym (s : Term.sym) : J.t = + if s.Term.sym_path = Sign.Ghost.path then `Null + else + let file = + Library.(file_of_path s.Term.sym_path ^ lp_src_extension) in + let pos = Option.get (Pos.file_start file) s.Term.sym_pos in + mk_definfo file pos + in + (* Fallback when the identifier RangeMap has no resolvable entry + at the cursor: the module paths of require/open commands (jump + to the start of that module's file), then the raw token under + the cursor against the in-scope symbol table — the latter also + covers regions the checker never reached (mid-edit text, code + past a parse error). *) + let def_fallback () = + match RangeMap.find pt doc.path_map with + | Some (_, path) -> + let file = Library.(file_of_path path ^ lp_src_extension) in + mk_definfo file (Pos.file_start file) + | None -> + match token_at_pos doc ln pos with + | None -> + LIO.log_error "do_definition" "no symbol at point"; `Null + | Some tok -> + match Extra.StrMap.find_opt tok (Pure.get_symbols ss) with + | Some s -> definfo_of_sym s + | None -> + LIO.log_error "do_definition" "no symbol at point"; `Null + in let sym_info = match get_symbol pt doc.map with - | None -> - LIO.log_error "do_definition" "no symbol at point"; `Null | Some (qid, _) -> LIO.log_error "do_definition" (snd qid); - match Pure.find_sym ss qid with - | None -> `Null - (* Ghost symbols (internal symbols used e.g. for unification - rules and string literals) have no user-facing definition - site one could jump to. *) - | 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 + (match Pure.find_sym ss qid with + | Some s -> definfo_of_sym s + | None when fst qid = [] -> def_fallback () + | None -> `Null) + | None -> def_fallback () in let msg = LSP.mk_reply ~id ~result:sym_info in LIO.send_json ofmt msg From eec0202d93228d4c975884972c7a61479594ae38 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:18:05 +0200 Subject: [PATCH 10/14] LSP: keyword documentation and hypothesis types on hover - documentation for tactic keywords (inside proofs) and for command and query keywords and modifiers, sourced from doc/*.rst; the tables carry (name, detail, doc, snippet) so completion can reuse them - types of the hypotheses introduced by assume, from the goal snapshots; names in a tactic's arguments resolve in the state before the tactic runs (snapshots are post-tactic, so a tactic that closes its subgoal or the proof used to lose its own arguments' hypotheses) - types print with the document's own printer state (set_print_state), not whichever document's notations were installed last - fallback to the token under the cursor when the identifier map misses: keyword docs, hypotheses and in-scope symbols hover in mid-edit text and past parse errors; the proof context of a broken edit comes from the nodes of the last parse-error-free check (good_nodes) --- src/lsp/lp_doc.ml | 14 +- src/lsp/lp_lsp.ml | 556 +++++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 557 insertions(+), 13 deletions(-) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 0c4be484c..0d846a843 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -39,6 +39,13 @@ type t = { mutable root : Pure.state option; (* Only mutated after parsing. *) mutable final : Pure.state option; (* Only mutated after parsing. *) nodes : doc_node list; + (* [nodes] of the last parse-error-free check. A mid-edit text (a + partial tactic name, say) fails to parse, dropping the command + being edited from [nodes]; queries that need the cursor's command + (proof context for completion and hover) fall back to these. + Edits happen within a line, so line-based positions stay valid + until the next clean parse resyncs them. *) + good_nodes : doc_node list; (* severity is same as LSP specifications : https://git.io/JiGAB *) logs : ((int * string) * Pos.popt) list; (*((severity, message), location)*) map : Core.Term.qident RangeMap.t; @@ -165,6 +172,7 @@ let new_doc ~uri ~version ~text = root; final = root; nodes = []; + good_nodes = []; logs = logs; map = RangeMap.empty; path_map = RangeMap.empty; @@ -211,5 +219,9 @@ let check_text ~doc = in let map = Pure.rangemap cmds in let path_map = Pure.path_rangemap cmds in - let doc = { doc with nodes; final=Some(final); map; path_map; logs } in + let good_nodes = + match error with None -> nodes | Some _ -> doc.good_nodes in + let doc = + { doc with nodes; good_nodes; final=Some(final); map; path_map; logs } + in doc, LSP.mk_diagnostics ~uri ~version diags diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 35b566aaa..19f0f27ce 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -361,12 +361,30 @@ let in_range ?loc (line, pos) = (compare (start_line, start_col) (line, pos)) * (compare (end_line, end_col) (line, pos)) <= 0 -let get_node_at_pos doc line pos = +let find_node_at_pos nodes line pos = let open Lp_doc in List.find_opt (fun { cmd; _ } -> let loc = Pure.Command.get_pos cmd in in_range ?loc (line,pos) - ) doc.Lp_doc.nodes + ) nodes + +let get_node_at_pos doc line pos = + find_node_at_pos doc.Lp_doc.nodes line pos + +(* --- Cursor context: proof scripts, raw tokens, tactic docs -------- *) + +(* Like [get_node_at_pos], but falling back to the nodes of the last + parse-error-free check. A mid-edit text (a partial tactic name, + say) fails to parse, dropping the command being edited from + [nodes] — exactly when completion and hover need its proof + context. [good_nodes] equals [nodes] whenever the text parses, so + the fallback only ever serves stale data while the text is broken; + edits happen within a line, so its line-based positions stay valid + until the next clean parse. *) +let get_context_node doc line pos = + match get_node_at_pos doc line pos with + | Some n -> Some n + | None -> find_node_at_pos doc.Lp_doc.good_nodes line pos (* Identifier-ish token at the (0-based) [line]/[col] of [doc]'s text: the maximal run of non-delimiter code points around the cursor. @@ -406,6 +424,475 @@ let token_at_pos (doc : Lp_doc.t) line col : string option = while !e + 1 < ncp && not (is_delim (!e + 1)) do incr e done; Some (String.sub str offs.(!s) (offs.(!e + 1) - offs.(!s))) +(* [begin_pos_of doc n] is the position (1-based line, code point + column) of the [begin] keyword of [n]'s command in [doc]'s current + text, if any. [begin] is a reserved word, so the first + word-delimited occurrence within the command's span opens the + proof script. *) +let begin_pos_of (doc : Lp_doc.t) (n : Lp_doc.doc_node) + : (int * int) option = + match Pure.Command.get_pos n.Lp_doc.cmd with + | None -> None + | Some Pos.{start_line; end_line; _} -> + let lines = String.split_on_char '\n' doc.Lp_doc.text in + let delim c = + match c with + | ' ' | '\t' | '\r' | '(' | ')' | '[' | ']' | '{' | '}' + | ';' | ',' | '"' | '.' | ':' | '@' -> true + | _ -> false + in + let find_in_line l = + match List.nth_opt lines (l - 1) with + | None -> None + | Some str -> + let len = String.length str in + let rec search i = + if i + 5 > len then None + else if String.sub str i 5 = "begin" + && (i = 0 || delim str.[i - 1]) + && (i + 5 = len || delim str.[i + 5]) + then + (* Byte index to code point column ("b" is ASCII, so it + sits on a code point boundary). *) + let offs = codepoint_offsets str in + let rec cp j = if offs.(j) = i then j else cp (j + 1) in + Some (l, cp 0) + else search (i + 1) + in + search 0 + in + let rec scan l = + if l > end_line then None + else match find_in_line l with + | Some p -> Some p + | None -> scan (l + 1) + in + scan start_line + +(* True iff the cursor is inside the proof script of the command at + the cursor. Carrying a proof ([p_sym_prf]) is not enough: the + command's span also covers the statement (name, type), which is + not a proof position — require the cursor to be at or after the + [begin] keyword. *) +let in_proof_at (doc : Lp_doc.t) line character : bool = + match get_context_node doc line character with + | Some n -> + (match Pure.Command.get_elt n.Lp_doc.cmd with + | Parsing.Syntax.P_symbol {p_sym_prf = Some _; _} -> + (match begin_pos_of doc n with + | Some bpos -> compare bpos (line + 1, character) <= 0 + | None -> false) + | _ -> false) + | None -> false + +(** Tactic keywords offered as completions inside a proof and + documented on hover. Each entry is [(name, detail, doc, snippet)]: + [detail] is a one-line summary shown next to the completion label, + [doc] the fuller documentation (sourced from [doc/tactics.rst], + [doc/tacticals.rst] and [doc/equality.rst]) shown in the completion + docs panel and on hover, and [snippet] a TextMate-style template + used when the client advertises [snippetSupport] (otherwise the + label is inserted verbatim). Covers every tactic documented in + those files — enforced by the test suite, which extracts the + documented names and checks them against this list. Queries, + which double as tactics ([P_tac_query]), live in + [query_completions]. [P_tac_and] is deliberately absent: it has + no concrete syntax (only built internally by [eval]). *) +let tactic_completions : (string * string * string * string) list = [ + "admit", "discharge goal as axiom", + "Adds new symbols (axioms) to the environment proving the focused goal.", + "admit"; + + "all_hyps", "apply a term to every hypothesis", + "`all_hyps t` (with `t : Π p, Prf p → T`) applies `t _ xₙ`, …, \ + `t _ x₁` on the hypotheses `x₁ … xₙ`, ignoring failing calls; \ + fails if every call failed.", + "all_hyps ${1:term}"; + + "apply", "apply a term to the goal", + "`apply t` refines the current goal with `t _ … _`, generating one \ + subgoal for each argument that cannot be inferred.", + "apply ${1:term}"; + + "assume", "introduce hypotheses", + "If the focused goal is of the form `Π x₁ … xₙ, T`, then \ + `assume h₁ … hₙ` replaces it by `T` with each `xᵢ` replaced by \ + `hᵢ`.", + "assume ${1:h}"; + + "assumption", "close goal by an hypothesis", + "Proves the current goal if it is (an instance of) an hypothesis.", + "assumption"; + + "change", "change the goal type", + "`change t` replaces the current goal `u` by `t`, provided \ + `t ≡ u`.", + "change ${1:type}"; + + "eval", "interpret a term as a tactic", + "`eval t` normalizes the term `t` and interprets the result as a \ + tactic expression built from the tactic builtins.", + "eval ${1:term}"; + + "fail", "always fail", + "Always fails. Useful to stop at a particular point while \ + developing a proof.", + "fail"; + + "first_hyp", "apply a term to hypotheses until one succeeds", + "`first_hyp t` (with `t : Π p, Prf p → T`) applies `t _ xₙ` on the \ + last hypothesis; if the goal is not solved, tries the next \ + hypothesis, and so on, failing if none succeeds.", + "first_hyp ${1:term}"; + + "focus", "move goal n to the front", + "`focus n` moves the n-th goal (`n ≥ 2`) to position 1.", + "focus ${1:n}"; + + "generalize", "generalize a variable", + "If the focused goal is `x₁:A₁, …, y₁:B₁, …, yₚ:Bₚ ⊢ U`, then \ + `generalize y₁` transforms it into \ + `x₁:A₁, … ⊢ Π y₁:B₁, …, Π yₚ:Bₚ, U`.", + "generalize ${1:x}"; + + "have", "introduce an intermediate lemma", + "`have x: t` generates a new goal for `t`, then lets you prove the \ + focused goal with the additional hypothesis `x: t`.", + "have ${1:h}: ${2:type}"; + + "induction", "structural induction", + "If the focused goal is of the form `Π x:I, …` with `I` an \ + inductive type, refines it by applying the induction principle \ + of `I`.", + "induction"; + + "orelse", "try a tactic, else another", + "`orelse t₁ t₂` applies `t₁`; if `t₁` fails, applies `t₂`.", + "orelse ${1:tac1} ${2:tac2}"; + + "refine", "provide a partial proof term", + "`refine t` instantiates the focused goal by `t`, which may \ + contain underscores `_` and metavariable names `?n`; \ + metavariables that cannot be solved become new goals.", + "refine ${1:term}"; + + "reflexivity", "close goal by reflexivity", + "Solves a goal of the form `Π x₁, …, Π xₙ, P (t = u)` when \ + `t ≡ u`.", + "reflexivity"; + + "remove", "remove a hypothesis", + "`remove h₁ … hₙ` erases the hypotheses `h₁ … hₙ` from the \ + context; the goal and the remaining hypotheses must not depend on \ + them.", + "remove ${1:h}"; + + "repeat", "repeat a tactic", + "`repeat t` applies `t` on the first goal until the number of \ + goals decreases.", + "repeat ${1:tac}"; + + "rewrite", "rewrite using an equation", + "`rewrite t` rewrites the goal with an equation \ + `t : Π x₁ … xₙ, P (l = r)` from left to right; prefix with `left` \ + to rewrite right to left; an optional pattern restricts the \ + rewritten occurrences.", + "rewrite ${1:eq}"; + + "set", "define a local abbreviation", + "`set x \xe2\x89\x94 t` extends the current context with \ + `x \xe2\x89\x94 t`.", + "set ${1:x} \xe2\x89\x94 ${2:term}"; + + "simplify", "simplify the goal", + "Normalizes the focused goal with respect to β-reduction and \ + rewriting rules; `simplify rule off` uses β-reduction only; \ + `simplify f` unfolds the definition of `f` or applies its rules.", + "simplify"; + + "solve", "simplify unification goals", + "Simplifies unification goals as much as possible.", + "solve"; + + "symmetry", "swap sides of an equation", + "Replaces a goal of the form `P (t = u)` by `P (u = t)`.", + "symmetry"; + + "try", "try a tactic; never fails", + "`try t` applies `t`; if `t` fails, the goal is left unchanged.", + "try ${1:tac}"; + + "why3", "dispatch to an external prover", + "Calls an external prover through the Why3 platform to solve the \ + current goal; `why3 \"prover\"` selects a specific prover (default \ + Alt-Ergo, or the one set with the `prover` command).", + "why3"; +] + +(** Documentation of a tactic keyword, if [name] is one. *) +let tactic_doc (name : string) : string option = + List.find_map + (fun (tn, _, doc, _) -> if tn = name then Some doc else None) + tactic_completions + +(** Command keywords and symbol modifiers: offered as completions + where the grammar accepts them (anywhere outside proofs when the + prefix does not parse) and documented on hover anywhere in a + document. Same [(name, detail, doc, snippet)] entries as + [tactic_completions]; docs sourced from [doc/commands.rst]. *) +let keyword_completions : (string * string * string * string) list = [ + "symbol", "declare or define a symbol", + "Declares or defines a symbol. Syntax: \ + `modifiers symbol id params [: type] [≔ [term]] [begin proof end] \ + ;`. Without `≔` it is a declaration (axiom); with `≔` a \ + definition or theorem.", + "symbol ${1:id} : ${2:type};"; + + "inductive", "define an inductive type", + "Defines inductive types with their constructors, and generates \ + their induction principles `ind_` and rules (requires the \ + `Prop` and `P` builtins). Mutually defined types are linked with \ + `with`.", + "inductive ${1:id} : ${2:type} \xe2\x89\x94\n| ${3:c} : $1;"; + + "rule", "declare a rewriting rule", + "Declares rewriting rules for definable symbols, e.g. \ + `rule add zero $n ↪ $n;`. `$`-prefixed identifiers are pattern \ + variables. Rules should form a confluent and terminating system; \ + chain several with `with`.", + "rule ${1:lhs} \xe2\x86\xaa ${2:rhs};"; + + "with", "chain rules or inductive types", + "Chains additional rewriting rules (`rule … with …`) or links \ + mutually defined inductive types.", + "with ${1:lhs} \xe2\x86\xaa ${2:rhs}"; + + "require", "import modules", + "Imports the non-private symbols, rules and builtins of other \ + modules, usable qualified (`Stdlib.Bool.true`); `require open` \ + also puts them in scope; `require … as …` gives the module an \ + alias.", + (* [open], [private] and module paths complete after the keyword, + so the snippet presumes none of the alternatives. *) + "require $0;"; + + "open", "bring module symbols into scope", + "Puts into scope the symbols of previously required modules. \ + Non-private `open`s are transitively inherited.", + "open $0;"; + + "builtin", "map a builtin name to a symbol", + "Maps an internal string literal to a user symbol, e.g. \ + `builtin \"P\" ≔ …;` — required by some commands, tactics and \ + notations.", + "builtin \"${1:name}\" \xe2\x89\x94 ${2:id};"; + + "notation", "set a symbol's notation", + "Sets the notation of a symbol: `infix`/`prefix`/`postfix` with an \ + optional priority, or `quantifier`.", + (* The notation kind is completed contextually after the id, so + the snippet does not presume one. *) + "notation ${1:id} $0"; + + "opaque", "never unfold the definition", + "The symbol is never reduced to its definition (typical for \ + theorems). As a command, `opaque x;` makes a previously defined \ + symbol opaque.", + "opaque"; + + "unif_rule", "declare a unification rule", + "Declares a unification rule `t ≡ u ↪ [t₁ ≡ u₁; …]`, tried by the \ + unification engine when a problem cannot be solved by the default \ + algorithm.", + "unif_rule"; + + "coerce_rule", "declare a coercion rule", + "Declares a coercion rule, used to automatically insert coercions \ + between types.", + "coerce_rule"; + + "begin", "start a proof script", + "Starts a proof script solving the pending goals with tactics; \ + close it with `end`, `admitted` or `abort`.", + "begin\n $0\nend;"; + + "constant", "modifier: no rules or definition", + "Property modifier: no rewriting rule or definition can ever be \ + given to the symbol.", + "constant"; + + "injective", "modifier: may be considered injective", + "Property modifier: the symbol may be considered injective, i.e. \ + if `f t₁ … tₙ ≡ f u₁ … uₙ` then `t₁ ≡ u₁`, …, `tₙ ≡ uₙ`. The \ + verification is left to the user.", + "injective"; + + "commutative", "modifier: add commutativity", + "Property modifier: adds the equation `f t u ≡ f u t` to the \ + conversion.", + "commutative"; + + "associative", "modifier: add associativity", + "Property modifier: adds the equation `f (f t u) v ≡ f t (f u v)` \ + to the conversion (in conjunction with `commutative` only); \ + `left`/`right` selects the canonical form.", + "associative"; + + "private", "modifier: not visible outside the module", + "Exposition modifier: the symbol cannot be used outside the module \ + where it is defined.", + "private"; + + "protected", "modifier: only rule LHS outside the module", + "Exposition modifier: outside its module, the symbol can only be \ + used in the left-hand side of rewriting rules.", + "protected"; + + "sequential", "modifier: try rules in declaration order", + "Matching strategy modifier: apply the symbol's rules in \ + declaration order instead of the default order-independent \ + strategy. Warning: this can break important properties.", + "sequential"; +] + +(** Proof-closing keywords, offered as completions inside proofs. *) +let proof_end_completions : (string * string * string * string) list = [ + "end", "close a finished proof", + "Ends a proof script once all goals are solved.", + "end;"; + + "admitted", "accept the remaining goals as axioms", + "Ends a proof accepting the remaining goals as axioms.", + "admitted;"; + + "abort", "abort the proof", + "Aborts the proof: the symbol is not added to the environment.", + "abort;"; +] + +(** Queries, valid both as commands and as tactics ([P_tac_query]): + offered as completions in both contexts and documented on hover. + Docs sourced from [doc/queries.rst]. *) +let query_completions : (string * string * string * string) list = [ + "assert", "check a typing or a conversion", + "`assert x₁ … xₙ ⊢ t : A;` checks that `t` has type `A`; \ + `assert x₁ … xₙ ⊢ t ≡ u;` checks that `t` and `u` are \ + convertible. Fails if the judgment does not hold.", + "assert \xe2\x8a\xa2 ${1:term} : ${2:type}"; + + "assertnot", "check that a typing or conversion fails", + "Like `assert`, but succeeds when the typing or conversion \ + judgment does NOT hold.", + "assertnot \xe2\x8a\xa2 ${1:term} : ${2:type}"; + + "compute", "normalize a term", + "Computes the normal form of a term.", + "compute ${1:term}"; + + "debug", "toggle debug flags", + "Activates (`+`) or deactivates (`-`) debug modes, each named by \ + one character, e.g. `debug +ts;`. Without argument, lists the \ + available flags.", + "debug +${1:flags}"; + + "flag", "set an option flag on/off", + "Sets a flag `on` or `off`, e.g. `flag \"print_implicits\" on;`. \ + Most flags modify printing; only `\"eta_equality\"` changes the \ + rewrite engine. Without argument, lists the available flags.", + "flag \"${1:name}\" ${2:on}"; + + "print", "print a symbol or the goals", + "With a symbol identifier, displays information (type, notation, \ + rules, …) about that symbol; with `unif_rule` or `coerce_rule`, \ + the corresponding rules; without argument, the current goals.", + "print"; + + "proofterm", "print the current proof term", + "Outputs the current proof term.", + "proofterm"; + + "prover", "select the why3 prover", + "Changes the prover used by the `why3` tactic (default \ + *Alt-Ergo*), e.g. `prover \"Eprover\";`.", + "prover \"${1:name}\""; + + "prover_timeout", "set the why3 timeout", + "Changes the timeout (in seconds) of the `why3` tactic; initially \ + 2s.", + "prover_timeout ${1:seconds}"; + + "search", "query the search index", + "Runs a query (see the query language documentation) against the \ + index of the current file and its requirements, e.g. \ + `search spine >= (nat → nat);`.", + "search ${1:query}"; + + "type", "print the type of a term", + "Displays the type of a term in the current context.", + "type ${1:term}"; + + "verbose", "set the verbosity level", + "Takes a non-negative integer: the higher, the more details are \ + printed. Initially 1.", + "verbose ${1:level}"; +] + +(* Argument keywords (notation kinds, sides, switches, [as]) are + deliberately absent here: no hover docs for them, they are only + described in their completion items. *) +let keyword_doc (name : string) : string option = + List.find_map + (fun (kn, _, doc, _) -> if kn = name then Some doc else None) + (keyword_completions @ proof_end_completions @ query_completions) + +(** Hypotheses visible at the cursor inside a proof. Returns the + focused goal's [(name, type_string)] list, or [[]] when no goal + is active at that position. Goal printing prefixes hypothesis + types with ": "; strip it so consumers get the bare type, in line + with symbol hovers. *) +let hyps_at_cursor (doc : Lp_doc.t) line character : (string * string) list = + match get_context_node doc line character with + | None -> [] + | Some n -> + let strip_type t = + let t = String.trim t in + if String.length t > 0 && t.[0] = ':' then + String.trim (String.sub t 1 (String.length t - 1)) + else t + in + let hyps_of goals = + match goals with + | (hyps, _) :: _ -> + List.map (fun (hn, ht) -> (hn, strip_type ht)) hyps + | [] -> [] + in + (* Goal snapshots record the state after each tactic, anchored at + the tactic's keyword, so the snapshot at the cursor belongs to + the tactic the cursor is in. But a tactic's arguments are + elaborated in the state *before* it runs: the post-state may + focus a different goal when the tactic closes the current one + (dropping its local hypotheses), or no goal at all when it ends + the proof. So resolve names in the pre-state — the snapshot + preceding the anchor, not merely the start of the line, which + skips too far back when several tactics share a line — and keep + the post-state for names the tactic itself binds, e.g. the [x] + of [assume x]. *) + (match closest_before (line + 1, character) n.Lp_doc.goals with + | None -> [] + | Some (post_goals, gpos) -> + let post = hyps_of post_goals in + let pre = + match gpos with + | Some Pos.{start_line; start_col; _} -> + (match + closest_before (start_line, start_col - 1) n.Lp_doc.goals + with + | Some (goals, _) -> hyps_of goals + | None -> []) + | None -> [] + in + pre @ List.filter (fun (hn, _) -> not (List.mem_assoc hn pre)) post) + (** [get_first_error doc] returns the first error inferred from doc.logs *) let get_first_error doc = List.fold_left (fun acc b -> @@ -553,18 +1040,63 @@ let hover_symInfo ofmt ~id params = | None -> raise (Error.fatal_no_pos "Final state is missing: the document \ was never successfully loaded") in - Pure.restore_time ss; - + (* Not just [restore_time]: hover prints types, and the printer's + signature state ([Print.sig_state]) is a plain ref that time + restoration does not cover — without this, types would render + with whichever document's notations were installed last. *) + Pure.set_print_state ss; + + let send_type_hover ?range sym = + let sym_type = Format.asprintf "%a" Core.Print.sym_type sym in + let fields = ["contents", `String sym_type] in + let fields = match range with + | Some r -> fields @ ["range", LSP.mk_range_of_interval r] + | None -> fields + in + LIO.send_json ofmt (LSP.mk_reply ~id ~result:(`Assoc fields)) + in + let send_contents s = + LIO.send_json ofmt + (LSP.mk_reply ~id ~result:(`Assoc ["contents", `String s])) + in + (* Token-based fallback, tried when the identifier RangeMap has no + resolvable entry at the cursor: tactic keywords (inside proofs) + and hypotheses of the focused goal, then command keywords and + modifiers, then in-scope symbols. Text-based, so it also covers + regions the checker never reached (mid-edit text, code past a + parse error). *) + let hover_fallback () = + match token_at_pos doc ln pos with + | None -> send_null () + | Some tok -> + let in_proof = in_proof_at doc ln pos in + match (if in_proof then tactic_doc tok else None) with + | Some d -> send_contents d + | None -> + match + (if in_proof then + List.assoc_opt tok (hyps_at_cursor doc ln pos) + else None) + with + | Some htype -> send_contents htype + | None -> + match keyword_doc tok with + | Some d -> send_contents d + | None -> + match Extra.StrMap.find_opt tok (Pure.get_symbols ss) with + | Some sym when sym.Term.sym_path <> Sign.Ghost.path -> + send_type_hover sym + | _ -> send_null () + in match get_symbol pt doc.map with - | None -> send_null () | Some (qid, range) -> - match Pure.find_sym ss 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) + (match Pure.find_sym ss qid with + | Some sym -> send_type_hover ~range sym + (* Unresolvable unqualified identifier: typically a proof-local + name (hypothesis) — try the fallback chain. *) + | None when fst qid = [] -> hover_fallback () + | None -> send_null ()) + | None -> hover_fallback () with e -> LIO.log_error "hover_symInfo" (Printexc.to_string e); send_null () From ced33a1cffcc827e7579d75a4d2598b5292dc336 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:18:30 +0200 Subject: [PATCH 11/14] parser: expose the tokens acceptable at the end of a source prefix MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - expected-token recordings accumulate until the next consumed token instead of overwriting one another, and a finished application records that a term can be continued (a further argument, an arrow): syntax errors now list more of the true alternatives, with the full set of term starters rendered as one word: a term - new entry point Parser.Lp.expected_tokens (exposed as Pure.expected_tokens): parse a source prefix and return the tokens the grammar accepts at its end — the command starters between commands, the follow set of the truncated command within one, [] on a syntax error before the end. This is the follow set LSP completion is built on --- src/parsing/lpParser.ml | 88 +++++++++++++++++--------- src/parsing/oneLookaheadCellLexbuf.ml | 7 +- src/parsing/oneLookaheadCellLexbuf.mli | 6 +- src/parsing/parser.ml | 31 +++++++++ src/pure/pure.ml | 3 + src/pure/pure.mli | 8 +++ 6 files changed, 111 insertions(+), 32 deletions(-) diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 828401bb8..73b1d1a45 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -143,17 +143,45 @@ let match_token tok patt = let match_guard patts lb = List.exists (match_token (current_token lb)) patts +(* Structured version of the token lists rendered by [expected]: the + tokens acceptable at the position of the last syntax error it + raised. [SyntaxError] only carries the message; completion needs + the follow set itself (see [expected_tokens] at the end of this + file). *) +let last_expected : token list Stdlib.ref = ref [] + +(* Order-preserving deduplication: recorded tokens may repeat + alternatives already listed explicitly. *) +let rec uniq : token list -> token list = function + | [] -> [] + | t :: ts -> t :: uniq (List.filter (fun u -> u <> t) ts) + +(* Tokens that may start a term. Used by the term parser, and by + [expected] to render this whole set as "a term". *) +let term_tks = + [BACKQUOTE;(*EXISTS;FORALL;FUN;*)PI;LAMBDA;LET; + UID"";QID[];UID_EXPL"";QID_EXPL[];UNDERSCORE; + TYPE_TERM;UID_META 0;UID_PATT"";L_PAREN;L_SQ_BRACKET; + INT"";QINT([],"");STRINGLIT""] + let expected lb (msg:string) (tokens:token list) : 'a = + let tokens = uniq (tokens @ get_expected_tokens lb) in + last_expected := tokens; if msg <> "" then syntax_error (current_pos lb) ("Expected: "^msg^".") else - match tokens with + (* Positions that continue a term expect all its starters: + collapse them into one word so they don't drown the other + alternatives. *) + let shown, term = + if List.for_all (fun t -> List.mem t tokens) term_tks then + List.filter (fun t -> not (List.mem t term_tks)) tokens, true + else tokens, false in + let soft t = String.add_quotes (string_of_token t) in + match List.map soft shown @ (if term then ["a term"] else []) with | [] -> assert false - | t::ts -> - let ts = ts @ get_expected_tokens lb in - let soft t = String.add_quotes (string_of_token t) in + | p::ps -> syntax_error (current_pos lb) - (List.fold_left (fun s t -> s^", "^soft t) ("Expected: "^soft t) ts - ^".") + (List.fold_left (fun s p -> s^", "^p) ("Expected: "^p) ps ^ ".") (* building positions and terms *) @@ -200,14 +228,14 @@ let prefix (token:token) (elt:'token lexbuf -> 'a) (lb:'token lexbuf): 'a = let opt (tk : 'token) (lb:'token lexbuf) : bool = if log_enabled() then log "%s" __FUNCTION__; if current_token lb = tk then (consume_token lb; true) - else (set_expected_tokens lb [tk]; false) + else (add_expected_tokens lb [tk]; false) let list (guard: 'token list) (elt:'token lexbuf -> 'a) (lb:'token lexbuf) : 'a list = if log_enabled() then log "%s" __FUNCTION__; let acc = ref [] in while match_guard guard lb do acc := elt lb :: !acc done ; - set_expected_tokens lb guard; + add_expected_tokens lb guard; List.rev !acc let list_with_sep (guard: 'token list) (elt:'token lexbuf -> 'a) (sep:'token) @@ -221,7 +249,7 @@ let list_with_sep (guard: 'token list) (elt:'token lexbuf -> 'a) (sep:'token) guard := [sep] ; el := prefix sep elt done ; - set_expected_tokens lb !guard ; + add_expected_tokens lb !guard ; List.rev !acc let list_with_sep_or_termin @@ -234,7 +262,7 @@ let list_with_sep_or_termin if !match_sep then (consume sep lb; match_sep := false) else (acc := elt lb :: !acc; match_sep := true) done ; - set_expected_tokens lb (if !match_sep then [sep] else guard) ; + add_expected_tokens lb (if !match_sep then [sep] else guard) ; List.rev !acc let nelist (guard: 'token list) (elt:'token lexbuf -> 'a) (lb:'token lexbuf) @@ -447,6 +475,15 @@ let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux = let ps = nelist path_tks path lb in if req then P_require(Some priv,ps) else P_open(kw_pos,priv,ps) +(* Tokens that may start a command. *) +let command_tks = + [ SIDE Pratter.Left ; ASSOCIATIVE ; COMMUTATIVE ; CONSTANT ; + INJECTIVE ; SEQUENTIAL ; PRIVATE ; OPAQUE ; PROTECTED ; REQUIRE ; + OPEN ; SYMBOL ; L_PAREN ; L_SQ_BRACKET ; INDUCTIVE ; RULE ; + UNIF_RULE ; COERCE_RULE ; BUILTIN ; NOTATION ; ASSERT false ; + COMPUTE ; DEBUG ; FLAG ; PRINT ; PROOFTERM ; PROVER ; + PROVER_TIMEOUT ; SEARCH ; TYPE_QUERY ; VERBOSE ] + let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = if log_enabled() then log "%s" __FUNCTION__; let p_sym_kw = Some(locate (current_pos lb)) in @@ -574,7 +611,7 @@ and command (lb:'token lexbuf) : p_command = let i = uid lb in extend_pos lb (*__FUNCTION__*) pos1 (P_require_as(p,i)) | _ -> - set_expected_tokens lb [AS] ; + add_expected_tokens lb [AS] ; extend_pos lb (*__FUNCTION__*) pos1 (P_require(None,ps)) end @@ -641,13 +678,7 @@ and command (lb:'token lexbuf) : p_command = let q = query lb in extend_pos lb (*__FUNCTION__*) pos1 (P_query(q)) | _ -> - expected lb "" - [ SIDE Pratter.Left ; ASSOCIATIVE ; COMMUTATIVE ; CONSTANT ; - INJECTIVE ; SEQUENTIAL ; PRIVATE ; OPAQUE ; PROTECTED ; REQUIRE ; - OPEN ; SYMBOL ; L_PAREN ; L_SQ_BRACKET ; INDUCTIVE ; RULE ; - UNIF_RULE ; COERCE_RULE ; BUILTIN ; NOTATION ; ASSERT false ; - COMPUTE ; DEBUG ; FLAG ; PRINT ; PROOFTERM ; PROVER ; - PROVER_TIMEOUT ; SEARCH ; TYPE_QUERY ; VERBOSE ] + expected lb "" command_tks end and inductive (lb:'token lexbuf): p_inductive = @@ -911,7 +942,7 @@ and term_proof (lb:'token lexbuf): else Some t, None | _ -> - expected lb "term or proof" [] + expected lb "term or proof" (BEGIN :: term_tks) (* proofs *) @@ -969,7 +1000,8 @@ and proof (lb:'token lexbuf): p_proof * p_proof_end = let pe = proof_end lb in [], pe | _ -> - expected lb "subproof, tactic or query" [] + expected lb "subproof, tactic or query" + (L_CU_BRACKET :: ABORT :: ADMITTED :: END :: tactic_tks) and subproof_tks = [L_CU_BRACKET] and subproof (lb:'token lexbuf): p_proofstep list = @@ -1142,7 +1174,7 @@ and tactic (lb:'token lexbuf): p_tactic = let t = term lb in extend_pos lb (*__FUNCTION__*) pos1 (P_tac_rewrite(true,Some p,t)) | _ -> - set_expected_tokens lb [SIDE Pratter.Left;DOT] ; + add_expected_tokens lb [SIDE Pratter.Left;DOT] ; let t = term lb in extend_pos lb (*__FUNCTION__*) pos1 (P_tac_rewrite(true,None,t)) end @@ -1166,7 +1198,7 @@ and tactic (lb:'token lexbuf): p_tactic = consume (SWITCH false) lb; extend_pos lb (*__FUNCTION__*) pos1 (P_tac_simpl SimpBetaOnly) | _ -> - set_expected_tokens lb [UID"";QID[];RULE]; + add_expected_tokens lb [UID"";QID[];RULE]; extend_pos lb (*__FUNCTION__*) pos1 (P_tac_simpl SimpAll) end | SOLVE -> @@ -1190,7 +1222,7 @@ and tactic (lb:'token lexbuf): p_tactic = | STRINGLIT s -> let s = String.remove_quotes s in extend_pos lb (*__FUNCTION__*) pos1 (P_tac_why3 (Some s)) | _ -> - set_expected_tokens lb [STRINGLIT""] ; + add_expected_tokens lb [STRINGLIT""] ; make_pos pos1 (P_tac_why3 None) end | _ -> @@ -1241,7 +1273,7 @@ and rwpatt_content (lb:'token lexbuf): p_rwpatt = let x = ident_of_term pos1 t2 in extend_pos lb (*__FUNCTION__*) pos1 (Rw_TermAsIdInTerm(t1,(x,t3))) | _ -> - set_expected_tokens lb [IN;AS]; + add_expected_tokens lb [IN;AS]; extend_pos lb (*__FUNCTION__*) pos1 (Rw_Term(t1)) end | IN -> @@ -1314,11 +1346,6 @@ and params (lb:'token lexbuf): p_params = | _ -> expected lb "" params_tks -and term_tks = - [BACKQUOTE;(*EXISTS;FORALL;FUN;*)PI;LAMBDA;LET; - UID"";QID[];UID_EXPL"";QID_EXPL[];UNDERSCORE; - TYPE_TERM;UID_META 0;UID_PATT"";L_PAREN;L_SQ_BRACKET; - INT"";QINT([],"");STRINGLIT""] and term (lb:'token lexbuf): p_term = if log_enabled() then log "%s" __FUNCTION__; match current_token lb with @@ -1383,6 +1410,9 @@ and app (pos1:position * position) (t: p_term) (lb:'token lexbuf): p_term = let u = term lb in extend_pos lb (*__FUNCTION__*) pos1 (P_Arro(t,u)) | _ -> + (* A term can always be continued: applied to a further + argument or extended by an arrow. *) + add_expected_tokens lb (ARROW :: term_tks); t and bterm (lb:'token lexbuf): p_term = diff --git a/src/parsing/oneLookaheadCellLexbuf.ml b/src/parsing/oneLookaheadCellLexbuf.ml index e20fdfb8e..79ff3eae0 100644 --- a/src/parsing/oneLookaheadCellLexbuf.ml +++ b/src/parsing/oneLookaheadCellLexbuf.ml @@ -34,8 +34,11 @@ let consume_token (lb:'token lexbuf) : unit = let p = Common.Pos.locate (p1,p2) in log "read new token %a %a" Common.Pos.short (Some p) (pp_token lb) t -let set_expected_tokens lb l = - lb.expected_tokens <- l +(* The tokens recorded since the last [consume_token] all describe + alternatives rejected at the same lookahead token, so they + accumulate rather than replace each other. *) +let add_expected_tokens lb l = + lb.expected_tokens <- l @ lb.expected_tokens let get_expected_tokens lb = lb.expected_tokens diff --git a/src/parsing/oneLookaheadCellLexbuf.mli b/src/parsing/oneLookaheadCellLexbuf.mli index a0ea89d85..d0ff13ef9 100644 --- a/src/parsing/oneLookaheadCellLexbuf.mli +++ b/src/parsing/oneLookaheadCellLexbuf.mli @@ -6,5 +6,9 @@ val new_parser : val current_token : 'token lexbuf -> 'token val current_pos : 'token lexbuf -> Lexing.position * Lexing.position val consume_token : 'token lexbuf -> unit -val set_expected_tokens: 'token lexbuf -> 'token list -> unit +val add_expected_tokens: 'token lexbuf -> 'token list -> unit +(** Record tokens that would have been accepted at the current + lookahead token. Recordings accumulate until the next + [consume_token], which clears them. *) + val get_expected_tokens: 'token lexbuf -> 'token list diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml index be2d65fa8..b6fed4da6 100644 --- a/src/parsing/parser.ml +++ b/src/parsing/parser.ml @@ -111,6 +111,14 @@ sig (fun/forall/exists) [~alone] to parse the query only if followed by EOF. *) + val expected_tokens: string -> LpLexer.token list + (** [expected_tokens s] parses [s] as a sequence of commands up to its + end and returns the tokens the parser accepts there: the command + starters when [s] ends between commands, the follow set of the + truncated last command when it ends inside one, and [] when [s] + has a syntax error before its end. [s] is typically a source file + prefix truncated at a cursor, for completion. *) + end = struct @@ -161,6 +169,29 @@ sig Stream.next (parse_lexbuf' ~allow_rocq_syntax None entry lb) + let expected_tokens (s: string) : LpLexer.token list = + let lb = Utf8.from_string s in + (* One fresh one-token cell per command, like [parse_lexbuf']: a + finished command leaves its ";" in the old cell. *) + let mk () = + OneLookaheadCellLexbuf.new_parser ~pp:LpParser.pp_token + ~lexer_:(fun () -> LpLexer.token ~allow_rocq_syntax:false lb) in + LpParser.last_expected := []; + let rec loop () = + let zlb = mk () in + match LpParser.command zlb with + | _ -> loop () + | exception End_of_file -> LpParser.command_tks + | exception LpLexer.SyntaxError _ -> + (* Only a failure on the end of input describes the cursor + position; an earlier one is a plain syntax error. *) + if OneLookaheadCellLexbuf.current_token zlb = LpLexer.EOF + then !LpParser.last_expected else [] + in + (* A lexing error (unterminated comment or string reaching the + truncation point) aborts the first token of a fresh cell. *) + try loop () with LpLexer.SyntaxError _ -> [] + (* exported functions *) let parse_term_string = parse_entry_string ~allow_rocq_syntax:false LpParser.term diff --git a/src/pure/pure.ml b/src/pure/pure.ml index c8042406e..52a8714bd 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -106,6 +106,9 @@ let parse_text : | Fatal(Some(None) , _ , _) -> assert false | Fatal(None , _ , _) -> assert false +let expected_tokens : string -> LpLexer.token list = + Parser.Lp.expected_tokens + let parse_file : fname:string -> Command.t list * (Pos.pos * string) option = fun ~fname -> diff --git a/src/pure/pure.mli b/src/pure/pure.mli index 840aa639f..b6e6acb95 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -57,6 +57,14 @@ type proof_state val parse_text : fname:string -> string -> Command.t list * (Pos.pos * string) option +(** [expected_tokens prefix] parses [prefix] (lp syntax) up to its end and + returns the tokens the parser accepts there: the command starters when + [prefix] ends between commands, the follow set of the truncated last + command when it ends inside one, and [] when [prefix] has a syntax error + before its end. For completion, with [prefix] the document text truncated + at the cursor. *) +val expected_tokens : string -> Parsing.LpLexer.token list + (** [current_goals s] returns the list of open goals for proof state [s]. *) val current_goals : proof_state -> Goal.info list From 34b2afad7817e7d27b19f7cbf9662aade2f35a33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:18:58 +0200 Subject: [PATCH 12/14] LSP: grammar-driven completion MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - in-scope symbols (ghost symbols excluded; no completion kind — the LSP kinds don't match lambdapi's notions), offered only where the grammar accepts an identifier reference, never in binder positions; per-item type details attach lazily on completionItem/resolve - keyword membership comes from the parser's follow sets: exactly the keywords the grammar accepts at the cursor are offered, with docs and snippets from the hover tables; when the prefix does not parse (a broken edit earlier in the file), fall back to the context-blind tables — tactics and proof enders inside proofs, command keywords outside, queries in both - "." as trigger character: module paths after require/open (as a textEdit — "." is not a word character), qualified names after M. (the non-private symbols of that module, resolving require-as aliases; new Pure.get_aliases), flag names inside flag "..." - hypotheses of the focused goal complete inside proofs, ranked first in the argument of apply, rewrite, etc.; already-typed modifiers are filtered from the offers --- src/lsp/lp_lsp.ml | 559 ++++++++++++++++++++++++++++++++++++++++++++++ src/pure/pure.ml | 3 + src/pure/pure.mli | 4 + 3 files changed, 566 insertions(+) diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 19f0f27ce..246c75e3e 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -132,6 +132,12 @@ let do_initialize ofmt ~id params = ; "documentSymbolProvider", `Bool true ; "hoverProvider", `Bool true ; "definitionProvider", `Bool true + (* "." separates module-path and qualified-name segments; the + completion handler resolves both contexts (and stays quiet + on a dot-trigger anywhere else). *) + ; "completionProvider", + `Assoc [ "resolveProvider", `Bool true + ; "triggerCharacters", `List [`String "."] ] ; "codeActionProvider", `Bool false ]]) in LIO.send_json ofmt msg @@ -403,6 +409,21 @@ let codepoint_offsets (str : string) : int array = done; Array.of_list (List.rev (n :: !offs)) +(* Number of code points of [s]. *) +let cp_len (s : string) : int = Array.length (codepoint_offsets s) - 1 + +(** [line_prefix doc line col] is the text of the (0-based) [line] of + [doc] before the cursor column [col] (counted in code points, + like every position in the server). *) +let line_prefix (doc : Lp_doc.t) line col : string option = + match List.nth_opt (String.split_on_char '\n' doc.Lp_doc.text) line with + | None -> None + | Some str -> + let offs = codepoint_offsets str in + let ncp = Array.length offs - 1 in + let col = if col < 0 then 0 else if col > ncp then ncp else col in + Some (String.sub str 0 offs.(col)) + let token_at_pos (doc : Lp_doc.t) line col : string option = match List.nth_opt (String.split_on_char '\n' doc.Lp_doc.text) line with | None -> None @@ -485,6 +506,233 @@ let in_proof_at (doc : Lp_doc.t) line character : bool = | _ -> false) | None -> false +(* --- Completion context ------------------------------------------- *) + +(* Complete whitespace-separated words of [s], and the token still + being typed (empty when [s] ends in whitespace). *) +let words_and_partial (s : string) : string list * string = + let s = String.map (fun c -> if c = '\t' then ' ' else c) s in + match List.rev (String.split_on_char ' ' s) with + | [] -> [], "" + | partial :: rest -> + List.rev (List.filter (fun w -> w <> "") rest), partial + +(** Cursor context for completion, determined lexically from the + line before the cursor. Only the contexts the parser's follow + sets cannot provide remain here: those about the partial token + being typed (module paths, qualified names, flag names) and the + ranking of hypotheses in tactic arguments; keyword membership + itself comes from the grammar (see [follow_at]). *) +type completion_context = + | Ctx_require of string * int + (** Module path of a [require]/[open]: the typed partial path + and its start column. *) + | Ctx_qualified of string * string + (** Dotted token before the cursor: the module part (before the + last dot) and the partial name after it. *) + | Ctx_flag_name (** Inside the string argument of [flag]. *) + | Ctx_tactic_arg + (** Argument of a tactic that names existing hypotheses. *) + | Ctx_default + +(* Tactics whose argument commonly mentions hypotheses. *) +let arg_tactics = ["apply"; "refine"; "rewrite"; "remove"; "generalize"] + +(* Symbol modifiers and their sides. Repeating one is grammatical, + so follow sets keep offering them; it is never useful, so the + already-typed ones are filtered from completions. *) +let modifier_words = + ["left"; "right"; "associative"; "commutative"; "constant"; + "injective"; "opaque"; "private"; "protected"; "sequential"] + +(* [qualified_of partial] splits the dotted token ending [partial] at + its last dot: [Some ("Stdlib.Nat", "ze")] for ["(Stdlib.Nat.ze"]. + [None] when there is no dot or nothing before it. *) +let qualified_of (partial : string) : (string * string) option = + let is_delim c = String.contains "()[]{};,\":@" c in + let start = ref 0 in + String.iteri (fun i c -> if is_delim c then start := i + 1) partial; + let tok = + String.sub partial !start (String.length partial - !start) in + match String.rindex_opt tok '.' with + | Some i when i > 0 -> + Some (String.sub tok 0 i, + String.sub tok (i + 1) (String.length tok - i - 1)) + | _ -> None + +let completion_context (doc : Lp_doc.t) line col : completion_context = + match line_prefix doc line col with + | None -> Ctx_default + | Some prefix -> + let words, partial = words_and_partial prefix in + (* [require] accepts several paths; [as] switches to an alias + name and [;] ends the command. *) + let path_words ws = + List.for_all + (fun w -> w = "open" + || (w <> "as" && not (String.contains w ';'))) + ws + in + let quotes = + String.fold_left + (fun n c -> if c = '"' then n + 1 else n) 0 prefix + in + match words with + | ("require" | "open") :: rest + | "private" :: ("require" | "open") :: rest + when path_words rest -> + Ctx_require (partial, col - cp_len partial) + | "flag" :: _ when quotes = 1 -> Ctx_flag_name + | _ -> + match qualified_of partial with + | Some (mpath, name) -> Ctx_qualified (mpath, name) + | None -> + match words with + | t :: _ when List.mem t arg_tactics -> Ctx_tactic_arg + | _ -> Ctx_default + +(* [doc] text before the cursor at (0-based) [line],[col] counted in + code points, minus the partial word ending at the cursor: what the + parser should see to tell what may come next (the client filters + the items against the typed word itself). Word boundaries are the + delimiters of [token_at_pos]; a multi-byte code point always + belongs to a word. *) +let doc_prefix (doc : Lp_doc.t) line col : string = + let cur = + match line_prefix doc line col with + | None -> "" + | Some prefix -> + let is_delim = function + | ' ' | '\t' | '\r' | '(' | ')' | '[' | ']' | '{' | '}' + | ';' | ',' | '"' | '.' | ':' | '@' -> true + | _ -> false + in + let i = ref (String.length prefix) in + while !i > 0 && not (is_delim prefix.[!i - 1]) do decr i done; + String.sub prefix 0 !i + in + let lines = String.split_on_char '\n' doc.Lp_doc.text in + let rec before i = function + | l :: ls when i < line -> l :: before (i + 1) ls + | _ -> [] + in + String.concat "\n" (before 0 lines @ [cur]) + +(** Tokens the grammar accepts at the cursor, from the parser: the + command starters between commands, the follow set of the + truncated command within one, and [] when the text before the + cursor has a syntax error (a broken edit earlier in the file) — + callers then fall back to context-blind items. *) +let follow_at (doc : Lp_doc.t) line col : Parsing.LpLexer.token list = + Pure.expected_tokens (doc_prefix doc line col) + +(* Module paths under the current library mappings (the workspace + package and every map-dir), found by scanning the mapped + directories for source files. *) +let module_path_candidates () : string list = + let out = ref [] in + let rec scan prefix dir depth = + if depth > 0 then + match Sys.readdir dir with + | exception Sys_error _ -> () + | entries -> + Array.iter (fun e -> + if e <> "" && e.[0] <> '.' then + let p = Filename.concat dir e in + if (try Sys.is_directory p with Sys_error _ -> false) then + scan (prefix @ [e]) p (depth - 1) + else + List.iter (fun ext -> + match Filename.chop_suffix_opt ~suffix:ext e with + | Some base -> + out := String.concat "." (prefix @ [base]) :: !out + | None -> ()) + [".lp"; ".dk"; ".lpo"]) + entries + in + Library.iter (fun mp dir -> scan mp dir 8); + List.sort_uniq Stdlib.compare !out + +(* Raw LSP range on one line (character units as sent by clients). *) +let mk_char_range line scol ecol : J.t = + `Assoc [ + "start", `Assoc ["line", `Int line; "character", `Int scol]; + "end", `Assoc ["line", `Int line; "character", `Int ecol]; + ] + +(* Completion items replacing the typed [partial] (running from + [start_col] to the cursor) by a full module path. The explicit + [textEdit] matters: "." is not a word character in editors, so a + plain label would be inserted after the last dot. *) +let mk_module_path_items ~line ~start_col ~cursor_col partial + : J.t list = + module_path_candidates () + |> List.filter (String.is_prefix partial) + |> List.map (fun mp -> + `Assoc [ + "label", `String mp; + "kind", `Int 9; (* Module *) + "filterText", `String mp; + "textEdit", `Assoc + [ "range", mk_char_range line start_col cursor_col + ; "newText", `String mp ]; + ]) + +(* Completion items for the qualified name [mstr].[partial]: the + non-private symbols of that module (resolving a [require as] + alias), plus the next segments of loaded module paths extending + it. Only loaded (i.e. required) modules can be referenced, so no + filesystem scan here. The client inserts after the dot, so plain + labels are enough. *) +let mk_qualified_items ss uri (mstr : string) : J.t list = + let seg = String.split_on_char '.' mstr in + let path = + match seg with + | [a] -> + (match Extra.StrMap.find_opt a (Pure.get_aliases ss) with + | Some p -> p + | None -> seg) + | _ -> seg + in + let loaded = Timed.(!) Sign.loaded in + let sym_items = + match Path.Map.find_opt path loaded with + | None -> [] + | Some sign -> + Extra.StrMap.fold (fun name (s : Term.sym) acc -> + if s.Term.sym_expo = Term.Privat then acc + else + `Assoc [ + "label", `String name; + "data", `Assoc + [ "kind", `String "qualified" + ; "uri", `String uri + ; "path", `String (String.concat "." path) ]; + ] :: acc) + (Timed.(!) sign.Sign.sign_symbols) [] + in + let rec list_is_prefix xs ys = + match xs, ys with + | [], _ -> true + | x :: xs, y :: ys -> x = y && list_is_prefix xs ys + | _, [] -> false + in + let n = List.length path in + let segments = + Path.Map.fold (fun p _ acc -> + if list_is_prefix path p then + match List.nth_opt p n with + | Some seg -> seg :: acc + | None -> acc + else acc) + loaded [] + in + let seg_items = + List.map (fun seg -> `Assoc ["label", `String seg; "kind", `Int 9]) + (List.sort_uniq Stdlib.compare segments) + in + sym_items @ seg_items + (** Tactic keywords offered as completions inside a proof and documented on hover. Each entry is [(name, detail, doc, snippet)]: [detail] is a one-line summary shown next to the completion label, @@ -635,6 +883,8 @@ let tactic_doc (name : string) : string option = (fun (tn, _, doc, _) -> if tn = name then Some doc else None) tactic_completions +let is_tactic_name n = tactic_doc n <> None + (** Command keywords and symbol modifiers: offered as completions where the grammar accepts them (anywhere outside proofs when the prefix does not parse) and documented on hover anywhere in a @@ -1101,6 +1351,304 @@ let hover_symInfo ofmt ~id params = LIO.log_error "hover_symInfo" (Printexc.to_string e); send_null () +(* --- Completion ------------------------------------------------------- *) + +(** Completion items for a keyword table ([tactic_completions], + [keyword_completions], [proof_end_completions]): docs as markdown + and snippet insertions when the client supports them. + [sort_prefix] orders keyword groups relative to each other and to + the hypotheses group ("1"). *) +let mk_keyword_items (sort_prefix : string) + (entries : (string * string * string * string) list) : J.t list = + List.map (fun (name, detail, doc, snippet) -> + let doc_field = + if !markdown_completion_docs then + `Assoc [ "kind", `String "markdown" + ; "value", `String doc ] + else `String doc + in + let base = [ + "label", `String name; + "kind", `Int 14; (* Keyword *) + "detail", `String detail; + "documentation", doc_field; + "sortText", `String (sort_prefix ^ name); + ] in + `Assoc ( + if !snippet_support then + base @ + [ "insertText", `String snippet + ; "insertTextFormat", `Int 2 ] (* Snippet *) + else base) + ) entries + +(* Argument keywords of the [notation] command. *) +let notation_arg_completions : (string * string * string * string) list = [ + "infix", "infix notation", + "`notation f infix [left|right] p;` sets an infix notation for \ + `f` with priority `p`, optionally left/right associative.", + "infix ${1:priority}"; + + "prefix", "prefix notation", + "`notation f prefix p;` sets a prefix notation for `f` with \ + priority `p`.", + "prefix ${1:priority}"; + + "postfix", "postfix notation", + "`notation f postfix p;` sets a postfix notation for `f` with \ + priority `p`.", + "postfix ${1:priority}"; + + "quantifier", "binder notation", + "`notation f quantifier;` allows writing `` `f x, t`` for \ + `f (λ x, t)`.", + "quantifier"; +] + +(* Associativity sides, after [associative] or [infix]. *) +let assoc_side_completions : (string * string * string * string) list = [ + "left", "left associative", "Selects left associativity.", "left"; + "right", "right associative", "Selects right associativity.", "right"; +] + +(* The switch argument of [flag "..."]. *) +let switch_completions : (string * string * string * string) list = [ + "on", "enable the flag", "Turns the flag on.", "on"; + "off", "disable the flag", "Turns the flag off.", "off"; +] + +(* Keywords only valid as arguments of other commands, never offered + without grammar support. *) +let arg_keyword_completions : (string * string * string * string) list = [ + "as", "alias for the required module", + "`require M as N;` gives the module `M` the alias `N`, usable in \ + qualified names (`N.symb`).", + "as ${1:alias}"; +] + +(* Names of the registered boolean flags, offered inside the string + argument of [flag]. *) +let flag_name_items () : J.t list = + Extra.StrMap.fold + (fun name _ acc -> `Assoc ["label", `String name] :: acc) + Stdlib.(!Console.boolean_flags) [] + +(* Names under which a follow-set token may appear in the keyword + tables. Tokens without a keyword rendering (identifiers, literals, + punctuation) map to a phrase no table entry uses, and to nothing + in the end. *) +let token_names (tk : Parsing.LpLexer.token) : string list = + match tk with + | Parsing.LpLexer.ASSERT _ -> ["assert"; "assertnot"] + | Parsing.LpLexer.SIDE _ -> ["left"; "right"] + | Parsing.LpLexer.SWITCH _ -> ["on"; "off"] + | _ -> [Parsing.LpParser.string_of_token tk] + +(* The keyword tables, with the rank their items keep relative to + each other when offered from a follow set: queries and proof + enders sort after the keywords specific to the context. *) +let follow_tables : (string * (string * string * string * string) list) list = + [ "0", tactic_completions; + "0", keyword_completions; + "0", notation_arg_completions; + "0", assoc_side_completions; + "0", switch_completions; + "0", arg_keyword_completions; + "2", query_completions; + "2", proof_end_completions ] + +(** Completion items for the keywords of a parser follow set: the + grammar decides membership, the tables provide the docs and + snippets. [exclude] drops named keywords (already-typed + modifiers). *) +let follow_keyword_items ?(exclude : string list = []) + (follow : Parsing.LpLexer.token list) : J.t list = + let names = + List.filter (fun n -> not (List.mem n exclude)) + (List.concat_map token_names follow) in + List.concat_map (fun (rank, table) -> + mk_keyword_items rank + (List.filter (fun (n, _, _, _) -> List.mem n names) table)) + follow_tables + +(* Whether the grammar accepts a qualified identifier at a position + with this follow set: a symbol reference (term or identifier + position) or a module path (after [require]/[open]). Binder + positions (a fresh name after [as], [assume], [symbol], …) only + accept unqualified identifiers, so they don't trigger symbol + completion. *) +let follow_accepts_qid (follow : Parsing.LpLexer.token list) : bool = + List.exists + (function + | Parsing.LpLexer.QID _ | Parsing.LpLexer.QID_EXPL _ -> true + | _ -> false) + follow + +let do_completion ofmt ~id params = + let uri, line, character = get_docTextPosition params in + let empty = `Assoc ["isIncomplete", `Bool false; "items", `List []] in + match Hashtbl.find_opt completed_table uri with + | None -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:empty) + | Some doc -> + match doc.Lp_doc.final with + | None -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:empty) + | Some ss -> + Pure.restore_time ss; + let reply items = + LIO.send_json ofmt (LSP.mk_reply ~id ~result:(`Assoc [ + "isIncomplete", `Bool false; "items", `List items])) in + (* A "."-triggered popup only makes sense in the contexts that + understand dots; stay quiet in the others. *) + let dot_triggered = + match json_path (`Assoc params) ["context"; "triggerKind"] with + | Some (`Int 2) -> true + | _ -> false + in + let ctx = completion_context doc line character in + match ctx with + | Ctx_require (partial, start_col) -> + (* Module paths, plus the keywords the grammar still accepts + at the cursor ([open], [private], [as], …). No paths where + the grammar refuses one (after [require private]); an + empty follow set (a partial path ending in ".") cannot + tell, so it offers them. *) + let follow = follow_at doc line character in + let path_items = + if follow = [] || follow_accepts_qid follow then + mk_module_path_items ~line ~start_col + ~cursor_col:character partial + else [] in + reply (path_items @ follow_keyword_items follow) + | Ctx_qualified (mpath, _) -> + reply (mk_qualified_items ss uri mpath) + | Ctx_flag_name -> reply (flag_name_items ()) + | (Ctx_default | Ctx_tactic_arg) when dot_triggered -> reply [] + | Ctx_default | Ctx_tactic_arg -> + let follow = follow_at doc line character in + let in_proof = in_proof_at doc line character in + (* Symbols, where the grammar accepts a symbol reference (a + term or identifier position). An unparseable prefix (a + broken edit earlier in the file) yields no follow set; + offer them regardless then. No [kind]: the LSP completion + kinds don't match lambdapi's notions, so we don't force a + classification. `detail` is filled in on + [completionItem/resolve]; [data] carries what resolve + needs to find the symbol again. *) + let symbol_items = + if follow <> [] && not (follow_accepts_qid follow) then [] + else + Extra.StrMap.fold (fun name s acc -> + (* Ghost symbols (internal, e.g. for unification rules) + are not part of the user-facing scope. Inside a proof, + tactic keywords shadow symbols of the same name in the + completion list: the user almost certainly means the + tactic. *) + if s.Term.sym_path = Sign.Ghost.path + || (in_proof && is_tactic_name name) then acc + else + `Assoc [ + "label", `String name; + "data", `Assoc [ "kind", `String "symbol" + ; "uri", `String uri ]; + ] :: acc + ) (Pure.get_symbols ss) [] in + (* Keywords the grammar accepts at the cursor. Without a + follow set, fall back to context-blind tables: tactic + keywords and proof enders inside proofs, command keywords + outside, queries in both. *) + let typed_modifiers = + match line_prefix doc line character with + | Some p -> + List.filter (fun w -> List.mem w modifier_words) + (fst (words_and_partial p)) + | None -> [] in + let keyword_items = + match follow with + | _ :: _ -> follow_keyword_items ~exclude:typed_modifiers follow + | [] -> + match ctx with + (* The argument of a tactic is a term position: keywords + are not valid there. *) + | Ctx_tactic_arg -> [] + | _ when in_proof -> + mk_keyword_items "0" tactic_completions + @ mk_keyword_items "2" (query_completions + @ proof_end_completions) + | _ -> + mk_keyword_items "0" keyword_completions + @ mk_keyword_items "2" query_completions in + (* Hypotheses of the focused goal, ranked before the symbols + in the argument position of a hypothesis-taking tactic. *) + let hyp_rank = + match ctx with Ctx_tactic_arg -> "0" | _ -> "1" in + let hyp_items = + if not in_proof then [] else + List.map (fun (hname, htype) -> + `Assoc [ + "label", `String hname; + "kind", `Int 6; (* Variable *) + "detail", `String htype; + "sortText", `String (hyp_rank ^ hname); + ] + ) (hyps_at_cursor doc line character) in + let result = `Assoc [ + "isIncomplete", `Bool false; + "items", `List (symbol_items @ keyword_items @ hyp_items); + ] in + LIO.send_json ofmt (LSP.mk_reply ~id ~result) + +(** Attach [detail] (and eventually other fields) to the completion + item the client highlighted. The initial completion response is + kept light by omitting per-symbol type strings; they're + pretty-printed here, lazily, once per highlighted item. *) +let do_completion_resolve ofmt ~id params = + let echo () = + LIO.send_json ofmt (LSP.mk_reply ~id ~result:(`Assoc params)) + in + (* Re-find the completed symbol via [find] (with the document's + print state installed) and send the item back with its + pretty-printed type as [detail]. *) + let resolve_with uri (find : Pure.state -> Term.sym option) = + match Hashtbl.find_opt completed_table uri with + | None -> echo () + | Some doc -> + match doc.Lp_doc.final with + | None -> echo () + | Some ss -> + Pure.set_print_state ss; + match find ss with + | None -> echo () + | Some sym -> + let type_str = + Format.asprintf "%a" Core.Print.sym_type sym in + let fields = + ("detail", `String type_str) :: + List.remove_assoc "detail" params in + LIO.send_json ofmt (LSP.mk_reply ~id ~result:(`Assoc fields)) + in + match List.assoc_opt "data" params with + | Some (`Assoc data) -> + let uri = try string_field "uri" data with _ -> "" in + let label = try string_field "label" params with _ -> "" in + (match List.assoc_opt "kind" data with + | Some (`String "symbol") -> + (* Items are generated from the in-scope symbol map, keyed by + the label; resolve the highlighted item from the same map. *) + resolve_with uri (fun ss -> + Extra.StrMap.find_opt label (Pure.get_symbols ss)) + | Some (`String "qualified") -> + let path = + try String.split_on_char '.' (string_field "path" data) + with _ -> [] in + resolve_with uri (fun _ss -> + match Path.Map.find_opt path (Timed.(!) Sign.loaded) with + | None -> None + | Some sign -> + Extra.StrMap.find_opt label + (Timed.(!) sign.Sign.sign_symbols)) + | _ -> echo ()) + | _ -> echo () + let protect_dispatch p f x = try f x with @@ -1140,6 +1688,17 @@ let dispatch_message ofmt dict = (try do_definition ofmt ~id params with _ -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null)) + | "textDocument/completion" -> + (try do_completion ofmt ~id params + with _ -> + let empty = `Assoc ["isIncomplete", `Bool false; "items", `List []] in + LIO.send_json ofmt (LSP.mk_reply ~id ~result:empty)) + + | "completionItem/resolve" -> + (try do_completion_resolve ofmt ~id params + with _ -> + LIO.send_json ofmt (LSP.mk_reply ~id ~result:(`Assoc params))) + | "proof/goals" -> do_goals ofmt ~id params diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 52a8714bd..d2bfafea0 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -198,6 +198,9 @@ let end_proof : proof_state -> command_result = let get_symbols : state -> Term.sym Extra.StrMap.t = fun (_, ss) -> ss.in_scope +let get_aliases : state -> Common.Path.t Extra.StrMap.t = + fun (_, ss) -> ss.alias_path + let find_sym : state -> Term.qident -> Term.sym option = fun (_, ss) qid -> try Some (Sig_state.find_sym ~prt:true ~prv:true ss (Pos.none qid)) diff --git a/src/pure/pure.mli b/src/pure/pure.mli index b6e6acb95..557c910a3 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -108,6 +108,10 @@ 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 +(** [get_aliases st] returns the [require ... as] aliases of state [st], + mapping each alias to the module path it stands for. *) +val get_aliases : state -> Path.t 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. *) From 4e13d2cabbd18a0823c205993b660f11817f7f41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:19:08 +0200 Subject: [PATCH 13/14] LSP: integration test suite (make test_lsp) - Python tests speaking JSON-RPC over stdio to a lambdapi lsp subprocess: lifecycle, diagnostics, document symbols, hover, definition, completion (including the grammar follow-set contexts), goals, incremental changes, and cross-cutting invariants (range validity, repeated-request stability, boundary positions, both protocol modes) - the tactic and query completion lists are checked against the names documented in doc/*.rst, so the tables cannot silently fall behind - Python >= 3.8, standard library only; stdlib-dependent tests skip when no lambdapi stdlib is installed; runs as part of make test --- .gitignore | 2 + Makefile | 5 + tests/lsp/FEATURES.md | 115 +++++++ tests/lsp/README.md | 42 +++ tests/lsp/__init__.py | 0 tests/lsp/__main__.py | 20 ++ tests/lsp/base.py | 162 ++++++++++ tests/lsp/client.py | 295 +++++++++++++++++ tests/lsp/fixtures/imports.lp | 5 + tests/lsp/fixtures/inductive.lp | 8 + tests/lsp/fixtures/modifiers.lp | 8 + tests/lsp/fixtures/multiple_errors.lp | 4 + tests/lsp/fixtures/proof.lp | 13 + tests/lsp/fixtures/qualified.lp | 3 + tests/lsp/fixtures/simple.lp | 6 + tests/lsp/fixtures/unicode_cols.lp | 3 + tests/lsp/fixtures/with_error.lp | 3 + tests/lsp/source.py | 48 +++ tests/lsp/test_completion.py | 352 ++++++++++++++++++++ tests/lsp/test_completion_context.py | 446 ++++++++++++++++++++++++++ tests/lsp/test_definition.py | 204 ++++++++++++ tests/lsp/test_diagnostics.py | 93 ++++++ tests/lsp/test_goals.py | 62 ++++ tests/lsp/test_hover.py | 305 ++++++++++++++++++ tests/lsp/test_incremental.py | 87 +++++ tests/lsp/test_invariants.py | 381 ++++++++++++++++++++++ tests/lsp/test_lifecycle.py | 214 ++++++++++++ tests/lsp/test_symbols.py | 104 ++++++ 28 files changed, 2990 insertions(+) create mode 100644 tests/lsp/FEATURES.md create mode 100644 tests/lsp/README.md create mode 100644 tests/lsp/__init__.py create mode 100644 tests/lsp/__main__.py create mode 100644 tests/lsp/base.py create mode 100644 tests/lsp/client.py create mode 100644 tests/lsp/fixtures/imports.lp create mode 100644 tests/lsp/fixtures/inductive.lp create mode 100644 tests/lsp/fixtures/modifiers.lp create mode 100644 tests/lsp/fixtures/multiple_errors.lp create mode 100644 tests/lsp/fixtures/proof.lp create mode 100644 tests/lsp/fixtures/qualified.lp create mode 100644 tests/lsp/fixtures/simple.lp create mode 100644 tests/lsp/fixtures/unicode_cols.lp create mode 100644 tests/lsp/fixtures/with_error.lp create mode 100644 tests/lsp/source.py create mode 100644 tests/lsp/test_completion.py create mode 100644 tests/lsp/test_completion_context.py create mode 100644 tests/lsp/test_definition.py create mode 100644 tests/lsp/test_diagnostics.py create mode 100644 tests/lsp/test_goals.py create mode 100644 tests/lsp/test_hover.py create mode 100644 tests/lsp/test_incremental.py create mode 100644 tests/lsp/test_invariants.py create mode 100644 tests/lsp/test_lifecycle.py create mode 100644 tests/lsp/test_symbols.py diff --git a/.gitignore b/.gitignore index 770cae275..09fed7de5 100644 --- a/.gitignore +++ b/.gitignore @@ -21,3 +21,5 @@ libraries/zenon_modulo .DS_Store *.map *.log +__pycache__/ +*.pyc diff --git a/Makefile b/Makefile index 3c017b996..940e5ed4b 100644 --- a/Makefile +++ b/Makefile @@ -36,6 +36,11 @@ test_all: test test: lambdapi @dune runtest @tests/dtrees.sh + @$(MAKE) test_lsp + +.PHONY: test_lsp +test_lsp: lambdapi + @python3 -m tests.lsp .PHONY: test_load test_load: lambdapi diff --git a/tests/lsp/FEATURES.md b/tests/lsp/FEATURES.md new file mode 100644 index 000000000..17a9222d9 --- /dev/null +++ b/tests/lsp/FEATURES.md @@ -0,0 +1,115 @@ +# LSP feature inventory + +Snapshot of what the lambdapi LSP implements, what it stubs, and what it +omits — keyed to the LSP specification. Use this as the reference when +planning editor-UX work or picking a next feature. Source of truth is +`src/lsp/lp_lsp.ml` (dispatch + capabilities); when that diverges from +this document, update this document. + +Status key: **✅** implemented · **⚠️** partial/stub · **❌** not implemented · **➕** custom extension + +## Lifecycle & meta + +| Feature | LSP method | Status | Notes | +|---|---|---|---| +| Initialize handshake | `initialize` | ✅ | `lp_lsp.ml` `do_initialize`. Returns static capability set. Reads `clientCapabilities.textDocument.{completion.completionItem.snippetSupport, documentSymbol.hierarchicalDocumentSymbolSupport}`. Applies `Package.apply_config` for `rootUri` and every `workspaceFolders[].uri` so module mappings are live before the first `didOpen`. `initializationOptions` is still ignored. | +| Initialized notification | `initialized` | ⚠️ | NOOP. | +| Shutdown | `shutdown` | ✅ | Replies `null`. | +| Exit | `exit` | ✅ | Hard `exit 0`. | +| Unknown requests | (any unmapped method with `id`) | ✅ | Replies JSON-RPC `-32601 Method not found`. Unknown *notifications* (no `id`) are logged and dropped per spec. | +| Request cancellation | `$/cancelRequest` | ❌ | Single-threaded loop; long requests block. `didChange` notifications are debounced (later edits coalesce older ones for the same URI) but other requests still queue. | +| Progress reporting | `$/progress`, `window/workDoneProgress/*` | ❌ | | +| Log / show messages | `window/logMessage`, `window/showMessage` | ❌ | Server logs to a file (`/tmp/lambdapi_lsp_log.txt`) instead. | +| Telemetry | `telemetry/event` | ❌ | | +| Dynamic capability registration | `client/registerCapability` | ❌ | All capabilities static at init. | +| Configuration pull | `workspace/configuration` | ❌ | | + +## Text synchronization + +| Feature | LSP method | Status | Notes | +|---|---|---|---| +| Full-document sync | `textDocumentSync: 1` | ✅ | Whole document re-sent and re-checked on every edit. | +| Incremental sync | `textDocumentSync: 2` | ❌ | | +| didOpen | `textDocument/didOpen` | ✅ | Triggers full check; emits diagnostics. | +| didChange | `textDocument/didChange` | ✅ | Reuses full-sync replace; re-checks whole file. **Debounced**: when more `didChange` notifications for the same URI are already queued (peeked via the unbuffered IO reader), the current re-check is skipped — the trailing change triggers it instead. | +| didClose | `textDocument/didClose` | ✅ | Clears both `doc_table` and `completed_table`. | +| willSave | `textDocument/willSave` | ❌ | | +| willSaveWaitUntil | `textDocument/willSaveWaitUntil` | ❌ | | +| didSave | `textDocument/didSave` | ❌ | | + +## Language features (per-position) + +| Feature | LSP method | Status | Notes | +|---|---|---|---| +| Hover | `textDocument/hover` | ✅ | Plain-string type for symbols; `null` otherwise. | +| Go to definition | `textDocument/definition` | ✅ | Symbols → declaration pos; module paths in `require`/`open` → file start. | +| Go to declaration | `textDocument/declaration` | ❌ | | +| Go to type definition | `textDocument/typeDefinition` | ❌ | | +| Go to implementation | `textDocument/implementation` | ❌ | | +| Find references | `textDocument/references` | ❌ | | +| Document highlight | `textDocument/documentHighlight` | ❌ | | +| Completion | `textDocument/completion` | ✅ | In-scope symbols (no eager `detail`, resolved lazily), 19 hardcoded tactic keywords with snippet `insertText` when the client advertises `snippetSupport`, and visible hypotheses (kind Variable) inside a proof. No prefix awareness after `.`. | +| Completion resolve | `completionItem/resolve` | ✅ | Pretty-prints the symbol type and fills `detail` on the item being highlighted. | +| Signature help | `textDocument/signatureHelp` | ❌ | | +| Code action | `textDocument/codeAction` | ❌ | Explicitly `codeActionProvider: false`. | +| Code action resolve | `codeAction/resolve` | ❌ | | +| Code lens | `textDocument/codeLens` | ❌ | | +| Inlay hint | `textDocument/inlayHint` | ❌ | | +| Semantic tokens | `textDocument/semanticTokens/*` | ❌ | Clients rely on tree-sitter / TextMate grammars. | +| Document symbol | `textDocument/documentSymbol` | ✅ | When the client advertises `hierarchicalDocumentSymbolSupport: true`, returns `DocumentSymbol[]` walked from the AST: `symbol`/`opaque symbol` as Function, `inductive` as Enum with constructors as EnumMember children. Falls back to flat `SymbolInformation[]` (legacy shape) when the cap is absent. | +| Document link | `textDocument/documentLink` | ❌ | | +| Document color | `textDocument/documentColor` | ❌ | | +| Folding range | `textDocument/foldingRange` | ❌ | | +| Selection range | `textDocument/selectionRange` | ❌ | | +| Linked editing range | `textDocument/linkedEditingRange` | ❌ | | +| Moniker | `textDocument/moniker` | ❌ | | +| Call hierarchy | `textDocument/prepareCallHierarchy` | ❌ | | +| Type hierarchy | `textDocument/prepareTypeHierarchy` | ❌ | | +| Inline value | `textDocument/inlineValue` | ❌ | | +| Pull diagnostics | `textDocument/diagnostic` | ❌ | Uses push model only. | + +## Formatting & refactoring + +| Feature | LSP method | Status | Notes | +|---|---|---|---| +| Document formatting | `textDocument/formatting` | ❌ | | +| Range formatting | `textDocument/rangeFormatting` | ❌ | | +| On-type formatting | `textDocument/onTypeFormatting` | ❌ | | +| Rename | `textDocument/rename` | ❌ | | +| Prepare rename | `textDocument/prepareRename` | ❌ | | + +## Diagnostics + +| Feature | LSP method | Status | Notes | +|---|---|---|---| +| Publish diagnostics (push) | `textDocument/publishDiagnostics` | ✅ | Emitted on every `didOpen`/`didChange`. Severity 1/2/3/4 (error/warn/info/hint). With `--standard-lsp` off, diagnostics carry an extra `goal_info` field so proof state can be embedded per-sentence. | +| Diagnostic-related information | `DiagnosticRelatedInformation[]` | ❌ | No secondary locations attached to errors. | + +## Workspace + +| Feature | LSP method | Status | Notes | +|---|---|---|---| +| Workspace symbol | `workspace/symbol` | ❌ | | +| Execute command | `workspace/executeCommand` | ❌ | | +| Apply edit | `workspace/applyEdit` | ❌ | | +| Configuration changed | `workspace/didChangeConfiguration` | ❌ | | +| Workspace folders changed | `workspace/didChangeWorkspaceFolders` | ❌ | | +| Watched files changed | `workspace/didChangeWatchedFiles` | ❌ | | +| Will/did create/rename/delete files | `workspace/{will,did}{Create,Rename,Delete}Files` | ❌ | | +| Refresh requests | `workspace/diagnostic/refresh`, `…/semanticTokens/refresh`, `…/inlayHint/refresh`, `…/codeLens/refresh` | ❌ | | + +## Lambdapi-specific extensions + +| Feature | Method | Status | Notes | +|---|---|---|---| +| Proof goals at position | `proof/goals` | ➕ | Custom request: `{textDocument, position}` → `{goals, logs}`. Falls back to the closest goal *before* the cursor when asked mid-sentence. Primary API for clients showing live proof state. | +| Embedded goal info in diagnostics | `goal_info` field on each `Diagnostic` | ➕ | Only when `--standard-lsp` is **off**. Carries the same goal-snapshot payload as `proof/goals`, inlined per sentence. Strictly a protocol extension. | +| CLI flags | `--standard-lsp`, `--log-file`, `--lib-root`, `--map-dir` | — | Client launcher toggles. `--standard-lsp` suppresses the two ➕ extensions above. | + +## Summary + +**Implemented (9 core + 2 custom)**: `initialize`, `shutdown`/`exit`, text sync (full), `publishDiagnostics`, `hover`, `definition`, `documentSymbol`, `completion`, `completionItem/resolve` · `proof/goals`, `goal_info` diagnostic field. + +**Glaring gaps given the editor story we want**: `references`, `rename`/`prepareRename`, `semanticTokens`, `signatureHelp`, `codeAction` (e.g. "admit this goal", "intros", "insert tactic skeleton"), `codeLens` (per-theorem "check"/"run"), `inlayHint` (inferred types, implicit args), `foldingRange` (proof blocks). + +**Protocol-hygiene issues**: no request cancellation (`didChange` is debounced but other requests still queue); `initialize` still drops `initializationOptions` and most non-feature `clientCapabilities`; no `didSave`. diff --git a/tests/lsp/README.md b/tests/lsp/README.md new file mode 100644 index 000000000..8661ba899 --- /dev/null +++ b/tests/lsp/README.md @@ -0,0 +1,42 @@ +# LSP integration tests + +End-to-end tests for the lambdapi LSP server. Each test spawns a +`lambdapi lsp` subprocess, speaks JSON-RPC over stdio, and asserts on the +responses. + +## Running + +From the repository root: + +``` +make test_lsp # runs as part of `make test` too +python3 -m tests.lsp # equivalent, more verbose +python3 -m unittest tests.lsp.test_hover -v # single file +``` + +The harness prefers a locally-built binary (`_build/install/default/bin/lambdapi`) +over whatever is on `PATH`, so you always test the current tree. + +## Environment variables + +| Name | Purpose | +|---|---| +| `LAMBDAPI_LIB_ROOT` | override stdlib location (defaults to the opam install) | +| `LSP_TEST_LOG` | when set, pass `--log-file=$LSP_TEST_LOG` to the server | + +## Layout + +- `__init__.py` — empty; marks `tests/lsp` as a regular Python package + so the modules can import each other (`from .base import …`) and the + suite runs as `python3 -m tests.lsp` on every supported Python +- `__main__.py` — entry point for `python3 -m tests.lsp`: discovers + and runs the whole suite +- `base.py` — `LSPTestCase` with per-test server + fixture helpers +- `client.py` — JSON-RPC / stdio client (`LSPServer` class) +- `source.py` — pattern-based position finder for fixtures +- `fixtures/*.lp` — small focused test documents +- `test_*.py` — one file per LSP concern (lifecycle, diagnostics, …) + +## Requirements + +Python ≥ 3.8, stdlib only. No pip packages. diff --git a/tests/lsp/__init__.py b/tests/lsp/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/tests/lsp/__main__.py b/tests/lsp/__main__.py new file mode 100644 index 000000000..9ba804037 --- /dev/null +++ b/tests/lsp/__main__.py @@ -0,0 +1,20 @@ +"""Entry point: `python3 -m tests.lsp` runs the whole suite.""" + +import os +import sys +import unittest + + +if __name__ == "__main__": + # Ensure the tests can find each other as a package. + here = os.path.dirname(__file__) + repo_root = os.path.abspath(os.path.join(here, "..", "..")) + if repo_root not in sys.path: + sys.path.insert(0, repo_root) + + loader = unittest.TestLoader() + suite = loader.discover(start_dir=here, pattern="test_*.py", + top_level_dir=repo_root) + runner = unittest.TextTestRunner(verbosity=2) + result = runner.run(suite) + sys.exit(0 if result.wasSuccessful() else 1) diff --git a/tests/lsp/base.py b/tests/lsp/base.py new file mode 100644 index 000000000..20f3986e4 --- /dev/null +++ b/tests/lsp/base.py @@ -0,0 +1,162 @@ +"""Shared test base class and fixture helpers.""" + +import os +import pathlib +import shutil +import tempfile +import unittest + +from .client import LSPServer +from .source import SourceFile + + +HERE = pathlib.Path(__file__).resolve().parent +FIXTURES = HERE / "fixtures" +REPO_ROOT = HERE.parent.parent + + +def _lambdapi_binary(): + """Prefer a freshly-built local binary over whatever's on PATH.""" + local = REPO_ROOT / "_build" / "install" / "default" / "bin" / "lambdapi" + if local.exists(): + return str(local) + return shutil.which("lambdapi") + + +def _opam_stdlib(): + """Locate the installed lambdapi Stdlib (for --map-dir).""" + for base in [ + os.environ.get("LAMBDAPI_LIB_ROOT"), + os.path.expanduser("~/.opam/default/lib/lambdapi/lib_root"), + ]: + if base and os.path.isdir(os.path.join(base, "Stdlib")): + return os.path.join(base, "Stdlib") + return None + + +def has_stdlib(): + """True when the opam Stdlib is reachable (for conditional tests).""" + return _opam_stdlib() is not None + + +def stdlib_map_dir(): + """[--map-dir] value for Stdlib, or None if not installed.""" + d = _opam_stdlib() + return f"Stdlib:{d}" if d else None + + +def requires_stdlib(test): + """Decorator: skip a test method if Stdlib is not available.""" + return unittest.skipUnless( + has_stdlib(), + "lambdapi Stdlib not installed; set LAMBDAPI_LIB_ROOT")(test) + + +class LSPTestCase(unittest.TestCase): + """Base class: starts one server per test, exposes helpers.""" + + standard_lsp = True + advertise_snippet_support = False + advertise_hierarchical_symbols = False + advertise_markdown_docs = False + extra_map_dirs = () + + @classmethod + def setUpClass(cls): + cls._tmpdir = tempfile.TemporaryDirectory(prefix="lptest-") + cls.lib_root = cls._tmpdir.name + # Copy fixtures into the lib root so relative references resolve. + for fixture in FIXTURES.glob("*.lp"): + dest = pathlib.Path(cls.lib_root) / fixture.name + dest.write_text(fixture.read_text()) + # A lambdapi.pkg is required for the server to treat the dir as a + # package root. + pkg = pathlib.Path(cls.lib_root) / "lambdapi.pkg" + pkg.write_text("package_name = test\nroot_path = test\n") + + @classmethod + def tearDownClass(cls): + cls._tmpdir.cleanup() + + def setUp(self): + map_dirs = list(self.extra_map_dirs) + md = stdlib_map_dir() + if md: + map_dirs.append(md) + self.server = LSPServer( + lib_root=self.lib_root, + map_dirs=map_dirs, + standard_lsp=self.standard_lsp, + log_file=os.environ.get("LSP_TEST_LOG"), + binary=_lambdapi_binary(), + ) + self.server.start() + self.addCleanup(self.server.stop) + td = {} + completion_item = {} + if self.advertise_snippet_support: + completion_item["snippetSupport"] = True + if self.advertise_markdown_docs: + completion_item["documentationFormat"] = ["markdown", + "plaintext"] + if completion_item: + td["completion"] = {"completionItem": completion_item} + if self.advertise_hierarchical_symbols: + td["documentSymbol"] = { + "hierarchicalDocumentSymbolSupport": True} + caps = {"textDocument": td} if td else {} + self.server.initialize( + root_uri=f"file://{self.lib_root}", capabilities=caps) + + # --- Fixture helpers -------------------------------------------------- + + def fixture_path(self, name): + return os.path.join(self.lib_root, name) + + def fixture_uri(self, name): + return "file://" + self.fixture_path(name) + + def open_fixture(self, name, wait=True): + """Open a fixture and return (uri, text, SourceFile, diagnostics).""" + path = self.fixture_path(name) + with open(path) as f: + text = f.read() + uri = "file://" + path + self.server.did_open(uri, text) + diags = [] + if wait: + notifs = self.server.drain_notifications(timeout=5.0) + diags = self.server.extract_diagnostics(notifs, uri=uri) + return uri, text, SourceFile(text), diags + + def open_text(self, name, text, wait=True): + """Open an inline text as a fresh doc under [name].""" + path = os.path.join(self.lib_root, name) + with open(path, "w") as f: + f.write(text) + self.addCleanup(lambda: os.path.exists(path) and os.remove(path)) + uri = "file://" + path + self.server.did_open(uri, text) + diags = [] + if wait: + notifs = self.server.drain_notifications(timeout=5.0) + diags = self.server.extract_diagnostics(notifs, uri=uri) + return uri, SourceFile(text), diags + + # --- Diagnostic helpers ---------------------------------------------- + + @staticmethod + def errors(diagnostics): + return [d for d in diagnostics if d.get("severity") == 1] + + @staticmethod + def hints(diagnostics): + return [d for d in diagnostics if d.get("severity") == 4] + + def assertNoErrors(self, diagnostics, msg=""): + errs = self.errors(diagnostics) + if errs: + self.fail( + f"{msg}: {len(errs)} error(s), first: {errs[0].get('message')}" + if msg else + f"{len(errs)} error(s), first: {errs[0].get('message')}") diff --git a/tests/lsp/client.py b/tests/lsp/client.py new file mode 100644 index 000000000..f0d49ed04 --- /dev/null +++ b/tests/lsp/client.py @@ -0,0 +1,295 @@ +"""LSP client over JSON-RPC/stdio for testing the lambdapi LSP server. + +The client is small by design: it writes framed JSON-RPC to stdin and reads +framed replies / notifications from stdout. stderr is collected in a +background thread and surfaced when the server crashes. + +Typical use: + + with LSPServer(lib_root="...") as srv: + srv.initialize() + diags = srv.did_open("file:///foo.lp", text) + resp = srv.hover("file:///foo.lp", line=3, character=10) + +All line/character indices follow the LSP convention (0-based). +""" + +import json +import os +import queue +import shutil +import subprocess +import threading + + +class LSPError(Exception): + """Raised when the server returns an error or times out.""" + + +class LSPServer: + """A running lambdapi LSP subprocess.""" + + def __init__(self, lib_root, map_dirs=None, standard_lsp=True, + log_file=None, binary=None, timeout=15.0): + self.lib_root = lib_root + self.map_dirs = list(map_dirs or []) + self.standard_lsp = standard_lsp + self.log_file = log_file + self.binary = binary or shutil.which("lambdapi") + if not self.binary: + raise LSPError("lambdapi binary not found on PATH") + self.timeout = timeout + self._proc = None + self._stderr = [] + self._notifications = queue.Queue() + # [_pending] maps request id -> reply queue. Writer (test thread) + # adds entries before sending; reader thread pops on response. + # [_next_id] is touched only from the test thread today, but we + # guard both behind [_lock] so the invariant survives refactors. + self._lock = threading.Lock() + self._pending = {} + # Start at 0, like Zed: id 0 is a valid JSON-RPC request id and + # servers must reply to it (regression: an `id <> 0` sentinel + # in the server left Zed's initialize unanswered). + self._next_id = 0 + self._reader_thread = None + self._stderr_thread = None + self._stop = threading.Event() + + # --- Process lifecycle ------------------------------------------------ + + def start(self): + cmd = [self.binary, "lsp"] + if self.standard_lsp: + cmd.append("--standard-lsp") + cmd.append(f"--lib-root={self.lib_root}") + for md in self.map_dirs: + cmd.append(f"--map-dir={md}") + if self.log_file: + cmd.append(f"--log-file={self.log_file}") + self._proc = subprocess.Popen( + cmd, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + bufsize=0, + ) + self._reader_thread = threading.Thread( + target=self._read_stdout, daemon=True) + self._stderr_thread = threading.Thread( + target=self._read_stderr, daemon=True) + self._reader_thread.start() + self._stderr_thread.start() + + def stop(self): + self._stop.set() + if not self._proc: + return + if self._proc.poll() is None: + try: + self._proc.stdin.close() + except Exception: + pass + try: + self._proc.terminate() + self._proc.wait(timeout=2) + except subprocess.TimeoutExpired: + self._proc.kill() + self._proc.wait(timeout=1) + # Close remaining pipes (also unblocks readers still in read()). + for pipe in (self._proc.stdout, self._proc.stderr, self._proc.stdin): + try: + pipe and pipe.close() + except Exception: + pass + # Join reader threads so file descriptors aren't left dangling — + # avoids ResourceWarning without needing -W ignore in the runner. + for t in (self._reader_thread, self._stderr_thread): + if t is not None: + t.join(timeout=1.0) + + def __enter__(self): + self.start() + return self + + def __exit__(self, *exc): + self.stop() + + # --- JSON-RPC framing ------------------------------------------------- + + def _write(self, msg): + body = json.dumps(msg).encode() + header = f"Content-Length: {len(body)}\r\n\r\n".encode() + self._proc.stdin.write(header + body) + self._proc.stdin.flush() + + def _read_stdout(self): + buf = b"" + while not self._stop.is_set(): + # Read header + while b"\r\n\r\n" not in buf: + chunk = self._proc.stdout.read(1) + if not chunk: + return + buf += chunk + header, _, buf = buf.partition(b"\r\n\r\n") + size = None + for line in header.decode().splitlines(): + if line.lower().startswith("content-length:"): + size = int(line.split(":", 1)[1].strip()) + if size is None: + return + while len(buf) < size: + chunk = self._proc.stdout.read(size - len(buf)) + if not chunk: + return + buf += chunk + body, buf = buf[:size], buf[size:] + try: + msg = json.loads(body.decode()) + except json.JSONDecodeError: + continue + if "id" in msg and ("result" in msg or "error" in msg): + # Response to a request + with self._lock: + q = self._pending.pop(msg["id"], None) + if q is not None: + q.put(msg) + else: + # Notification (from server to client) + self._notifications.put(msg) + + def _read_stderr(self): + for line in self._proc.stderr: + self._stderr.append(line.decode(errors="replace").rstrip()) + + # --- Request / notification ----------------------------------------- + + def request(self, method, params=None): + reply = queue.Queue(maxsize=1) + # Reserve the id and register the reply slot *before* sending so + # the response can never arrive before we're listening for it. + with self._lock: + mid = self._next_id + self._next_id += 1 + self._pending[mid] = reply + self._write({"jsonrpc": "2.0", "id": mid, + "method": method, "params": params or {}}) + try: + msg = reply.get(timeout=self.timeout) + except queue.Empty: + with self._lock: + self._pending.pop(mid, None) + raise LSPError( + f"timeout waiting for {method} (id={mid}); " + f"stderr={self._stderr[-5:]}") + if "error" in msg: + raise LSPError(f"{method}: {msg['error']}") + return msg.get("result") + + def request_with_id(self, rid, method, params=None): + """Send a request with an explicit id (JSON-RPC also allows + string ids) and return the raw response message.""" + reply = queue.Queue(maxsize=1) + with self._lock: + self._pending[rid] = reply + self._write({"jsonrpc": "2.0", "id": rid, + "method": method, "params": params or {}}) + try: + return reply.get(timeout=self.timeout) + except queue.Empty: + with self._lock: + self._pending.pop(rid, None) + raise LSPError( + f"timeout waiting for {method} (id={rid!r}); " + f"stderr={self._stderr[-5:]}") + + def notify(self, method, params=None): + self._write({"jsonrpc": "2.0", + "method": method, "params": params or {}}) + + def drain_notifications(self, timeout=2.0): + """Collect all notifications that arrive within [timeout] of silence.""" + out = [] + try: + while True: + msg = self._notifications.get(timeout=timeout) + out.append(msg) + timeout = 0.2 # subsequent reads are quick polls + except queue.Empty: + pass + return out + + # --- Convenience LSP methods ------------------------------------------ + + def initialize(self, root_uri=None, capabilities=None): + params = {"capabilities": capabilities or {}} + if root_uri is not None: + params["rootUri"] = root_uri + result = self.request("initialize", params) + self.notify("initialized", {}) + return result + + def resolve_completion(self, item): + return self.request("completionItem/resolve", item) + + def shutdown(self): + self.request("shutdown") + self.notify("exit") + + def did_open(self, uri, text, language_id="lp", version=1): + self.notify("textDocument/didOpen", { + "textDocument": {"uri": uri, "languageId": language_id, + "version": version, "text": text}}) + + def did_change(self, uri, text, version): + self.notify("textDocument/didChange", { + "textDocument": {"uri": uri, "version": version}, + "contentChanges": [{"text": text}]}) + + def did_close(self, uri): + self.notify("textDocument/didClose", { + "textDocument": {"uri": uri}}) + + def hover(self, uri, line, character): + return self.request("textDocument/hover", { + "textDocument": {"uri": uri}, + "position": {"line": line, "character": character}}) + + def definition(self, uri, line, character): + return self.request("textDocument/definition", { + "textDocument": {"uri": uri}, + "position": {"line": line, "character": character}}) + + def document_symbol(self, uri): + return self.request("textDocument/documentSymbol", { + "textDocument": {"uri": uri}}) + + def goals(self, uri, line, character): + return self.request("proof/goals", { + "textDocument": {"uri": uri}, + "position": {"line": line, "character": character}}) + + # --- Diagnostics helpers --------------------------------------------- + + def extract_diagnostics(self, notifications, uri=None): + """Return the latest publishDiagnostics for [uri] (or any URI). + + Each publishDiagnostics notification *supersedes* the previous one + for the same URI (LSP spec), so the last one wins.""" + latest = {} + for msg in notifications: + if msg.get("method") != "textDocument/publishDiagnostics": + continue + params = msg.get("params", {}) + u = params.get("uri") + if uri is not None and u != uri: + continue + latest[u] = params.get("diagnostics", []) + if uri is not None: + return latest.get(uri, []) + # If no URI was specified, flatten all latest-per-URI lists. + out = [] + for v in latest.values(): + out.extend(v) + return out diff --git a/tests/lsp/fixtures/imports.lp b/tests/lsp/fixtures/imports.lp new file mode 100644 index 000000000..f147d50bf --- /dev/null +++ b/tests/lsp/fixtures/imports.lp @@ -0,0 +1,5 @@ +require open Stdlib.Nat; + +symbol double : ℕ → ℕ; +rule double 0 ↪ 0 +with double (+1 $n) ↪ +1 (+1 (double $n)); diff --git a/tests/lsp/fixtures/inductive.lp b/tests/lsp/fixtures/inductive.lp new file mode 100644 index 000000000..2503ad5f7 --- /dev/null +++ b/tests/lsp/fixtures/inductive.lp @@ -0,0 +1,8 @@ +constant symbol Bool : TYPE; + +inductive Tree : TYPE ≔ +| leaf : Tree +| node : Tree → Tree → Tree; + +symbol height : Tree → Bool; +symbol mirror : Tree → Tree ≔ λ t, t; diff --git a/tests/lsp/fixtures/modifiers.lp b/tests/lsp/fixtures/modifiers.lp new file mode 100644 index 000000000..aa40fe285 --- /dev/null +++ b/tests/lsp/fixtures/modifiers.lp @@ -0,0 +1,8 @@ +constant symbol Nat : TYPE; +constant symbol zero : Nat; + +injective symbol inj : Nat → Nat; +private symbol priv : Nat; +protected symbol prot : Nat; +sequential symbol seq : Nat → Nat; +opaque symbol op : Nat ≔ zero; diff --git a/tests/lsp/fixtures/multiple_errors.lp b/tests/lsp/fixtures/multiple_errors.lp new file mode 100644 index 000000000..7bccd8e9c --- /dev/null +++ b/tests/lsp/fixtures/multiple_errors.lp @@ -0,0 +1,4 @@ +constant symbol Nat : TYPE; +symbol bad1 : Undef1; +constant symbol zero : Nat; +symbol bad2 : Undef2; diff --git a/tests/lsp/fixtures/proof.lp b/tests/lsp/fixtures/proof.lp new file mode 100644 index 000000000..ca6724c4b --- /dev/null +++ b/tests/lsp/fixtures/proof.lp @@ -0,0 +1,13 @@ +require open Stdlib.Set Stdlib.Prop Stdlib.Eq Stdlib.Nat; + +opaque symbol zero_eq_zero : π (0 = 0) ≔ +begin + reflexivity; +end; + +opaque symbol eq_sym_nat : Π (x y : ℕ), π (x = y) → π (y = x) ≔ +begin + assume x y h; + symmetry; + apply h; +end; diff --git a/tests/lsp/fixtures/qualified.lp b/tests/lsp/fixtures/qualified.lp new file mode 100644 index 000000000..7c877cc72 --- /dev/null +++ b/tests/lsp/fixtures/qualified.lp @@ -0,0 +1,3 @@ +require Stdlib.Nat; + +symbol two : Stdlib.Nat.ℕ ≔ Stdlib.Nat.+1 (Stdlib.Nat.+1 Stdlib.Nat.0); diff --git a/tests/lsp/fixtures/simple.lp b/tests/lsp/fixtures/simple.lp new file mode 100644 index 000000000..3a0d382b8 --- /dev/null +++ b/tests/lsp/fixtures/simple.lp @@ -0,0 +1,6 @@ +constant symbol Nat : TYPE; +constant symbol zero : Nat; +constant symbol succ : Nat → Nat; +symbol double : Nat → Nat; +rule double zero ↪ zero +with double (succ $n) ↪ succ (succ (double $n)); diff --git a/tests/lsp/fixtures/unicode_cols.lp b/tests/lsp/fixtures/unicode_cols.lp new file mode 100644 index 000000000..1af0fdd5d --- /dev/null +++ b/tests/lsp/fixtures/unicode_cols.lp @@ -0,0 +1,3 @@ +constant symbol α : TYPE; +constant symbol β : α; +symbol x : α ≔ β; diff --git a/tests/lsp/fixtures/with_error.lp b/tests/lsp/fixtures/with_error.lp new file mode 100644 index 000000000..2ab83994d --- /dev/null +++ b/tests/lsp/fixtures/with_error.lp @@ -0,0 +1,3 @@ +constant symbol Nat : TYPE; +constant symbol zero : Nat; +symbol bad : Undefined; diff --git a/tests/lsp/source.py b/tests/lsp/source.py new file mode 100644 index 000000000..442360c93 --- /dev/null +++ b/tests/lsp/source.py @@ -0,0 +1,48 @@ +"""Position finder: locate (line, character) for a pattern in source text. + +Tests need stable positions even when a fixture gains a leading line. Use +this helper to search for a distinctive pattern in the source and return +the 0-based (line, character) for a substring within the match. + +Example: + + src = SourceFile(text) + # Line-based: find the word "foo" on the line that contains "symbol foo" + line, col = src.find(r"symbol foo", "foo") +""" + +import re + + +class SourceFile: + def __init__(self, text): + self.text = text + self.lines = text.split("\n") + + def find(self, line_pattern, token=None): + """Find [token] on the first line matching [line_pattern]. + + If [token] is None, returns the start of [line_pattern]'s match. + Both arguments are treated as regexes. + """ + line_re = re.compile(line_pattern) + for lineno, line in enumerate(self.lines): + m = line_re.search(line) + if not m: + continue + if token is None: + return lineno, m.start() + t = re.search(token, line[m.start():]) + if not t: + continue + return lineno, m.start() + t.start() + raise AssertionError( + f"pattern {line_pattern!r} / token {token!r} not found") + + def line_of(self, pattern): + """Return the 0-based line number of the first line matching [pattern].""" + line_re = re.compile(pattern) + for lineno, line in enumerate(self.lines): + if line_re.search(line): + return lineno + raise AssertionError(f"pattern {pattern!r} not found") diff --git a/tests/lsp/test_completion.py b/tests/lsp/test_completion.py new file mode 100644 index 000000000..7ee5a51eb --- /dev/null +++ b/tests/lsp/test_completion.py @@ -0,0 +1,352 @@ +"""Completion tests: symbols, proof-context tactic keywords, hypotheses, +and lazy detail via completionItem/resolve.""" + +import re +import unittest + +from .base import LSPTestCase, REPO_ROOT + + +def _completion_request(srv, uri, line, character): + return srv.request("textDocument/completion", { + "textDocument": {"uri": uri}, + "position": {"line": line, "character": character}, + }) + + +class TestCompletion(LSPTestCase): + + def test_in_scope_symbols_listed(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 5, 0) + items = r.get("items", []) + labels = [i["label"] for i in items] + for expected in ("Nat", "zero", "succ", "double"): + self.assertIn(expected, labels, + f"{expected!r} should appear in completion list") + + def test_symbol_items_omit_detail_but_carry_resolve_data(self): + """Symbol detail is computed on [completionItem/resolve], not in + the initial response. The initial response carries a [data] field + pointing back at the symbol so resolve can look it up.""" + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 5, 0) + by_label = {i["label"]: i for i in r.get("items", [])} + succ = by_label.get("succ") + self.assertIsNotNone(succ) + self.assertNotIn("detail", succ, + f"detail should be attached lazily via resolve; got {succ!r}") + data = succ.get("data") + self.assertIsInstance(data, dict, + f"symbol item needs a [data] field for resolve; got {succ!r}") + # [data] is opaque to the client (the server reads it back on + # resolve); only pin down what resolve relies on. + self.assertEqual(data.get("kind"), "symbol") + self.assertEqual(data.get("uri"), uri) + + def test_resolve_attaches_type_detail(self): + """completionItem/resolve on a symbol item returns the same item + with [detail] populated.""" + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 5, 0) + succ = next(i for i in r.get("items", []) if i["label"] == "succ") + resolved = self.server.resolve_completion(succ) + self.assertIsNotNone(resolved) + self.assertIn("Nat", resolved.get("detail", ""), + f"resolved detail should mention Nat; got {resolved!r}") + + def test_symbol_items_carry_no_kind(self): + """The LSP completion kinds don't match lambdapi's notions + (axiom, constructor, definable symbol, …), so symbol items + don't claim one.""" + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 5, 0) + for item in r.get("items", []): + if item["label"] in ("Nat", "zero", "succ", "double"): + self.assertNotIn("kind", item, + f"symbol items should not be classified; got {item!r}") + + def test_no_ghost_symbols_in_completions(self): + """Internal ghost symbols (unification-rule machinery such as + `≡` and `;`) must not be offered as completions.""" + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 5, 0) + labels = {i["label"] for i in r.get("items", [])} + leaked = {"≡", ";", "coerce"} & labels + self.assertFalse(leaked, + f"ghost symbols leaked into completions: {leaked}") + + def test_no_tactic_completions_outside_proof(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 0, 0) + labels = [i["label"] for i in r.get("items", [])] + self.assertNotIn("refine", labels) + self.assertNotIn("rewrite", labels) + + +class TestCompletionInProof(LSPTestCase): + """Inside a begin..end block, tactic keywords + hypotheses appear.""" + + PROOF = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol triv : Nat \u2192 Nat \u2254\n" + "begin\n" + " assume n;\n" + " refine n;\n" + "end;\n" + ) + + def test_tactic_completions_in_proof(self): + uri, _src, _ = self.open_text("prf.lp", self.PROOF) + # Line 5 is " refine n;" — cursor at col 0 is inside the proof. + r = _completion_request(self.server, uri, 5, 0) + labels = [i["label"] for i in r.get("items", [])] + for kw in ("refine", "reflexivity", "apply", "assume", + "eval", "fail"): + self.assertIn(kw, labels, + f"{kw!r} should be offered inside a proof; got {labels[:8]}") + + def test_tactic_completions_carry_documentation(self): + """Tactic items carry [documentation] so clients can show what + the tactic does in the completion docs panel.""" + uri, _src, _ = self.open_text("prf.lp", self.PROOF) + r = _completion_request(self.server, uri, 5, 0) + refine = next(i for i in r.get("items", []) + if i["label"] == "refine") + doc = refine.get("documentation", "") + self.assertIn("goal", doc, + f"refine's documentation should describe the tactic; " + f"got {doc!r}") + + def test_hypothesis_completions_in_proof(self): + """After `assume n`, the hypothesis `n` should appear as a + completion with CompletionItemKind.Variable (6) and its type.""" + uri, _src, _ = self.open_text("prf.lp", self.PROOF) + # Line 5 (` refine n;`), col 0: after `assume n;` on line 4. + r = _completion_request(self.server, uri, 5, 0) + by_label = {i["label"]: i for i in r.get("items", [])} + self.assertIn("n", by_label, + f"hypothesis 'n' should appear; got {sorted(by_label)[:20]}") + n_item = by_label["n"] + self.assertEqual(n_item["kind"], 6, + f"hypothesis kind should be Variable (6); got {n_item['kind']}") + self.assertIn("Nat", n_item.get("detail", ""), + f"hypothesis detail should carry its type; got {n_item!r}") + + +class TestSnippetSupport(LSPTestCase): + """Tactic completions carry TextMate-style [insertText] / + [insertTextFormat=2] when the client advertises snippetSupport, + and omit them otherwise.""" + + advertise_snippet_support = True + + PROOF = TestCompletionInProof.PROOF + + def test_tactic_with_arg_emits_snippet(self): + uri, _src, _ = self.open_text("prf.lp", self.PROOF) + r = _completion_request(self.server, uri, 5, 0) + apply_item = next(i for i in r.get("items", []) + if i["label"] == "apply") + self.assertEqual(apply_item.get("insertTextFormat"), 2, + f"snippet format expected; got {apply_item!r}") + self.assertIn("${1:", apply_item.get("insertText", ""), + f"insertText should contain a tab-stop; got {apply_item!r}") + + def test_command_keyword_snippet_at_toplevel(self): + uri, _src, _ = self.open_text("prf2.lp", self.PROOF) + r = _completion_request(self.server, uri, 0, 0) + sym = next(i for i in r.get("items", []) + if i["label"] == "symbol") + self.assertEqual(sym.get("insertTextFormat"), 2, + f"snippet format expected; got {sym!r}") + self.assertIn("${1:", sym.get("insertText", ""), + f"insertText should contain a tab-stop; got {sym!r}") + + +class TestMarkdownDocumentation(LSPTestCase): + """When the client advertises markdown [documentationFormat], + tactic docs are sent as MarkupContent so backticks render as + code spans; otherwise they stay plain strings.""" + + advertise_markdown_docs = True + + def test_tactic_documentation_is_markup_content(self): + uri, _src, _ = self.open_text("prf.lp", TestCompletionInProof.PROOF) + r = _completion_request(self.server, uri, 5, 0) + refine = next(i for i in r.get("items", []) + if i["label"] == "refine") + doc = refine.get("documentation") + self.assertIsInstance(doc, dict, + f"markdown-capable client should get MarkupContent; got {doc!r}") + self.assertEqual(doc.get("kind"), "markdown") + self.assertIn("`refine t`", doc.get("value", ""), + "documentation should carry markdown code spans") + + +class TestNoSnippetSupport(LSPTestCase): + """With snippetSupport off, tactic items have no [insertText].""" + + advertise_snippet_support = False + + def test_tactic_lacks_insertText(self): + uri, _src, _ = self.open_text("prf.lp", TestCompletionInProof.PROOF) + r = _completion_request(self.server, uri, 5, 0) + apply_item = next(i for i in r.get("items", []) + if i["label"] == "apply") + self.assertNotIn("insertText", apply_item, + f"expected no insertText without snippetSupport; got {apply_item!r}") + self.assertNotIn("insertTextFormat", apply_item) + + +class TestCommandKeywordCompletions(LSPTestCase): + """Outside proofs, command keywords and modifiers are offered with + documentation; inside proofs the proof enders are, instead.""" + + def test_command_keywords_at_toplevel(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _completion_request(self.server, uri, 0, 0) + by_label = {i["label"]: i for i in r.get("items", [])} + for kw in ("symbol", "inductive", "rule", "require", "opaque"): + self.assertIn(kw, by_label, + f"{kw!r} should be offered at toplevel") + self.assertIn("rewriting", by_label["rule"].get("documentation"), + "keyword items should carry their documentation") + + def test_command_keywords_not_in_proof(self): + uri, _src, _ = self.open_text("kw.lp", TestCompletionInProof.PROOF) + r = _completion_request(self.server, uri, 5, 0) + labels = {i["label"] for i in r.get("items", [])} + self.assertNotIn("notation", labels) + self.assertNotIn("require", labels) + + def test_proof_enders_in_proof_only(self): + uri, _src, _ = self.open_text("kw2.lp", TestCompletionInProof.PROOF) + r = _completion_request(self.server, uri, 5, 0) + by_label = {i["label"]: i for i in r.get("items", [])} + for kw in ("end", "admitted", "abort"): + self.assertIn(kw, by_label, + f"{kw!r} should be offered inside a proof") + self.assertIn("axioms", by_label["admitted"].get("documentation")) + r2 = _completion_request(self.server, uri, 0, 0) + labels2 = {i["label"] for i in r2.get("items", [])} + self.assertNotIn("admitted", labels2, + "proof enders should not be offered at toplevel") + + +class TestCompletionMidEdit(LSPTestCase): + """Typing a partial tactic name breaks the parse of the enclosing + command; proof-context completions must survive via the nodes of + the last successful parse, and resync on the next clean parse.""" + + BROKEN = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol triv : Nat → Nat ≔\n" + "begin\n" + " assume n;\n" + " re\n" # mid-word edit: parse error + " refine n;\n" + "end;\n" + ) + + def test_proof_context_survives_broken_parse(self): + uri, _src, _ = self.open_text("mid.lp", TestCompletionInProof.PROOF) + self.server.did_change(uri, self.BROKEN, 2) + notifs = self.server.drain_notifications(timeout=5.0) + diags = self.server.extract_diagnostics(notifs, uri=uri) + self.assertTrue(self.errors(diags), + "the mid-word text should fail to parse") + # Cursor right after the "re" being typed (line 5, col 4). + r = _completion_request(self.server, uri, 5, 4) + labels = {i["label"] for i in r.get("items", [])} + self.assertIn("refine", labels, + f"tactics must survive a mid-word edit; got {sorted(labels)[:10]}") + self.assertIn("n", labels, + "hypotheses must survive a mid-word edit") + self.assertNotIn("zero", labels, + "a proof step starts with a tactic, never a symbol") + # In a term position (the argument of the refine below the + # breakage), symbols checked before it must still be offered. + r = _completion_request(self.server, uri, 6, 9) + labels = {i["label"] for i in r.get("items", [])} + self.assertIn("zero", labels, + "symbols checked before the breakage must still be offered") + + def test_context_resyncs_after_clean_parse(self): + uri, _src, _ = self.open_text("mid2.lp", TestCompletionInProof.PROOF) + self.server.did_change(uri, self.BROKEN, 2) + self.server.drain_notifications(timeout=5.0) + # Replace the proof by a plain definition: the text parses + # again, so the retained proof context must be dropped. + flat = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol triv : Nat → Nat ≔ λ n, n;\n" + ) + self.server.did_change(uri, flat, 3) + self.server.drain_notifications(timeout=5.0) + r = _completion_request(self.server, uri, 2, 0) + labels = {i["label"] for i in r.get("items", [])} + self.assertNotIn("refine", labels, + "stale proof context must clear after a clean parse") + + +class TestTacticDocSync(LSPTestCase): + """The completion list must cover every tactic and query + documented in the manual. Extracts the ``name`` section headings + from the doc pages and checks each is offered — catching drift + when a tactic or query is added to the docs but not to the LSP.""" + + TACTIC_FILES = ("tactics.rst", "tacticals.rst", "equality.rst") + QUERY_FILES = ("queries.rst",) + + @staticmethod + def documented_names(fnames): + item = r"``[a-z_0-9]+(?: <[^>]+>)?``" + heading = re.compile(rf"^{item}(?:, {item})*$") + name_re = re.compile(r"``([a-z_0-9]+)") + underline = re.compile(r"^[-~^\"'=+#*]{3,}$") + names = set() + for fname in fnames: + lines = (REPO_ROOT / "doc" / fname).read_text().splitlines() + for i in range(len(lines) - 1): + if heading.match(lines[i].strip()) \ + and underline.match(lines[i + 1].strip()): + names.update(name_re.findall(lines[i])) + return names + + def _labels(self, uri, line): + r = _completion_request(self.server, uri, line, 0) + return {i["label"] for i in r.get("items", [])} + + def test_documented_tactics_are_offered(self): + documented = self.documented_names(self.TACTIC_FILES) + self.assertGreaterEqual(len(documented), 20, + f"suspiciously few tactic headings extracted from " + f"{self.TACTIC_FILES}: {sorted(documented)}") + uri, _src, _ = self.open_text("sync.lp", TestCompletionInProof.PROOF) + missing = documented - self._labels(uri, 5) + self.assertFalse(missing, + f"tactics documented in doc/*.rst but not offered as " + f"completions: {sorted(missing)}") + + def test_documented_queries_are_offered_in_both_contexts(self): + """Queries are commands and tactics at once; they must be + offered at toplevel and inside proofs.""" + documented = self.documented_names(self.QUERY_FILES) + self.assertGreaterEqual(len(documented), 10, + f"suspiciously few query headings extracted: " + f"{sorted(documented)}") + uri, _src, _ = self.open_text("syncq.lp", + TestCompletionInProof.PROOF) + for line, where in ((0, "at toplevel"), (5, "inside a proof")): + missing = documented - self._labels(uri, line) + self.assertFalse(missing, + f"queries documented in doc/queries.rst but not " + f"offered {where}: {sorted(missing)}") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_completion_context.py b/tests/lsp/test_completion_context.py new file mode 100644 index 000000000..58831dbe6 --- /dev/null +++ b/tests/lsp/test_completion_context.py @@ -0,0 +1,446 @@ +"""Context-aware completion: module paths, qualified names, argument +keywords. Keyword membership comes from the parser's follow set at +the cursor; the partial-token contexts (paths, qualified names, flag +names) are detected lexically from the line before the cursor, so +they also work while the text does not parse.""" + +import unittest + +from .base import LSPTestCase, requires_stdlib + + +def _complete(srv, uri, line, character, context=None): + params = {"textDocument": {"uri": uri}, + "position": {"line": line, "character": character}} + if context is not None: + params["context"] = context + return srv.request("textDocument/completion", params) + + +def _labels(r): + return {i["label"] for i in (r or {}).get("items", [])} + + +class TestRequirePathCompletion(LSPTestCase): + """After `require`/`open`, complete module paths from the library + mappings, replacing the typed partial path via a textEdit.""" + + def test_require_offers_local_modules(self): + uri, _src, _ = self.open_text("req1.lp", "require test.\n") + r = _complete(self.server, uri, 0, 13) + by_label = {i["label"]: i for i in r.get("items", [])} + self.assertIn("test.simple", by_label, + f"local module should be offered; got " + f"{sorted(by_label)[:10]}") + item = by_label["test.simple"] + self.assertEqual(item.get("kind"), 9) # Module + te = item.get("textEdit") + self.assertIsNotNone(te, "path items need a textEdit: '.' is " + "not a word character, a label would insert after the dot") + self.assertEqual(te["newText"], "test.simple") + self.assertEqual(te["range"]["start"], + {"line": 0, "character": 8}) + self.assertEqual(te["range"]["end"], + {"line": 0, "character": 13}) + + def test_require_open_offers_paths_only(self): + uri, _src, _ = self.open_text("req2.lp", "require open test.\n") + labels = _labels(_complete(self.server, uri, 0, 18)) + self.assertIn("test.simple", labels) + self.assertNotIn("symbol", labels, + "a path position should not offer command keywords") + + def test_open_offers_paths(self): + uri, _src, _ = self.open_text("req3.lp", "open test.\n") + self.assertIn("test.simple", + _labels(_complete(self.server, uri, 0, 10))) + + def test_partial_path_filters(self): + uri, _src, _ = self.open_text("req4.lp", "require test.sim\n") + labels = _labels(_complete(self.server, uri, 0, 16)) + self.assertIn("test.simple", labels) + self.assertNotIn("test.proof", labels, + "candidates should be filtered by the typed prefix") + + @requires_stdlib + def test_require_offers_stdlib(self): + uri, _src, _ = self.open_text("req5.lp", "require Stdlib.\n") + self.assertIn("Stdlib.Nat", + _labels(_complete(self.server, uri, 0, 15))) + + def test_indented_require_offers_paths(self): + uri, _src, _ = self.open_text("req6.lp", " require test.\n") + self.assertIn("test.simple", + _labels(_complete(self.server, uri, 0, 15))) + + def test_second_path_on_the_same_require(self): + uri, _src, _ = self.open_text("req7.lp", + "require test.simple test.\n") + self.assertIn("test.inductive", + _labels(_complete(self.server, uri, 0, 25))) + + def test_no_paths_after_as(self): + """`require M as ` expects a fresh alias name, not a + module path.""" + uri, _src, _ = self.open_text("req8.lp", + "require test.simple as \n") + self.assertNotIn("test.simple", + _labels(_complete(self.server, uri, 0, 23))) + + def test_private_require_offers_paths(self): + uri, _src, _ = self.open_text("req9.lp", "private open test.\n") + self.assertIn("test.simple", + _labels(_complete(self.server, uri, 0, 18))) + + +class TestQualifiedCompletion(LSPTestCase): + """After `M.` in term position, complete the non-private symbols + of the (required) module M, resolving `require as` aliases, plus + the next segments of loaded module paths.""" + + def test_qualified_offers_module_symbols(self): + uri, _src, _ = self.open_text("qual1.lp", + "require test.simple;\n" + "symbol z : test.simple.\n") + r = _complete(self.server, uri, 1, 23) + labels = _labels(r) + for name in ("Nat", "zero", "succ", "double"): + self.assertIn(name, labels, + f"{name!r} of test.simple should be offered; " + f"got {sorted(labels)[:10]}") + + def test_qualified_resolve_attaches_type(self): + uri, _src, _ = self.open_text("qual2.lp", + "require test.simple;\n" + "symbol z : test.simple.\n") + r = _complete(self.server, uri, 1, 23) + item = next(i for i in r.get("items", []) + if i["label"] == "succ") + resolved = self.server.resolve_completion(item) + self.assertIn("Nat", resolved.get("detail", ""), + f"resolved detail should carry the type; got {resolved!r}") + + def test_alias_resolves(self): + uri, _src, _ = self.open_text("qual3.lp", + "require test.simple as S;\n" + "symbol z : S.\n") + self.assertIn("Nat", _labels(_complete(self.server, uri, 1, 13))) + + def test_private_symbols_excluded(self): + uri, _src, _ = self.open_text("qual4.lp", + "require test.modifiers;\n" + "symbol z : test.modifiers.\n") + labels = _labels(_complete(self.server, uri, 1, 26)) + self.assertIn("inj", labels) + self.assertNotIn("priv", labels, + "private symbols must not be offered outside their module") + + def test_qualified_in_tactic_argument(self): + uri, _src, _ = self.open_text("qual6.lp", + "require test.simple;\n" + "symbol z : test.simple.Nat ≔\n" + "begin\n" + " apply test.simple.\n" + "end;\n") + labels = _labels(_complete(self.server, uri, 3, 20)) + self.assertIn("zero", labels, + "qualified completion should work in tactic arguments") + + def test_intermediate_segment_offered(self): + """`test.` in term position: `test` is not itself a module, + but loaded paths extend it — offer the next segment.""" + uri, _src, _ = self.open_text("qual5.lp", + "require test.simple;\n" + "symbol z : test.\n") + r = _complete(self.server, uri, 1, 16) + by_label = {i["label"]: i for i in r.get("items", [])} + self.assertIn("simple", by_label, + f"next path segment should be offered; " + f"got {sorted(by_label)[:10]}") + self.assertEqual(by_label["simple"].get("kind"), 9) # Module + + +class TestDotTrigger(LSPTestCase): + """A "."-triggered request outside the dot-aware contexts must + return no items (e.g. after a number), while normal invocation at + the same position still completes.""" + + def test_dot_trigger_outside_context_is_quiet(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _complete(self.server, uri, 5, 0, + context={"triggerKind": 2, "triggerCharacter": "."}) + self.assertEqual(r.get("items"), [], + "dot-trigger outside path/qualified contexts must be quiet") + + def test_invoked_at_same_position_completes(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + r = _complete(self.server, uri, 5, 0, + context={"triggerKind": 1}) + self.assertIn("double", _labels(r)) + + +class TestArgumentContexts(LSPTestCase): + """Focused completions in argument positions: notation kinds, + associativity sides, flag names and switches; hypotheses ranked + first in hypothesis-taking tactic arguments.""" + + def test_notation_arguments(self): + uri, _src, _ = self.open_text("arg1.lp", + "constant symbol Nat : TYPE;\nnotation Nat \n") + labels = _labels(_complete(self.server, uri, 1, 13)) + for kw in ("infix", "prefix", "postfix", "quantifier"): + self.assertIn(kw, labels, + f"{kw!r} should be offered after `notation `") + self.assertNotIn("Nat", labels, + "the notation-argument list should not offer symbols") + + def test_associativity_sides(self): + uri, _src, _ = self.open_text("arg2.lp", + "constant symbol Nat : TYPE;\nnotation Nat infix \n") + labels = _labels(_complete(self.server, uri, 1, 19)) + self.assertIn("left", labels) + self.assertIn("right", labels) + self.assertNotIn("infix", labels) + + def test_flag_names(self): + uri, _src, _ = self.open_text("arg3.lp", 'flag "\n') + labels = _labels(_complete(self.server, uri, 0, 6)) + self.assertIn("print_implicits", labels, + f"registered flags should be offered; got {sorted(labels)}") + self.assertIn("eta_equality", labels) + + def test_flag_switch(self): + uri, _src, _ = self.open_text("arg4.lp", + 'flag "print_implicits" \n') + labels = _labels(_complete(self.server, uri, 0, 23)) + self.assertEqual(labels, {"on", "off"}, + f"after the flag string, only on/off; got {sorted(labels)}") + + def test_hypotheses_ranked_first_in_tactic_args(self): + proof = ( + "constant symbol Nat : TYPE;\n" + "symbol triv : Nat → Nat ≔\n" + "begin\n" + " assume n;\n" + " apply n;\n" + "end;\n" + ) + uri, _src, _ = self.open_text("arg5.lp", proof) + # Cursor after " apply " (line 4, col 8). + r = _complete(self.server, uri, 4, 8) + n_item = next(i for i in r.get("items", []) + if i["label"] == "n") + self.assertTrue(n_item.get("sortText", "").startswith("0"), + f"hypothesis should rank first after `apply`; got {n_item!r}") + + def test_no_keywords_in_tactic_args(self): + """The argument of a tactic is a term position: offering + `have` (or any keyword) after `apply ` would be invalid.""" + proof = ( + "constant symbol Nat : TYPE;\n" + "symbol triv : Nat → Nat ≔\n" + "begin\n" + " assume n;\n" + " apply n;\n" + "end;\n" + ) + uri, _src, _ = self.open_text("arg6.lp", proof) + labels = _labels(_complete(self.server, uri, 4, 8)) + for kw in ("have", "apply", "admitted", "print"): + self.assertNotIn(kw, labels, + f"{kw!r} is not valid in a tactic argument") + self.assertIn("n", labels) + self.assertIn("triv", labels, + "in-scope symbols are valid tactic arguments") + + +class TestProofRegion(LSPTestCase): + """Being inside the command of a theorem is not being inside its + proof: tactics belong strictly between `begin` and `end`.""" + + THM = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol triv : Nat → Nat ≔\n" + "begin\n" + " assume n;\n" + " refine n;\n" + "end;\n" + ) + + def test_no_tactics_on_the_statement_line(self): + uri, _src, _ = self.open_text("region1.lp", self.THM) + # Line 2 is the statement (`symbol triv : Nat → Nat ≔`). + labels = _labels(_complete(self.server, uri, 2, 24)) + self.assertNotIn("refine", labels, + "the statement is not a proof position") + self.assertIn("zero", labels) + + def test_tactics_inside_the_script(self): + uri, _src, _ = self.open_text("region2.lp", self.THM) + labels = _labels(_complete(self.server, uri, 5, 2)) + self.assertIn("refine", labels) + + def test_new_line_above_a_proof_gets_keywords(self): + """Typing a new declaration above an existing proof: the doc + no longer parses and the stale node's span covers the cursor + line, but that line is before `begin` — command keywords, not + tactics.""" + uri, _src, _ = self.open_text("region3.lp", self.THM) + broken = self.THM.replace("symbol triv", "co\nsymbol triv", 1) + self.server.did_change(uri, broken, 2) + self.server.drain_notifications(timeout=5.0) + # Line 2 is the fresh "co" line. + labels = _labels(_complete(self.server, uri, 2, 2)) + self.assertIn("constant", labels, + "command keywords should be offered above the proof") + self.assertNotIn("refine", labels, + "tactics must not leak out of the proof script") + + +class TestModifierContext(LSPTestCase): + """After modifiers, only further modifiers and the declarations + they qualify are valid.""" + + def test_symbol_offered_after_modifier(self): + uri, _src, _ = self.open_text("mod1.lp", + "constant symbol Nat : TYPE;\nconstant \n") + r = _complete(self.server, uri, 1, 9) + by_label = {i["label"]: i for i in r.get("items", [])} + self.assertIn("symbol", by_label, + f"symbol should follow a modifier; got " + f"{sorted(by_label)[:10]}") + self.assertTrue( + by_label["symbol"]["sortText"].startswith("0"), + "symbol should rank first after a modifier") + self.assertIn("injective", by_label) + self.assertNotIn("constant", by_label, + "already-typed modifiers are not repeated") + self.assertNotIn("rule", by_label, + "rule cannot follow a modifier") + self.assertNotIn("Nat", by_label, + "a modifier position does not take terms") + + def test_private_offers_open_not_require(self): + uri, _src, _ = self.open_text("mod2.lp", "private \n") + labels = _labels(_complete(self.server, uri, 0, 8)) + for kw in ("symbol", "open", "protected"): + self.assertIn(kw, labels, + f"{kw!r} can follow `private`") + # `private` comes after `require`, not before: + # `require private open M;` vs `private open M;`. + self.assertNotIn("require", labels, + "`private require` does not parse") + + def test_associative_offers_sides_and_symbol(self): + uri, _src, _ = self.open_text("mod3.lp", + "commutative associative \n") + labels = _labels(_complete(self.server, uri, 0, 24)) + for kw in ("left", "right", "symbol"): + self.assertIn(kw, labels, + f"{kw!r} can follow `associative`") + + +class TestGrammarFollowSets(LSPTestCase): + """Keyword completions come from the parser's follow sets: what + the grammar accepts at the cursor, nothing else.""" + + def test_require_offers_open_private_and_paths(self): + uri, _src, _ = self.open_text("fol1.lp", "require \n") + labels = _labels(_complete(self.server, uri, 0, 8)) + for kw in ("open", "private"): + self.assertIn(kw, labels, f"{kw!r} can follow `require`") + self.assertIn("test.simple", labels, + "module paths complete after `require`") + self.assertNotIn("symbol", labels, + "`require symbol` does not parse") + + def test_require_path_offers_as(self): + uri, _src, _ = self.open_text("fol2.lp", + "require test.simple \n") + labels = _labels(_complete(self.server, uri, 0, 20)) + self.assertIn("as", labels, + "`require M as N;` aliases the module") + self.assertIn("test.inductive", labels, + "`require` takes several paths") + self.assertNotIn("open", labels, + "`open` only comes right after `require`") + + def test_require_alias_position_is_quiet(self): + """`require M as ` wants a fresh name: no keywords, + no symbols.""" + uri, _src, _ = self.open_text("fol3.lp", + "require test.simple as \n") + self.assertEqual(_labels(_complete(self.server, uri, 0, 23)), + set()) + + def test_require_private_offers_only_open(self): + uri, _src, _ = self.open_text("fol4.lp", "require private \n") + labels = _labels(_complete(self.server, uri, 0, 16)) + self.assertIn("open", labels) + self.assertNotIn("test.simple", labels, + "`require private` must be followed by `open`, not a path") + + def test_notation_offers_kinds(self): + uri, _src, _ = self.open_text("fol5.lp", + "constant symbol Nat : TYPE;\n" + "notation Nat \n") + labels = _labels(_complete(self.server, uri, 1, 13)) + for kw in ("infix", "prefix", "postfix", "quantifier"): + self.assertIn(kw, labels, f"{kw!r} can follow `notation f`") + self.assertNotIn("Nat", labels, + "a notation kind position does not take terms") + + def test_infix_offers_sides(self): + uri, _src, _ = self.open_text("fol6.lp", + "constant symbol Nat : TYPE;\n" + "notation Nat infix \n") + labels = _labels(_complete(self.server, uri, 1, 19)) + for kw in ("left", "right"): + self.assertIn(kw, labels, f"{kw!r} can follow `infix`") + + def test_flag_string_offers_switch(self): + uri, _src, _ = self.open_text("fol7.lp", + 'flag "eta_equality" \n') + labels = _labels(_complete(self.server, uri, 0, 20)) + self.assertIn("on", labels) + self.assertIn("off", labels) + + def test_simplify_offers_rule(self): + uri, _src, _ = self.open_text("fol8.lp", + "constant symbol P : TYPE;\n" + "constant symbol p : P;\n" + "symbol thm : P ≔\n" + "begin\n" + " simplify \n" + " refine p;\n" + "end;\n") + labels = _labels(_complete(self.server, uri, 4, 11)) + self.assertIn("rule", labels, + "`simplify rule off` disables rewrite rules") + self.assertIn("p", labels, + "`simplify f` takes a symbol") + self.assertNotIn("apply", labels, + "a tactic cannot follow `simplify` without a separator") + + def test_statement_type_offers_begin(self): + uri, _src, _ = self.open_text("fol9.lp", + "constant symbol P : TYPE;\n" + "symbol thm : P \n") + labels = _labels(_complete(self.server, uri, 1, 15)) + self.assertIn("begin", labels, + "a proof can start after the statement's type") + self.assertIn("P", labels, + "the type may also continue with more term") + self.assertNotIn("symbol", labels, + "a command cannot start before the previous one ends") + + def test_left_offers_associative(self): + uri, _src, _ = self.open_text("fol10.lp", "left \n") + labels = _labels(_complete(self.server, uri, 0, 5)) + self.assertEqual(labels, {"associative"}, + "`left` must be followed by `associative`") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_definition.py b/tests/lsp/test_definition.py new file mode 100644 index 000000000..f0d1b8294 --- /dev/null +++ b/tests/lsp/test_definition.py @@ -0,0 +1,204 @@ +"""Go-to-definition tests.""" + +import os +import unittest + +from .base import LSPTestCase, requires_stdlib + + +def _first_definition(result): + """Normalize the definition result to a single {uri, range} dict or None. + + LSP allows: null | Location | Location[] | LocationLink[].""" + if result is None: + return None + if isinstance(result, dict): + return result + if isinstance(result, list) and result: + return result[0] + return None + + +class TestDefinitionLocal(LSPTestCase): + """Go-to-def within a single file.""" + + def test_definition_of_local_symbol(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + # Jump from use of `zero` in `rule double zero ↪ zero` + line, col = src.find(r"rule double zero", "zero") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d, "definition should be non-null for local use") + self.assertEqual(d["uri"], uri, "local def should point to same URI") + # The declaration of `zero` is on line 1 (0-based). + decl_line, _ = src.find(r"constant symbol zero", "zero") + self.assertEqual(d["range"]["start"]["line"], decl_line) + + def test_definition_of_undefined_is_null(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + # Line 0, col 0 is the start of `constant` keyword — not a symbol. + result = self.server.definition(uri, 0, 0) + d = _first_definition(result) + self.assertIsNone(d, f"expected null def, got {d}") + + +class TestDefinitionUncheckedRegion(LSPTestCase): + """Go-to-definition falls back to the in-scope symbol table for + text the checker never reached (e.g. past a parse error).""" + + TEXT = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol ;\n" # parse error: no name + "symbol later : Nat;\n" # never parsed / checked + ) + + def test_definition_after_parse_error_uses_symbol_table(self): + uri, _src, diags = self.open_text("def_err.lp", self.TEXT) + self.assertTrue(self.errors(diags), + "fixture should produce a parse error") + col = self.TEXT.splitlines()[3].index("Nat") + d = _first_definition(self.server.definition(uri, 3, col)) + self.assertIsNotNone(d, + "definition should fall back to the in-scope symbol table") + self.assertEqual(d["uri"], uri) + self.assertEqual(d["range"]["start"]["line"], 0, + "should jump to the declaration of Nat on line 0") + + +@requires_stdlib +class TestDefinitionStdlib(LSPTestCase): + """Go-to-def on symbols defined in another file (stdlib).""" + + def test_definition_of_stdlib_symbol(self): + uri, _text, src, _ = self.open_fixture("imports.lp") + # Jump from `ℕ` in `symbol double : ℕ → ℕ;` + line, col = src.find(r"symbol double :", r"ℕ") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d, "stdlib go-to-def must not be null") + self.assertNotEqual(d["uri"], uri, + "stdlib def should point to another file") + self.assertTrue(d["uri"].endswith("Nat.lp"), + f"stdlib def should point to Nat.lp, got {d['uri']}") + # And the range must be plausible (not the line-1 fallback for all + # external symbols). + self.assertGreaterEqual(d["range"]["start"]["line"], 0) + + +class TestDefinitionModulePath(LSPTestCase): + """Go-to-definition on the module path of a require/open jumps to + the start of that module's file (no stdlib needed).""" + + MOD_A = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n") + + def test_go_to_def_on_local_required_module(self): + path_a = os.path.join(self.lib_root, "DefModA.lp") + with open(path_a, "w") as f: + f.write(self.MOD_A) + self.addCleanup(lambda: os.path.exists(path_a) and os.remove(path_a)) + uri, src, _ = self.open_text("DefModB.lp", + "require open test.DefModA;\n" + "symbol z : Nat ≔ zero;\n") + line, col = src.find(r"require open test\.DefModA", "DefModA") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d, "module-path go-to-def should resolve") + self.assertTrue(d["uri"].endswith("DefModA.lp"), + f"should resolve to DefModA.lp; got {d.get('uri')}") + self.assertEqual(d["range"]["start"]["line"], 0) + + +@requires_stdlib +class TestCrossFileDefinitionLine(LSPTestCase): + """Cross-file go-to-def must land on the actual declaration, not + fall back to line 0 / char 0 (a regression seen in live usage).""" + + def test_stdlib_nat_lands_on_declaration(self): + uri, _text, src, _ = self.open_fixture("imports.lp") + line, col = src.find(r"symbol double :", r"ℕ") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d) + self.assertTrue(d["uri"].endswith("Nat.lp")) + got_line = d["range"]["start"]["line"] + # We don't hardcode the actual declaration line (it shifts as + # stdlib evolves); just guard the line-1-fallback regression. + self.assertGreater(got_line, 1, + f"stdlib go-to-def landed on line {got_line} " + f"(regression of the line-1 fallback bug)") + + def test_user_module_lands_on_declaration(self): + mod_a = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "constant symbol succ : Nat → Nat;\n") + mod_b = ( + "require open test.ModA;\n" + "symbol two : Nat ≔ succ (succ zero);\n") + path_a = os.path.join(self.lib_root, "ModA.lp") + with open(path_a, "w") as f: + f.write(mod_a) + self.addCleanup(lambda: os.remove(path_a) + if os.path.exists(path_a) else None) + uri, src, _ = self.open_text("ModB.lp", mod_b) + # `succ` is declared on line 2 (0-based) of ModA.lp at col 16. + line, col = src.find(r"symbol two :", r"\bsucc\b") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d) + self.assertTrue(d["uri"].endswith("ModA.lp")) + r = d["range"]["start"] + self.assertEqual(r["line"], 2, + f"expected succ on line 2 of ModA.lp, got {r}") + # The pre-fix fallback always returned char 0. + self.assertGreater(r["character"], 0, + f"cross-file go-to-def fell back to char 0: {r}") + + +@requires_stdlib +class TestRequireOpenDefinition(LSPTestCase): + """Go-to-def on a module name in `require open` should navigate to + that module.""" + + def test_go_to_def_on_required_module(self): + uri, _text, src, _ = self.open_fixture("imports.lp") + # `Nat` in `require open Stdlib.Nat;` + line, col = src.find(r"require open Stdlib\.Nat", r"\bNat") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d, + "go-to-def on module in `require open` should resolve") + self.assertTrue(d["uri"].endswith("Nat.lp"), + f"should resolve to Nat.lp, got {d.get('uri')}") + + +@requires_stdlib +class TestDefinitionQualified(LSPTestCase): + """#1366 fix: find_sym resolves qualified names rather than the + short-name in_scope lookup.""" + + def test_qualified_name_resolves_to_qualified(self): + uri, _text, src, _ = self.open_fixture("qualified.lp") + # Hover on `ℕ` in `Stdlib.Nat.ℕ` — should resolve to the stdlib def. + line, col = src.find(r"symbol two : Stdlib", r"ℕ") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d, "qualified name should resolve") + self.assertTrue(d["uri"].endswith("Nat.lp"), + f"Stdlib.Nat.ℕ should resolve to Nat.lp, got {d['uri']}") + + def test_qualified_name_with_local_shadow(self): + """Even if a symbol with the same short name exists locally, + a qualified reference must resolve to the qualified target.""" + text = ( + "require Stdlib.Nat;\n" + "symbol ℕ : TYPE;\n" # local shadow + "symbol x : Stdlib.Nat.ℕ ≔ Stdlib.Nat.0;\n" + ) + uri, src, _ = self.open_text("shadow.lp", text) + line, col = src.find(r"symbol x : Stdlib", r"ℕ") + d = _first_definition(self.server.definition(uri, line, col)) + self.assertIsNotNone(d) + # The qualified reference should NOT resolve to the local ℕ. + self.assertTrue(d["uri"].endswith("Nat.lp"), + f"Stdlib.Nat.ℕ must resolve to stdlib, got {d['uri']}") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_diagnostics.py b/tests/lsp/test_diagnostics.py new file mode 100644 index 000000000..0e5906757 --- /dev/null +++ b/tests/lsp/test_diagnostics.py @@ -0,0 +1,93 @@ +"""Diagnostics: errors, positions, and hint ranges.""" + +import unittest + +from .base import LSPTestCase + + +class TestErrorDiagnostics(LSPTestCase): + + def test_single_error_at_correct_line(self): + _uri, _text, _src, diags = self.open_fixture("with_error.lp") + errs = self.errors(diags) + self.assertEqual(len(errs), 1, + f"expected 1 error, got {len(errs)}") + # Error is `symbol bad : Undefined;` on line 3 (0-based: 2). + self.assertEqual(errs[0]["range"]["start"]["line"], 2) + self.assertIn("Undefined", errs[0]["message"]) + + def test_error_range_does_not_crash_client(self): + _uri, _, _, diags = self.open_fixture("with_error.lp") + for d in diags: + r = d["range"] + # LSP requires 0-based, non-negative positions + self.assertGreaterEqual(r["start"]["line"], 0) + self.assertGreaterEqual(r["start"]["character"], 0) + self.assertGreaterEqual(r["end"]["line"], r["start"]["line"]) + + +class TestFocusedHints(LSPTestCase): + """OK hints should underline a focused span (roughly keyword-sized), + never the whole statement. (Keyword-anchored ranges are asserted + precisely by the tests accompanying #1444.)""" + + MAX_HINT_WIDTH = 30 # a "focused" hint shouldn't exceed this + + def test_hints_are_narrow(self): + _uri, _, _, diags = self.open_fixture("simple.lp") + hints = self.hints(diags) + self.assertGreater(len(hints), 0, + "simple.lp should emit OK hints") + too_wide = [] + for h in hints: + r = h["range"] + if r["start"]["line"] != r["end"]["line"]: + continue # skip multi-line ranges + width = r["end"]["character"] - r["start"]["character"] + if width > self.MAX_HINT_WIDTH: + too_wide.append((h.get("message"), width, r)) + self.assertFalse(too_wide, + f"{len(too_wide)}/{len(hints)} hints exceed {self.MAX_HINT_WIDTH} " + f"chars: {too_wide[:2]}") + + +class TestMultipleErrors(LSPTestCase): + + def test_errors_in_multiple_places(self): + _uri, _text, _src, diags = self.open_fixture("multiple_errors.lp") + errs = self.errors(diags) + # The LSP should report at least the first error; both is better. + self.assertGreaterEqual(len(errs), 1, + f"expected at least 1 error, got {len(errs)}") + # Errors should be sorted by position (ascending line). + for a, b in zip(errs, errs[1:]): + self.assertLessEqual(a["range"]["start"]["line"], + b["range"]["start"]["line"], + "errors should be in position order") + + +class TestTacticHintMessage(LSPTestCase): + """Every successful tactic emits a severity-4 hint with message 'OK', + matching upstream behaviour.""" + + @classmethod + def _has_stdlib(cls): + from .base import _opam_stdlib + return _opam_stdlib() is not None + + def test_hint_message_is_OK(self): + if not self._has_stdlib(): + self.skipTest("stdlib required") + _uri, _text, _src, diags = self.open_fixture("proof.lp") + hints_on_tactics = [ + d for d in self.hints(diags) + if d.get("message") and d["range"]["start"]["line"] > 0 + ] + ok_hints = [d for d in hints_on_tactics if d["message"] == "OK"] + self.assertGreater(len(ok_hints), 0, + f"expected at least one 'OK' hint; " + f"got {[d['message'] for d in hints_on_tactics]}") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_goals.py b/tests/lsp/test_goals.py new file mode 100644 index 000000000..a562abe90 --- /dev/null +++ b/tests/lsp/test_goals.py @@ -0,0 +1,62 @@ +"""proof/goals: the custom request that backs lp-goals / Zed's goal panel.""" + +import unittest + +from .base import LSPTestCase, requires_stdlib +from .client import LSPError + + +@requires_stdlib +class TestGoals(LSPTestCase): + + def test_goals_outside_proof_is_empty(self): + uri, _text, src, _ = self.open_fixture("proof.lp") + # Above any proof. + result = self.server.goals(uri, line=0, character=0) + goals = (result or {}).get("goals") or [] + self.assertEqual(goals, [], + f"outside any proof, expected no goals; got {goals}") + + def test_goals_inside_proof(self): + uri, _text, src, _ = self.open_fixture("proof.lp") + # Line after `begin` in zero_eq_zero; should have a goal. + begin_line, _ = src.find(r"^\s*reflexivity;", "reflexivity") + result = self.server.goals(uri, line=begin_line, character=0) + goals = (result or {}).get("goals") or [] + self.assertGreater(len(goals), 0, + f"inside proof, expected >=1 goal; got {goals}") + + def test_goals_after_tactic(self): + uri, _text, src, _ = self.open_fixture("proof.lp") + # After `assume x y h;` in eq_sym_nat there are still 1 goal, + # with 3 hypotheses in context. + line, _ = src.find(r"^\s*symmetry;", "symmetry") + result = self.server.goals(uri, line=line, character=0) + goals = (result or {}).get("goals") or [] + self.assertGreater(len(goals), 0, + "proof in progress should have >=1 goal") + # If hypotheses are exposed, they should include `h`. + hyps = goals[0].get("hyps") or goals[0].get("hypotheses") or [] + if hyps: + names = [h.get("name", h.get("hname", "")) for h in hyps] + self.assertIn("h", names, + f"expected `h` in hypotheses after `assume ... h`; got {names}") + + +class TestGoalsUriHandling(LSPTestCase): + """goals request should behave sensibly on unknown URIs.""" + + def test_goals_on_unopened_doc_does_not_crash(self): + # An error/null response is OK; a timeout (hang) is not. + try: + self.server.goals("file:///not-opened.lp", line=0, character=0) + except LSPError as e: + self.assertNotIn("timeout", str(e).lower(), + "server must reply to goals on an unknown URI, not hang") + # Server should still handle subsequent requests. + uri, _, _, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags) + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_hover.py b/tests/lsp/test_hover.py new file mode 100644 index 000000000..2df46f323 --- /dev/null +++ b/tests/lsp/test_hover.py @@ -0,0 +1,305 @@ +"""Hover tests.""" + +import unittest + +from .base import LSPTestCase, requires_stdlib + + +def _hover_text(result): + """Extract the hover markdown/text from a hover response.""" + if result is None: + return None + contents = result.get("contents") + if contents is None: + return None + if isinstance(contents, dict): + return contents.get("value", "") + if isinstance(contents, list): + return "\n".join( + c.get("value", c) if isinstance(c, dict) else str(c) + for c in contents) + return str(contents) + + +class TestHoverBasic(LSPTestCase): + """Hover works on uses of a symbol (the RangeMap tracks uses).""" + + def test_hover_on_use_of_symbol(self): + uri, _text, src, _diags = self.open_fixture("simple.lp") + # Use of `zero` in `rule double zero ↪ zero;` — its type is Nat. + line, col = src.find(r"rule double zero", "zero") + result = self.server.hover(uri, line, col) + text = _hover_text(result) + self.assertIsNotNone(text, "hover on use of zero should not be null") + # In either plain or rich mode, the type string "Nat" should appear. + self.assertIn("Nat", text) + + def test_hover_on_blank_position_returns_null(self): + uri, _text, _src, _diags = self.open_fixture("simple.lp") + # Col 8 of "constant symbol Nat : TYPE;" is the space between + # `constant` and `symbol` — no token there. + result = self.server.hover(uri, 0, 8) + self.assertIsNone(result, + f"hover on whitespace should be null; got {result!r}") + + +class TestHoverPlainString(LSPTestCase): + """Upstream-compatible hover: [contents] is a plain string carrying + the type of the hovered symbol. Guards against accidental markdown + divergence that VSCode/Emacs clients haven't had to handle.""" + + def test_contents_is_plain_string(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"rule double zero", "zero") + result = self.server.hover(uri, line, col) + self.assertIsNotNone(result) + contents = result.get("contents") + self.assertIsInstance(contents, str, + f"contents must be a plain string; " + f"got {type(contents).__name__}: {contents!r}") + + +class TestHoverTacticKeyword(LSPTestCase): + """Inside a proof, hovering a tactic keyword shows the tactic's + documentation; outside a proof, tactic names are not special.""" + + PROOF = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol triv : Nat → Nat ≔\n" + "begin\n" + " assume n;\n" + " refine n;\n" + "end;\n" + ) + + def test_hover_on_tactic_keyword_in_proof(self): + uri, _src, _ = self.open_text("prf.lp", self.PROOF) + # Line 5 is " refine n;" — cols 2..7 are `refine`. + text = _hover_text(self.server.hover(uri, 5, 3)) + self.assertIsNotNone(text, + "hover on a tactic keyword inside a proof should document it") + self.assertIn("goal", text, + f"tactic documentation should describe the tactic; got {text!r}") + + def test_hover_on_hypothesis_in_proof(self): + """After `assume n`, hovering the use of `n` should show its + type (hypotheses are proof-local: not symbols, not in the + identifier RangeMap).""" + uri, _src, _ = self.open_text("prf.lp", self.PROOF) + # Line 5 is " refine n;" — col 9 is `n`. + text = _hover_text(self.server.hover(uri, 5, 9)) + self.assertIsNotNone(text, + "hover on a hypothesis should show its type") + self.assertIn("Nat", text, + f"hypothesis `n` has type Nat; got {text!r}") + + +class TestHoverSameLineTactics(LSPTestCase): + """Hypothesis hovers work in every tactic of a line, not just the + first. Goal snapshots are anchored at each tactic's keyword and + record the state after it; when the tactic under the cursor closes + the proof, the fallback must step back to the snapshot before that + tactic — not to the start of the line, which with several tactics + on one line lands before the hypothesis was introduced.""" + + PROOF = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol triv : Nat → Nat ≔\n" + "begin\n" + " assume n; refine n;\n" + "end;\n" + ) + + def test_hover_on_hypothesis_in_second_tactic(self): + uri, src, _ = self.open_text("sameline.lp", self.PROOF) + # `n` in `refine n;` — the second tactic on the line, and the + # one that finishes the proof. (`refine` itself contains an + # `n`; the hypothesis use is the one followed by `;`.) + line, col = src.find(r"refine n", "n;") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, + "hover on a hypothesis used in the second tactic of a line " + "should show its type") + self.assertIn("Nat", text, + f"hypothesis `n` has type Nat; got {text!r}") + + def test_hover_on_hypothesis_in_first_tactic(self): + uri, src, _ = self.open_text("sameline2.lp", self.PROOF) + # `n` in `assume n;` — introduced by the tactic under the + # cursor (`assume` contains no `n`, so plain `n` finds it). + line, col = src.find(r"assume n", "n") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, + "hover on a hypothesis named in `assume` should show its type") + self.assertIn("Nat", text, + f"hypothesis `n` has type Nat; got {text!r}") + + +class TestHoverSubgoalClosingTactic(LSPTestCase): + """Hypothesis hovers resolve in the tactic's pre-application state. + Goal snapshots record the state *after* each tactic, so when the + tactic under the cursor closes the current subgoal while a sibling + goal remains, the snapshot at the cursor is the *next* goal's + context — which lacks the subproof-local hypotheses the tactic's + own arguments refer to.""" + + PROOF = ( + "constant symbol A : TYPE;\n" + "constant symbol B : TYPE;\n" + "constant symbol P : TYPE;\n" + "constant symbol mk : (A → A) → (B → B) → P;\n" + "symbol thm : P ≔\n" + "begin\n" + " apply mk\n" + " { assume ha; refine ha }\n" + " { assume hb; refine hb };\n" + "end;\n" + ) + + def test_hover_on_argument_of_subgoal_closing_tactic(self): + """`ha` in `refine ha`: the refine closes the first subgoal and + the second (`B → B`) is still open, with no `ha` in context.""" + uri, src, _ = self.open_text("subgoal.lp", self.PROOF) + line, col = src.find(r"refine ha", "ha") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, + "hover on a hypothesis used by a subgoal-closing tactic " + "should show its type from the pre-application state") + self.assertIn("A", text, + f"hypothesis `ha` has type A; got {text!r}") + + def test_hover_on_argument_of_proof_closing_tactic(self): + """`hb` in `refine hb`: the refine finishes the whole proof, so + the post-state has no goals at all.""" + uri, src, _ = self.open_text("subgoal2.lp", self.PROOF) + line, col = src.find(r"refine hb", "hb") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, + "hover on a hypothesis used by the proof-closing tactic " + "should show its type") + self.assertIn("B", text, + f"hypothesis `hb` has type B; got {text!r}") + + def test_hover_on_binder_of_assume(self): + """`ha` in `assume ha`: the name only exists in the tactic's + post-state, which must remain a fallback.""" + uri, src, _ = self.open_text("subgoal3.lp", self.PROOF) + line, col = src.find(r"assume ha", "ha") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, + "hover on the hypothesis bound by `assume` should show its type") + self.assertIn("A", text, + f"hypothesis `ha` has type A; got {text!r}") + + +class TestHoverMidEdit(LSPTestCase): + """Tactic docs and hypothesis hovers survive a mid-word edit that + breaks the parse (served from the last successfully parsed nodes).""" + + def test_tactic_hover_survives_broken_parse(self): + proof = TestHoverTacticKeyword.PROOF + uri, _src, _ = self.open_text("hovmid.lp", proof) + broken = proof.replace(" refine n;\n", " re\n refine n;\n") + self.server.did_change(uri, broken, 2) + self.server.drain_notifications(timeout=5.0) + # `assume` on line 4 sits before the edit point, so its stale + # position is exact. + text = _hover_text(self.server.hover(uri, 4, 3)) + self.assertIsNotNone(text, + "tactic hover should survive a broken parse") + self.assertIn("goal", text, + f"expected the `assume` documentation; got {text!r}") + + def test_hypothesis_hover_survives_broken_parse(self): + proof = TestHoverTacticKeyword.PROOF + uri, _src, _ = self.open_text("hovmid2.lp", proof) + # Mid-word edit after the refine line: earlier lines (and the + # goal snapshots recorded for them) keep their positions. + broken = proof.replace("end;\n", " re\nend;\n") + self.server.did_change(uri, broken, 2) + self.server.drain_notifications(timeout=5.0) + # `n` in the unshifted `refine n;` line (line 5, col 9). + text = _hover_text(self.server.hover(uri, 5, 9)) + self.assertIsNotNone(text, + "hypothesis hover should survive a broken parse") + self.assertIn("Nat", text, + f"hypothesis `n` has type Nat; got {text!r}") + + +class TestHoverCommandKeywords(LSPTestCase): + """Command keywords and symbol modifiers are documented on hover, + anywhere in a document.""" + + def test_hover_on_symbol_command(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"constant symbol Nat", "symbol") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, "hover on `symbol` should document it") + self.assertIn("Declares or defines", text) + + def test_hover_on_constant_modifier(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"constant symbol Nat", "constant") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, "hover on `constant` should document it") + self.assertIn("modifier", text) + + def test_hover_on_rule_command(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"^rule double", "rule") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, "hover on `rule` should document it") + self.assertIn("rewriting", text) + + def test_hover_on_settings_query(self): + text_lp = ( + "constant symbol Nat : TYPE;\n" + "flag \"print_implicits\" on;\n" + ) + uri, src, _ = self.open_text("settings.lp", text_lp) + line, col = src.find(r"^flag", "flag") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, "hover on `flag` should document it") + self.assertIn("Sets a flag", text) + + +class TestHoverUncheckedRegion(LSPTestCase): + """Hover falls back to the in-scope symbol table for text the + checker never reached (e.g. past a parse error), where the + RangeMap has no entries.""" + + TEXT = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + "symbol ;\n" # parse error: no name + "symbol later : Nat;\n" # never parsed / checked + ) + + def test_hover_after_parse_error_uses_symbol_table(self): + uri, _src, diags = self.open_text("hov_err.lp", self.TEXT) + self.assertTrue(self.errors(diags), + "fixture should produce a parse error") + # `Nat` on the last line is past the error: not in the RangeMap, + # but in scope from the checked prefix. + col = self.TEXT.splitlines()[3].index("Nat") + text = _hover_text(self.server.hover(uri, 3, col)) + self.assertIsNotNone(text, + "hover should fall back to the in-scope symbol table") + self.assertIn("TYPE", text) + + +class TestHoverStdlib(LSPTestCase): + + @requires_stdlib + def test_hover_on_stdlib_symbol(self): + uri, _text, src, _ = self.open_fixture("imports.lp") + line, col = src.find(r"symbol double :", r"ℕ") + text = _hover_text(self.server.hover(uri, line, col)) + self.assertIsNotNone(text, + "hover on stdlib type should return content, got null") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_incremental.py b/tests/lsp/test_incremental.py new file mode 100644 index 000000000..5d6776e70 --- /dev/null +++ b/tests/lsp/test_incremental.py @@ -0,0 +1,87 @@ +"""Incremental checking: didChange and position shifting.""" + +import unittest + +from .base import LSPTestCase + + +class TestIncrementalEdit(LSPTestCase): + + def test_edit_clean_file_stays_clean(self): + uri, text, _src, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags) + # Insert a blank line at the top. + new_text = "\n" + text + self.server.did_change(uri, new_text, 2) + notifs = self.server.drain_notifications(timeout=5.0) + new_diags = self.server.extract_diagnostics(notifs, uri=uri) + self.assertNoErrors(new_diags, "after inserting blank line") + + def test_edit_introduces_error(self): + uri, text, _src, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags) + new_text = text + "\nsymbol bad : Undefined;\n" + self.server.did_change(uri, new_text, 2) + notifs = self.server.drain_notifications(timeout=5.0) + new_diags = self.server.extract_diagnostics(notifs, uri=uri) + errs = self.errors(new_diags) + self.assertGreater(len(errs), 0, + "error introduced by edit should produce a diagnostic") + self.assertIn("Undefined", errs[0]["message"]) + + def test_edit_fixes_error(self): + uri, text, _src, diags = self.open_fixture("with_error.lp") + self.assertGreater(len(self.errors(diags)), 0) + # Replace the body with a clean version. + new_text = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + ) + self.server.did_change(uri, new_text, 2) + notifs = self.server.drain_notifications(timeout=5.0) + new_diags = self.server.extract_diagnostics(notifs, uri=uri) + self.assertNoErrors(new_diags, + "errors should clear after fixing the source") + + +class TestPositionShifting(LSPTestCase): + """When content is inserted above existing code, positions must shift + correctly — both for diagnostic ranges and goals.""" + + def test_diagnostic_position_shifts_on_insert(self): + uri, text, _src, diags = self.open_fixture("with_error.lp") + err_line = self.errors(diags)[0]["range"]["start"]["line"] + # Insert two blank lines above. + new_text = "\n\n" + text + self.server.did_change(uri, new_text, 2) + notifs = self.server.drain_notifications(timeout=5.0) + new_errs = self.errors( + self.server.extract_diagnostics(notifs, uri=uri)) + self.assertGreater(len(new_errs), 0) + self.assertEqual(new_errs[0]["range"]["start"]["line"], + err_line + 2, + "error line should shift by +2 after inserting 2 lines") + + def test_column_shifts_when_line_gets_leading_whitespace(self): + """Inserting whitespace at the start of a line should shift the + diagnostic's column, not just its line number.""" + uri, text, _src, diags = self.open_fixture("with_error.lp") + orig_err = self.errors(diags)[0] + # Insert 4 spaces at the start of the error line. + lines = text.split("\n") + err_line = orig_err["range"]["start"]["line"] + lines[err_line] = " " + lines[err_line] + new_text = "\n".join(lines) + self.server.did_change(uri, new_text, 2) + notifs = self.server.drain_notifications(timeout=5.0) + new_errs = self.errors( + self.server.extract_diagnostics(notifs, uri=uri)) + self.assertGreater(len(new_errs), 0) + self.assertEqual( + new_errs[0]["range"]["start"]["character"], + orig_err["range"]["start"]["character"] + 4, + "column should shift by +4 after inserting whitespace") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_invariants.py b/tests/lsp/test_invariants.py new file mode 100644 index 000000000..54be06bf6 --- /dev/null +++ b/tests/lsp/test_invariants.py @@ -0,0 +1,381 @@ +"""Invariant tests: properties that should always hold. + +These tests are written to find bugs, not confirm known behavior. Each test +asserts a property that should hold across many inputs; a failure likely +indicates a real defect. +""" + +import re +import unittest + +from .base import LSPTestCase, requires_stdlib + + +def _valid_range(r): + """Return (ok, reason) for a well-formed LSP range.""" + s, e = r.get("start") or {}, r.get("end") or {} + sl, sc = s.get("line", -1), s.get("character", -1) + el, ec = e.get("line", -1), e.get("character", -1) + if sl < 0 or sc < 0 or el < 0 or ec < 0: + return False, f"negative coordinate in {r}" + if (sl, sc) > (el, ec): + return False, f"start > end in {r}" + return True, "" + + +def _range_within_text(r, text): + lines = text.split("\n") + el = r["end"]["line"] + if el >= len(lines): + return False, f"end line {el} past file ({len(lines)} lines)" + # Allow end.character == len(line) (LSP permits this). + if r["end"]["character"] > len(lines[el]) + 1: + return False, ( + f"end.char {r['end']['character']} past line len " + f"{len(lines[el])}") + return True, "" + + +def _all_identifier_positions(src): + """Yield (line, col) for every Unicode/ASCII identifier-like token.""" + ident = re.compile(r"[A-Za-z_ℕ\u03b1-\u03c9][A-Za-z0-9_\u03b1-\u03c9]*") + for lineno, line in enumerate(src.lines): + for m in ident.finditer(line): + yield lineno, m.start() + + +class TestRangeValidity(LSPTestCase): + """Every LSP range we ever receive must be well-formed.""" + + def _check_all_ranges(self, payloads, text, label): + """[payloads] is a list of dicts that may contain "range" keys.""" + bad = [] + def walk(obj, path): + if isinstance(obj, dict): + if "range" in obj and isinstance(obj["range"], dict): + ok, why = _valid_range(obj["range"]) + if not ok: + bad.append((path + ".range", why)) + else: + ok, why = _range_within_text(obj["range"], text) + if not ok: + bad.append((path + ".range", why)) + for k, v in obj.items(): + walk(v, f"{path}.{k}") + elif isinstance(obj, list): + for i, v in enumerate(obj): + walk(v, f"{path}[{i}]") + for i, p in enumerate(payloads): + walk(p, f"{label}[{i}]") + self.assertFalse(bad, + f"malformed ranges: {bad[:5]}{' ...' if len(bad) > 5 else ''}") + + def test_diagnostics_have_valid_ranges(self): + _uri, text, _, diags = self.open_fixture("simple.lp") + self._check_all_ranges(diags, text, "simple.lp") + _uri, text, _, diags = self.open_fixture("with_error.lp") + self._check_all_ranges(diags, text, "with_error.lp") + _uri, text, _, diags = self.open_fixture("multiple_errors.lp") + self._check_all_ranges(diags, text, "multiple_errors.lp") + _uri, text, _, diags = self.open_fixture("modifiers.lp") + self._check_all_ranges(diags, text, "modifiers.lp") + + def test_hover_ranges_valid_on_every_identifier(self): + """Hover on every identifier-like position; any returned range + must be well-formed. Bugs in position synthesis show up here.""" + uri, text, src, _ = self.open_fixture("simple.lp") + responses = [] + for line, col in _all_identifier_positions(src): + r = self.server.hover(uri, line, col) + if r is not None and "range" in r: + responses.append(r) + self._check_all_ranges(responses, text, "hover responses") + + def test_document_symbol_ranges_valid(self): + uri, text, _, _ = self.open_fixture("modifiers.lp") + syms = self.server.document_symbol(uri) or [] + # mk_syminfo wraps the range inside "location", so flatten. + flat = [{"range": s.get("location", {}).get("range")} + for s in syms if s.get("location")] + self._check_all_ranges(flat, text, "documentSymbol") + + +class TestIncrementalConsistency(LSPTestCase): + """Re-introducing identical source should produce identical diagnostics.""" + + def test_reintroduced_error_matches_original(self): + uri, error_text, _, diags0 = self.open_fixture("with_error.lp") + errs0 = self.errors(diags0) + self.assertEqual(len(errs0), 1) + r0 = errs0[0]["range"] + + # Fix: remove the bad line. + clean = error_text.replace( + "symbol bad : Undefined;\n", "") + self.server.did_change(uri, clean, 2) + self.server.drain_notifications(timeout=5.0) + + # Re-introduce the exact same text. + self.server.did_change(uri, error_text, 3) + new_diags = self.server.extract_diagnostics( + self.server.drain_notifications(timeout=5.0), uri=uri) + errs1 = self.errors(new_diags) + self.assertEqual(len(errs1), 1, + f"after reintroducing error, expected 1, got {len(errs1)}") + r1 = errs1[0]["range"] + self.assertEqual((r0["start"], r0["end"]), (r1["start"], r1["end"]), + "re-introduced identical error should have identical range") + + +class TestDocumentSymbolCompleteness(LSPTestCase): + """Every `symbol X` declaration in the source should appear in + documentSymbol (modulo the ones without sym_pos, e.g. ghost).""" + + def test_all_declared_symbols_listed(self): + uri, text, _src, _ = self.open_fixture("simple.lp") + # Names declared via `constant symbol X` / `symbol X`. + decl = re.findall(r"(?:^|\s)symbol\s+(\w+)", text, re.M) + syms = self.server.document_symbol(uri) or [] + names = {s.get("name") for s in syms} + missing = [d for d in decl if d not in names] + self.assertFalse(missing, + f"declared but missing from documentSymbol: {missing}; " + f"got {sorted(names)}") + + def test_modifiers_file_completeness(self): + uri, text, _, _ = self.open_fixture("modifiers.lp") + decl = re.findall(r"(?:^|\s)symbol\s+(\w+)", text, re.M) + syms = self.server.document_symbol(uri) or [] + names = {s.get("name") for s in syms} + missing = [d for d in decl if d not in names] + self.assertFalse(missing, + f"modifiers.lp: missing {missing}; got {sorted(names)}") + + +@requires_stdlib +class TestGoalsContinuity(LSPTestCase): + """Throughout an in-progress proof, proof/goals must return goals.""" + + def test_goals_nonempty_at_every_line_mid_proof(self): + uri, text, src, _ = self.open_fixture("proof.lp") + # Find the begin/end lines for the second (multi-tactic) proof. + begin_line = None + end_line = None + for i, line in enumerate(src.lines): + if "eq_sym_nat" in line: + # Next `begin` after this is our target. + for j in range(i, len(src.lines)): + if src.lines[j].strip() == "begin": + begin_line = j + break + break + self.assertIsNotNone(begin_line) + for j in range(begin_line + 1, len(src.lines)): + if src.lines[j].strip() == "end;": + end_line = j + break + self.assertIsNotNone(end_line) + + # Each non-blank, non-`end` line between begin and end should + # report at least one goal. + empty_lines = [] + for line in range(begin_line + 1, end_line): + stripped = src.lines[line].strip() + if not stripped or stripped.startswith("(*"): + continue + result = self.server.goals(uri, line=line, character=0) + goals = (result or {}).get("goals") or [] + if not goals: + empty_lines.append(line) + self.assertFalse(empty_lines, + f"mid-proof lines with no goals: {empty_lines}") + + +class TestSequentialStability(LSPTestCase): + """Repeated identical requests should return identical results. + + If any stateful (Timed) side-effect leaks, we'll see drift.""" + + def test_repeated_hover_stable(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"symbol zero : Nat", "Nat") + first = self.server.hover(uri, line, col) + for _ in range(5): + again = self.server.hover(uri, line, col) + self.assertEqual(again, first, + "hover result drifted between identical calls") + + def test_repeated_definition_stable(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"rule double zero", "zero") + first = self.server.definition(uri, line, col) + for _ in range(5): + again = self.server.definition(uri, line, col) + self.assertEqual(again, first, + "definition result drifted between identical calls") + + +class TestNonStandardMode(LSPTestCase): + """When standard_lsp is OFF, diagnostics carry embedded goal_info. + + This is the mode the Zed extension and lp-goals rely on; it's + completely untested otherwise.""" + + standard_lsp = False + + @requires_stdlib + def test_diagnostics_embed_goal_info_in_proofs(self): + _uri, _text, _src, diags = self.open_fixture("proof.lp") + # At least one diagnostic inside a proof should carry goal_info. + with_goals = [d for d in diags if "goal_info" in d] + self.assertGreater(len(with_goals), 0, + "non-standard mode should embed goal_info on proof diagnostics") + + def test_simple_file_still_works(self): + _uri, _text, _src, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags) + + +class TestStandardModeNoGoalInfo(LSPTestCase): + """The dual of [TestNonStandardMode]: with [--standard-lsp] on (our + default), the non-standard [goal_info] extension must NOT leak into + diagnostics, or strict LSP clients will choke.""" + + standard_lsp = True + + @requires_stdlib + def test_proof_diagnostics_have_no_goal_info(self): + _uri, _text, _src, diags = self.open_fixture("proof.lp") + leaked = [d for d in diags if "goal_info" in d] + self.assertFalse(leaked, + f"standard mode must not emit goal_info; leaked {len(leaked)}") + + +class TestBoundaryPositions(LSPTestCase): + """Hovering / jumping at boundary positions must not hang or crash.""" + + def test_hover_past_end_of_line(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + # First line: "constant symbol Nat : TYPE;" — hover way past it. + result = self.server.hover(uri, 0, 1000) + # Must return (null or well-formed); must not hang. + if result is not None and "range" in result: + ok, why = _valid_range(result["range"]) + self.assertTrue(ok, f"bad range: {why}") + + def test_hover_past_last_line(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + result = self.server.hover(uri, 10000, 0) + if result is not None and "range" in result: + ok, why = _valid_range(result["range"]) + self.assertTrue(ok, f"bad range: {why}") + + def test_definition_past_end_of_line(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + # Must return null / not crash. + self.server.definition(uri, 0, 1000) + self.server.definition(uri, 10000, 0) + + def test_hover_at_exact_line_end(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + for lineno, line in enumerate(src.lines): + if not line: + continue + result = self.server.hover(uri, lineno, len(line)) + if result is not None and "range" in result: + ok, why = _valid_range(result["range"]) + self.assertTrue(ok, f"line {lineno}: {why}") + + +class TestErrorRecovery(LSPTestCase): + """Server must remain responsive after errors — no hangs, no crashes.""" + + def test_hover_on_error_bearing_symbol(self): + uri, _text, src, diags = self.open_fixture("with_error.lp") + # There's an error on `symbol bad : Undefined;`. Hover on each + # identifier in that line should either null-out or return a + # well-formed response. + err_line, _ = src.find(r"symbol bad : Undefined", "bad") + for col in range(len(src.lines[err_line])): + result = self.server.hover(uri, err_line, col) + if result is not None and "range" in result: + ok, why = _valid_range(result["range"]) + self.assertTrue(ok, + f"col {col} on error line: {why}") + + def test_rapid_didChange_converges(self): + """The final diagnostics must match the final text, however many + changes were queued up in between.""" + uri, text, _src, _ = self.open_fixture("simple.lp") + clean = text + broken = text + "\nsymbol bad : Undefined;\n" + # Flip-flop many times, no reads in between: v=2,4,… broken, + # v=3,5,… clean; the last change (v=9) is clean. + for v in range(2, 10): + self.server.did_change(uri, broken if v % 2 == 0 else clean, v) + final_diags = self.server.extract_diagnostics( + self.server.drain_notifications(timeout=5.0), uri=uri) + self.assertNoErrors(final_diags, + "after rapid-fire flips ending clean, errors remain") + + +class TestMultibyteColumns(LSPTestCase): + """LSP positions are counted in UTF-16 code units (spec default). For + BMP-only content this coincides with Python codepoint indices, so we + can send a codepoint column and expect the server to agree — as long + as it does NOT interpret columns as UTF-8 byte offsets.""" + + def test_hover_on_symbol_after_non_ascii_idents(self): + uri, _text, src, _ = self.open_fixture("unicode_cols.lp") + # In `symbol x : α ≔ β;`, β is at codepoint col 15 but byte col 18. + # Asking for hover at col 15 must land on β, not inside ≔. + line, col = src.find(r"symbol x :", r"β") + result = self.server.hover(uri, line, col) + contents = (result or {}).get("contents") + text = contents.get("value") if isinstance(contents, dict) \ + else contents if isinstance(contents, str) else "" + self.assertIsNotNone(result, + "hover at codepoint col of β should return a result") + # β : α — the type "α" should appear in the hover text. + self.assertIn("α", text or "", + f"hover text should mention α (β's type); got {text!r}") + + def test_definition_on_symbol_after_non_ascii_idents(self): + uri, _text, src, _ = self.open_fixture("unicode_cols.lp") + line, col = src.find(r"symbol x :", r"β") + d = self.server.definition(uri, line, col) + if isinstance(d, list): + d = d[0] if d else None + self.assertIsNotNone(d, + "go-to-def on β (after multibyte prefix) should resolve") + self.assertEqual(d["range"]["start"]["line"], 1, + f"β declared on line 1 of unicode_cols.lp; got {d!r}") + + +class TestSymPosAbsent(LSPTestCase): + """Symbols without sym_pos (ghost symbols) must not crash go-to-def.""" + + def test_definition_on_unif_rule_symbol(self): + """Hover on a built-in/ghost symbol should return null, not crash.""" + text = ( + "constant symbol Nat : TYPE;\n" + "constant symbol zero : Nat;\n" + # Implicit uses of ghost equivs can appear during unification; + # we can't easily force a ghost in user source, but we CAN + # exercise the null-handling path by asking for a def on a + # non-symbol position. + "symbol x : Nat ≔ zero;\n" + ) + uri, src, _ = self.open_text("ghostprobe.lp", text) + # Position on the `≔` character — not a symbol identifier. + line, _ = src.find(r"symbol x") + col = src.lines[line].index("≔") + # Must return (null / empty / well-formed) without hanging. + result = self.server.definition(uri, line, col) + if result is not None and isinstance(result, dict) and "range" in result: + ok, why = _valid_range(result["range"]) + self.assertTrue(ok, f"bad range: {why}") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_lifecycle.py b/tests/lsp/test_lifecycle.py new file mode 100644 index 000000000..24f890241 --- /dev/null +++ b/tests/lsp/test_lifecycle.py @@ -0,0 +1,214 @@ +"""Basic LSP lifecycle tests: initialize, document open/close, shutdown.""" + +import time +import unittest + +from .base import LSPTestCase, _lambdapi_binary, stdlib_map_dir +from .client import LSPServer + + +def _server_with_stdlib(lib_root): + map_dirs = [md for md in [stdlib_map_dir()] if md] + return LSPServer(lib_root=lib_root, map_dirs=map_dirs, + standard_lsp=True, binary=_lambdapi_binary()) + + +class TestInitialize(LSPTestCase): + """Tests that want to drive [initialize] themselves. + + [LSPTestCase.setUp] already performs [initialize] so post-init tests can + just [open_fixture]. These tests need the un-initialized server, so they + replace setUp entirely (no [super().setUp()] call).""" + + def setUp(self): + self.server = _server_with_stdlib(self.lib_root) + self.server.start() + self.addCleanup(self.server.stop) + + def test_returns_capabilities(self): + result = self.server.initialize() + self.assertIn("capabilities", result) + caps = result["capabilities"] + self.assertEqual(caps.get("textDocumentSync"), 1) + self.assertTrue(caps.get("documentSymbolProvider")) + self.assertTrue(caps.get("hoverProvider")) + self.assertTrue(caps.get("definitionProvider")) + comp = caps.get("completionProvider") or {} + self.assertTrue(comp.get("resolveProvider")) + self.assertEqual(comp.get("triggerCharacters"), ["."], + '"." triggers module-path and qualified-name completion') + + def test_initialize_with_root_uri(self): + result = self.server.initialize( + root_uri=f"file://{self.lib_root}") + self.assertIn("capabilities", result) + + def test_initialize_with_rooturi_and_matching_folder(self): + """Zed (like many clients) sends BOTH [rootUri] and + [workspaceFolders] for the same directory. Applying the package + config twice used to abort initialize with "Module path [...] + is already mapped." — the client then killed the server and + retried in a loop.""" + params = { + "capabilities": {}, + "rootUri": f"file://{self.lib_root}", + "workspaceFolders": [ + {"uri": f"file://{self.lib_root}", "name": "test"}, + ], + } + result = self.server.request("initialize", params) + self.server.notify("initialized", {}) + self.assertIsNotNone(result, + "initialize must succeed with duplicated root/folder") + self.assertIn("capabilities", result) + # And the workspace still works. + uri, _, _, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags, "open after duplicated-folder init") + + def test_initialize_with_workspace_folders(self): + """When the client provides [workspaceFolders] instead of (or in + addition to) [rootUri], each folder's package config must still + be applied — otherwise module resolution silently breaks.""" + params = { + "capabilities": {}, + "workspaceFolders": [ + {"uri": f"file://{self.lib_root}", "name": "test"}, + ], + } + result = self.server.request("initialize", params) + self.server.notify("initialized", {}) + self.assertIn("capabilities", result) + # Prove the folder actually took effect: opening a fixture that + # references other fixtures in this root should check cleanly. + uri, _, _, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags, "open after workspaceFolders init") + + +class TestDocumentLifecycle(LSPTestCase): + """didOpen / didChange / didClose sequence on a clean document.""" + + def test_did_open_clean_document(self): + uri, _text, _src, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags, "simple.lp") + syms = self.server.document_symbol(uri) + self.assertIsNotNone(syms) + + def test_did_close_then_server_still_alive(self): + uri, _, _, _ = self.open_fixture("simple.lp") + self.server.did_close(uri) + # Open another doc to confirm the server is still responsive. + uri2, _, _, _ = self.open_fixture("modifiers.lp") + syms = self.server.document_symbol(uri2) + self.assertIsNotNone(syms) + + def test_multiple_documents(self): + uri1, _, _, d1 = self.open_fixture("simple.lp") + uri2, _, _, d2 = self.open_fixture("modifiers.lp") + self.assertNoErrors(d1) + self.assertNoErrors(d2) + self.assertIsNotNone(self.server.document_symbol(uri1)) + self.assertIsNotNone(self.server.document_symbol(uri2)) + + +class TestUnknownMethod(LSPTestCase): + """Unknown methods should not crash the server.""" + + def test_unknown_notification_ignored(self): + self.server.notify("workspace/someUnknownMethod", {}) + # Server still alive afterwards. + uri, _, _, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags) + + +class TestStringRequestIds(LSPTestCase): + """JSON-RPC request ids may be strings, not just integers; the + server must echo them back verbatim instead of failing silently.""" + + def test_hover_with_string_id_is_answered(self): + uri, _text, src, _ = self.open_fixture("simple.lp") + line, col = src.find(r"rule double zero", "zero") + msg = self.server.request_with_id( + "hover-1", "textDocument/hover", { + "textDocument": {"uri": uri}, + "position": {"line": line, "character": col}}) + self.assertEqual(msg.get("id"), "hover-1", + f"reply must echo the string id verbatim; got {msg!r}") + self.assertIn("result", msg) + + def test_unknown_method_with_string_id_gets_error_reply(self): + msg = self.server.request_with_id( + "nope-1", "workspace/doesNotExist", {}) + self.assertEqual(msg.get("id"), "nope-1") + self.assertEqual(msg.get("error", {}).get("code"), -32601, + f"expected MethodNotFound; got {msg!r}") + + +class TestShutdownExit(LSPTestCase): + """shutdown replies null; exit terminates the process.""" + + def test_shutdown_then_exit_terminates_process(self): + # [shutdown] returns null and then [exit] tears the server down. + self.server.request("shutdown") + self.server.notify("exit") + # Give the process a moment to wind down. + for _ in range(20): + if self.server._proc.poll() is not None: + break + time.sleep(0.05) + self.assertIsNotNone(self.server._proc.poll(), + "server should exit after `exit` notification") + self.assertEqual(self.server._proc.returncode, 0, + f"expected clean exit; got {self.server._proc.returncode}") + + +class TestStdinEOF(LSPTestCase): + """A client that dies without sending [exit] closes the server's + stdin. The server must terminate on EOF, never linger or spin.""" + + def test_stdin_eof_terminates_process(self): + # Open a document first so EOF can also land while the server + # is busy checking, not only while blocked reading. + uri = self.fixture_uri("simple.lp") + with open(self.fixture_path("simple.lp")) as f: + self.server.did_open(uri, f.read()) + self.server._proc.stdin.close() + for _ in range(100): + if self.server._proc.poll() is not None: + break + time.sleep(0.05) + self.assertIsNotNone(self.server._proc.poll(), + "server should terminate when its stdin reaches EOF") + + +class TestServerUnknownRequest(LSPTestCase): + """Unknown requests must receive a JSON-RPC MethodNotFound reply so + strict LSP clients don't block waiting for a response.""" + + def test_unknown_request_method_not_found(self): + from .client import LSPError + with self.assertRaises(LSPError) as ctx: + self.server.request("workspace/doesNotExist", {}) + msg = str(ctx.exception) + self.assertNotIn("timeout", msg.lower(), + f"server should reply with error, not time out: {msg}") + self.assertIn("Method not found", msg, + f"expected MethodNotFound message; got {msg}") + # Server is still alive after rejecting an unknown method. + uri, _, _, diags = self.open_fixture("simple.lp") + self.assertNoErrors(diags) + + def test_unknown_notification_no_reply(self): + """Notifications (no id) must NOT get a reply — sending one back + would confuse clients that track pending ids.""" + self.server.notify("workspace/doesNotExist", {}) + # Give the server a moment; any reply would be queued as a + # notification because we never registered an id. + notifs = self.server.drain_notifications(timeout=0.3) + # Filter: nothing should have flowed back for that method. + bad = [n for n in notifs if n.get("method") is None] + self.assertFalse(bad, + f"notifications should get no reply; got {bad}") + + +if __name__ == "__main__": + unittest.main() diff --git a/tests/lsp/test_symbols.py b/tests/lsp/test_symbols.py new file mode 100644 index 000000000..fec335d6c --- /dev/null +++ b/tests/lsp/test_symbols.py @@ -0,0 +1,104 @@ +"""documentSymbol: list of symbols declared in a document.""" + +import unittest + +from .base import LSPTestCase + + +class TestDocumentSymbol(LSPTestCase): + + def test_symbols_listed_for_simple_doc(self): + uri, _text, _src, _ = self.open_fixture("simple.lp") + syms = self.server.document_symbol(uri) + self.assertIsInstance(syms, list) + self.assertGreater(len(syms), 0, + "simple.lp declares symbols; documentSymbol should list them") + names = [s.get("name") for s in syms] + for expected in ("Nat", "zero", "succ", "double"): + self.assertIn(expected, names, + f"{expected!r} should appear in documentSymbol result") + + def test_symbol_kind_is_numeric(self): + uri, _, _, _ = self.open_fixture("simple.lp") + syms = self.server.document_symbol(uri) + for s in syms: + self.assertIn("kind", s) + self.assertIsInstance(s["kind"], int) + + def test_symbols_have_locations(self): + uri, _, _, _ = self.open_fixture("simple.lp") + syms = self.server.document_symbol(uri) + for s in syms: + loc = s.get("location") or {} + self.assertIn("uri", loc) + self.assertIn("range", loc) + r = loc["range"] + self.assertGreaterEqual(r["start"]["line"], 0) + + def test_modifiers_file_lists_all_symbols(self): + uri, _, _, _ = self.open_fixture("modifiers.lp") + syms = self.server.document_symbol(uri) + names = [s.get("name") for s in syms] + for expected in ("Nat", "zero", "inj", "priv", "prot", "seq", "op"): + self.assertIn(expected, names, + f"{expected!r} missing from documentSymbol on modifiers.lp") + + +class TestHierarchicalDocumentSymbol(LSPTestCase): + """When the client advertises [hierarchicalDocumentSymbolSupport], + the server must return [DocumentSymbol[]] (objects with [range] + + [selectionRange] + [children]) instead of the legacy flat + [SymbolInformation[]] (objects with [location]).""" + + advertise_hierarchical_symbols = True + + def test_inductive_has_constructors_as_children(self): + uri, _, _, _ = self.open_fixture("inductive.lp") + syms = self.server.document_symbol(uri) + self.assertIsInstance(syms, list) + # Hierarchical shape: every symbol has [range] / [selectionRange], + # and the inductive type carries its constructors as children. + for s in syms: + self.assertIn("range", s, + f"hierarchical DocumentSymbol must have [range]; got {s!r}") + self.assertIn("selectionRange", s, + f"hierarchical DocumentSymbol must have [selectionRange]; " + f"got {s!r}") + self.assertNotIn("location", s, + f"hierarchical mode shouldn't emit legacy [location]; " + f"got {s!r}") + by_name = {s["name"]: s for s in syms} + tree = by_name.get("Tree") + self.assertIsNotNone(tree, f"expected 'Tree' in outline; got {syms}") + children = tree.get("children", []) + child_names = [c["name"] for c in children] + self.assertEqual(child_names, ["leaf", "node"], + f"Tree's constructors should appear as children in order; " + f"got {child_names}") + for c in children: + self.assertEqual(c["kind"], 22, # EnumMember + f"constructor should have kind EnumMember (22); got {c!r}") + + def test_top_level_symbol_has_no_children(self): + uri, _, _, _ = self.open_fixture("inductive.lp") + syms = self.server.document_symbol(uri) + bool_sym = next((s for s in syms if s["name"] == "Bool"), None) + self.assertIsNotNone(bool_sym) + self.assertEqual(bool_sym.get("children", []), []) + + def test_symbols_share_one_kind(self): + """No LSP SymbolKind matches lambdapi's notions, so `symbol` + entries are not classified: they all carry the same kind. + Inductive types keep the structural Enum/EnumMember shape.""" + uri, _, _, _ = self.open_fixture("inductive.lp") + syms = self.server.document_symbol(uri) + kinds = {s["name"]: s["kind"] for s in syms} + self.assertEqual(kinds.get("Bool"), kinds.get("height"), + f"symbols should not be classified; got {kinds}") + self.assertEqual(kinds.get("height"), kinds.get("mirror"), + f"symbols should not be classified; got {kinds}") + self.assertEqual(kinds.get("Tree"), 10) + + +if __name__ == "__main__": + unittest.main() From f235ea53b5756d91dab3966042b8859ac2b559d2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 21:19:13 +0200 Subject: [PATCH 14/14] add CHANGES.md entry --- CHANGES.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 2b1b61b39..23e418c4d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -22,6 +22,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). - Tactic `#print` to print a symbol or the current goal. - Export to Lean. - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls. +- LSP server: completion (in-scope symbols; command keywords with snippets; inside proofs, documented tactic keywords and the local symbols introduced by `assume`), documentation on hover for tactics, command keywords and modifiers, hover on `assume`-introduced local symbols showing their types, hierarchical document symbols, go-to-definition on `require`/`open` module paths, hover/go-to-definition fallback to in-scope symbols in unchecked regions, and an integration test suite (`make test_lsp`). +- LSP server: context-aware completion, with `.` as a trigger character: module paths after `require`/`open`, qualified identifiers (symbols of the required module, resolving `require as` aliases), notation/associativity/flag arguments, and hypothesis-first ranking in the argument of `apply`, `rewrite`, etc. +- LSP server: keyword completions are driven by the parser's follow sets: at any cursor position, exactly the keywords the grammar accepts there are offered (`open`/`private`/`as` after `require`, `rule` after `simplify`, `begin` after a statement's type, etc.), and symbols are only offered where a term or identifier reference can appear. New parser entry point `Parser.Lp.expected_tokens` returning the acceptable tokens at the end of a source prefix; parser error messages list more of the acceptable alternatives and render term starters as "a term". ### Changed