Properly implement expression/statement results

rust-semantics/execution.md

@@ -3,16 +3,18 @@
 requires "execution/configuration.md"
 requires "execution/block.md"
 requires "execution/calls.md"
+requires "execution/expression.md"
 requires "execution/let.md"
 requires "execution/stack.md"
 requires "execution/statements.md"
 
 module RUST-EXECUTION
-    imports RUST-BLOCK
-    imports RUST-CALLS
-    imports RUST-LET
-    imports RUST-STACK
-    imports RUST-STATEMENTS
+    imports private RUST-BLOCK
+    imports private RUST-CALLS
+    imports private RUST-STATEMENT-EXPRESSION
+    imports private RUST-LET
+    imports private RUST-STACK
+    imports private RUST-STATEMENTS
 endmodule
 
 ```

rust-semantics/execution/expression.md

@@ -0,0 +1,14 @@
+```k
+
+module RUST-STATEMENT-EXPRESSION
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+
+    syntax Instruction ::= "clearValue"
+
+    rule E:Expression ; => (E ~> clearValue)
+    rule (_:PtrValue ~> clearValue) => .K
+    rule clearValue => .K
+endmodule
+
+```

rust-semantics/execution/statements.md

@@ -1,11 +1,16 @@
 ```k
 
 module RUST-STATEMENTS
-    imports RUST-SHARED-SYNTAX
+    imports private RUST-SHARED-SYNTAX
+    imports private RUST-VALUE-SYNTAX
 
-    rule Nes:NonEmptyStatements E:Expression => Nes ~> E
-    rule S:Statement Ss:NonEmptyStatements => S ~> Ss
-    rule .NonEmptyStatements => .K
+    syntax K ::= statementsToK(NonEmptyStatements)  [function, total]
+    rule statementsToK(.NonEmptyStatements) => .K
+    rule statementsToK(S:Statement Ss:NonEmptyStatements)
+        => S ~> statementsToK(Ss)
+
+    rule Nes:NonEmptyStatements E:Expression => statementsToK(Nes) ~> E
+    rule Ss:NonEmptyStatements => statementsToK(Ss) ~> ptrValue(null, tuple(.ValueList))
 endmodule
 
 ```

rust-semantics/expression.md

@@ -9,6 +9,7 @@ requires "expression/conditionals.md"
 requires "expression/literals.md"
 requires "expression/references.md"
 requires "expression/struct.md"
+requires "expression/tuple.md"
 requires "expression/variables.md"
 
 module RUST-EXPRESSION
@@ -21,6 +22,7 @@ module RUST-EXPRESSION
     imports private RUST-EXPRESSION-REFERENCES
     imports private RUST-EXPRESSION-STRUCT
     imports private RUST-EXPRESSION-VARIABLES
+    imports private RUST-EXPRESSION-TUPLE
     imports private RUST-INTEGER-OPERATIONS
     imports private RUST-BOOL-OPERATIONS
 endmodule

rust-semantics/expression/casts.md

@@ -38,6 +38,8 @@ module RUST-CASTS
 
     rule implicitCast(V:Bool, bool) => V
 
+    rule implicitCast(tuple(.ValueList) #as V, ():Type) => V
+
     rule implicitCast(struct(T, _) #as V, T) => V
     rule implicitCast(struct(T, _) #as V, T < _ >) => V
 

rust-semantics/expression/tuple.md

@@ -0,0 +1,10 @@
+```k
+
+module RUST-EXPRESSION-TUPLE
+    imports RUST-REPRESENTATION
+    imports RUST-VALUE-SYNTAX
+
+    rule ():Expression => ptrValue(null, tuple(.ValueList))
+
+endmodule
+```

tests/execution/if-expressions.5.run

@@ -1,2 +1,4 @@
 new IfExpressions;
-call IfExpressions.test_if_no_return
+call IfExpressions.test_if_no_return;
+return_value;
+check_eq ()