From 3853f9b9ba4cddcbc5f31f92f854d5484f1e8fe8 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Tue, 27 Aug 2024 09:18:12 +0300
Subject: [PATCH] Make the Rust config more modular (#61)

* Import only the configuration parts that are strictly needed.

* Filter preprocessing imports
---
 rust-semantics/execution/calls.md              | 10 ++++++----
 rust-semantics/execution/stack.md              |  5 +++--
 rust-semantics/preprocessing/constants.md      |  3 ++-
 rust-semantics/preprocessing/crate.md          |  2 +-
 rust-semantics/preprocessing/initialization.md |  3 ++-
 rust-semantics/rust-common.md                  |  1 -
 .../targets/execution/configuration.md         | 13 ++++++++++---
 rust-semantics/targets/execution/rust.md       |  1 +
 .../targets/preprocessing/configuration.md     | 18 ++++++++++++++----
 rust-semantics/targets/preprocessing/rust.md   |  8 ++++++--
 rust-semantics/test/execution.md               | 13 ++++++++-----
 11 files changed, 53 insertions(+), 24 deletions(-)

diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md
index a106844..7ea8177 100644
--- a/rust-semantics/execution/calls.md
+++ b/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
 
diff --git a/rust-semantics/execution/stack.md b/rust-semantics/execution/stack.md
index 8652a1f..c01475f 100644
--- a/rust-semantics/execution/stack.md
+++ b/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"
diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md
index 43fbcd7..db7a118 100644
--- a/rust-semantics/preprocessing/constants.md
+++ b/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)
diff --git a/rust-semantics/preprocessing/crate.md b/rust-semantics/preprocessing/crate.md
index a305429..66d5e3b 100644
--- a/rust-semantics/preprocessing/crate.md
+++ b/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
 
     syntax Initializer  ::= crateParser(crate: Crate, traitName: MaybeIdentifier, traitFunctions: Map)
 
diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md
index e35e93d..2e4ff58 100644
--- a/rust-semantics/preprocessing/initialization.md
+++ b/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
 
diff --git a/rust-semantics/rust-common.md b/rust-semantics/rust-common.md
index 41c1abc..ecacecc 100644
--- a/rust-semantics/rust-common.md
+++ b/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
diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md
index 27781ab..e5f0d55 100644
--- a/rust-semantics/targets/execution/configuration.md
+++ b/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>
diff --git a/rust-semantics/targets/execution/rust.md b/rust-semantics/targets/execution/rust.md
index d6a0c33..d051f5f 100644
--- a/rust-semantics/targets/execution/rust.md
+++ b/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
 
 ```
\ No newline at end of file
diff --git a/rust-semantics/targets/preprocessing/configuration.md b/rust-semantics/targets/preprocessing/configuration.md
index 9238cbf..d122260 100644
--- a/rust-semantics/targets/preprocessing/configuration.md
+++ b/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
 
diff --git a/rust-semantics/targets/preprocessing/rust.md b/rust-semantics/targets/preprocessing/rust.md
index ca5122a..0390e57 100644
--- a/rust-semantics/targets/preprocessing/rust.md
+++ b/rust-semantics/targets/preprocessing/rust.md
@@ -1,7 +1,9 @@
 ```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
@@ -9,7 +11,9 @@ module RUST-SYNTAX
 endmodule
 
 module RUST
-    imports RUST-COMMON
+    imports private RUST-EXPRESSION
+    imports private RUST-PREPROCESSING
+    imports private RUST-RUNNING-CONFIGURATION
 endmodule
 
 ```
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index 77e6021..7d92941 100644
--- a/rust-semantics/test/execution.md
+++ b/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