From 2ced9de64ce420381ad27861083b5e607d279901 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 20 Jun 2024 08:26:02 +0200
Subject: [PATCH] [kernel] fix module name parsing

---
 src/kernel_internals/parsing/logic_parser.mly | 20 +++++++++++--------
 tests/spec/module.i                           | 12 +++++------
 tests/spec/oracle/module.res.oracle           | 13 ++++++------
 3 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 0229fbb0fb..99cefda697 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1681,10 +1681,14 @@ logic_def:
     { LDaxiomatic($2,$4) }
 | MODULE push_module_identifier LBRACE logic_decls RBRACE
     { pop_module_types () ; LDmodule($2,$4) }
-| IMPORT drv = module_driver mId = LONGIDENT SEMICOLON
-    { LDimport(drv,mId,None) }
-| IMPORT drv = module_driver mId = LONGIDENT AS asId = identifier SEMICOLON
-    { LDimport(drv,mId,Some asId) }
+| IMPORT mId = module_name SEMICOLON
+    { LDimport(None,mId,None) }
+| IMPORT mId = module_name AS id = identifier SEMICOLON
+    { LDimport(None,mId,Some id) }
+| IMPORT drv = identifier COLON mId = module_name SEMICOLON
+    { LDimport(Some drv,mId,None) }
+| IMPORT drv = identifier COLON mId = module_name AS id = identifier SEMICOLON
+    { LDimport(Some drv,mId,Some id) }
 | TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
         { let (id,tvars) = $2 in
           exit_type_variables_scope ();
@@ -1692,13 +1696,13 @@ logic_def:
         }
 ;
 
-module_driver:
-| identifier_or_typename_full COMMA { Some $1 }
-| { None }
+module_name:
+| identifier { $1 }
+| LONGIDENT  { $1 }
 ;
 
 push_module_identifier:
-| LONGIDENT { Stack.push $1 module_stack ; $1 }
+| module_name { Stack.push $1 module_stack ; $1 }
 ;
 
 deprecated_logic_decl:
diff --git a/tests/spec/module.i b/tests/spec/module.i
index 507088d525..28f9198080 100644
--- a/tests/spec/module.i
+++ b/tests/spec/module.i
@@ -3,19 +3,19 @@
  */
 
 /*@
-  module foo::Bar {
+  module Foo {
     type t;
     logic t e;
     logic t op(t x, t y);
     logic t opN(t x, integer n) = n >= 0 ? op(x, opN(x,n-1)) : e;
   }
-  module foo::Jazz {
-    import foo::Bar \as X;
+  module foo::bar {
+    import Foo \as X;
     logic t inv(X::t x);
     logic t opN(t x, integer n) = n >= 0 ? X::opN(x,n) : X::opN(inv(x),-n);
   }
-  import foo::Bar \as A;
-  import foo::Jazz \as B;
-  lemma AbsOp: \forall foo::Bar::t x, integer n;
+  import Foo \as A;
+  import foo::bar \as B;
+  lemma AbsOp: \forall Foo::t x, integer n;
     B::opN(x,\abs(n)) == A::opN(x,\abs(n));
  */
diff --git a/tests/spec/oracle/module.res.oracle b/tests/spec/oracle/module.res.oracle
index e851c8719f..5f7e65ce72 100644
--- a/tests/spec/oracle/module.res.oracle
+++ b/tests/spec/oracle/module.res.oracle
@@ -1,7 +1,7 @@
 [kernel] Parsing module.i (no preprocessing)
 /* Generated by Frama-C */
 /*@
-module foo::Bar {
+module Foo {
   type t;
   
   logic t e;
@@ -13,17 +13,16 @@ module foo::Bar {
   }
  */
 /*@
-module foo::Jazz {
-  logic foo::Bar::t inv(foo::Bar::t x) ;
+module foo::bar {
+  logic Foo::t inv(Foo::t x) ;
   
-  logic foo::Bar::t opN(foo::Bar::t x, ℤ n) =
-    n ≥ 0? foo::Bar::opN(x, n): foo::Bar::opN(inv(x), -n);
+  logic Foo::t opN(Foo::t x, ℤ n) =
+    n ≥ 0? Foo::opN(x, n): Foo::opN(inv(x), -n);
   
   }
  */
 /*@
 lemma AbsOp:
-  ∀ foo::Bar::t x, ℤ n;
-    foo::Jazz::opN(x, \abs(n)) ≡ foo::Bar::opN(x, \abs(n));
+  ∀ Foo::t x, ℤ n; foo::bar::opN(x, \abs(n)) ≡ Foo::opN(x, \abs(n));
  */
 
-- 
GitLab