Properly implement expression/statement results (#94)

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

@@ -27,6 +27,7 @@ module RUST-EXPRESSION
     imports private RUST-EXPRESSION-STRUCT
     imports private RUST-EXPRESSION-TUPLE
     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
 

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 ()