Refactor crate parsing

Pi-Squared-Inc · Oct 4, 2024 · d194889 · d194889
1 parent 8a52f7d
commit d194889
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 9 deletions.
diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md
@@ -1,9 +1,11 @@
 ```k
 
 module RUST-PREPROCESSING-SYNTAX
+    imports RUST-CRATE-LIST-SYNTAX
     imports RUST-SHARED-SYNTAX
 
-    syntax Initializer ::= crateParser(crate: Crate)
+    syntax Initializer  ::= cratesParser(crates: WrappedCrateList)
+                          | crateParser(crate: Crate)
 endmodule
 
 module RUST-PREPROCESSING-PRIVATE-SYNTAX

diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md
@@ -21,6 +21,19 @@ module RUST-COMMON-SYNTAX
   syntax Identifier ::= r"[A-Za-z_][A-Za-z0-9\\_]*"  [token]
 endmodule
 
+module RUST-CRATES-SYNTAX
+    imports RUST-COMMON-SYNTAX
+    imports RUST-CRATE-LIST-SYNTAX
+endmodule
+
+module RUST-CRATE-LIST-SYNTAX
+  syntax TypePath
+  syntax Crate
+
+  syntax WrappedCrate ::= "<(<" absolutePath: TypePath "<|>" crate: Crate ">)>"
+  syntax WrappedCrateList ::= NeList{WrappedCrate, ""}
+endmodule
+
 module RUST-SHARED-SYNTAX
   imports STRING-SYNTAX
   imports BOOL-SYNTAX

diff --git a/ukm-semantics/targets/preprocessing/configuration.md b/ukm-semantics/targets/preprocessing/configuration.md
@@ -13,10 +13,7 @@ module COMMON-K-CELL
 
     configuration
         <k>
-            crateParser($CRATE1:Crate)
-            ~> crateParser($CRATE2:Crate)
-            ~> crateParser($CRATE3:Crate)
-            ~> crateParser($CRATE4:Crate)
+            cratesParser($PGM:WrappedCrateList)
             ~> ukmPreprocessCrates
             ~> ukmEncodePreprocessedCell
         </k>

diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md
@@ -12,10 +12,7 @@ module COMMON-K-CELL
 
     configuration
         <k>
-            crateParser($CRATE1:Crate)
-            ~> crateParser($CRATE2:Crate)
-            ~> crateParser($CRATE3:Crate)
-            ~> crateParser($CRATE4:Crate)
+            cratesParser($PGM:WrappedCrateList)
             ~> $TEST:ExecutionTest
         </k>
 endmodule