tmp

mx-rust-semantics/main/expression/rust-to-mx.md

@@ -7,6 +7,7 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
     imports private MAP
     imports private MX-COMMON-SYNTAX
     imports private MX-RUST-REPRESENTATION-CONVERSIONS
+    imports private RUST-CONVERSIONS-SYNTAX
     imports private RUST-EXECUTION-CONFIGURATION
     imports private RUST-REPRESENTATION
 
@@ -26,34 +27,6 @@ module MX-RUST-EXPRESSION-RUST-TO-MX
     rule rustToMx(S:String => mxStringValue(S))
     rule rustToMx(tuple(V:ValueList)) => rustValuesToMxListValue(V, .MxValueList)
 
-    syntax PtrListOrError ::= concat(Ptr, PtrListOrError)  [function, total]
-    rule concat(P:Ptr, L:PtrList) => P , L
-    rule concat(_:Ptr, E:SemanticsError) => E
-
-    syntax PtrListOrError ::= listToPtrList(List)  [function, total]
-    rule listToPtrList(.List) => .PtrList
-    rule listToPtrList(ListItem(P:Int) L:List) => concat(ptr(P), listToPtrList(L))
-    rule listToPtrList(L:List) => error("Unrecognized element (listToPtrList)", L)
-        [owise]
-
-    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
-    rule ptrListToValueList(.PtrList, _:Map) => .ValueList
-    rule ptrListToValueList((ptr(P:Int) , Ps:PtrList), M:Map)
-        => concat({M[P:Int:KItem]}:>Value, ptrListToValueList(Ps, M:Map))
-        requires P:Int:KItem in_keys(M) andBool isValue(M[P:Int:KItem] orDefault 0)
-        [preserves-definedness]
-    rule ptrListToValueList(Ps:PtrList, M:Map)
-        => error("element not in map or wrong value type (ptrListToValueList)", ListItem(Ps) ListItem(M))
-        [owise]
-
     syntax RustMxInstruction ::= rustValuesToMxListValue(ValueListOrError, MxValueList)
     rule rustValuesToMxListValue(.ValueList, L:MxValueList)
         => rustToMx(mxListValue(reverse(L, .MxValueList)))

mx-rust-semantics/main/preprocessing/methods.md

@@ -278,6 +278,8 @@ module MX-RUST-PREPROCESSING-METHODS
               S . #token("return_type", "Identifier") = ptrValue(null, ReturnType);
               S
             }
+
+    // TODO: Move this to the Rust semantics
     syntax MaybeTupleElements ::= paramsToMaybeTupleElements(NormalizedFunctionParameterList)  [function, total]
     rule paramsToMaybeTupleElements(.NormalizedFunctionParameterList) => `noTupleElements`(.KList)
     rule paramsToMaybeTupleElements(Name:Identifier : _ , .NormalizedFunctionParameterList)

mx-rust-semantics/main/representation.md

@@ -33,12 +33,10 @@ module MX-RUST-REPRESENTATION
     syntax MxRustTypeOrError ::= MxRustType | SemanticsError
     syntax Value ::= MxRustType
 
-    syntax SemanticsError ::= unknownMxRustType(GenericArg)
-
     syntax Expression ::= concatString(Expression, Expression)  [seqstrict]
                         | toString(Expression)  [strict]
                         | rawValue(Value)
-                        | SemanticsError
+                        | SemanticsError  // TODO: Remove.
 
     syntax MxValue ::= rustDestination(Int, MxRustType)
 

rust-semantics/conversions.md

@@ -0,0 +1,32 @@
+```k
+
+module RUST-CONVERSIONS-SYNTAX
+    imports LIST
+    imports RUST-REPRESENTATION
+
+    syntax PtrListOrError ::= listToPtrList(List)  [function, total]
+    syntax ValueListOrError ::= ptrListToValueList(PtrListOrError, Map)  [function, total]
+endmodule
+
+module RUST-CONVERSIONS
+    imports private RUST-CONVERSIONS-SYNTAX
+    imports private RUST-ERROR-SYNTAX
+
+    rule listToPtrList(.List) => .PtrList
+    rule listToPtrList(ListItem(P:Int) L:List) => concat(ptr(P), listToPtrList(L))
+    rule listToPtrList(L:List) => error("Unrecognized element (listToPtrList)", L)
+        [owise]
+
+    rule ptrListToValueList(E:SemanticsError, _:Map) => E
+    rule ptrListToValueList(.PtrList, _:Map) => .ValueList
+    rule ptrListToValueList((ptr(P:Int) , Ps:PtrList), M:Map)
+        => concat({M[P:Int:KItem]}:>Value, ptrListToValueList(Ps, M:Map))
+        requires P:Int:KItem in_keys(M) andBool isValue(M[P:Int:KItem] orDefault 0)
+        [preserves-definedness]
+    rule ptrListToValueList(Ps:PtrList, M:Map)
+        => error("element not in map or wrong value type (ptrListToValueList)", ListItem(Ps) ListItem(M))
+        [owise]
+
+endmodule
+
+```

rust-semantics/error.md

