Use multiple crates (#145)

* Start using absolute names for items

* Use multiple crates

Makefile

@@ -19,6 +19,11 @@ PREPROCESSING_OUTPUTS ::= $(patsubst $(PREPROCESSING_INPUT_DIR)/%,$(PREPROCESSIN
 EXECUTION_INPUTS ::= $(wildcard $(EXECUTION_INPUT_DIR)/*.*.run)
 EXECUTION_OUTPUTS ::= $(patsubst $(EXECUTION_INPUT_DIR)/%,$(EXECUTION_OUTPUT_DIR)/%.executed.kore,$(EXECUTION_INPUTS))
 
+CRATES_TESTING_INPUT_DIR ::= tests/crates
+CRATES_TESTING_OUTPUT_DIR ::= .build/crates/output
+CRATES_TESTING_INPUTS ::= $(wildcard $(CRATES_TESTING_INPUT_DIR)/*.run)
+CRATES_TESTING_OUTPUTS ::= $(patsubst $(CRATES_TESTING_INPUT_DIR)/%,$(CRATES_TESTING_OUTPUT_DIR)/%.executed.kore,$(CRATES_TESTING_INPUTS))
+
 MX_SEMANTICS_FILES ::= $(shell find mx-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
 MX_TESTING_KOMPILED ::= .build/mx-testing-kompiled
 MX_TESTING_TIMESTAMP ::= $(MX_TESTING_KOMPILED)/timestamp
@@ -91,7 +96,7 @@ build-legacy: \
 		$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
 
-test: build syntax-test preprocessing-test execution-test
+test: build syntax-test preprocessing-test execution-test crates-test
 
 test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
@@ -101,6 +106,8 @@ preprocessing-test: $(PREPROCESSING_OUTPUTS)
 
 execution-test: $(EXECUTION_OUTPUTS)
 
+crates-test: $(CRATES_TESTING_OUTPUTS)
+
 mx-test: $(MX_TESTING_OUTPUTS)
 
 mx-rust-test: $(MX_RUST_TESTING_OUTPUTS)
@@ -186,13 +193,18 @@ $(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREP
 	mkdir -p $(RUST_SYNTAX_OUTPUT_DIR)
 	kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
 
-$(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
+$(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: \
+		$(PREPROCESSING_INPUT_DIR)/%.rs \
+		$(RUST_PREPROCESSING_TIMESTAMP) \
+		parsers/type-path-rust-preprocessing.sh
 	mkdir -p $(PREPROCESSING_OUTPUT_DIR)
 	krun \
 		$< \
 		--definition $(RUST_PREPROCESSING_KOMPILED) \
 		--output kore \
-		--output-file $@.tmp
+		--output-file $@.tmp \
+		-cCRATE_PATH="$(shell echo "$<" | sed 's%^.*/%%' | sed 's/.rs//' | sed 's/^/::/')" \
+		-pCRATE_PATH=$(CURDIR)/parsers/type-path-rust-preprocessing.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
 
@@ -205,10 +217,15 @@ $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \
 			parsers/contract-rust.sh \
 			parsers/test-rust.sh
 	mkdir -p $(EXECUTION_OUTPUT_DIR)
+	echo "<(<" > $@.in.tmp
+	echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/' >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
 	krun \
-		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
+		$@.in.tmp \
 		--definition $(RUST_EXECUTION_KOMPILED) \
-		--parser $(CURDIR)/parsers/contract-rust.sh \
+		--parser $(CURDIR)/parsers/crates-rust-execution.sh \
 		--output kore \
 		--output-file $@.tmp \
 		-cTEST="$(shell cat $<)" \
@@ -233,14 +250,17 @@ $(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 			$(MX_RUST_TESTING_TIMESTAMP) \
 			$(wildcard parsers/inc-*.sh) \
 			parsers/contract-mx-rust.sh \
-			parsers/test-mx-rust.sh
+			parsers/test-mx-rust.sh \
+			parsers/type-path-mx-rust.sh
 	mkdir -p $(MX_RUST_TESTING_OUTPUT_DIR)
 	krun \
 		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
 		--definition $(MX_RUST_TESTING_KOMPILED) \
 		--parser $(CURDIR)/parsers/contract-mx-rust.sh \
 		--output kore \
 		--output-file $@.tmp \
+		-cCRATE_PATH="$(shell echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/')" \
+		-pCRATE_PATH=$(CURDIR)/parsers/type-path-mx-rust.sh \
 		-cTEST='$(shell cat $<)' \
 		-pTEST=$(CURDIR)/parsers/test-mx-rust.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
@@ -320,3 +340,36 @@ $(DEMOS_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-pARGS=$(CURDIR)/parsers/args-mx-rust-contract.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
+
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(CRATES_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+			$(CRATES_TESTING_INPUT_DIR)/%.run \
+			$(CRATES_TESTING_INPUT_DIR)/crate_1.rs \
+			$(CRATES_TESTING_INPUT_DIR)/crate_2.rs \
+			$(RUST_EXECUTION_TIMESTAMP) \
+			$(wildcard parsers/inc-*.sh) \
+			parsers/crates-rust-execution.sh \
+			parsers/test-rust.sh
+	mkdir -p $(CRATES_TESTING_OUTPUT_DIR)
+	echo "<(<" > $@.in.tmp
+	echo "::crate_1" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(CRATES_TESTING_INPUT_DIR)/crate_1.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+	echo "<(<" >> $@.in.tmp
+	echo "::crate_2" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(CRATES_TESTING_INPUT_DIR)/crate_2.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+	krun \
+		$@.in.tmp \
+		--parser $(CURDIR)/parsers/crates-rust-execution.sh \
+		--definition $(RUST_EXECUTION_KOMPILED) \
+		--output kore \
+		--output-file $@.tmp \
+		-cTEST="$(shell cat $<)" \
+		-pTEST=$(CURDIR)/parsers/test-rust.sh
+	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f $@.tmp $@

mx-rust-semantics/setup/mx.md

@@ -28,7 +28,7 @@ module MX-RUST-SETUP-MX
             , args: Args:MxValueList
             )
         =>  MxRust#clearPreprocessed
-            ~> crateParser(Code)
+            ~> crateParser(Code, #token("contract", "Identifier"):Identifier)
             ~> mxRustPreprocessTraits
             ~> MxRust#addAccountWithPreprocessedCode
                 (... owner: Owner

mx-rust-semantics/targets/testing/configuration.md

@@ -8,7 +8,10 @@ module COMMON-K-CELL
     syntax MxRustTest
 
     configuration
-        <k> crateParser($PGM:Crate) ~> mxRustPreprocessTraits ~> ($TEST:MxRustTest):KItem </k>
+        <k> crateParser($PGM:Crate, $CRATE_PATH:TypePath)
+            ~> mxRustPreprocessTraits
+            ~> ($TEST:MxRustTest):KItem
+        </k>
 endmodule
 
 ```

parsers/crates-rust-execution.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-crates.sh
+
+parse_crates .build/rust-execution-kompiled $1

parsers/inc-crates.sh

@@ -0,0 +1,8 @@
+function parse_crates() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module RUST-CRATES-SYNTAX \
+        --sort WrappedCrateList \
+        $2
+}

parsers/inc-type-path.sh

@@ -0,0 +1,8 @@
+function parse_type_path() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module RUST-COMMON-SYNTAX \
+        --sort TypePath \
+        $2
+}

parsers/type-path-mx-rust.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-type-path.sh
+
+parse_type_path .build/mx-rust-testing-kompiled $1

parsers/type-path-rust-preprocessing.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-type-path.sh
+
+parse_type_path .build/rust-preprocessing-kompiled $1

parsers/type-path-rust.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-type-path.sh
+
+parse_type_path .build/rust-execution-kompiled $1

rust-semantics/conversions.md

@@ -7,6 +7,8 @@ module RUST-CONVERSIONS-SYNTAX
     syntax PtrListOrError ::= listToPtrList(List)  [function, total]
     syntax ValueListOrError ::= ptrListToValueList(PtrListOrError, Map)  [function, total]
     syntax ValueListOrError ::= callParamsToValueList(CallParamsList)  [function, total]
+    syntax PathInExpression ::= typePathToPathInExpression(TypePath)  [function, total]
+    syntax PathExprSegments ::= typePathSegmentsToPathExprSegments(TypePathSegments)  [function, total]
 endmodule
 
 module RUST-CONVERSIONS
@@ -34,6 +36,26 @@ module RUST-CONVERSIONS
     rule callParamsToValueList(L:CallParamsList)
         => error("callParamsToValueList: Unexpected value", ListItem(L))
         [owise]
+
+    rule typePathToPathInExpression(S:TypePathSegments)
+        => typePathSegmentsToPathExprSegments(S)
+    rule typePathToPathInExpression(:: S:TypePathSegments)
+        => :: typePathSegmentsToPathExprSegments(S)
+
+    rule typePathSegmentsToPathExprSegments(S:PathIdentSegment)
+        => S
+    rule typePathSegmentsToPathExprSegments(S:PathIdentSegment A:GenericArgs)
+        => S :: A
+    rule typePathSegmentsToPathExprSegments(S:PathIdentSegment :: A:GenericArgs)
+        => S :: A
+
+    rule typePathSegmentsToPathExprSegments(S:PathIdentSegment :: Ss:TypePathSegments)
+        => S :: typePathSegmentsToPathExprSegments(Ss)
+    rule typePathSegmentsToPathExprSegments(S:PathIdentSegment A:GenericArgs :: Ss:TypePathSegments)
+        => S :: A :: typePathSegmentsToPathExprSegments(Ss)
+    rule typePathSegmentsToPathExprSegments(S:PathIdentSegment :: A:GenericArgs :: Ss:TypePathSegments)
+        => S :: A :: typePathSegmentsToPathExprSegments(Ss)
+
 endmodule
 
 ```

rust-semantics/expression/constants.md

@@ -6,10 +6,14 @@ module RUST-EXPRESSION-CONSTANTS
     imports private RUST-REPRESENTATION
     imports private RUST-PREPROCESSING-CONFIGURATION
 
-    rule <k> Name:Identifier => ptrValue(null, V) ... </k>
+    rule <k> Name:PathInExpression => ptrValue(null, V) ... </k>
         <constant-name> Name </constant-name>
         <constant-value> V:Value </constant-value>
-        requires notBool isLocalVariable(Name)
+
+    // rule <k> Name:Identifier => ptrValue(null, V) ... </k>
+    //     <constant-name> Name </constant-name>
+    //     <constant-value> V:Value </constant-value>
+    //     requires notBool isLocalVariable(Name)
 
     rule [[isConstant(Name:Identifier) => true]]
         <constant-name> Name </constant-name>

rust-semantics/full-preprocessing.md

@@ -1,5 +1,6 @@
 ```k
 
+requires "conversions.md"
 requires "error.md"
 requires "expression/bool-operations.md"
 requires "expression/casts.md"
@@ -12,6 +13,7 @@ requires "rust-common-syntax.md"
 
 module RUST-FULL-PREPROCESSING
     imports private RUST-BOOL-OPERATIONS
+    imports private RUST-CONVERSIONS
     imports private RUST-ERROR
     imports private RUST-EXPRESSION-CONSTANTS
     imports private RUST-EXPRESSION-LITERALS

rust-semantics/helpers.md

@@ -20,7 +20,7 @@ module RUST-HELPERS
     rule isSameType(u16(_), u16) => true
     rule isSameType(i8(_), i8) => true
     rule isSameType(u8(_), u8) => true
-    rule isSameType(struct(T, _), T:Type) => true
+    rule isSameType(struct(T, _), T:TypePath) => true
     rule isSameType(struct(T, _), T:Identifier _:GenericArgs ) => true
 
 endmodule

rust-semantics/preprocessing/configuration.md

@@ -10,7 +10,7 @@ module RUST-PREPROCESSING-CONFIGURATION
         <preprocessed>
             <constants>
                 <constant multiplicity="*" type="Map">
-                    <constant-name> .Identifier </constant-name>
+                    <constant-name> .PathInExpression </constant-name>
                     <constant-value> tuple(.ValueList) </constant-value>
                 </constant>
             </constants>

rust-semantics/preprocessing/constants.md

@@ -2,24 +2,31 @@
 module RUST-CONSTANTS
     imports private COMMON-K-CELL
     imports private RUST-CASTS
+    imports private RUST-CONVERSIONS-SYNTAX
     imports private RUST-PREPROCESSING-CONFIGURATION
+    imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
     imports private RUST-REPRESENTATION
     imports private RUST-SHARED-SYNTAX
 
-    syntax KItem ::= setConstant(Identifier, ValueOrError)
+    syntax KItem ::= setConstant(TypePath, ValueOrError)
+
+    rule isKResult((const _:Identifier : _T:Type = ptrValue(_, _);):ConstantItem:KItem) => true
 
     rule
-        (const Name:Identifier : T:Type = ptrValue(_, V:Value);):ConstantItem:KItem
-        => setConstant(Name, implicitCast(V, T))
+        constantParser
+            ( const Name:Identifier : T:Type = ptrValue(_, V:Value);
+            , ParentPath:TypePath
+            )
+        => setConstant(append(ParentPath, Name), implicitCast(V, T))
 
     rule
         <k>
-            setConstant(Name, V:Value) => .K
+            setConstant(Path, V:Value) => .K
             ...
         </k>
         <constants>
             .Bag => <constant>
-                <constant-name> Name </constant-name>
+                <constant-name> typePathToPathInExpression(Path) </constant-name>
                 <constant-value> V </constant-value>
             </constant>
             ...

rust-semantics/preprocessing/crate.md

@@ -8,28 +8,37 @@ module CRATE
     imports private RUST-PREPROCESSING-SYNTAX
     imports private RUST-REPRESENTATION
 
+    rule cratesParser(.WrappedCrateList) => .K
+    rule cratesParser(<(< Path:TypePath <|> Crate:Crate >)> Crates:WrappedCrateList)
+        => crateParser(Crate, Path) ~> cratesParser(Crates)
+
     rule crateParser
         ( (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate
           => (.InnerAttributes Is):Crate
+        , _:TypePath
         )
-    rule (.K => moduleParser(M))
+    rule (.K => moduleParser(M, CratePath))
         ~> crateParser
           ( (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _V:MaybeVisibility M:Module):Item Is:Items):Crate
             => (.InnerAttributes Is):Crate
+          , CratePath:TypePath
           )
     rule
-        (.K => traitParser(T, .TypePath, ItemAtts))
+        (.K => traitParser(T, CratePath, ItemAtts))
         ~> crateParser
           ( (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate
             => (.InnerAttributes Is):Crate
+          , CratePath:TypePath
           )
-    rule (.K => CI:ConstantItem:KItem)
+    rule (.K => constantParser(CI:ConstantItem, CratePath))
         ~> crateParser
           ( (Atts:InnerAttributes (_ItemAtts:OuterAttributes _:MaybeVisibility CI:ConstantItem):Item Is:Items):Crate
             => (Atts Is):Crate
+          , CratePath:TypePath
           )
 
-    rule crateParser( (_Atts:InnerAttributes .Items):Crate) => .K
+    rule crateParser( (_Atts:InnerAttributes .Items):Crate, _Path:TypePath)
+        => .K //resolveCrateNames(Path)
 endmodule
 
 ```

rust-semantics/preprocessing/module.md

@@ -3,8 +3,11 @@
 module RUST-MODULE
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
 
-    rule moduleParser(mod Name:Identifier { _:InnerAttributes Contents:Items })
-        => moduleItemsParser(Contents, Name)
+    rule moduleParser
+            ( mod Name:Identifier { _:InnerAttributes Contents:Items }
+            , ParentPath:TypePath
+            )
+        => moduleItemsParser(Contents, append(ParentPath, Name))
 
     rule moduleItemsParser(.Items, _Name) => .K
     rule

rust-semantics/preprocessing/syntax.md

@@ -5,7 +5,7 @@ module RUST-PREPROCESSING-SYNTAX
     imports RUST-SHARED-SYNTAX
 
     syntax Initializer  ::= cratesParser(crates: WrappedCrateList)
-                          | crateParser(crate: Crate)
+                          | crateParser(crate: Crate, crateModule: TypePath)
 endmodule
 
 module RUST-PREPROCESSING-PRIVATE-SYNTAX
@@ -14,17 +14,16 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
     imports RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
 
-    syntax MaybeTypePath ::= ".TypePath" | TypePath
-
     syntax Initializer  ::= traitParser(Trait, MaybeTypePath, OuterAttributes)
                           | traitMethodsParser(AssociatedItems, traitName:TypePath)
                           | traitInitializer
                                 ( traitName: TypePath
                                 , atts: OuterAttributes
                                 )
-    syntax Initializer  ::= moduleParser(Module)
+    syntax Initializer  ::= moduleParser(Module, TypePath)
                           | moduleItemsParser(Items, TypePath)
-
+                          | constantParser(ConstantItem, TypePath)  [strict(1)]
+                          | resolveCrateNames(TypePath)
 
     syntax Initializer  ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes)
                           | #addMethod(