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/CHANGES.md b/CHANGES.md index 783f6da8e..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 @@ -36,6 +39,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. @@ -49,6 +55,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 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/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/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 d7f0f87c4..0d846a843 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 @@ -39,9 +39,17 @@ 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; + path_map : Common.Path.t RangeMap.t; } let option_default o1 d = @@ -63,7 +71,10 @@ 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. *) + 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 @@ -83,27 +94,32 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -let process_cmd _file (nodes,st,dg,logs) ast = +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 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 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 "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) -> @@ -123,7 +139,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 @@ -156,8 +172,10 @@ let new_doc ~uri ~version ~text = root; final = root; nodes = []; + good_nodes = []; logs = logs; map = RangeMap.empty; + path_map = RangeMap.empty; } (* XXX: Save on close. *) @@ -200,5 +218,10 @@ 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 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 22d76b2f6..246c75e3e 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))) @@ -33,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 [ @@ -42,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 @@ -66,13 +162,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 +184,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 @@ -130,18 +228,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 @@ -150,21 +292,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 = @@ -220,12 +367,781 @@ 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 { 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 + ) 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. + 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)) + +(* 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 + | 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))) + +(* [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 + +(* --- 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, + [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 + +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 + 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 = @@ -313,23 +1229,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 @@ -350,22 +1290,365 @@ 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 () +(* --- 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 @@ -379,7 +1662,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 *) @@ -403,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 @@ -423,11 +1719,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 +1741,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 +1771,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) 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 3bdd29d4c..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) @@ -433,14 +461,32 @@ 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]). 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 - P_require(Some priv,ps) + 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 consume SYMBOL lb; let p_sym_nam = uid lb in let p_sym_arg = list params_tks params lb in @@ -456,7 +502,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 -> @@ -464,7 +510,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 -> @@ -472,7 +518,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) | _ -> @@ -484,7 +530,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) | _ -> @@ -497,10 +543,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 = @@ -520,7 +567,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 +593,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 @@ -564,13 +611,14 @@ 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] ; - extend_pos lb (*__FUNCTION__*) pos1 (P_require(None,ps)) + add_expected_tokens lb [AS] ; + extend_pos lb (*__FUNCTION__*) pos1 + (P_require(None,ps)) end | _ -> 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 @@ -630,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 = @@ -900,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 *) @@ -958,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 = @@ -1131,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 @@ -1155,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 -> @@ -1179,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 | _ -> @@ -1230,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 -> @@ -1303,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 @@ -1372,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 dcc83fa18..b6fed4da6 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 @@ -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/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 be3357f14..79f0ff271 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -298,6 +298,63 @@ 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" + +(** [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 @@ -337,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 *) @@ -348,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 @@ -362,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 @@ -493,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 @@ -511,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 @@ -717,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;_} -> @@ -731,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 2efd2f992..d2bfafea0 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -22,6 +22,8 @@ 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 @@ -42,11 +44,22 @@ 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 let equal = Syntax.eq_p_tactic let get_pos t = Pos.(t.pos) + let keyword_pos = Syntax.tactic_keyword_pos let print = Util.located Pretty.tactic end @@ -93,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 -> @@ -182,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)) @@ -194,6 +213,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 b865e9f71..557c910a3 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -10,16 +10,30 @@ 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 + parameters may precede it. *) val print : t Base.pp [@@ocaml.toplevel_printer] 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 val equal : t -> t -> bool val get_pos : t -> Pos.popt + 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 @@ -43,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 @@ -86,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. *) @@ -97,6 +123,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. *) 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; 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()