Rename cast -> implicitCast

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

Hide file tree

Showing 5 changed files with 31 additions and 31 deletions.
diff --git a/rust-semantics/execution/calls.md b/rust-semantics/execution/calls.md
@@ -24,7 +24,7 @@ module RUST-CALLS
                 ~> clearLocalState
                 ~> setArgs(Args, Params)
                 ~> FunctionBody
-                ~> castTo(ReturnType)
+                ~> implicitCastTo(ReturnType)
                 ~> popLocalState
             ...
         </k>

diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md
@@ -3,44 +3,44 @@
 module RUST-CASTS
     imports private RUST-REPRESENTATION
 
-    syntax ValueOrError ::= cast(Value, Type)  [function, total]
+    syntax ValueOrError ::= implicitCast(Value, Type)  [function, total]
 
-    rule cast(V:Value, T:Type) => error("Unknown cast.", ListItem(V) ListItem(T))
+    rule implicitCast(V:Value, T:Type) => error("Unknown implicitCast.", ListItem(V) ListItem(T))
         [owise]
 
-    // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-cast
+    // https://doc.rust-lang.org/stable/reference/expressions/operator-expr.html#numeric-implicitCast
 
-    rule cast(i32(Value), i32) => i32(Value)
-    rule cast(i32(Value), u32) => u32(Value)
-    rule cast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value)))
-    rule cast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i32(Value), i32) => i32(Value)
+    rule implicitCast(i32(Value), u32) => u32(Value)
+    rule implicitCast(i32(Value), i64) => i64(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i32(Value), u64) => u64(Int2MInt(MInt2Signed(Value)))
 
-    rule cast(u32(Value), i32) => i32(Value)
-    rule cast(u32(Value), u32) => u32(Value)
-    rule cast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
-    rule cast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u32(Value), i32) => i32(Value)
+    rule implicitCast(u32(Value), u32) => u32(Value)
+    rule implicitCast(u32(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u32(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
 
-    rule cast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value)))
-    rule cast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value)))
-    rule cast(i64(Value), i64) => i64(Value)
-    rule cast(i64(Value), u64) => u64(Value)
+    rule implicitCast(i64(Value), i32) => i32(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i64(Value), u32) => u32(Int2MInt(MInt2Signed(Value)))
+    rule implicitCast(i64(Value), i64) => i64(Value)
+    rule implicitCast(i64(Value), u64) => u64(Value)
 
-    rule cast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
-    rule cast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
-    rule cast(u64(Value), i64) => i64(Value)
-    rule cast(u64(Value), u64) => u64(Value)
+    rule implicitCast(u64(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u64(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u64(Value), i64) => i64(Value)
+    rule implicitCast(u64(Value), u64) => u64(Value)
 
-    rule cast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
-    rule cast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
-    rule cast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
-    rule cast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u128(Value), i32) => i32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u128(Value), u32) => u32(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u128(Value), i64) => i64(Int2MInt(MInt2Unsigned(Value)))
+    rule implicitCast(u128(Value), u64) => u64(Int2MInt(MInt2Unsigned(Value)))
 
     // Rewrites
 
-    rule V:Value ~> castTo(T:Type) => cast(V, T)
+    rule V:Value ~> implicitCastTo(T:Type) => implicitCast(V, T)
     // We don't need a value for the unit type
-    rule castTo(( )) => .K
+    rule implicitCastTo(( )) => .K
 
 endmodule
 

diff --git a/rust-semantics/preprocessing/constants.md b/rust-semantics/preprocessing/constants.md
@@ -10,7 +10,7 @@ module RUST-CONSTANTS
 
     rule
         (const Name:Identifier : T:Type = V:Value;):ConstantItem:KItem
-        => setConstant(Name, cast(V, T))
+        => setConstant(Name, implicitCast(V, T))
 
     rule
         <k>

diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
@@ -44,7 +44,7 @@ module RUST-REPRESENTATION
     syntax NormalizedCallParams ::=List{Int, ","}
 
     syntax Instruction  ::= normalizedMethodCall(TypePath, Identifier, NormalizedCallParams)
-                          | castTo(Type)
+                          | implicitCastTo(Type)
 
     syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
 

diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md
@@ -454,7 +454,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 
 ```
 
-  https://doc.rust-lang.org/reference/expressions/operator-expr.html#type-cast-expressions
+  https://doc.rust-lang.org/reference/expressions/operator-expr.html#type-implicitCast-expressions
 
 ```k
 
@@ -952,15 +952,15 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
   //
   // As an example, this means that you can't simply write
   //
-  // rule cast(u64(Value), u64) => u64(Value)
+  // rule implicitCast(u64(Value), u64) => u64(Value)
   //
   // because that rule will compile just fine, but it will never apply at
   // runtime because it uses an injection (why??? there is no injection
   // available!), while the parser will produce actual TypePathSegments lists
   // (the K rule will also produce lists from `u64` sometimes, I'm not yet sure
   // when). Instead, you need to write
   //
-  // rule cast(u64(Value), u64 :: .TypePathSegments) => u64(Value)
+  // rule implicitCast(u64(Value), u64 :: .TypePathSegments) => u64(Value)
   //
   // which will work, but you have to figure out all cases where this may happen
   // without any help from the compiler.