Merge branch 'main' into trait-init

rust-semantics/execution/calls.md

@@ -2,10 +2,12 @@
 
 module RUST-CALLS
     imports BOOL
-    imports RUST-STACK
-    imports RUST-HELPERS
-    imports RUST-REPRESENTATION
-    imports RUST-RUNNING-CONFIGURATION
+    imports private COMMON-K-CELL
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-HELPERS
+    imports private RUST-PREPROCESSING-CONFIGURATION
+    imports private RUST-REPRESENTATION
+    imports private RUST-STACK
 
     // https://doc.rust-lang.org/stable/reference/expressions/method-call-expr.html
 

rust-semantics/execution/stack.md

@@ -1,8 +1,9 @@
 ```k
 
 module RUST-STACK
-    imports LIST
-    imports RUST-RUNNING-CONFIGURATION
+    imports private COMMON-K-CELL
+    imports private LIST
+    imports private RUST-EXECUTION-CONFIGURATION
 
     syntax Instruction  ::= "pushLocalState"
                           | "popLocalState"

rust-semantics/preprocessing/constants.md

@@ -1,8 +1,9 @@
 ```k
 module RUST-CONSTANTS
+    imports private COMMON-K-CELL
     imports private RUST-CASTS
+    imports private RUST-PREPROCESSING-CONFIGURATION
     imports private RUST-REPRESENTATION
-    imports private RUST-RUNNING-CONFIGURATION
     imports private RUST-SHARED-SYNTAX
 
     syntax KItem ::= setConstant(Identifier, ValueOrError)

rust-semantics/preprocessing/crate.md

@@ -1,12 +1,12 @@
 ```k
 
 module CRATE
+    imports private COMMON-K-CELL
     imports private LIST
     imports private MAP
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
     imports private RUST-PREPROCESSING-SYNTAX
     imports private RUST-REPRESENTATION
-    imports private RUST-RUNNING-CONFIGURATION
 
     rule crateParser
         ( (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate

rust-semantics/preprocessing/initialization.md

@@ -1,7 +1,8 @@
 ```k
 
 module INITIALIZATION
-    imports private RUST-RUNNING-CONFIGURATION
+    imports private COMMON-K-CELL
+    imports private RUST-PREPROCESSING-CONFIGURATION
     imports private RUST-PREPROCESSING-PRIVATE-HELPERS
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
 

rust-semantics/rust-common.md

@@ -13,7 +13,6 @@ module RUST-COMMON
   imports RUST-HELPERS
   imports RUST-PREPROCESSING
   imports RUST-REPRESENTATION
-  imports RUST-RUNNING-CONFIGURATION
   imports RUST-SHARED-SYNTAX
 
 endmodule

rust-semantics/targets/execution/configuration.md

@@ -1,14 +1,21 @@
 ```k
 
-module RUST-RUNNING-CONFIGURATION
-    imports private RUST-PREPROCESSING-SYNTAX
+module COMMON-K-CELL
     imports private RUST-EXECUTION-TEST-PARSING-SYNTAX
+    imports private RUST-PREPROCESSING-SYNTAX
+    
+    configuration
+        <k> crateParser($PGM:Crate) ~> $TEST:ExecutionTest </k>
+endmodule
+
+module RUST-RUNNING-CONFIGURATION
+    imports COMMON-K-CELL
     imports RUST-CONFIGURATION
     imports RUST-EXECUTION-TEST-CONFIGURATION
 
     configuration
         <rust-mx>
-            <k> crateParser($PGM:Crate) ~> $TEST:ExecutionTest </k>
+            <k/>
             <rust/>
             <rust-test/>
         </rust-mx>

rust-semantics/targets/execution/rust.md

@@ -13,6 +13,7 @@ endmodule
 module RUST
     imports RUST-COMMON
     imports RUST-EXECUTION-TEST
+    imports RUST-RUNNING-CONFIGURATION
 endmodule
 
 ```

rust-semantics/targets/preprocessing/configuration.md

@@ -1,13 +1,23 @@
 ```k
 
-module RUST-RUNNING-CONFIGURATION
+module COMMON-K-CELL
     imports private RUST-PREPROCESSING-SYNTAX
-    imports RUST-CONFIGURATION
+
+    configuration
+        <k> crateParser($PGM:Crate) </k>
+
+endmodule
+
+module RUST-RUNNING-CONFIGURATION
+    imports COMMON-K-CELL
+    imports RUST-PREPROCESSING-CONFIGURATION
 
     configuration
         <rust-mx>
-            <k> crateParser($PGM:Crate) </k>
-            <rust/>
+            <k/>
+            <rust>
+                <preprocessed/>
+            </rust>
         </rust-mx>
 endmodule
 

rust-semantics/targets/preprocessing/rust.md

@@ -1,15 +1,19 @@
 ```k
 
 requires "configuration.md"
-requires "../../rust-common.md"
+requires "../../preprocessing.md"
+requires "../../representation.md"
+requires "../../expression.md"
 requires "../../rust-common-syntax.md"
 
 module RUST-SYNTAX
     imports RUST-COMMON-SYNTAX
 endmodule
 
 module RUST
-    imports RUST-COMMON
+    imports private RUST-EXPRESSION
+    imports private RUST-PREPROCESSING
+    imports private RUST-RUNNING-CONFIGURATION
 endmodule
 
 ```

rust-semantics/test/execution.md

@@ -10,11 +10,14 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
 endmodule
 
 module RUST-EXECUTION-TEST
-    imports LIST
-    imports RUST-EXECUTION-TEST-PARSING-SYNTAX
-    imports RUST-HELPERS
-    imports RUST-REPRESENTATION
-    imports RUST-RUNNING-CONFIGURATION
+    imports private COMMON-K-CELL
+    imports private LIST
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-EXECUTION-TEST-PARSING-SYNTAX
+    imports private RUST-EXECUTION-TEST-CONFIGURATION
+    imports private RUST-HELPERS
+    imports private RUST-PREPROCESSING-CONFIGURATION
+    imports private RUST-REPRESENTATION
 
     rule E:ExecutionItem ; Es:ExecutionTest => E ~> Es
     rule .ExecutionTest => .K