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/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/config.md b/rust-semantics/config.md
index 5c6edc5..f072f87 100644
--- a/rust-semantics/config.md
+++ b/rust-semantics/config.md
@@ -1,17 +1,17 @@
```k
module RUST-CONFIGURATION
- imports RUST-INDEXING-CONFIGURATION
+ imports RUST-PREPROCESSING-CONFIGURATION
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/indexing/configuration.md b/rust-semantics/indexing/configuration.md
deleted file mode 100644
index f6498b1..0000000
--- a/rust-semantics/indexing/configuration.md
+++ /dev/null
@@ -1,32 +0,0 @@
-```k
-
-module RUST-INDEXING-CONFIGURATION
- imports private RUST-REPRESENTATION
- imports private RUST-SHARED-SYNTAX
-
- syntax Identifier ::= "my_identifier" [token]
-
- configuration
-
-
-
- my_identifier
- tuple(.ValueList)
-
-
-
- my_identifier
-
-
- my_identifier
- .NormalizedFunctionParameterList
- ():Type
- empty:FunctionBodyRepresentation
-
-
-
-
-endmodule
-
-
-```
\ No newline at end of file
diff --git a/rust-semantics/indexing/helpers.md b/rust-semantics/indexing/helpers.md
deleted file mode 100644
index 7ebd3ea..0000000
--- a/rust-semantics/indexing/helpers.md
+++ /dev/null
@@ -1,35 +0,0 @@
-```k
-
-module RUST-INDEXING-PRIVATE-HELPERS
- 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 ( ) ;)
- => Name
- rule getFunctionName(fn Name:Identifier _P:GenericParams ( _Params:FunctionParameters ) ;)
- => Name
- rule getFunctionName(fn Name:Identifier ( _Params:FunctionParameters ) ;)
- => Name
-
- 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/indexing/initialization.md b/rust-semantics/indexing/initialization.md
deleted file mode 100644
index 1ced14d..0000000
--- a/rust-semantics/indexing/initialization.md
+++ /dev/null
@@ -1,119 +0,0 @@
-```k
-
-module INITIALIZATION
- imports private RUST-RUNNING-CONFIGURATION
- imports private RUST-INDEXING-PRIVATE-HELPERS
- imports private RUST-INDEXING-PRIVATE-SYNTAX
-
- // rule
- // crateInitializer
- // ( ... constantNames:(ListItem(Name:Identifier) => .List) _Cts:List
- // , constants: _Constants (Name |-> V:Value => .Map)
- // )
- // ...
- //
- //
- //
- // .Bag =>
- //
- // Name:Identifier
- // V:Value
- //
- //
- // ...
- //
-
- rule (.K => addMethod(F, A))
- ~> crateInitializer
- ( ... constantNames: .List
- , functionNames: (ListItem(Name:Identifier) => .List) _Names:List
- , functions: _Functions:Map
- ((Name |-> (A:OuterAttributes F:Function):AssociatedItem) => .Map)
- )
- rule
- crateInitializer
- ( ... constantNames : .List
- , functionNames : .List
- , traitName : Name:Identifier
- ) => .K
- ...
-
-
- ...
-
- ...
- _Name => Name:Identifier
-
-
-
- // 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 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 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(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
- addMethod4(
- Name:Identifier, P:NormalizedFunctionParameterList,
- R:Type, B:BlockExpression,
- _A:OuterAttributes
- ) => .K
- ...
-
-
- ...
-
- ...
-
- .Bag =>
-
- Name:Identifier
- P
- R
- block(B)
-
- ...
-
-
-
-
-endmodule
-
-```
diff --git a/rust-semantics/indexing/syntax.md b/rust-semantics/indexing/syntax.md
deleted file mode 100644
index 5313228..0000000
--- a/rust-semantics/indexing/syntax.md
+++ /dev/null
@@ -1,46 +0,0 @@
-```k
-
-module RUST-INDEXING-SYNTAX
- imports RUST-SHARED-SYNTAX
-
- syntax Initializer ::= crateParser(crate: Crate)
-endmodule
-
-module RUST-INDEXING-PRIVATE-SYNTAX
- imports LIST
- imports MAP
- imports RUST-REPRESENTATION
- imports RUST-SHARED-SYNTAX
-
- syntax Initializer ::= traitParser(Trait)
- | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier)
- | crateInitializer
- ( constantNames:List, constants: Map
- , traitName: Identifier
- , functionNames:List, functions: Map
- )
-
- syntax Initializer ::= addMethod(function: Function, atts:OuterAttributes)
- | addMethod1(
- FunctionWithWhere, BlockExpressionOrSemicolon,
- OuterAttributes
- )
- | addMethod2(
- FunctionWithParams, Type,
- BlockExpressionOrSemicolon, OuterAttributes
- )
- | addMethod3(
- Identifier, NormalizedFunctionParameterList,
- FunctionParameterList, Type,
- BlockExpressionOrSemicolon, OuterAttributes
- )
- | addMethod4(
- Identifier, NormalizedFunctionParameterList, Type,
- BlockExpressionOrSemicolon, OuterAttributes
- )
-
- // TODO: Move to a more generic place
- syntax Identifier ::= "self" [token]
-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/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md
new file mode 100644
index 0000000..c2f5162
--- /dev/null
+++ b/rust-semantics/preprocessing/configuration.md
@@ -0,0 +1,34 @@
+```k
+
+module RUST-PREPROCESSING-CONFIGURATION
+ imports private RUST-REPRESENTATION
+ imports private RUST-SHARED-SYNTAX
+
+ syntax Identifier ::= "my_identifier" [token]
+
+ configuration
+
+
+
+ my_identifier
+ tuple(.ValueList)
+
+
+
+
+ my_identifier:TypePath
+
+
+ my_identifier
+ .NormalizedFunctionParameterList
+ ():Type
+ empty:FunctionBodyRepresentation
+
+
+
+
+
+endmodule
+
+
+```
\ No newline at end of file
diff --git a/rust-semantics/indexing/crate.md b/rust-semantics/preprocessing/crate.md
similarity index 86%
rename from rust-semantics/indexing/crate.md
rename to rust-semantics/preprocessing/crate.md
index 2f310e7..7acd05d 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
@@ -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/helpers.md b/rust-semantics/preprocessing/helpers.md
new file mode 100644
index 0000000..2da8f06
--- /dev/null
+++ b/rust-semantics/preprocessing/helpers.md
@@ -0,0 +1,96 @@
+```k
+
+module RUST-PREPROCESSING-PRIVATE-HELPERS
+ imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
+ imports private RUST-REPRESENTATION
+ imports RUST-SHARED-SYNTAX
+
+ 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 getFunctionWithParamsName(fn Name:Identifier ( ))
+ => Name
+ 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)
+ [owise]
+
+ 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
+
+endmodule
+
+```
diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md
new file mode 100644
index 0000000..c455036
--- /dev/null
+++ b/rust-semantics/preprocessing/initialization.md
@@ -0,0 +1,68 @@
+```k
+
+module INITIALIZATION
+ imports private RUST-RUNNING-CONFIGURATION
+ imports private RUST-PREPROCESSING-PRIVATE-HELPERS
+ imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
+
+ rule constantInitializer(... constantNames : .List) => .K
+
+ 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
+ traitInitializer(Name:TypePath) => .K
+ ...
+
+
+ ...
+ .Bag
+ =>
+ Name
+ .Bag
+
+
+
+ rule addMethod(Trait:TypePath, F:Function, A:OuterAttributes)
+ => #addMethod
+ ( Trait
+ , getFunctionName(F)
+ , extractFunctionNormalizedParams(F)
+ , getFunctionReturnType(F)
+ , getFunctionBlockOrSemicolon(F)
+ , A
+ )
+
+ rule
+ #addMethod(
+ Trait:TypePath,
+ Name:Identifier, P:NormalizedFunctionParameterList,
+ R:Type, B:BlockExpression,
+ _A:OuterAttributes
+ ) => .K
+ ...
+
+
+ ...
+ Trait
+
+ .Bag =>
+
+ Name:Identifier
+ P
+ R
+ block(B)
+
+ ...
+
+
+
+endmodule
+
+```
diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md
new file mode 100644
index 0000000..768bd1a
--- /dev/null
+++ b/rust-semantics/preprocessing/syntax.md
@@ -0,0 +1,41 @@
+```k
+
+module RUST-PREPROCESSING-SYNTAX
+ imports RUST-SHARED-SYNTAX
+
+ syntax Initializer ::= crateParser(crate: Crate)
+endmodule
+
+module RUST-PREPROCESSING-PRIVATE-SYNTAX
+ imports LIST
+ imports MAP
+ imports RUST-REPRESENTATION
+ imports RUST-SHARED-SYNTAX
+
+ syntax Initializer ::= traitParser(Trait)
+ | traitMethodsParser(AssociatedItems, functions: Map, traitName:Identifier)
+ | constantInitializer
+ ( constantNames: List, constants: Map )
+ | traitInitializer
+ ( traitName: TypePath
+ )
+ | traitMethodInitializer
+ ( traitName: TypePath
+ , functionNames:List, functions: Map
+ )
+
+ syntax Initializer ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes)
+ | #addMethod(
+ TypePath,
+ Identifier,
+ NormalizedFunctionParameterListOrError,
+ Type,
+ BlockExpressionOrSemicolon,
+ OuterAttributes
+ )
+
+ // TODO: Move to a more generic place
+ syntax Identifier ::= "self" [token]
+endmodule
+
+```
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/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})
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
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) {}
+}
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 {}
+
+}