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/2] 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 1a9657b57f6d0c967553e5536ac3203d0739902e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jul 2026 22:58:41 +0200 Subject: [PATCH 2/2] revert CHANGES because the problem was not in the previous release --- CHANGES.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 16574018e..783f6da8e 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.