tmp

Pi-Squared-Inc · Sep 20, 2024 · 7dfc09a · 7dfc09a
1 parent 161aaa0
commit 7dfc09a
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 7 deletions.
diff --git a/mx-rust-semantics/main/expression/rust-to-mx.md b/mx-rust-semantics/main/expression/rust-to-mx.md
@@ -8,6 +8,7 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
     imports private MX-COMMON-SYNTAX
     imports private MX-RUST-REPRESENTATION-CONVERSIONS
     imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-REPRESENTATION
 
     rule V:MxValue ~> rustToMx => rustToMx(V)
 
@@ -38,6 +39,9 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
     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]
 
     syntax ValueListOrError ::= ptrListToValueList(PtrListOrError, Map)  [function, total]
     rule ptrListToValueList(E:SemanticsError, _:Map) => E

diff --git a/rust-semantics/execution/let.md b/rust-semantics/execution/let.md
@@ -1,11 +1,12 @@
 ```k
 
 module RUST-LET
-    imports COMMON-K-CELL
-    imports RUST-CASTS
-    imports RUST-EXECUTION-CONFIGURATION
-    imports RUST-VALUE-SYNTAX
-    imports RUST-SHARED-SYNTAX
+    imports private COMMON-K-CELL
+    imports private RUST-CASTS
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-REPRESENTATION
+    imports private RUST-SHARED-SYNTAX
+    imports private RUST-VALUE-SYNTAX
 
     // Not all cases are implemented
     rule

diff --git a/rust-semantics/expression/assignments.md b/rust-semantics/expression/assignments.md
@@ -9,7 +9,7 @@ module RUST-EXPRESSION-ASSIGNMENTS
     rule
         <k>
             ptrValue(ptr(P:Int), _) = ptrValue(_, V:Value)
-            => ptrValue(null, ())
+            => ptrValue(null, tuple(.ValueList))
             ...
         </k>
         <values>

diff --git a/rust-semantics/expression/constants.md b/rust-semantics/expression/constants.md
@@ -6,7 +6,7 @@ module RUST-EXPRESSION-CONSTANTS
     imports private RUST-REPRESENTATION
     imports private RUST-PREPROCESSING-CONFIGURATION
 
-    rule <k> Name:Identifier::.PathExprSegments => ptrValue(null, V) ... </k>
+    rule <k> Name:Identifier => ptrValue(null, V) ... </k>
         <constant-name> Name </constant-name>
         <constant-value> V:Value </constant-value>
         requires notBool isLocalVariable(Name)