Cast the returned value to the right type

Pi-Squared-Inc · Aug 27, 2024 · 94beb83 · 94beb83
1 parent a992543
commit 94beb83
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 1 deletion.
diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md
@@ -24,12 +24,14 @@ module RUST-CALLS
                 ~> clearLocalState
                 ~> setArgs(Args, Params)
                 ~> FunctionBody
+                ~> castTo(ReturnType)
                 ~> popLocalState
             ...
         </k>
         <trait-path> TraitName </trait-path>
         <method-name> MethodName </method-name>
         <method-params> Params:NormalizedFunctionParameterList </method-params>
+        <method-return-type> ReturnType:Type </method-return-type>
         <method-implementation> block(FunctionBody) </method-implementation>
 
     rule

diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md
@@ -36,6 +36,12 @@ module RUST-CASTS
     rule cast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
     rule cast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
+    // Rewrites
+
+    rule V:Value ~> castTo(T:Type) => cast(V, T)
+    // We don't need a value for the unit type
+    rule castTo(( )) => .K
+
 endmodule
 
 ```
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
@@ -43,7 +43,8 @@ module RUST-REPRESENTATION
 
     syntax NormalizedCallParams ::=List{Int, ","}
 
-    syntax Instruction ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams)
+    syntax Instruction  ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams)
+                          | castTo(Type)
 
     syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError