Tuples and assignments

rust-semantics/error.md

@@ -0,0 +1,14 @@
+```k
+
+module RUST-ERROR
+    imports private RUST-REPRESENTATION
+
+    rule concat(V:Value, L:ValueList) => V , L
+    rule concat(_:Value, E:SemanticsError) => E
+    rule concat(E:SemanticsError, _:ValueListOrError) => E
+    rule concat(E:ValueOrError, L:ValueListOrError)
+        => error("unexpected branch (concat(ValueOrError, ValueListOrError))", ListItem(E) ListItem(L))
+        [owise]
+endmodule
+
+```

rust-semantics/expression.md

@@ -1,25 +1,31 @@
 ```k
-requires "expression/calls.md"
-requires "expression/integer-operations.md"
+requires "expression/assignments.md"
 requires "expression/blocks.md"
 requires "expression/bool-operations.md"
+requires "expression/calls.md"
 requires "expression/constants.md"
 requires "expression/casts.md"
 requires "expression/conditionals.md"
+requires "expression/expression-list.md"
+requires "expression/integer-operations.md"
 requires "expression/literals.md"
 requires "expression/references.md"
 requires "expression/struct.md"
+requires "expression/tuple.md"
 requires "expression/variables.md"
 
 module RUST-EXPRESSION
     imports private RUST-CASTS
-    imports private RUST-EXPRESSION-CALLS
-    imports private RUST-EXPRESSION-CONSTANTS
     imports private RUST-BLOCK-EXPRESSIONS
     imports private RUST-CONDITIONAL-EXPRESSIONS
+    imports private RUST-EXPRESSION-ASSIGNMENTS
+    imports private RUST-EXPRESSION-CALLS
+    imports private RUST-EXPRESSION-CONSTANTS
+    imports private RUST-EXPRESSION-EXPRESSION-LIST
     imports private RUST-EXPRESSION-LITERALS
     imports private RUST-EXPRESSION-REFERENCES
     imports private RUST-EXPRESSION-STRUCT
+    imports private RUST-EXPRESSION-TUPLE
     imports private RUST-EXPRESSION-VARIABLES
     imports private RUST-INTEGER-OPERATIONS
     imports private RUST-BOOL-OPERATIONS

rust-semantics/expression/assignments.md

@@ -0,0 +1,20 @@
+```k
+
+module RUST-EXPRESSION-ASSIGNMENTS
+    imports private COMMON-K-CELL
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-SHARED-SYNTAX
+    imports private RUST-VALUE-SYNTAX
+    rule
+        <k>
+            ptrValue(ptr(P:Int), _) = ptrValue(_, V:Value)
+            => ptrValue(null, tuple(.ValueList))
+            ...
+        </k>
+        <values>
+            Values:Map => Values[P <- V]
+        </values>
+        requires P in_keys(Values)
+endmodule
+
+```

rust-semantics/expression/expression-list.md

@@ -0,0 +1,23 @@
+```k
+
+module RUST-EXPRESSION-EXPRESSION-LIST
+    imports RUST-REPRESENTATION
+    imports RUST-VALUE-SYNTAX
+
+    rule evaluate(L:ExpressionList) => evaluate(expressionListToValueList(L))
+
+    rule isValueWithPtr(.ExpressionList) => true
+    rule isValueWithPtr(E:Expression , T:ExpressionList)
+        => isValueWithPtr(E) andBool isValueWithPtr(T)
+
+    syntax ValueListOrError ::= expressionListToValueList(ExpressionList)  [function, total]
+
+    rule expressionListToValueList(.ExpressionList) => .ValueList
+    rule expressionListToValueList(ptrValue(_, V:Value) , T:ExpressionList)
+        => concat(V , expressionListToValueList(T))
+    rule expressionListToValueList(E:Expression , T:ExpressionList)
+        => error("Unrecognized expression (expressionListToValueList)", ListItem(E) ListItem(T))
+        [owise]
+endmodule
+
+```

rust-semantics/expression/tuple.md

@@ -0,0 +1,29 @@
+```k
+
+module RUST-EXPRESSION-TUPLE
+    imports RUST-REPRESENTATION
+    imports RUST-VALUE-SYNTAX
+
+    rule ():Expression => ptrValue(null, tuple(.ValueList))
+    rule (E:Expression , ):TupleExpression
+        => tupleExpression(E , .TupleElementsNoEndComma)
+    rule (E:Expression , T:TupleElementsNoEndComma):TupleExpression
+        => tupleExpression(E , T)
+    rule (E:Expression , T:TupleElementsNoEndComma,):TupleExpression
+        => tupleExpression(E , T)
+
+    syntax Instruction ::= tupleExpression(TupleElementsNoEndComma)
+
+    rule (.K => evaluate(tupleElementsToExpressionList(Es)))
+        ~> tupleExpression(Es:TupleElementsNoEndComma)
+    rule (evaluate(L:ValueList) ~> tupleExpression(_:TupleElementsNoEndComma))
+        => ptrValue(null, tuple(L))
+
+    syntax ExpressionList ::= tupleElementsToExpressionList(TupleElementsNoEndComma)  [function, total]
+
+    rule tupleElementsToExpressionList(.TupleElementsNoEndComma) => .ExpressionList
+    rule tupleElementsToExpressionList(E:Expression , Es:TupleElementsNoEndComma)
+        => E , tupleElementsToExpressionList(Es)
+endmodule
+
+```

rust-semantics/representation.md

@@ -29,6 +29,9 @@ module RUST-VALUE-SYNTAX
     syntax ValueList ::= List{Value, ","}
     syntax ValueOrError ::= Value | SemanticsError
 
+    syntax ValueListOrError ::= ValueList | SemanticsError
+    syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError)  [function, total]
+
     syntax Ptr ::= "null" | ptr(Int)
     syntax PtrValue ::= ptrValue(Ptr, Value)
     syntax PtrValueOrError ::= PtrValue | SemanticsError
@@ -101,6 +104,10 @@ module RUST-REPRESENTATION
 
     syntax CallParamsList ::= reverse(CallParamsList, CallParamsList)  [function, total]
 
+    syntax ExpressionList ::= ".ExpressionList"
+                            | Expression "," ExpressionList  [seqstrict, result(ValueWithPtr)]
+    syntax InstructionList  ::= evaluate(ExpressionList)  [strict(1), result(ValueWithPtr)]
+                              | evaluate(ValueListOrError)
 endmodule
 
 ```

