[kernel] fix module name parsing

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:

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));
  */

tests/spec/oracle/module.res.oracle

 [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));
  */