Prepare for building multiple semantics targets (#11)

* Prepare for building multiple semantics targets

* Fix compilation directory

---------

Co-authored-by: Virgil Serbanuta <Virgil Serbanuta>

Makefile

@@ -1,6 +1,6 @@
 SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
-RUST_KOMPILED ::= .build/rust-kompiled
-RUST_TIMESTAMP ::= $(RUST_KOMPILED)/timestamp
+RUST_PREPROCESSING_KOMPILED ::= .build/rust-preprocessing-kompiled
+RUST_PREPROCESSING_TIMESTAMP ::= $(RUST_PREPROCESSING_KOMPILED)/timestamp
 SYNTAX_INPUT_DIR ::= tests/syntax
 SYNTAX_OUTPUT_DIR ::= .build/syntax-output
 PREPROCESSING_INPUT_DIR ::= tests/preprocessing
@@ -18,26 +18,26 @@ PREPROCESSING_STATUSES ::= $(patsubst %.rs.preprocessed.kore,%.rs.status,$(PREPR
 clean:
 	rm -r .build
 
-build: $(RUST_TIMESTAMP)
+build: $(RUST_PREPROCESSING_TIMESTAMP)
 
 test: syntax-test preprocessing-test
 
 syntax-test: $(SYNTAX_OUTPUTS)
 
 preprocessing-test: $(PREPROCESSING_OUTPUTS)
 
-$(RUST_TIMESTAMP): $(SEMANTICS_FILES)
-	$$(which kompile) rust-semantics/rust.md --emit-json -o $(RUST_KOMPILED)
+$(RUST_PREPROCESSING_TIMESTAMP): $(SEMANTICS_FILES)
+	$$(which kompile) rust-semantics/targets/preprocessing/rust.md -o $(RUST_PREPROCESSING_KOMPILED)
 
-$(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_TIMESTAMP)
+$(SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
 	mkdir -p $(SYNTAX_OUTPUT_DIR)
-	kast --definition $(RUST_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
+	kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
 
-$(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%.rs $(RUST_TIMESTAMP)
+$(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
 	mkdir -p $(PREPROCESSING_OUTPUT_DIR)
 	krun \
 		$< \
-		--definition $(RUST_KOMPILED) \
+		--definition $(RUST_PREPROCESSING_KOMPILED) \
 		--output kore \
 		--output-file $@.tmp
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"

rust-semantics/config.md

@@ -10,15 +10,4 @@ module RUST-CONFIGURATION
 
 endmodule
 
-module RUST-RUNNING-CONFIGURATION
-    imports private RUST-PREPROCESSING-SYNTAX
-    imports RUST-CONFIGURATION
-
-    configuration
-        <rust-mx>
-            <k> crateParser($PGM:Crate) </k>
-            <rust/>
-        </rust-mx>
-endmodule
-
 ```

rust-semantics/syntax.md → rust-semantics/rust-common-syntax.md

@@ -6,7 +6,7 @@ macros being already expanded. However, expanding macros on MultiversX code
 would force us to support more Rust features in the main semantics.
 
 ```k
-module RUST-SYNTAX
+module RUST-COMMON-SYNTAX
     imports RUST-SHARED-SYNTAX
 
     syntax Underscore ::= "_"  [token]
@@ -18,7 +18,7 @@ module RUST-SYNTAX
 ```k
 
   // TODO: Not implemented properly
-  syntax Identifier ::= r"[A-Za-z_][A-Za-z0-9\\_]*"  [prec(2), token]
+  syntax Identifier ::= r"[A-Za-z_][A-Za-z0-9\\_]*"  [token]
 endmodule
 
 module RUST-SHARED-SYNTAX

rust-semantics/rust.md → rust-semantics/rust-common.md

@@ -3,15 +3,15 @@ requires "config.md"
 requires "expression.md"
 requires "preprocessing.md"
 requires "representation.md"
-requires "syntax.md"
+requires "rust-common-syntax.md"
 
-module RUST
-  imports RUST-CONFIGURATION
+module RUST-COMMON
+  imports RUST-RUNNING-CONFIGURATION
   imports RUST-EXPRESSION
   imports RUST-PREPROCESSING
   imports RUST-REPRESENTATION
   imports RUST-SHARED-SYNTAX
 
 endmodule
 
-```
+```

rust-semantics/targets/preprocessing/configuration.md

@@ -0,0 +1,11 @@
+```k
+module RUST-RUNNING-CONFIGURATION
+    imports private RUST-PREPROCESSING-SYNTAX
+    imports RUST-CONFIGURATION
+    configuration
+        <rust-mx>
+            <k> crateParser($PGM:Crate) </k>
+            <rust/>
+        </rust-mx>
+endmodule
+```

rust-semantics/targets/preprocessing/rust.md

@@ -0,0 +1,13 @@
+```k
+
+requires "configuration.md"
+requires "../../rust-common.md"
+requires "../../rust-common-syntax.md"
+module RUST-SYNTAX
+    imports RUST-COMMON-SYNTAX
+endmodule
+module RUST
+    imports RUST-COMMON
+endmodule
+
+```