rust-semantics/rust-common.md

@@ -1,5 +1,6 @@
 ```k
 requires "config.md"
+requires "error.md"
 requires "execution.md"
 requires "expression.md"
 requires "helpers.md"
@@ -8,6 +9,7 @@ requires "representation.md"
 requires "rust-common-syntax.md"
 
 module RUST-COMMON
+  imports RUST-ERROR
   imports RUST-EXECUTION
   imports RUST-EXPRESSION
   imports RUST-HELPERS

rust-semantics/targets/preprocessing/rust.md

@@ -1,20 +1,22 @@
 ```k
 
 requires "configuration.md"
-requires "../../preprocessing.md"
-requires "../../representation.md"
+requires "../../error.md"
+requires "../../expression/bool-operations.md"
 requires "../../expression/casts.md"
 requires "../../expression/constants.md"
+requires "../../expression/integer-operations.md"
 requires "../../expression/literals.md"
+requires "../../preprocessing.md"
+requires "../../representation.md"
 requires "../../rust-common-syntax.md"
-requires "../../expression/integer-operations.md"
-requires "../../expression/bool-operations.md"
 
 module RUST-SYNTAX
     imports RUST-COMMON-SYNTAX
 endmodule
 
 module RUST
+    imports private RUST-ERROR
     imports private RUST-EXPRESSION-LITERALS
     imports private RUST-INTEGER-OPERATIONS
     imports private RUST-BOOL-OPERATIONS