From 4d9e95d11da4b3d1c4d93f32779394df9adc0230 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 19:01:00 +0200 Subject: [PATCH 1/6] parser: map a bare open to P_open again A bare open (not preceded by require) was parsed as require open since the LL(1) parser rework (#1441), silently loading not yet required modules instead of failing, and pretty-printing back as require open. --- CHANGES.md | 3 +++ src/parsing/lpParser.ml | 16 ++++++++++------ tests/KO/open_not_required.lp | 3 +++ 3 files changed, 16 insertions(+), 6 deletions(-) create mode 100644 tests/KO/open_not_required.lp diff --git a/CHANGES.md b/CHANGES.md index 783f6da8e..16574018e 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -36,6 +36,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). ### Fixed +- A bare `open` (not preceded by `require`) was parsed as `require open` + since the parser rework, silently loading not yet required modules + instead of failing. - Convertibility test of non-linear higher-order pattern variables in rule LHS. - Syntactical errors in Dedukti export. - Weak head normal form test. diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 3bdd29d4c..9f953b0ed 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -433,11 +433,15 @@ let term_id (lb:'token lexbuf): p_term = (* commands *) -let open_ (priv:bool) (lb:'token lexbuf) : p_command_aux = +(* [req] tells whether the command starts with the [require] keyword: + [require [private] open] loads the modules and opens them + ([P_require]), while a bare [[private] open] only opens modules + that are already loaded ([P_open]). *) +let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux = if log_enabled() then log "%s" __FUNCTION__; consume OPEN lb; let ps = nelist path_tks path lb in - P_require(Some priv,ps) + if req then P_require(Some priv,ps) else P_open(priv,ps) let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = if log_enabled() then log "%s" __FUNCTION__; @@ -520,7 +524,7 @@ and command (lb:'token lexbuf) : p_command = end | [{elt=P_expo Term.Privat;_}] -> begin match current_token lb with - | OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb) + | OPEN -> extend_pos lb (*__FUNCTION__*) pos1 (open_ false true lb) | SYMBOL -> extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb) | L_PAREN @@ -546,10 +550,10 @@ and command (lb:'token lexbuf) : p_command = begin match current_token lb with | OPEN -> - extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb) + extend_pos lb (*__FUNCTION__*) pos1 (open_ true false lb) | PRIVATE -> consume_token lb; - extend_pos lb (*__FUNCTION__*) pos1 (open_ true lb) + extend_pos lb (*__FUNCTION__*) pos1 (open_ true true lb) | QID _ -> let ps = nelist path_tks path lb in begin @@ -570,7 +574,7 @@ and command (lb:'token lexbuf) : p_command = | _ -> expected lb "" [OPEN;PRIVATE;QID[]] end | OPEN -> - extend_pos lb (*__FUNCTION__*) pos1 (open_ false lb) + extend_pos lb (*__FUNCTION__*) pos1 (open_ false false lb) | SYMBOL -> extend_pos lb (*__FUNCTION__*) pos1 (symbol p_sym_mod lb) | L_PAREN diff --git a/tests/KO/open_not_required.lp b/tests/KO/open_not_required.lp new file mode 100644 index 000000000..dfc4496a9 --- /dev/null +++ b/tests/KO/open_not_required.lp @@ -0,0 +1,3 @@ +// A bare [open] does not load modules: the module must have been +// required first (with [require] or [require open]). +open tests.OK.boolean; From 070c614ead4b6a81ca3381a01186d37ec7bbd664 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Wed, 8 Jul 2026 15:32:10 +0200 Subject: [PATCH 2/6] LSP: success hints on the ";" of commands and the keyword of tactics The severity-4 "OK" diagnostic of a command or tactic previously spanned the whole command or tactic, so the success underline covered symbol bodies, rule right-hand sides and whole proofs. Instead: - A command's hint is shown on its terminating ";". The command's recorded position stops one character before it (the parser's extend_pos), so lp_doc derives the ";" position from it (at_semicolon). - Symbol declarations always create proof data, so their "OK" went through the proof path and landed on the symbol name. The initial goals stay anchored at the symbol (for the goals panel), but the visible hint now goes on the ";". - A tactic's hint is shown on its leading keyword (Syntax.tactic_keyword, exposed as Pure.Tactic.keyword), since a tactic's end is ill-defined once it has subproofs. These diagnostics also anchor the goals panel, whose lookup (closest_before) only reads the start of each position, which does not move. Also rename the lp_doc node field "ast" to "cmd". --- CHANGES.md | 4 ++++ src/lsp/lp_doc.ml | 53 ++++++++++++++++++++++++++++++++++--------- src/lsp/lp_lsp.ml | 4 ++-- src/parsing/syntax.ml | 49 +++++++++++++++++++++++++++++++++++++++ src/pure/pure.ml | 1 + src/pure/pure.mli | 2 ++ 6 files changed, 100 insertions(+), 13 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 16574018e..6d59bd962 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,6 +52,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/). duplicated directory component. - LSP server: go-to-definition and hover on qualified identifiers, and session state leaking between open documents. +- LSP server: the success ("OK") diagnostic of a command is now shown on its + terminating ";", and that of a tactic on its leading keyword, instead of + underlining the whole command or tactic (symbol body, rule right-hand + side, proof, etc.). ## 3.0.0 (2025-07-16) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index d7f0f87c4..a8a1d46f3 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -22,7 +22,7 @@ module LSP = Lsp_base let lp_logger = Buffer.create 100 type doc_node = - { ast : Pure.Command.t + { cmd : Pure.Command.t ; exec : bool (*; tactics : Proof.Tactic.t list*) ; goals : (Goal.info list * Pos.popt) list @@ -54,6 +54,16 @@ let buf_get_and_clear buf = let res = Buffer.contents buf in Buffer.clear buf; res +(* [at_keyword p kw] is the sub-position of [p] covering only its leading + keyword [kw] (keywords are ASCII, so their column width is their string + length). *) +let at_keyword : Pos.popt -> string -> Pos.popt = fun p kw -> + match p with + | None -> None + | Some p -> + Pos.(Some { p with end_line = p.start_line + ; end_col = p.start_col + String.length kw }) + let process_pstep (pstate,diags,logs) tac nb_subproofs = let open Pure in let tac_loc = Tactic.get_pos tac in @@ -63,7 +73,14 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs = | Tac_OK (pstate, qres) -> let goals = Some (current_goals pstate) in let qres = match qres with None -> "OK" | Some x -> x in - pstate, (tac_loc, 4, qres, goals) :: diags, logs + (* Show the success hint on the tactic's leading keyword only. This + tuple also anchors the goals panel (see [get_goals]), whose lookup + reads the start of the position: the start must not move. *) + let hint_loc = match Tactic.keyword tac with + | Some kw -> at_keyword tac_loc kw + | None -> tac_loc + in + pstate, (hint_loc, 4, qres, goals) :: diags, logs | Tac_Error(loc,msg) -> let loc = option_default loc tac_loc in let goals = Some (current_goals pstate) in @@ -83,27 +100,41 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -let process_cmd _file (nodes,st,dg,logs) ast = +(* A command's recorded position ends one character before its terminating + ";" (the parser's [extend_pos] stops at the start of the following token). + [at_semicolon p] returns the position of that ";", where success ("OK") + hints are shown so that they do not underline the whole command. *) +let at_semicolon : Pos.popt -> Pos.popt = function + | None -> None + | Some p -> + Pos.(Some { p with start_line = p.end_line; start_col = p.end_col + 1 + ; end_line = p.end_line; end_col = p.end_col + 2 }) + +let process_cmd _file (nodes,st,dg,logs) cmd = let open Pure in (* let open Timed in *) (* XXX: Capture output *) (* Console.out_fmt := lp_fmt; * Console.err_fmt := lp_fmt; *) - let cmd_loc = Command.get_pos ast in - let hndl_cmd_res = handle_command st ast in + let cmd_loc = Command.get_pos cmd in + let hndl_cmd_res = handle_command st cmd in let logs = ((3, buf_get_and_clear lp_logger), cmd_loc) :: logs in match hndl_cmd_res with | Cmd_OK (st, qres) -> let qres = match qres with None -> "OK" | Some x -> x in - let nodes = { ast; exec = true; goals = [] } :: nodes in - let ok_diag = cmd_loc, 4, qres, None in + let nodes = { cmd; exec = true; goals = [] } :: nodes in + (* Show the success hint on the terminating ";", not the whole command. *) + let ok_diag = at_semicolon cmd_loc, 4, qres, None in nodes, st, ok_diag :: dg, logs | Cmd_Proof (pst, tlist, thm_loc, qed_loc) -> let start_goals = current_goals pst in let pst, dg_proof, logs = process_proof pst tlist logs in - let dg_proof = (thm_loc, 4, "OK", Some start_goals) :: dg_proof in - let goals = get_goals dg_proof in - let nodes = { ast; exec = true; goals } :: nodes in + (* Initial goals stay anchored at the symbol, for the goals panel. *) + let goals = + get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in + let nodes = { cmd; exec = true; goals } :: nodes in + (* Visible success hint on the terminating ";", not on the symbol name. *) + let dg_proof = (at_semicolon cmd_loc, 4, "OK", None) :: dg_proof in let st, dg_proof, logs = match end_proof pst with | Cmd_OK (st, qres) -> @@ -123,7 +154,7 @@ let process_cmd _file (nodes,st,dg,logs) ast = nodes, st, dg_proof @ dg, logs | Cmd_Error(loc, msg) -> - let nodes = { ast; exec = false; goals = [] } :: nodes in + let nodes = { cmd; exec = false; goals = [] } :: nodes in let cmd_loc, loc, diag, log = match cmd_loc, loc with | Some l, Some Some l' -> if l.fname = l'.fname then diff --git a/src/lsp/lp_lsp.ml b/src/lsp/lp_lsp.ml index 22d76b2f6..a9b0847bc 100644 --- a/src/lsp/lp_lsp.ml +++ b/src/lsp/lp_lsp.ml @@ -222,8 +222,8 @@ let in_range ?loc (line, pos) = let get_node_at_pos doc line pos = let open Lp_doc in - List.find_opt (fun { ast; _ } -> - let loc = Pure.Command.get_pos ast in + List.find_opt (fun { cmd; _ } -> + let loc = Pure.Command.get_pos cmd in in_range ?loc (line,pos) ) doc.Lp_doc.nodes diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index be3357f14..b21f3c213 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -298,6 +298,55 @@ and p_tactic = p_tactic_aux loc (** [is_destructive t] says whether tactic [t] changes the current goal. *) let is_destructive {elt;_} = match elt with P_tac_have _ -> false | _ -> true +(** [query_keyword q] returns the keyword introducing query [q]. *) +let query_keyword : p_query -> string = fun {elt;_} -> + match elt with + | P_query_verbose _ -> "verbose" + | P_query_debug _ -> "debug" + | P_query_flag _ -> "flag" + | P_query_assert(true,_) -> "assertnot" + | P_query_assert(false,_) -> "assert" + | P_query_infer _ -> "type" + | P_query_normalize _ -> "compute" + | P_query_prover _ -> "prover" + | P_query_prover_timeout _ -> "prover_timeout" + | P_query_print _ -> "print" + | P_query_proofterm -> "proofterm" + | P_query_search _ -> "search" + +(** [tactic_keyword t] returns the keyword introducing tactic [t], or + [None] for tactics that no single keyword introduces (not produced by + the LP parser). *) +let tactic_keyword : p_tactic -> string option = fun {elt;_} -> + match elt with + | P_tac_admit -> Some "admit" + | P_tac_and _ -> None + | P_tac_all_hyps _ -> Some "all_hyps" + | P_tac_apply _ -> Some "apply" + | P_tac_assume _ -> Some "assume" + | P_tac_assumption -> Some "assumption" + | P_tac_change _ -> Some "change" + | P_tac_eval _ -> Some "eval" + | P_tac_fail -> Some "fail" + | P_tac_first_hyp _ -> Some "first_hyp" + | P_tac_focus _ -> Some "focus" + | P_tac_generalize _ -> Some "generalize" + | P_tac_have _ -> Some "have" + | P_tac_induction -> Some "induction" + | P_tac_orelse _ -> Some "orelse" + | P_tac_query q -> Some (query_keyword q) + | P_tac_refine _ -> Some "refine" + | P_tac_refl -> Some "reflexivity" + | P_tac_remove _ -> Some "remove" + | P_tac_repeat _ -> Some "repeat" + | P_tac_rewrite _ -> Some "rewrite" + | P_tac_set _ -> Some "set" + | P_tac_simpl _ -> Some "simplify" + | P_tac_solve -> Some "solve" + | P_tac_sym -> Some "symmetry" + | P_tac_try _ -> Some "try" + | P_tac_why3 _ -> Some "why3" + (** Parser-level representation of a proof. *) type p_subproof = p_proofstep list diff --git a/src/pure/pure.ml b/src/pure/pure.ml index 2efd2f992..ad0dca261 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -47,6 +47,7 @@ module Tactic = struct type t = Syntax.p_tactic let equal = Syntax.eq_p_tactic let get_pos t = Pos.(t.pos) + let keyword = Syntax.tactic_keyword let print = Util.located Pretty.tactic end diff --git a/src/pure/pure.mli b/src/pure/pure.mli index b865e9f71..f8bc60bcf 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -20,6 +20,8 @@ module Tactic : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val keyword : t -> string option + (** Keyword introducing the tactic, if a single keyword does. *) val print : t Base.pp [@@ocaml.toplevel_printer] end From b490ace893c5019229efe4df30ba3d2b2770c7b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 11:46:54 +0200 Subject: [PATCH 3/6] LSP: review fixes for success hint positions Set the character offsets of hint positions consistently with their columns (at_keyword left end_offset at the end of the whole tactic, at_semicolon did not update offsets at all). Handle a ";" at the beginning of a line: the parser's extend_pos does not back up at column 0, so a command position with end_col = 0 cannot distinguish a ";" at column 0 from one at column 1 (the hint used to underline column 1, one character past a line-initial ";"). Cover both columns in that case. --- src/lsp/lp_doc.ml | 34 +++++++++++++++++++++++++--------- 1 file changed, 25 insertions(+), 9 deletions(-) diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index a8a1d46f3..27b492362 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -55,14 +55,15 @@ let buf_get_and_clear buf = Buffer.clear buf; res (* [at_keyword p kw] is the sub-position of [p] covering only its leading - keyword [kw] (keywords are ASCII, so their column width is their string - length). *) + keyword [kw] (keywords are ASCII, so their string length is their width + both in columns and in character offsets). *) let at_keyword : Pos.popt -> string -> Pos.popt = fun p kw -> match p with | None -> None | Some p -> Pos.(Some { p with end_line = p.start_line - ; end_col = p.start_col + String.length kw }) + ; end_col = p.start_col + String.length kw + ; end_offset = p.start_offset + String.length kw }) let process_pstep (pstate,diags,logs) tac nb_subproofs = let open Pure in @@ -100,15 +101,30 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -(* A command's recorded position ends one character before its terminating - ";" (the parser's [extend_pos] stops at the start of the following token). - [at_semicolon p] returns the position of that ";", where success ("OK") - hints are shown so that they do not underline the whole command. *) +(* [at_semicolon p] is the position of the ";" terminating a command whose + position is [p]. Success ("OK") hints are shown there so that they do + not underline the whole command. Position ends are exclusive (as in the + LSP ranges they are mapped to), so the position of the one-character + ";" ends one column after it. The parser's [extend_pos] ends [p] one + character before the ";", except when the ";" is at column 0, where it + does not back up over the newline: a ";" at column 0 and one at column + 1 both yield [end_col = 0] (with [end_offset] the offset of column 0), + so in that case the returned position covers both columns. *) let at_semicolon : Pos.popt -> Pos.popt = function | None -> None | Some p -> - Pos.(Some { p with start_line = p.end_line; start_col = p.end_col + 1 - ; end_line = p.end_line; end_col = p.end_col + 2 }) + Pos.( + if p.end_col = 0 then + Some { p with start_line = p.end_line; start_col = 0 + ; start_offset = p.end_offset + ; end_col = 2 + ; end_offset = p.end_offset + 2 } + else + Some { p with start_line = p.end_line + ; start_col = p.end_col + 1 + ; start_offset = p.end_offset + 1 + ; end_col = p.end_col + 2 + ; end_offset = p.end_offset + 2 }) let process_cmd _file (nodes,st,dg,logs) cmd = let open Pure in From 1e2e768c4c802f273670c2f88dadbfaed526f303 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ciar=C3=A1n=20Dunne?= Date: Thu, 9 Jul 2026 13:50:01 +0200 Subject: [PATCH 4/6] LSP: show command success hints on the introducing keyword Show the "OK" hint of a command on its keyword ("symbol", "rule", "require", ...) rather than on the terminating ";". The keyword of a symbol, inductive or open command is not always at the command's start (modifiers or parameters may precede it), so the parser records the keyword position in the AST for these three constructors. For the other commands, Syntax.command_keyword_pos computes it as a prefix of the command's position. Tactics use the same mechanism (tactic_keyword_pos); at_keyword and at_semicolon disappear from lp_doc, replaced by Pos.prefix. --- CHANGES.md | 6 ++-- src/cli/lambdapi.ml | 3 +- src/common/pos.ml | 10 +++++++ src/export/coq.ml | 6 ++-- src/export/lean.ml | 6 ++-- src/export/rawdk.ml | 2 +- src/handle/command.ml | 8 +++--- src/lsp/lp_doc.ml | 51 ++++------------------------------ src/parsing/dkParser.mly | 4 ++- src/parsing/lpParser.ml | 23 ++++++++++------ src/parsing/parser.ml | 2 +- src/parsing/pretty.ml | 10 +++---- src/parsing/syntax.ml | 59 ++++++++++++++++++++++++++++++++-------- src/pure/pure.ml | 3 +- src/pure/pure.mli | 9 ++++-- 15 files changed, 112 insertions(+), 90 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 6d59bd962..2b1b61b39 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,9 +52,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). duplicated directory component. - LSP server: go-to-definition and hover on qualified identifiers, and session state leaking between open documents. -- LSP server: the success ("OK") diagnostic of a command is now shown on its - terminating ";", and that of a tactic on its leading keyword, instead of - underlining the whole command or tactic (symbol body, rule right-hand +- LSP server: the success ("OK") diagnostic of a command or tactic is now + shown on its introducing keyword ("symbol", "rule", "assume", …), instead + of underlining the whole command or tactic (symbol body, rule right-hand side, proof, etc.). ## 3.0.0 (2025-07-16) diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml index fac04645c..0ed9822ea 100644 --- a/src/cli/lambdapi.ml +++ b/src/cli/lambdapi.ml @@ -28,7 +28,8 @@ let sig_state_of_require l : Sig_state.sig_state = Handle.Command.handle Compile.compile ss (Pos.none (Parsing.Syntax.P_require - (Some false, [Pos.none (Parsing.Parser.path_of_string req)])))) + (Some false, + [Pos.none (Parsing.Parser.path_of_string req)])))) Core.Sig_state.dummy l let search_cmd cfg rules require s dbpath_opt = diff --git a/src/common/pos.ml b/src/common/pos.ml index 395777779..754df1d53 100644 --- a/src/common/pos.ml +++ b/src/common/pos.ml @@ -111,6 +111,16 @@ let cat : popt -> popt -> popt = fun p1 p2 -> | None, Some p -> Some p | None, None -> None +(** [prefix n p] is the sub-position of [p] covering only its first [n] + characters, which are assumed to lie on the first line of [p] and to be + ASCII (so that [n] is both a column count and a character count). *) +let prefix : int -> popt -> popt = fun n p -> + match p with + | None -> None + | Some p -> Some { p with end_line = p.start_line + ; end_col = p.start_col + n + ; end_offset = p.start_offset + n } + (** [shift k p] returns a position that is [k] characters after [p]. *) let shift : int -> popt -> popt = fun k p -> match p with diff --git a/src/export/coq.ml b/src/export/coq.ml index 6defb5ba5..c9d438918 100644 --- a/src/export/coq.ml +++ b/src/export/coq.ml @@ -114,9 +114,9 @@ and typopt oc t = Option.iter (prefix " : " term oc) t let command oc {elt; pos} = begin match elt with - | P_open(true,ps) -> + | P_open(_,true,ps) -> string oc "Import "; list path " " oc ps; string oc ".\n" - | P_open(false,ps) -> + | P_open(_,false,ps) -> string oc "Export "; list path " " oc ps; string oc ".\n" | P_require (None, ps) -> string oc "Require "; list path " " oc ps; string oc ".\n" @@ -129,7 +129,7 @@ let command oc {elt; pos} = string oc "Module "; ident oc i; string oc " := "; path oc p; string oc ".\n" | P_symbol - { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_prf=_; p_sym_def } -> if not (is_mapped p_sym_nam.elt) then begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with diff --git a/src/export/lean.ml b/src/export/lean.ml index 6aebe4d46..cb00be6ca 100644 --- a/src/export/lean.ml +++ b/src/export/lean.ml @@ -140,7 +140,7 @@ let openings = ref [] let command oc {elt; pos} = begin match elt with - | P_open(_,ps) -> List.iter (open_mod oc) ps + | P_open(_,_,ps) -> List.iter (open_mod oc) ps | P_require(b,ps) -> List.iter (req_mod oc) ps; begin @@ -149,8 +149,8 @@ let command oc {elt; pos} = | _ -> () (*FIXME?*) end | P_require_as(p,i) -> Stt.alias := StrMap.add i.elt p.elt !Stt.alias - | P_symbol { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; - p_sym_prf=_; p_sym_def } -> + | P_symbol { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ; + p_sym_trm; p_sym_prf=_; p_sym_def } -> if not (is_mapped p_sym_nam.elt) then begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with | true, Some t, _, Some a when List.exists is_lem p_sym_mod -> diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml index b9b917e67..174d7f04e 100644 --- a/src/export/rawdk.ml +++ b/src/export/rawdk.ml @@ -198,7 +198,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) -> | P_query q -> query ppf q | P_require(None,ps) -> List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.mident elt) ps - | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg; p_sym_typ; + | P_symbol{p_sym_mod; p_sym_kw=_; p_sym_nam=n; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_prf=None; p_sym_def=_;} -> let ms = partition_modifiers p_sym_mod in begin match get_ac_typ pos ms p_sym_arg p_sym_typ with diff --git a/src/handle/command.ml b/src/handle/command.ml index d0a10f141..0ce0f2d8f 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -249,7 +249,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = | P_require(bo,ps) -> (List.fold_left (handle_require compile bo) ss ps, None, None) | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None) - | P_open(b,ps) -> (List.fold_left (handle_open b) ss ps, None, None) + | P_open(_,b,ps) -> (List.fold_left (handle_open b) ss ps, None, None) | P_rules(rs) -> (* Scope rules, and check that they preserve typing. Return the list of rules [srs] and also a [map] mapping every symbol defined by a rule @@ -344,7 +344,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = Console.out 2 (Color.gre "coercion %a") sym_rule r; (ss, None, None) - | P_inductive(ms, params, p_ind_list) -> + | P_inductive(_, ms, params, p_ind_list) -> (* Check modifiers. *) let (prop, expo, mstrat, opaq) = handle_modifiers ms in if prop <> Defin then @@ -446,8 +446,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = rec_sym_list; (ss, None, None) - | P_symbol {p_sym_mod;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf; - p_sym_def} -> + | P_symbol {p_sym_mod;p_sym_kw=_;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm; + p_sym_prf;p_sym_def} -> (* We check that the identifier is not already used. *) let {elt=id; _} = p_sym_nam in if Sign.mem ss.signature id then diff --git a/src/lsp/lp_doc.ml b/src/lsp/lp_doc.ml index 27b492362..11449acaa 100644 --- a/src/lsp/lp_doc.ml +++ b/src/lsp/lp_doc.ml @@ -54,17 +54,6 @@ let buf_get_and_clear buf = let res = Buffer.contents buf in Buffer.clear buf; res -(* [at_keyword p kw] is the sub-position of [p] covering only its leading - keyword [kw] (keywords are ASCII, so their string length is their width - both in columns and in character offsets). *) -let at_keyword : Pos.popt -> string -> Pos.popt = fun p kw -> - match p with - | None -> None - | Some p -> - Pos.(Some { p with end_line = p.start_line - ; end_col = p.start_col + String.length kw - ; end_offset = p.start_offset + String.length kw }) - let process_pstep (pstate,diags,logs) tac nb_subproofs = let open Pure in let tac_loc = Tactic.get_pos tac in @@ -77,11 +66,7 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs = (* Show the success hint on the tactic's leading keyword only. This tuple also anchors the goals panel (see [get_goals]), whose lookup reads the start of the position: the start must not move. *) - let hint_loc = match Tactic.keyword tac with - | Some kw -> at_keyword tac_loc kw - | None -> tac_loc - in - pstate, (hint_loc, 4, qres, goals) :: diags, logs + pstate, (Tactic.keyword_pos tac, 4, qres, goals) :: diags, logs | Tac_Error(loc,msg) -> let loc = option_default loc tac_loc in let goals = Some (current_goals pstate) in @@ -101,31 +86,6 @@ let get_goals dg_proof = in get_goals_aux [] dg_proof (* XXX: Imperative problem *) -(* [at_semicolon p] is the position of the ";" terminating a command whose - position is [p]. Success ("OK") hints are shown there so that they do - not underline the whole command. Position ends are exclusive (as in the - LSP ranges they are mapped to), so the position of the one-character - ";" ends one column after it. The parser's [extend_pos] ends [p] one - character before the ";", except when the ";" is at column 0, where it - does not back up over the newline: a ";" at column 0 and one at column - 1 both yield [end_col = 0] (with [end_offset] the offset of column 0), - so in that case the returned position covers both columns. *) -let at_semicolon : Pos.popt -> Pos.popt = function - | None -> None - | Some p -> - Pos.( - if p.end_col = 0 then - Some { p with start_line = p.end_line; start_col = 0 - ; start_offset = p.end_offset - ; end_col = 2 - ; end_offset = p.end_offset + 2 } - else - Some { p with start_line = p.end_line - ; start_col = p.end_col + 1 - ; start_offset = p.end_offset + 1 - ; end_col = p.end_col + 2 - ; end_offset = p.end_offset + 2 }) - let process_cmd _file (nodes,st,dg,logs) cmd = let open Pure in (* let open Timed in *) @@ -139,8 +99,8 @@ let process_cmd _file (nodes,st,dg,logs) cmd = | Cmd_OK (st, qres) -> let qres = match qres with None -> "OK" | Some x -> x in let nodes = { cmd; exec = true; goals = [] } :: nodes in - (* Show the success hint on the terminating ";", not the whole command. *) - let ok_diag = at_semicolon cmd_loc, 4, qres, None in + (* Show the success hint on the command's introducing keyword only. *) + let ok_diag = Command.keyword_pos cmd, 4, qres, None in nodes, st, ok_diag :: dg, logs | Cmd_Proof (pst, tlist, thm_loc, qed_loc) -> let start_goals = current_goals pst in @@ -149,8 +109,9 @@ let process_cmd _file (nodes,st,dg,logs) cmd = let goals = get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in let nodes = { cmd; exec = true; goals } :: nodes in - (* Visible success hint on the terminating ";", not on the symbol name. *) - let dg_proof = (at_semicolon cmd_loc, 4, "OK", None) :: dg_proof in + (* Visible success hint on the "symbol" keyword, not on the symbol + name. *) + let dg_proof = (Command.keyword_pos cmd, 4, "OK", None) :: dg_proof in let st, dg_proof, logs = match end_proof pst with | Cmd_OK (st, qres) -> diff --git a/src/parsing/dkParser.mly b/src/parsing/dkParser.mly index 8e5e867b6..9d34eb0e0 100644 --- a/src/parsing/dkParser.mly +++ b/src/parsing/dkParser.mly @@ -49,6 +49,7 @@ let symbol lps p_sym_mod i ps p_sym_typ p_sym_trm = make_pos lps (P_symbol { p_sym_mod + ; p_sym_kw = None (* Dedukti has no "symbol" keyword. *) ; p_sym_nam = p_ident i ; p_sym_arg = List.map (fun (i,t) -> params i (Some t)) ps ; p_sym_typ @@ -77,7 +78,8 @@ let query lps q = make_pos lps (P_query q) - let require (lps,id) = make_pos lps (P_require(None,[make_pos lps [id]])) + let require (lps,id) = + make_pos lps (P_require(None,[make_pos lps [id]])) let arrow lps a b = make_pos lps (P_Arro (a, b)) let binary lps a = arrow lps a (arrow lps a a) diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 9f953b0ed..828401bb8 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -436,15 +436,20 @@ let term_id (lb:'token lexbuf): p_term = (* [req] tells whether the command starts with the [require] keyword: [require [private] open] loads the modules and opens them ([P_require]), while a bare [[private] open] only opens modules - that are already loaded ([P_open]). *) + that are already loaded ([P_open]). For a bare open, the position + of the "open" keyword is recorded in the AST (a "private" modifier, + like modifiers of symbol declarations, is not part of the + keyword). *) let open_ (req:bool) (priv:bool) (lb:'token lexbuf) : p_command_aux = if log_enabled() then log "%s" __FUNCTION__; + let kw_pos = Some(locate (current_pos lb)) in consume OPEN lb; let ps = nelist path_tks path lb in - if req then P_require(Some priv,ps) else P_open(priv,ps) + if req then P_require(Some priv,ps) else P_open(kw_pos,priv,ps) let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = if log_enabled() then log "%s" __FUNCTION__; + let p_sym_kw = Some(locate (current_pos lb)) in consume SYMBOL lb; let p_sym_nam = uid lb in let p_sym_arg = list params_tks params lb in @@ -460,7 +465,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_prf = Some (proof lb) in let p_sym_def = false in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm=None; p_sym_def; p_sym_prf} in P_symbol(sym) | ASSIGN -> @@ -468,7 +473,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_trm, p_sym_prf = term_proof lb in let p_sym_def = true in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_def; p_sym_prf} in P_symbol(sym) | SEMICOLON -> @@ -476,7 +481,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_def = false in let p_sym_prf = None in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_def; p_sym_prf} in P_symbol(sym) | _ -> @@ -488,7 +493,7 @@ let rec symbol (p_sym_mod:p_modifier list) (lb:'token lexbuf): p_command_aux = let p_sym_def = true in let p_sym_typ = None in let sym = - {p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + {p_sym_mod; p_sym_kw; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_def; p_sym_prf} in P_symbol(sym) | _ -> @@ -501,10 +506,11 @@ and inductive_cmd (p_sym_mod:p_modifier list) (lb:'token lexbuf) let xs = list params_tks params lb in match current_token lb with | INDUCTIVE -> + let kw_pos = Some(locate (current_pos lb)) in consume INDUCTIVE lb; let i = inductive lb in let is = list [WITH] (prefix WITH inductive) lb in - P_inductive(p_sym_mod,xs,i::is) + P_inductive(kw_pos,p_sym_mod,xs,i::is) | _ -> expected lb "" [L_PAREN;L_SQ_BRACKET;INDUCTIVE] and command (lb:'token lexbuf) : p_command = @@ -569,7 +575,8 @@ and command (lb:'token lexbuf) : p_command = extend_pos lb (*__FUNCTION__*) pos1 (P_require_as(p,i)) | _ -> set_expected_tokens lb [AS] ; - extend_pos lb (*__FUNCTION__*) pos1 (P_require(None,ps)) + extend_pos lb (*__FUNCTION__*) pos1 + (P_require(None,ps)) end | _ -> expected lb "" [OPEN;PRIVATE;QID[]] end diff --git a/src/parsing/parser.ml b/src/parsing/parser.ml index dcc83fa18..be2d65fa8 100644 --- a/src/parsing/parser.ml +++ b/src/parsing/parser.ml @@ -75,7 +75,7 @@ module Dk : PARSER with type lexbuf := Lexing.lexbuf = struct parse_lexbuf None entry lb let command = - let r = ref (Pos.none (P_open(false,[]))) in + let r = ref (Pos.none (P_open(None,false,[]))) in fun (lb:lexbuf): p_command -> Debug.(record_time Parsing (fun () -> r := DkParser.line DkLexer.token lb)); !r diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index 6a1b790f0..f120de2f5 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -367,16 +367,16 @@ let proof : (p_proof * p_proof_end) pp = fun ppf (p, pe) -> let command : p_command pp = fun ppf { elt; _ } -> begin match elt with | P_builtin (s, qid) -> out ppf "@[builtin \"%s\"@ ≔ %a@]" s qident qid - | P_inductive (_, _, []) -> assert false (* not possible *) - | P_inductive (ms, xs, i :: il) -> + | P_inductive (_, _, _, []) -> assert false (* not possible *) + | P_inductive (_, ms, xs, i :: il) -> let with_ind ppf i = out ppf "@,%a" (inductive "with") i in out ppf "@[@[%a%a@]%a%a@]" modifiers ms (List.pp params " ") xs (inductive "inductive") i (List.pp with_ind "") il | P_notation (qid, n) -> out ppf "notation %a %a" qident qid (Print.notation string) n - | P_open(false,ps) -> out ppf "open %a" (List.pp path " ") ps - | P_open(true,ps) -> out ppf "private open %a" (List.pp path " ") ps + | P_open(_,false,ps) -> out ppf "open %a" (List.pp path " ") ps + | P_open(_,true,ps) -> out ppf "private open %a" (List.pp path " ") ps | P_query q -> query ppf q | P_require (None, ps) -> out ppf "require %a" (List.pp path " ") ps | P_require (Some false, ps) -> @@ -389,7 +389,7 @@ let command : p_command pp = fun ppf { elt; _ } -> let with_rule ppf r = out ppf "@.%a" (rule "with") r in rule "rule" ppf r; List.iter (with_rule ppf) rs | P_symbol - { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; + { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm; p_sym_prf; p_sym_def } -> begin out ppf "@[@[<2>%asymbol %a%a%a%a%a@]%a@]" diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index b21f3c213..91fa648e9 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -347,6 +347,14 @@ let tactic_keyword : p_tactic -> string option = fun {elt;_} -> | P_tac_try _ -> Some "try" | P_tac_why3 _ -> Some "why3" +(** [tactic_keyword_pos t] returns the position of the keyword introducing + tactic [t], or the position of the whole of [t] when no single keyword + does. *) +let tactic_keyword_pos : p_tactic -> Pos.popt = fun ({pos;_} as t) -> + match tactic_keyword t with + | Some kw -> Pos.prefix (String.length kw) pos + | None -> pos + (** Parser-level representation of a proof. *) type p_subproof = p_proofstep list @@ -386,6 +394,7 @@ let is_priv {elt; _} = match elt with P_expo Privat -> true | _ -> false (** Parser-level representation of symbol declarations. *) type p_symbol = { p_sym_mod : p_modifier list (** modifiers *) + ; p_sym_kw : Pos.popt (** position of the "symbol" keyword *) ; p_sym_nam : p_ident (** symbol name *) ; p_sym_arg : p_params list (** arguments before ":" *) ; p_sym_typ : p_term option (** symbol type *) @@ -397,10 +406,12 @@ type p_symbol = type p_command_aux = | P_require of (*private?*)bool (*open?*)option * p_path list | P_require_as of p_path * p_ident - | P_open of (*private?*)bool * p_path list + | P_open of (*"open" keyword position*)Pos.popt + * (*private?*)bool * p_path list | P_symbol of p_symbol | P_rules of p_rule list - | P_inductive of p_modifier list * p_params list * p_inductive list + | P_inductive of (*"inductive" keyword position*)Pos.popt + * p_modifier list * p_params list * p_inductive list | P_builtin of string * p_qident | P_notation of p_qident * string Term.notation | P_unif_rule of p_rule @@ -411,6 +422,29 @@ type p_command_aux = (** Parser-level representation of a single (located) command. *) type p_command = p_command_aux loc +(** [command_keyword_pos c] returns the position of the keyword introducing + command [c] ("symbol", "rule", "require", …). Symbol, inductive and + open commands record it in the AST, as modifiers or parameters may + precede their keyword; for the other commands it is a prefix of the + position of [c]. When no position was recorded (e.g. on Dedukti input), + the position of the whole of [c] is returned instead. *) +let command_keyword_pos : p_command -> Pos.popt = fun {elt; pos} -> + let prefix kw = Pos.prefix (String.length kw) pos in + match elt with + | P_open(kw,_,_) + | P_inductive(kw,_,_,_) + | P_symbol{p_sym_kw=kw;_} -> + (match kw with Some _ -> kw | None -> pos) + | P_require _ + | P_require_as _ -> prefix "require" + | P_rules _ -> prefix "rule" + | P_builtin _ -> prefix "builtin" + | P_notation _ -> prefix "notation" + | P_unif_rule _ -> prefix "unif_rule" + | P_coercion _ -> prefix "coerce_rule" + | P_query q -> prefix (query_keyword q) + | P_opaque _ -> prefix "opaque" + (** Top level AST returned by the parser. *) type ast = p_command Stream.t @@ -542,12 +576,12 @@ let eq_p_sym_prf : (p_proof * p_proof_end) eq = fun (p1, pe1) (p2, pe2) -> pe1.elt = pe2.elt && eq_p_proof p1 p2 let eq_p_symbol : p_symbol eq = fun - { p_sym_mod=p_sym_mod1; p_sym_nam=p_sym_nam1; p_sym_arg=p_sym_arg1; - p_sym_typ=p_sym_typ1; p_sym_trm=p_sym_trm1; p_sym_prf=p_sym_prf1; - p_sym_def=p_sym_def1} - { p_sym_mod=p_sym_mod2; p_sym_nam=p_sym_nam2; p_sym_arg=p_sym_arg2; - p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2; p_sym_prf=p_sym_prf2; - p_sym_def=p_sym_def2} -> + { p_sym_mod=p_sym_mod1; p_sym_kw=_; p_sym_nam=p_sym_nam1; + p_sym_arg=p_sym_arg1; p_sym_typ=p_sym_typ1; p_sym_trm=p_sym_trm1; + p_sym_prf=p_sym_prf1; p_sym_def=p_sym_def1} + { p_sym_mod=p_sym_mod2; p_sym_kw=_; p_sym_nam=p_sym_nam2; + p_sym_arg=p_sym_arg2; p_sym_typ=p_sym_typ2; p_sym_trm=p_sym_trm2; + p_sym_prf=p_sym_prf2; p_sym_def=p_sym_def2} -> List.eq eq_p_modifier p_sym_mod1 p_sym_mod2 && eq_p_ident p_sym_nam1 p_sym_nam2 && List.eq eq_p_params p_sym_arg1 p_sym_arg2 @@ -560,13 +594,14 @@ let eq_p_symbol : p_symbol eq = fun are compared up to source code positions. *) let eq_p_command : p_command eq = fun {elt=c1;_} {elt=c2;_} -> match c1, c2 with - | P_require(b1,l1), P_require(b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2 - | P_open(b1,l1), P_open(b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2 + | P_require(b1,l1), P_require(b2,l2) -> + b1 = b2 && List.eq eq_p_path l1 l2 + | P_open(_,b1,l1), P_open(_,b2,l2) -> b1 = b2 && List.eq eq_p_path l1 l2 | P_require_as(m1,i1), P_require_as(m2,i2) -> eq_p_path m1 m2 && eq_p_ident i1 i2 | P_symbol s1, P_symbol s2 -> eq_p_symbol s1 s2 | P_rules(r1), P_rules(r2) -> List.eq eq_p_rule r1 r2 - | P_inductive(m1,xs1,l1), P_inductive(m2,xs2,l2) -> + | P_inductive(_,m1,xs1,l1), P_inductive(_,m2,xs2,l2) -> m1 = m2 && List.eq eq_p_params xs1 xs2 && List.eq eq_p_inductive l1 l2 | P_builtin(s1,q1), P_builtin(s2,q2) -> s1 = s2 && eq_p_qident q1 q2 @@ -766,7 +801,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a = | P_coercion r | P_unif_rule r -> fold_rule a r | P_rules rs -> List.fold_left fold_rule a rs - | P_inductive (_, xs, ind_list) -> + | P_inductive (_, _, xs, ind_list) -> let vs, a = List.fold_left fold_args (StrSet.empty, a) xs in List.fold_left (fold_inductive_vars vs) a ind_list | P_symbol {p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;_} -> diff --git a/src/pure/pure.ml b/src/pure/pure.ml index ad0dca261..422cd26e3 100644 --- a/src/pure/pure.ml +++ b/src/pure/pure.ml @@ -22,6 +22,7 @@ module Command = struct (* TODO: Fixme not to use generic equality *) let equal_with_pos = (=) let get_pos c = Pos.(c.pos) + let keyword_pos = Syntax.command_keyword_pos let print = Util.located Pretty.command end @@ -47,7 +48,7 @@ module Tactic = struct type t = Syntax.p_tactic let equal = Syntax.eq_p_tactic let get_pos t = Pos.(t.pos) - let keyword = Syntax.tactic_keyword + let keyword_pos = Syntax.tactic_keyword_pos let print = Util.located Pretty.tactic end diff --git a/src/pure/pure.mli b/src/pure/pure.mli index f8bc60bcf..0634f3c7f 100644 --- a/src/pure/pure.mli +++ b/src/pure/pure.mli @@ -10,6 +10,10 @@ module Command : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt + val keyword_pos : t -> Pos.popt + (** Position of the keyword introducing the command ("symbol", "rule", + "require", …), which is not always at its start: modifiers or + parameters may precede it. *) val print : t Base.pp [@@ocaml.toplevel_printer] end @@ -20,8 +24,9 @@ module Tactic : sig type t val equal : t -> t -> bool val get_pos : t -> Pos.popt - val keyword : t -> string option - (** Keyword introducing the tactic, if a single keyword does. *) + val keyword_pos : t -> Pos.popt + (** Position of the keyword introducing the tactic, or of the whole + tactic when no single keyword does. *) val print : t Base.pp [@@ocaml.toplevel_printer] end From 9225bbd0d8bd3b423d73177aa3d2294cb004562f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 10 Jul 2026 09:33:47 +0200 Subject: [PATCH 5/6] minimize diff --- src/parsing/lpParser.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml index 828401bb8..65fdc1d0a 100644 --- a/src/parsing/lpParser.ml +++ b/src/parsing/lpParser.ml @@ -575,8 +575,7 @@ and command (lb:'token lexbuf) : p_command = extend_pos lb (*__FUNCTION__*) pos1 (P_require_as(p,i)) | _ -> set_expected_tokens lb [AS] ; - extend_pos lb (*__FUNCTION__*) pos1 - (P_require(None,ps)) + extend_pos lb (*__FUNCTION__*) pos1 (P_require(None,ps)) end | _ -> expected lb "" [OPEN;PRIVATE;QID[]] end From 8ca81c6173a659fbaad8e8702ff5996b90deeafa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 10 Jul 2026 09:35:23 +0200 Subject: [PATCH 6/6] fix CHANGES --- CHANGES.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 2b1b61b39..65fa9f8a8 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -36,9 +36,6 @@ 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.