diff --git a/mx-rust-semantics/main/glue.md b/mx-rust-semantics/main/glue.md index 0b07de7..9b9162d 100644 --- a/mx-rust-semantics/main/glue.md +++ b/mx-rust-semantics/main/glue.md @@ -17,6 +17,7 @@ module MX-RUST-GLUE ... Values:Map => Values[ValueId <- V] + requires ValueId >=Int 0 rule (.K => mxRustEmptyValue(T)) diff --git a/mx-rust-semantics/main/modules/storage.md b/mx-rust-semantics/main/modules/storage.md index 2d40490..582f64b 100644 --- a/mx-rust-semantics/main/modules/storage.md +++ b/mx-rust-semantics/main/modules/storage.md @@ -49,6 +49,38 @@ module MX-RUST-MODULES-STORAGE ... + rule + + normalizedMethodCall + ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier + , #token("set_if_empty", "Identifier"):Identifier + , ( ptr(SelfId:Int) + , ptr(ValueId:Int) + , .NormalizedCallParams + ) + ) + => MX#storageLoad(mxStringValue(StorageKey), rustDestination(-1, noType)) + ~> setIfEmpty + ~> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V)) + ... + + + SelfId |-> struct + ( Type + , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int + _:Map + ) + StorageKeyId |-> StorageKey:String + ValueId |-> V:Value + ... + + + rule mxRustEmptyValue(noType) ~> storeHostValue(...) ~> setIfEmpty + => .K + rule storeHostValue(... value: wrappedRust(_)) + ~> setIfEmpty ~> MX#storageStore(_) + => .K + rule normalizedMethodCall @@ -75,6 +107,7 @@ module MX-RUST-MODULES-STORAGE NextId:Int => NextId +Int 1 + syntax MxRustInstruction ::= "setIfEmpty" endmodule ``` diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md index 39c5be5..a17f947 100644 --- a/mx-rust-semantics/main/representation.md +++ b/mx-rust-semantics/main/representation.md @@ -11,7 +11,7 @@ module MX-RUST-REPRESENTATION | mxValueToRust(Type) | mxRustLoadPtr(Int) - syntax MxRustType ::= "BigUint" + syntax MxRustType ::= "noType" | "BigUint" syntax MxRustTypeOrError ::= MxRustType | SemanticsError syntax Value ::= MxRustType