-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
b303afe
commit 7d3a018
Showing
55 changed files
with
1,355 additions
and
101 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,9 +1,17 @@ | ||
| ```k | ||
| requires "expression/mx-to-rust.md" | ||
| requires "expression/raw-value.md" | ||
| requires "expression/rust-to-mx.md" | ||
| requires "expression/strings.md" | ||
| requires "expression/struct.md" | ||
| module MX-RUST-EXPRESSION | ||
| imports private MX-RUST-EXPRESSION-MX-TO-RUST | ||
| imports private MX-RUST-EXPRESSION-RAW-VALUE | ||
| imports private MX-RUST-EXPRESSION-RUST-TO-MX | ||
| imports private MX-RUST-EXPRESSION-STRINGS | ||
| imports private MX-RUST-EXPRESSION-STRUCT | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,85 @@ | ||
| ```k | ||
| module MX-RUST-EXPRESSION-MX-TO-RUST | ||
| imports private K-EQUAL-SYNTAX | ||
| imports private MX-COMMON-SYNTAX | ||
| imports private MX-RUST-REPRESENTATION | ||
| imports private RUST-HELPERS | ||
| imports private RUST-VALUE-SYNTAX | ||
| syntax Bool ::= isMxToRustValue(K) [function, total, symbol(isMxToRustValue)] | ||
| rule isMxToRustValue(_:K) => false [owise] | ||
| rule isMxToRustValue(_:PtrValue) => true | ||
| rule isMxToRustValue(mxToRustField(_, V:MxToRust)) => isMxToRustValue(V) | ||
| syntax Bool ::= isMxToRustFieldValue(K) [function, total, symbol(isMxToRustFieldValue)] | ||
| rule isMxToRustFieldValue(_:K) => false [owise] | ||
| rule isMxToRustFieldValue(_:PtrValue) => true | ||
| rule isMxToRustFieldValue(mxToRustField(_, V:MxToRust)) => isMxToRustValue(V) | ||
| rule isMxToRustFieldValue(.MxRustFieldValues) => true | ||
| rule isMxToRustFieldValue(A:MxRustFieldValue , As:MxRustFieldValues) | ||
| => isMxToRustFieldValue(A) andBool isMxToRustFieldValue(As) | ||
| rule V:MxValue ~> mxToRustTyped(T:Type) => mxToRustTyped(T, V) | ||
| rule mxToRustTyped(T:Type, mxIntValue(I:Int)) => mxRustNewValue(integerToValue(I, T)) | ||
| requires | ||
| (T ==K i32 orBool T ==K u32) | ||
| orBool (T ==K i64 orBool T ==K u64) | ||
| rule mxToRustTyped(str, mxStringValue(S:String)) => mxRustNewValue(S) | ||
| rule mxToRustTyped | ||
| ( rustStructType(StructName:TypePath, Fields:MxRustStructFields) | ||
| , mxListValue(Values:MxValueList) | ||
| ) | ||
| => mxToRustStruct(StructName, pairFields(Fields, Values)) | ||
| rule mxToRustTyped(() , mxUnitValue()) => ptrValue(null, tuple(.ValueList)) | ||
| context HOLE:MxRustFieldValue , _:MxRustFieldValues [result(MxToRustFieldValue)] | ||
| context V:MxRustFieldValue , HOLE:MxRustFieldValues requires isMxToRustFieldValue(V) | ||
| [result(MxToRustFieldValue)] | ||
| syntax MxRustFieldValues ::= pairFields(MxRustStructFields, MxValueList) [function, total] | ||
| rule pairFields(.MxRustStructFields, .MxValueList) => .MxRustFieldValues | ||
| rule pairFields | ||
| ( (mxRustStructField(Name:Identifier, T:MxRustType) , Fs:MxRustStructFields) | ||
| , (V:MxValue , Vs:MxValueList) | ||
| ) | ||
| => mxToRustField(Name, mxToRustTyped(T, V)) , pairFields(Fs, Vs) | ||
| rule pairFields(.MxRustStructFields, (_:MxValue , _:MxValueList) #as L:MxValueList) | ||
| => error("Not enough fields", ListItem(L)) | ||
| rule pairFields((_ , _:MxRustStructFields) #as F, .MxValueList) | ||
| => error("Not enough values", ListItem(F)) | ||
| rule pairFields(F:MxRustStructFields, V:MxValueList) | ||
| => error("Should not happen (pairFields)", ListItem(F) ListItem(V)) | ||
| [owise] | ||
| rule (.K => fieldsToMap(Fields, .Map)) | ||
| ~> mxToRustStruct(_StructName:TypePath, Fields:MxRustFieldValues) | ||
| requires isMxToRustFieldValue(Fields) | ||
| rule M:Map ~> mxToRustStruct(StructName:TypePath, _Fields:MxRustFieldValues) | ||
| => mxRustNewValue(struct(StructName, M)) | ||
| syntax MapOrError ::= fieldsToMap(MxRustFieldValues, Map) [function, total] | ||
| rule fieldsToMap(.MxRustFieldValues, M:Map) => M | ||
| rule fieldsToMap | ||
| ( mxToRustField(Name:Identifier, ptrValue(ptr(I:Int), _:Value)) | ||
| , Fields:MxRustFieldValues | ||
| , M | ||
| ) | ||
| => fieldsToMap(Fields, M[Name <- I]) | ||
| requires notBool Name in_keys(M) | ||
| rule fieldsToMap | ||
| ( ( (mxToRustField(Name:Identifier, _) #as Field:MxRustFieldValue) | ||
| , _Fields:MxRustFieldValues | ||
| ) | ||
| , M | ||
| ) | ||
| => error("Field name already in map", ListItem(Field) ListItem(M)) | ||
| requires Name in_keys(M) | ||
| rule fieldsToMap((Field , _:MxRustFieldValues), _:Map) | ||
| => error("Unexpected field", ListItem(Field)) | ||
| [owise] | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| ```k | ||
| module MX-RUST-EXPRESSION-RAW-VALUE | ||
| imports private MX-RUST-REPRESENTATION | ||
| rule rawValue(V:Value) => mxRustNewValue(V) | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| ```k | ||
| module MX-RUST-EXPRESSION-RUST-TO-MX | ||
| imports private COMMON-K-CELL | ||
| imports private K-EQUAL-SYNTAX | ||
| imports private LIST | ||
| 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 | ||
| rule V:MxValue ~> rustToMx => rustToMx(V) | ||
| rule | ||
| <k> | ||
| rustToMx(struct (_, Fields:Map)) | ||
| => rustValuesToMxListValue | ||
| ( ptrListToValueList(listToPtrList(values(Fields)), Values) | ||
| , .MxValueList | ||
| ) | ||
| ... | ||
| </k> | ||
| <values> Values:Map </values> | ||
| [priority(200)] | ||
| rule rustToMx(S:String => mxStringValue(S)) | ||
| rule rustToMx(tuple(V:ValueList)) => rustValuesToMxListValue(V, .MxValueList) | ||
| syntax RustMxInstruction ::= rustValuesToMxListValue(ValueListOrError, MxValueList) | ||
| rule rustValuesToMxListValue(.ValueList, L:MxValueList) | ||
| => rustToMx(mxListValue(reverse(L, .MxValueList))) | ||
| rule (.K => rustToMx(HOLE)) ~> rustValuesToMxListValue(((HOLE:Value , V:ValueList) => V), _:MxValueList) | ||
| rule (rustToMx(HOLE:MxValue) => .K) ~> rustValuesToMxListValue(_:ValueList, (L:MxValueList => (HOLE, L))) | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,40 @@ | ||
| ```k | ||
| module MX-RUST-EXPRESSION-STRUCT | ||
| imports private MX-RUST-REPRESENTATION | ||
| syntax MapOrError ::= pair(MxRustStructFields, PtrList, Map) [function, total] | ||
| rule (.K => reverseNormalizeParams(Args, .PtrList)) | ||
| ~> mxRustNewStruct | ||
| ( _ | ||
| , Args:CallParamsList | ||
| ) | ||
| rule reverseNormalizeParams(.CallParamsList, Ptrs:PtrList) | ||
| ~> mxRustNewStruct | ||
| ( rustStructType | ||
| ( StructName:TypePath | ||
| , Fields:MxRustStructFields | ||
| ) | ||
| , _:CallParamsList | ||
| ) | ||
| => Rust#newStruct(StructName, pair(Fields, reverse(Ptrs, .PtrList), .Map)) | ||
| rule pair(.MxRustStructFields, .PtrList, M:Map) => M | ||
| rule pair | ||
| ( (mxRustStructField(Name:Identifier, _) , Fs:MxRustStructFields) => Fs | ||
| , (ptr(P:Int) , Ps:PtrList) => Ps | ||
| , M:Map => M[Name <- P] | ||
| ) | ||
| requires notBool Name in_keys(M) | ||
| rule pair(Fs, Ps, M) | ||
| => error | ||
| ( "Unspecified error (pair)" | ||
| , ListItem(Fs) ListItem(Ps) ListItem(M) | ||
| ) | ||
| [owise] | ||
| endmodule | ||
| ``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,38 @@ | ||
| ```k | ||
| module MX-RUST-MODULES-ADDRESS | ||
| imports private MX-COMMON-SYNTAX | ||
| imports private MX-RUST-REPRESENTATION | ||
| imports private MX-RUST-REPRESENTATION-CONVERSIONS | ||
| imports private RUST-SHARED-SYNTAX | ||
| syntax MxRustType ::= "addressType" [function, total] | ||
| rule addressType | ||
| => rustStructType | ||
| ( #token("ManagedAddress", "Identifier"):Identifier | ||
| , ( mxRustStructField | ||
| ( #token("mx_address_value", "Identifier"):Identifier | ||
| , str | ||
| ) | ||
| , .MxRustStructFields | ||
| ) | ||
| ) | ||
| rule mxRustEmptyValue(rustType(#token("ManagedAddress", "Identifier"))) | ||
| => mxToRustTyped(addressType, mxListValue(mxStringValue(""))) | ||
| rule mxValueToRust(#token("ManagedAddress", "Identifier"), V:MxValue) | ||
| => mxToRustTyped(addressType, mxListValue(V)) | ||
| rule rustValueToMx | ||
| ( struct | ||
| ( #token("ManagedAddress", "Identifier"):Identifier | ||
| , #token("mx_address_value", "Identifier"):Identifier |-> AddressValueId:Int | ||
| _:Map | ||
| ) | ||
| ) | ||
| => ptr(AddressValueId) ~> rustValueToMx | ||
| endmodule | ||
| ``` |
Oops, something went wrong.