From c0550a102589fa63495e8351d8a5e0f7ba8778e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 20 Aug 2024 11:19:51 +0200
Subject: [PATCH] [modules] fix module-types stack
---
src/kernel_internals/parsing/logic_parser.mly | 19 ++++++++++---------
1 file changed, 10 insertions(+), 9 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 99cefda697..f2b23a2738 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -86,19 +86,20 @@
| (Lt|Le), (Unknown|Less) -> Less, true
| _ -> sense, false
- let module_stack = Stack.create ()
- let module_types = Hashtbl.create 0
+ let module_types : string list ref Stack.t = Stack.create ()
let push_typename t =
Logic_env.add_typename t ;
try
- let m = Stack.top module_stack in
- Hashtbl.add module_types m t
+ let r = Stack.top module_types in r := t :: !r
with Stack.Empty -> ()
+ let push_module_types () =
+ Stack.push (ref []) module_types
+
let pop_module_types () =
- let m = Stack.pop module_stack in
- List.iter Logic_env.remove_typename @@ Hashtbl.find_all module_types m
+ let r = Stack.pop module_types in
+ List.iter Logic_env.remove_typename !r
let type_variables_stack = Stack.create ()
@@ -1679,7 +1680,7 @@ logic_def:
LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
| AXIOMATIC any_identifier LBRACE logic_decls RBRACE
{ LDaxiomatic($2,$4) }
-| MODULE push_module_identifier LBRACE logic_decls RBRACE
+| MODULE push_module_name LBRACE logic_decls RBRACE
{ pop_module_types () ; LDmodule($2,$4) }
| IMPORT mId = module_name SEMICOLON
{ LDimport(None,mId,None) }
@@ -1701,8 +1702,8 @@ module_name:
| LONGIDENT { $1 }
;
-push_module_identifier:
-| module_name { Stack.push $1 module_stack ; $1 }
+push_module_name:
+| module_name { push_module_types () ; $1 }
;
deprecated_logic_decl:
--
GitLab