External blocks

rust-semantics/preprocessing.md

@@ -3,6 +3,7 @@
 requires "preprocessing/constants.md"
 requires "preprocessing/crate.md"
 requires "preprocessing/configuration.md"
+requires "preprocessing/extern-block.md"
 requires "preprocessing/functions.md"
 requires "preprocessing/helpers.md"
 requires "preprocessing/initialization.md"
@@ -17,6 +18,7 @@ module RUST-PREPROCESSING
     imports private INITIALIZATION
     imports private RUST-CONSTANTS
     imports private RUST-MODULE
+    imports private RUST-PREPROCESSING-EXTERN-BLOCK
     imports private RUST-PREPROCESSING-FUNCTIONS
     imports private RUST-PREPROCESSING-TOOLS
     imports private TRAIT

rust-semantics/preprocessing/crate.md

@@ -42,6 +42,12 @@ module CRATE
             => (Atts Is):Crate
           , CratePath:TypePath
           )
+    rule (.K => externBlockParser(Block, CratePath))
+        ~> crateParser
+          ( (Atts:InnerAttributes (_ItemAtts:OuterAttributes _:MaybeVisibility Block:ExternBlock):Item Is:Items):Crate
+            => (Atts Is):Crate
+          , CratePath:TypePath
+          )
 
     rule crateParser( (_Atts:InnerAttributes .Items):Crate, _Path:TypePath)
         => .K //resolveCrateNames(Path)

rust-semantics/preprocessing/extern-block.md

@@ -0,0 +1,25 @@
+```k
+
+module RUST-PREPROCESSING-EXTERN-BLOCK
+    imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
+
+    rule externBlockParser
+            ( _:MaybeUnsafe extern _:MaybeAbi { .InnerAttributes .ExternalItems }
+            , _Parent:TypePath
+            )
+        => .K
+
+    rule externBlockParser
+            ( _:MaybeUnsafe extern _:MaybeAbi
+                  { .InnerAttributes
+                      (Atts:OuterAttributes _:MaybeVisibility Fn:Function)
+                      Items:ExternalItems
+                  }
+            , Parent:TypePath
+            )
+        => functionParser(Fn, Parent, Atts)
+            ~> externBlockParser(extern {.InnerAttributes Items}, Parent)
+
+endmodule
+
+```

rust-semantics/preprocessing/syntax.md

@@ -24,6 +24,7 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
                           | moduleItemsParser(Items, TypePath)
                           | constantParser(ConstantItem, TypePath)  [strict(1)]
                           | functionParser(Function, TypePath, OuterAttributes)
+                          | externBlockParser(ExternBlock, TypePath)
                           | resolveCrateNames(TypePath)
 
     syntax Initializer  ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes)

rust-semantics/rust-common-syntax.md

@@ -180,6 +180,9 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
   syntax TypeOrDots ::= Type
   syntax FunctionReturnType ::= "->" Type
 
+  syntax Abi ::= StringLiteral | RawStringLiteral
+  syntax MaybeAbi ::= "" | Abi
+
 ```
   https://doc.rust-lang.org/reference/items/type-aliases.html
 
@@ -259,7 +262,11 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 
 ```k
 
-  syntax ExternBlock ::= "TODO: not needed yet, not implementing"
+  syntax ExternBlock ::= MaybeUnsafe "extern" MaybeAbi "{" InnerAttributes ExternalItems "}"
+  syntax ExternalItems ::= List{ExternalItem, ""}
+  syntax ExternalItem ::= OuterAttributes MacroInvocationSemi
+                        | OuterAttributes MaybeVisibility StaticItem
+                        | OuterAttributes MaybeVisibility Function
 
 ```
 

tests/preprocessing/extern_block.rs

@@ -0,0 +1,20 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait Empty {
+    #[init]
+    fn init(&self) {
+    }
+
+    #[upgrade]
+    fn upgrade(&self) {}
+
+}
+
+extern "C" {
+  fn f();
+  fn g(V:u64) -> u64;
+}