From bdd9731bcd5c80df3867f9872656184e28440960 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Tue, 20 Aug 2024 19:31:36 +0300 Subject: [PATCH 1/5] Rename indexing -> preprocessing --- rust-semantics/config.md | 4 ++-- rust-semantics/indexing.md | 19 ------------------- rust-semantics/preprocessing.md | 19 +++++++++++++++++++ .../configuration.md | 2 +- .../{indexing => preprocessing}/crate.md | 4 ++-- .../{indexing => preprocessing}/helpers.md | 2 +- .../initialization.md | 4 ++-- .../{indexing => preprocessing}/syntax.md | 4 ++-- .../trait-methods.md | 4 ++-- .../{indexing => preprocessing}/trait.md | 2 +- rust-semantics/rust.md | 4 ++-- 11 files changed, 34 insertions(+), 34 deletions(-) delete mode 100644 rust-semantics/indexing.md create mode 100644 rust-semantics/preprocessing.md rename rust-semantics/{indexing => preprocessing}/configuration.md (96%) rename rust-semantics/{indexing => preprocessing}/crate.md (96%) rename rust-semantics/{indexing => preprocessing}/helpers.md (97%) rename rust-semantics/{indexing => preprocessing}/initialization.md (97%) rename rust-semantics/{indexing => preprocessing}/syntax.md (95%) rename rust-semantics/{indexing => preprocessing}/trait-methods.md (71%) rename rust-semantics/{indexing => preprocessing}/trait.md (76%) diff --git a/rust-semantics/config.md b/rust-semantics/config.md index 5c6edc5..eb9325e 100644 --- a/rust-semantics/config.md +++ b/rust-semantics/config.md @@ -1,7 +1,7 @@ ```k module RUST-CONFIGURATION - imports RUST-INDEXING-CONFIGURATION + imports RUST-PREPROCESSING-CONFIGURATION configuration @@ -11,7 +11,7 @@ module RUST-CONFIGURATION endmodule module RUST-RUNNING-CONFIGURATION - imports private RUST-INDEXING-SYNTAX + imports private RUST-PREPROCESSING-SYNTAX imports RUST-CONFIGURATION configuration diff --git a/rust-semantics/indexing.md b/rust-semantics/indexing.md deleted file mode 100644 index bbe5319..0000000 --- a/rust-semantics/indexing.md +++ /dev/null @@ -1,19 +0,0 @@ -```k - -requires "indexing/crate.md" -requires "indexing/configuration.md" -requires "indexing/helpers.md" -requires "indexing/initialization.md" -requires "indexing/syntax.md" -requires "indexing/trait.md" -requires "indexing/trait-methods.md" - -module RUST-INDEXING - imports private CRATE - imports private INITIALIZATION - imports private TRAIT - imports private TRAIT-METHODS -endmodule - - -``` diff --git a/rust-semantics/preprocessing.md b/rust-semantics/preprocessing.md new file mode 100644 index 0000000..030bf02 --- /dev/null +++ b/rust-semantics/preprocessing.md @@ -0,0 +1,19 @@ +```k + +requires "preprocessing/crate.md" +requires "preprocessing/configuration.md" +requires "preprocessing/helpers.md" +requires "preprocessing/initialization.md" +requires "preprocessing/syntax.md" +requires "preprocessing/trait.md" +requires "preprocessing/trait-methods.md" + +module RUST-PREPROCESSING + imports private CRATE + imports private INITIALIZATION + imports private TRAIT + imports private TRAIT-METHODS +endmodule + + +``` diff --git a/rust-semantics/indexing/configuration.md b/rust-semantics/preprocessing/configuration.md similarity index 96% rename from rust-semantics/indexing/configuration.md rename to rust-semantics/preprocessing/configuration.md index f6498b1..2c6c7c8 100644 --- a/rust-semantics/indexing/configuration.md +++ b/rust-semantics/preprocessing/configuration.md @@ -1,6 +1,6 @@ ```k -module RUST-INDEXING-CONFIGURATION +module RUST-PREPROCESSING-CONFIGURATION imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX diff --git a/rust-semantics/indexing/crate.md b/rust-semantics/preprocessing/crate.md similarity index 96% rename from rust-semantics/indexing/crate.md rename to rust-semantics/preprocessing/crate.md index 2f310e7..475d4fa 100644 --- a/rust-semantics/indexing/crate.md +++ b/rust-semantics/preprocessing/crate.md @@ -3,8 +3,8 @@ module CRATE imports private LIST imports private MAP - imports private RUST-INDEXING-PRIVATE-SYNTAX - imports private RUST-INDEXING-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-SYNTAX imports private RUST-REPRESENTATION imports private RUST-RUNNING-CONFIGURATION diff --git a/rust-semantics/indexing/helpers.md b/rust-semantics/preprocessing/helpers.md similarity index 97% rename from rust-semantics/indexing/helpers.md rename to rust-semantics/preprocessing/helpers.md index 7ebd3ea..aaaf1ce 100644 --- a/rust-semantics/indexing/helpers.md +++ b/rust-semantics/preprocessing/helpers.md @@ -1,6 +1,6 @@ ```k -module RUST-INDEXING-PRIVATE-HELPERS +module RUST-PREPROCESSING-PRIVATE-HELPERS imports private RUST-REPRESENTATION imports RUST-SHARED-SYNTAX diff --git a/rust-semantics/indexing/initialization.md b/rust-semantics/preprocessing/initialization.md similarity index 97% rename from rust-semantics/indexing/initialization.md rename to rust-semantics/preprocessing/initialization.md index 1ced14d..90bd9e0 100644 --- a/rust-semantics/indexing/initialization.md +++ b/rust-semantics/preprocessing/initialization.md @@ -2,8 +2,8 @@ module INITIALIZATION imports private RUST-RUNNING-CONFIGURATION - imports private RUST-INDEXING-PRIVATE-HELPERS - imports private RUST-INDEXING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-HELPERS + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX // rule // crateInitializer diff --git a/rust-semantics/indexing/syntax.md b/rust-semantics/preprocessing/syntax.md similarity index 95% rename from rust-semantics/indexing/syntax.md rename to rust-semantics/preprocessing/syntax.md index 5313228..9e664dc 100644 --- a/rust-semantics/indexing/syntax.md +++ b/rust-semantics/preprocessing/syntax.md @@ -1,12 +1,12 @@ ```k -module RUST-INDEXING-SYNTAX +module RUST-PREPROCESSING-SYNTAX imports RUST-SHARED-SYNTAX syntax Initializer ::= crateParser(crate: Crate) endmodule -module RUST-INDEXING-PRIVATE-SYNTAX +module RUST-PREPROCESSING-PRIVATE-SYNTAX imports LIST imports MAP imports RUST-REPRESENTATION diff --git a/rust-semantics/indexing/trait-methods.md b/rust-semantics/preprocessing/trait-methods.md similarity index 71% rename from rust-semantics/indexing/trait-methods.md rename to rust-semantics/preprocessing/trait-methods.md index 84653c9..1b2c106 100644 --- a/rust-semantics/indexing/trait-methods.md +++ b/rust-semantics/preprocessing/trait-methods.md @@ -1,8 +1,8 @@ ```k module TRAIT-METHODS - imports private RUST-INDEXING-PRIVATE-HELPERS - imports private RUST-INDEXING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-HELPERS + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX rule traitMethodsParser( (A:OuterAttributes F:Function) AIs:AssociatedItems => AIs, diff --git a/rust-semantics/indexing/trait.md b/rust-semantics/preprocessing/trait.md similarity index 76% rename from rust-semantics/indexing/trait.md rename to rust-semantics/preprocessing/trait.md index fc17017..97c0ce1 100644 --- a/rust-semantics/indexing/trait.md +++ b/rust-semantics/preprocessing/trait.md @@ -1,7 +1,7 @@ ```k module TRAIT - imports private RUST-INDEXING-PRIVATE-SYNTAX + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX rule traitParser(trait Name:Identifier { .InnerAttributes Functions:AssociatedItems }) => traitMethodsParser(Functions, .Map, Name) diff --git a/rust-semantics/rust.md b/rust-semantics/rust.md index 965b45d..4b12db2 100644 --- a/rust-semantics/rust.md +++ b/rust-semantics/rust.md @@ -1,12 +1,12 @@ ```k requires "config.md" -requires "indexing.md" +requires "preprocessing.md" requires "representation.md" requires "syntax.md" module RUST imports RUST-CONFIGURATION - imports RUST-INDEXING + imports RUST-PREPROCESSING imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX From f873c409e643497ddb641db1dc44fd6ccc5ab046 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Tue, 20 Aug 2024 21:37:57 +0300 Subject: [PATCH 2/5] Refactor trait initialization --- rust-semantics/config.md | 2 +- rust-semantics/preprocessing/configuration.md | 40 +++++------ rust-semantics/preprocessing/crate.md | 12 ++-- .../preprocessing/initialization.md | 67 +++++++++---------- rust-semantics/preprocessing/syntax.md | 16 +++-- 5 files changed, 74 insertions(+), 63 deletions(-) diff --git a/rust-semantics/config.md b/rust-semantics/config.md index eb9325e..f072f87 100644 --- a/rust-semantics/config.md +++ b/rust-semantics/config.md @@ -5,7 +5,7 @@ module RUST-CONFIGURATION configuration - + endmodule diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md index 2c6c7c8..c2f5162 100644 --- a/rust-semantics/preprocessing/configuration.md +++ b/rust-semantics/preprocessing/configuration.md @@ -7,25 +7,27 @@ module RUST-PREPROCESSING-CONFIGURATION syntax Identifier ::= "my_identifier" [token] configuration - - - - my_identifier - tuple(.ValueList) - - - - my_identifier - - - my_identifier - .NormalizedFunctionParameterList - ():Type - empty:FunctionBodyRepresentation - - - - + + + + my_identifier + tuple(.ValueList) + + + + + my_identifier:TypePath + + + my_identifier + .NormalizedFunctionParameterList + ():Type + empty:FunctionBodyRepresentation + + + + + endmodule diff --git a/rust-semantics/preprocessing/crate.md b/rust-semantics/preprocessing/crate.md index 475d4fa..7acd05d 100644 --- a/rust-semantics/preprocessing/crate.md +++ b/rust-semantics/preprocessing/crate.md @@ -67,11 +67,13 @@ module CRATE , traitName : Name:Identifier , traitFunctions: Functions:Map ) - => crateInitializer - ( ... constantNames: keys_list(Constants), constants: Constants - , traitName: Name - , functionNames:keys_list(Functions), functions: Functions - ) + => constantInitializer + ( ... constantNames: keys_list(Constants), constants: Constants ) + ~> traitInitializer(Name) + ~> traitMethodInitializer + ( ... traitName: Name + , functionNames:keys_list(Functions), functions: Functions + ) endmodule ``` diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md index 90bd9e0..56ca934 100644 --- a/rust-semantics/preprocessing/initialization.md +++ b/rust-semantics/preprocessing/initialization.md @@ -22,46 +22,46 @@ module INITIALIZATION // // ... // + rule constantInitializer(... constantNames : .List) => .K - rule (.K => addMethod(F, A)) - ~> crateInitializer - ( ... constantNames: .List + rule (.K => addMethod(TraitName, F, A)) + ~> traitMethodInitializer + ( ... traitName : TraitName:TypePath , functionNames: (ListItem(Name:Identifier) => .List) _Names:List , functions: _Functions:Map ((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map) ) + rule traitMethodInitializer(... functionNames: .List) => .K + rule - crateInitializer - ( ... constantNames : .List - , functionNames : .List - , traitName : Name:Identifier - ) => .K + traitInitializer(Name:TypePath) => .K ... - - ... - + ... - _Name => Name:Identifier - - + .Bag + => + Name + .Bag + + // rule addMethod(_Q:FunctionQualifiers F:FunctionWithoutQualifiers, A:OuterAttributes) // => addMethod(F:FunctionWithoutQualifiers, A) - rule addMethod((F:FunctionWithWhere B:BlockExpressionOrSemicolon):FunctionWithoutQualifiers, A:OuterAttributes) - => addMethod1(F, B, A) + rule addMethod(Trait:TypePath, (F:FunctionWithWhere B:BlockExpressionOrSemicolon):FunctionWithoutQualifiers, A:OuterAttributes) + => addMethod1(Trait, F, B, A) // rule addMethod1(F:FunctionWithReturnType _W:WhereClause, B:BlockExpressionOrSemicolon, A:OuterAttributes) // => addMethod1(F, B, A) // rule addMethod1(F:FunctionWithParams -> RT:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) // => addMethod2(F, RT, B, A) - rule addMethod1(F:FunctionWithParams, B:BlockExpressionOrSemicolon, A:OuterAttributes) - => addMethod2(F, (), B, A) + rule addMethod1(Trait:TypePath, F:FunctionWithParams, B:BlockExpressionOrSemicolon, A:OuterAttributes) + => addMethod2(Trait, F, (), B, A) // rule addMethod2(fn Name ( ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) // => addMethod4(Name, .NormalizedFunctionParameterList, T, B, A) - rule addMethod2(fn Name (_:SelfParam), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - => addMethod4(Name, (self : $selftype), T, B, A) + rule addMethod2(Trait:TypePath, fn Name (_:SelfParam), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) + => addMethod4(Trait, Name, (self : $selftype), T, B, A) // rule addMethod2(fn Name (_:SelfParam , ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) // => addMethod4(Name, (self : $selftype), T, B, A) // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) @@ -91,28 +91,27 @@ module INITIALIZATION rule addMethod4( + Trait:TypePath, Name:Identifier, P:NormalizedFunctionParameterList, R:Type, B:BlockExpression, _A:OuterAttributes ) => .K ... - + ... - + Trait + + .Bag => + + Name:Identifier + P + R + block(B) + ... - - .Bag => - - Name:Identifier - P - R - block(B) - - ... - - - + + endmodule diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md index 9e664dc..3177354 100644 --- a/rust-semantics/preprocessing/syntax.md +++ b/rust-semantics/preprocessing/syntax.md @@ -14,27 +14,35 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX syntax Initializer ::= traitParser(Trait) | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier) - | crateInitializer - ( constantNames:List, constants: Map - , traitName: Identifier + | constantInitializer + ( constantNames: List, constants: Map ) + | traitInitializer + ( traitName: TypePath + ) + | traitMethodInitializer + ( traitName: TypePath , functionNames:List, functions: Map ) - syntax Initializer ::= addMethod(function: Function, atts:OuterAttributes) + syntax Initializer ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes) | addMethod1( + TypePath, FunctionWithWhere, BlockExpressionOrSemicolon, OuterAttributes ) | addMethod2( + TypePath, FunctionWithParams, Type, BlockExpressionOrSemicolon, OuterAttributes ) | addMethod3( + TypePath, Identifier, NormalizedFunctionParameterList, FunctionParameterList, Type, BlockExpressionOrSemicolon, OuterAttributes ) | addMethod4( + TypePath, Identifier, NormalizedFunctionParameterList, Type, BlockExpressionOrSemicolon, OuterAttributes ) From 0fd019845f2b2f1f6a6d34ec6434b80aeebea336 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Tue, 20 Aug 2024 22:53:30 +0300 Subject: [PATCH 3/5] Refactor addMethod --- .gitignore | 1 + rust-semantics/preprocessing/helpers.md | 103 ++++++++++++++---- .../preprocessing/initialization.md | 70 ++---------- rust-semantics/preprocessing/syntax.md | 23 +--- rust-semantics/representation.md | 4 + 5 files changed, 101 insertions(+), 100 deletions(-) diff --git a/.gitignore b/.gitignore index 84d8b56..c733e44 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ .build +.DS_store tmp diff --git a/rust-semantics/preprocessing/helpers.md b/rust-semantics/preprocessing/helpers.md index aaaf1ce..96fc6f1 100644 --- a/rust-semantics/preprocessing/helpers.md +++ b/rust-semantics/preprocessing/helpers.md @@ -1,35 +1,94 @@ ```k module RUST-PREPROCESSING-PRIVATE-HELPERS + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX imports private RUST-REPRESENTATION imports RUST-SHARED-SYNTAX - syntax Identifier ::= getFunctionName(Function) [function, total] - rule getFunctionName(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) - => getFunctionName(F) - rule getFunctionName(F:FunctionWithWhere _B:BlockExpression) - => getFunctionName(F ;) - rule getFunctionName(F:FunctionWithReturnType _W:WhereClause ;) - => getFunctionName(F ;) - rule getFunctionName(F:FunctionWithParams _R:FunctionReturnType ;) - => getFunctionName(F ;) - rule getFunctionName(fn Name:Identifier _P:GenericParams ( ) ;) - => Name - rule getFunctionName(fn Name:Identifier ( ) ;) + syntax FunctionWithParams ::= getFunctionWithParams(Function) [function, total] + rule getFunctionWithParams(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) + => getFunctionWithParams(F) + rule getFunctionWithParams(F:FunctionWithWhere _B:BlockExpression) + => getFunctionWithParams(F ;) + rule getFunctionWithParams(F:FunctionWithReturnType _W:WhereClause ;) + => getFunctionWithParams(F ;) + rule getFunctionWithParams(F:FunctionWithParams _R:FunctionReturnType ;) + => F + rule getFunctionWithParams(F:FunctionWithParams ;) + => F + + syntax Identifier ::= getFunctionWithParamsName(FunctionWithParams) [function, total] + rule getFunctionWithParamsName(fn Name:Identifier _P:GenericParams ( )) => Name - rule getFunctionName(fn Name:Identifier _P:GenericParams ( _Params:FunctionParameters ) ;) + rule getFunctionWithParamsName(fn Name:Identifier ( )) => Name - rule getFunctionName(fn Name:Identifier ( _Params:FunctionParameters ) ;) + rule getFunctionWithParamsName(fn Name:Identifier _P:GenericParams ( _Params:FunctionParameters )) => Name + rule getFunctionWithParamsName(fn Name:Identifier ( _Params:FunctionParameters )) + => Name + + syntax Identifier ::= getFunctionName(Function) [function, total] + rule getFunctionName(F:Function) + => getFunctionWithParamsName(getFunctionWithParams(F)) + + syntax NormalizedFunctionParameterListOrError ::= extractFunctionNormalizedParams(Function) [function, total] + rule extractFunctionNormalizedParams(F) => extractFunctionWithParamsNormalizedParams(getFunctionWithParams(F)) + + syntax NormalizedFunctionParameterListOrError ::= extractFunctionWithParamsNormalizedParams(FunctionWithParams) [function, total] + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier _P:GenericParams ( )) + => .NormalizedFunctionParameterList + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( )) + => .NormalizedFunctionParameterList + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier _P:GenericParams ( Params:FunctionParameters )) + => normalizeParams(Params) + rule extractFunctionWithParamsNormalizedParams(fn _Name:Identifier ( Params:FunctionParameters )) + => normalizeParams(Params) + + syntax NormalizedFunctionParameterListOrError ::= concat( + NormalizedFunctionParameterOrError, + NormalizedFunctionParameterListOrError + ) [function, total] + rule concat(P:NormalizedFunctionParameter, L:NormalizedFunctionParameterList) => P , L + rule concat(P:SemanticsError, _:NormalizedFunctionParameterListOrError) => P + rule concat(_:NormalizedFunctionParameter, L:SemanticsError) => L + + syntax NormalizedFunctionParameterListOrError ::= normalizeParams(FunctionParameters) [function, total] + // We should not need an explicit conactenation here, but the LLVM decision tree code crashes. + rule normalizeParams(_:SelfParam) => self : $selftype , .NormalizedFunctionParameterList + // We should not need an explicit conactenation here, but the LLVM decision tree code crashes. + rule normalizeParams(_:SelfParam , ) => self : $selftype , .NormalizedFunctionParameterList + rule normalizeParams(_:SelfParam , F:FunctionParameterList) => concat(self : $selftype, normalizeParams(F)) + rule normalizeParams(_:SelfParam , F:FunctionParameterList , ) => concat(self : $selftype, normalizeParams(F)) + rule normalizeParams(F:FunctionParameterList ,) => normalizeParams(F) + rule normalizeParams(.FunctionParameterList) => .NormalizedFunctionParameterList + rule normalizeParams(P:FunctionParam , F:FunctionParameterList) => concat(normalizeParam(P), normalizeParams(F)) + + syntax NormalizedFunctionParameterOrError ::= NormalizedFunctionParameter | SemanticsError + + syntax NormalizedFunctionParameterOrError ::= normalizeParam(FunctionParam) [function, total] + rule normalizeParam(_:OuterAttributes Name:Identifier : T:Type) => Name : T + rule normalizeParam(P:FunctionParam) => error("unimplemented normalizedParam case", P:FunctionParam:KItem) + + syntax BlockExpressionOrSemicolon ::= getFunctionBlockOrSemicolon(Function) [function, total] + rule getFunctionBlockOrSemicolon(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) + => getFunctionBlockOrSemicolon(F) + rule getFunctionBlockOrSemicolon(_F:FunctionWithWhere B:BlockExpressionOrSemicolon) + => B + + syntax Type ::= getFunctionReturnType(Function) + rule getFunctionReturnType(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) + => getFunctionReturnType(F) + rule getFunctionReturnType(F:FunctionWithWhere _B:BlockExpression) + => getFunctionReturnType(F ;) + rule getFunctionReturnType(F:FunctionWithReturnType _W:WhereClause ;) + => getFunctionReturnType(F ;) + rule getFunctionReturnType(_F:FunctionWithParams -> R:Type ;) + => R + // https://doc.rust-lang.org/stable/reference/items/functions.html + // If the output type is not explicitly stated, it is the unit type. + rule getFunctionReturnType(_F:FunctionWithParams ;) + => ( ):Type - syntax NormalizedFunctionParameterList ::= reverse(NormalizedFunctionParameterList) [function, total] - // See https://github.com/runtimeverification/k/issues/4587 - // for the "Non exhaustive match detected" warning - | #reverse(NormalizedFunctionParameterList, NormalizedFunctionParameterList) [function, total] - rule reverse(L:NormalizedFunctionParameterList) => #reverse(L, .NormalizedFunctionParameterList) - rule #reverse(.NormalizedFunctionParameterList, R) => R - rule #reverse((P:NormalizedFunctionParameter , L:NormalizedFunctionParameterList), R) - => #reverse(L, (P , R)) endmodule ``` diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md index 56ca934..c455036 100644 --- a/rust-semantics/preprocessing/initialization.md +++ b/rust-semantics/preprocessing/initialization.md @@ -5,23 +5,6 @@ module INITIALIZATION imports private RUST-PREPROCESSING-PRIVATE-HELPERS imports private RUST-PREPROCESSING-PRIVATE-SYNTAX - // rule - // crateInitializer - // ( ... constantNames:(ListItem(Name:Identifier) => .List) _Cts:List - // , constants: _Constants (Name |-> V:Value => .Map) - // ) - // ... - // - // - // - // .Bag => - // - // Name:Identifier - // V:Value - // - // - // ... - // rule constantInitializer(... constantNames : .List) => .K rule (.K => addMethod(TraitName, F, A)) @@ -46,51 +29,18 @@ module INITIALIZATION - // rule addMethod(_Q:FunctionQualifiers F:FunctionWithoutQualifiers, A:OuterAttributes) - // => addMethod(F:FunctionWithoutQualifiers, A) - rule addMethod(Trait:TypePath, (F:FunctionWithWhere B:BlockExpressionOrSemicolon):FunctionWithoutQualifiers, A:OuterAttributes) - => addMethod1(Trait, F, B, A) - - // rule addMethod1(F:FunctionWithReturnType _W:WhereClause, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod1(F, B, A) - // rule addMethod1(F:FunctionWithParams -> RT:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod2(F, RT, B, A) - rule addMethod1(Trait:TypePath, F:FunctionWithParams, B:BlockExpressionOrSemicolon, A:OuterAttributes) - => addMethod2(Trait, F, (), B, A) - - // rule addMethod2(fn Name ( ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod4(Name, .NormalizedFunctionParameterList, T, B, A) - rule addMethod2(Trait:TypePath, fn Name (_:SelfParam), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - => addMethod4(Trait, Name, (self : $selftype), T, B, A) - // rule addMethod2(fn Name (_:SelfParam , ), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod4(Name, (self : $selftype), T, B, A) - // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod3(Name, (self : $selftype), P, T, B, A) - // rule addMethod2(fn Name (_:SelfParam , P:FunctionParameterList ,), T:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes) - // => addMethod3(Name, (self : $selftype) , P, T, B, A) - - // rule addMethod3( - // _MethodName:Identifier, - // ReversedNormalizedParams:NormalizedFunctionParameterList - // => (ParamName : ParamType , ReversedNormalizedParams), - // (ParamName:Identifier : ParamType:Type , Params:FunctionParameterList) - // => Params, - // _MethodReturnType:Type, _B:BlockExpressionOrSemicolon, _A:OuterAttributes - // ) - // rule addMethod3( - // MethodName:Identifier, - // ReversedNormalizedParams:NormalizedFunctionParameterList, - // .FunctionParameterList, - // MethodReturnType:Type, B:BlockExpressionOrSemicolon, A:OuterAttributes - // ) - // => addMethod4( - // MethodName, - // reverse(ReversedNormalizedParams), - // MethodReturnType, B, A - // ) + rule addMethod(Trait:TypePath, F:Function, A:OuterAttributes) + => #addMethod + ( Trait + , getFunctionName(F) + , extractFunctionNormalizedParams(F) + , getFunctionReturnType(F) + , getFunctionBlockOrSemicolon(F) + , A + ) rule - addMethod4( + #addMethod( Trait:TypePath, Name:Identifier, P:NormalizedFunctionParameterList, R:Type, B:BlockExpression, diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md index 3177354..768bd1a 100644 --- a/rust-semantics/preprocessing/syntax.md +++ b/rust-semantics/preprocessing/syntax.md @@ -25,27 +25,14 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX ) syntax Initializer ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes) - | addMethod1( + | #addMethod( TypePath, - FunctionWithWhere, BlockExpressionOrSemicolon, + Identifier, + NormalizedFunctionParameterListOrError, + Type, + BlockExpressionOrSemicolon, OuterAttributes ) - | addMethod2( - TypePath, - FunctionWithParams, Type, - BlockExpressionOrSemicolon, OuterAttributes - ) - | addMethod3( - TypePath, - Identifier, NormalizedFunctionParameterList, - FunctionParameterList, Type, - BlockExpressionOrSemicolon, OuterAttributes - ) - | addMethod4( - TypePath, - Identifier, NormalizedFunctionParameterList, Type, - BlockExpressionOrSemicolon, OuterAttributes - ) // TODO: Move to a more generic place syntax Identifier ::= "self" [token] diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md index 96301e0..6e87048 100644 --- a/rust-semantics/representation.md +++ b/rust-semantics/representation.md @@ -10,12 +10,16 @@ module RUST-REPRESENTATION syntax MInt{32} syntax MInt{64} + syntax SemanticsError ::= error(String, KItem) + syntax FunctionBodyRepresentation ::= block(BlockExpression) | "empty" | storageAccessor(StringLiteral) syntax NormalizedFunctionParameter ::= Identifier ":" Type syntax NormalizedFunctionParameterList ::= List{NormalizedFunctionParameter, ","} + syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError + syntax Value ::= i32(MInt{32}) | u32(MInt{32}) | i64(MInt{64}) From 9ffb73984b8ac8e68e724ca9e03a64bc9a1d70f7 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 21 Aug 2024 01:55:41 +0300 Subject: [PATCH 4/5] Function arguments test --- Makefile | 2 +- rust-semantics/preprocessing/helpers.md | 4 +++- tests/execution/function-arguments.rs | 24 ++++++++++++++++++++++++ 3 files changed, 28 insertions(+), 2 deletions(-) create mode 100644 tests/execution/function-arguments.rs diff --git a/Makefile b/Makefile index b2af1fb..d5f00d3 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -name '*') +SEMANTICS_FILES ::= $(shell find rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') RUST_KOMPILED ::= .build/rust-kompiled RUST_TIMESTAMP ::= $(RUST_KOMPILED)/timestamp SYNTAX_INPUT_DIR ::= tests/syntax diff --git a/rust-semantics/preprocessing/helpers.md b/rust-semantics/preprocessing/helpers.md index 96fc6f1..2da8f06 100644 --- a/rust-semantics/preprocessing/helpers.md +++ b/rust-semantics/preprocessing/helpers.md @@ -67,7 +67,9 @@ module RUST-PREPROCESSING-PRIVATE-HELPERS syntax NormalizedFunctionParameterOrError ::= normalizeParam(FunctionParam) [function, total] rule normalizeParam(_:OuterAttributes Name:Identifier : T:Type) => Name : T - rule normalizeParam(P:FunctionParam) => error("unimplemented normalizedParam case", P:FunctionParam:KItem) + rule normalizeParam(P:FunctionParam) + => error("unimplemented normalizedParam case", P:FunctionParam:KItem) + [owise] syntax BlockExpressionOrSemicolon ::= getFunctionBlockOrSemicolon(Function) [function, total] rule getFunctionBlockOrSemicolon(_Q:FunctionQualifiers F:FunctionWithoutQualifiers) diff --git a/tests/execution/function-arguments.rs b/tests/execution/function-arguments.rs new file mode 100644 index 0000000..46d79b6 --- /dev/null +++ b/tests/execution/function-arguments.rs @@ -0,0 +1,24 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn self_with_comma(&self, ) {} + + fn self_and_arg(&self, first: BigUint) {} + + fn self_and_args(&self, first: BigUint, second: BigUint) {} + + fn self_and_args_comma(&self, first: BigUint, second: BigUint, ) {} + + fn reference_arg(&self, first: &BigUint) {} +} From a535bdde13f3b8516a9884c8c216ad706059666f Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Wed, 21 Aug 2024 01:58:21 +0300 Subject: [PATCH 5/5] Return type test --- tests/execution/function-return-type.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/execution/function-return-type.rs diff --git a/tests/execution/function-return-type.rs b/tests/execution/function-return-type.rs new file mode 100644 index 0000000..a970396 --- /dev/null +++ b/tests/execution/function-return-type.rs @@ -0,0 +1,17 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Empty { + #[init] + fn init(&self) { + } + + #[upgrade] + fn upgrade(&self) {} + + fn with_return_type(&self) -> BigUint {} + +}