@@ -0,0 +1,28 @@
+```k
+
+module RUST-ERROR-SYNTAX
+    imports RUST-REPRESENTATION
+
+    syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError)  [function, total]
+    syntax PtrListOrError ::= concat(Ptr, PtrListOrError)  [function, total]
+    syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError)  [function, total]
+endmodule
+
+module RUST-ERROR
+    imports private RUST-ERROR-SYNTAX
+
+    rule concat(P:Ptr, L:PtrList) => P , L
+    rule concat(_:Ptr, E:SemanticsError) => E
+
+    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]
+
+    rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V)
+    rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E
+endmodule
+
+```

rust-semantics/execution/expression.md

@@ -1,13 +1,14 @@
 ```k
 
 module RUST-STATEMENT-EXPRESSION
-    imports RUST-REPRESENTATION
-    imports RUST-SHARED-SYNTAX
+    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/casts.md

@@ -1,6 +1,7 @@
 ```k
 
 module RUST-CASTS
+    imports private RUST-ERROR-SYNTAX
     imports private RUST-REPRESENTATION
 
     rule implicitCast(V:Value, T:Type) => error("Unknown implicitCast.", ListItem(V) ListItem(T))

rust-semantics/expression/expression-list.md

@@ -1,8 +1,9 @@
 ```k
 
 module RUST-EXPRESSION-EXPRESSION-LIST
-    imports RUST-REPRESENTATION
-    imports RUST-VALUE-SYNTAX
+    imports private RUST-ERROR-SYNTAX
+    imports private RUST-REPRESENTATION
+    imports private RUST-VALUE-SYNTAX
 
     rule evaluate(L:ExpressionList) => evaluate(expressionListToValueList(L))
 

rust-semantics/expression/literals.md

@@ -4,12 +4,13 @@ module RUST-EXPRESSION-LITERALS
 endmodule
 
 module RUST-EXPRESSION-INTEGER-LITERALS
-    imports BOOL
-    imports INT
-    imports K-EQUAL-SYNTAX
-    imports STRING
+    imports private BOOL
+    imports private INT
+    imports private K-EQUAL-SYNTAX
+    imports private STRING
+    imports private RUST-ERROR-SYNTAX
     imports private RUST-REPRESENTATION
-    imports RUST-SHARED-SYNTAX
+    imports private RUST-SHARED-SYNTAX
 
     // https://doc.rust-lang.org/stable/reference/expressions/literal-expr.html#integer-literal-expressions
     // https://doc.rust-lang.org/stable/reference/tokens.html#number-literals

rust-semantics/representation.md

@@ -30,19 +30,13 @@ module RUST-VALUE-SYNTAX
     syntax ValueList ::= List{Value, ","}
     syntax ValueListOrError ::= ValueList | SemanticsError
 
-    syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError)  [function, total]
-
     syntax Ptr ::= "null" | ptr(Int)
     syntax PtrValue ::= ptrValue(Ptr, Value)
     syntax PtrValueOrError ::= PtrValue | SemanticsError
 
     syntax Expression ::= PtrValue
     syntax KResult ::= PtrValue
 
-    syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError)  [function, total]
-    rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V)
-    rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E
-
     syntax Bool ::= mayBeDefaultTypedInt(Value)  [function, total]
     rule mayBeDefaultTypedInt(_V) => false  [owise]
     rule mayBeDefaultTypedInt(u128(_)) => true

rust-semantics/rust-common.md

@@ -1,5 +1,7 @@
 ```k
 requires "config.md"
+requires "conversions.md"
+requires "error.md"
 requires "execution.md"
 requires "expression.md"
 requires "helpers.md"
@@ -8,6 +10,8 @@ requires "representation.md"
 requires "rust-common-syntax.md"
 
 module RUST-COMMON
+  imports RUST-CONVERSIONS
+  imports RUST-ERROR
   imports RUST-EXECUTION
   imports RUST-EXPRESSION
   imports RUST-HELPERS

rust-semantics/targets/preprocessing/rust.md

@@ -1,24 +1,26 @@
 ```k
 
 requires "configuration.md"
-requires "../../preprocessing.md"
-requires "../../representation.md"
+requires "../../error.md"
+requires "../../expression/bool-operations.md"
 requires "../../expression/casts.md"
 requires "../../expression/constants.md"
+requires "../../expression/integer-operations.md"
 requires "../../expression/literals.md"
+requires "../../preprocessing.md"
+requires "../../representation.md"
 requires "../../rust-common-syntax.md"
-requires "../../expression/integer-operations.md"
-requires "../../expression/bool-operations.md"
 
 module RUST-SYNTAX
     imports RUST-COMMON-SYNTAX
 endmodule
 
 module RUST
-    imports private RUST-EXPRESSION-LITERALS
-    imports private RUST-INTEGER-OPERATIONS
     imports private RUST-BOOL-OPERATIONS
+    imports private RUST-ERROR
     imports private RUST-EXPRESSION-CONSTANTS
+    imports private RUST-EXPRESSION-LITERALS
+    imports private RUST-INTEGER-OPERATIONS
     imports private RUST-PREPROCESSING
     imports private RUST-REPRESENTATION
     imports private RUST-RUNNING-CONFIGURATION