From 0ff3bb145c82de8f577165056d46a3b38ff60664 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 19 Jun 2024 16:36:32 +0200
Subject: [PATCH] [modules] no more need to import module types
---
src/kernel_internals/parsing/logic_parser.mly | 29 +++++--------------
1 file changed, 7 insertions(+), 22 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index a0113cf7b5..a4bccb1803 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -89,31 +89,16 @@
let module_stack = Stack.create ()
let module_types = Hashtbl.create 0
- let push_typename ?(export=true) t =
+ let push_typename t =
Logic_env.add_typename t ;
try
let m = Stack.top module_stack in
- Hashtbl.add module_types m (export,t)
+ Hashtbl.add module_types m t
with Stack.Empty -> ()
- let import_typenames mId asId =
- List.iter (fun (export,t) ->
- if export then
- begin
- push_typename ~export:false t ;
- match asId with
- | None -> ()
- | Some a ->
- push_typename ~export:false @@ Printf.sprintf "%s::%s" a t
- end
- ) @@ Hashtbl.find_all module_types mId
-
let pop_module_types () =
let m = Stack.pop module_stack in
- List.iter (fun (export,t) ->
- Logic_env.remove_typename t ;
- if export then Logic_env.add_typename (Printf.sprintf "%s::%s" m t)
- ) @@ Hashtbl.find_all module_types m
+ List.iter Logic_env.remove_typename @@ Hashtbl.find_all module_types m
let type_variables_stack = Stack.create ()
@@ -1696,10 +1681,10 @@ logic_def:
{ LDaxiomatic($2,$4) }
| MODULE push_module_identifier LBRACE logic_decls RBRACE
{ pop_module_types () ; LDmodule($2,$4) }
-| IMPORT LONGIDENT SEMICOLON
- { import_typenames $2 None ; LDimport($2,None) }
-| IMPORT LONGIDENT AS identifier SEMICOLON
- { let asId = Some $4 in import_typenames $2 asId ; LDimport($2,asId) }
+| IMPORT mId = LONGIDENT SEMICOLON
+ { LDimport(mId,None) }
+| IMPORT mId = LONGIDENT AS asId = identifier SEMICOLON
+ { LDimport(mId,Some asId) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
{ let (id,tvars) = $2 in
exit_type_variables_scope ();
--
GitLab