-
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.
* Allow passing args to the contract's init function (#84) (#87) * Allow passing args to the contract's init function * Contract call tests Co-authored-by: Virgil <[email protected]> * First implementation of for loops and implementing initial test * Fixing int operations not working for variables and introducing first draft of for loops * Adding test functions and corner case rule * Adding tests and correcting scope * Fixing range pattern definition working only for integer literals * Removing wrong unnecessary definition and for loops with multiple patterns * Removing empty spaces * Removing unnecessary variable creation * Properly handling the range expression for loops * changing function name and enabling different integer types on for loops * Addressing review * Organizing the rules and addressing review * Add missing token * Removing return from stack on tests --------- Co-authored-by: Virgil <[email protected]>
- Loading branch information
1 parent
655ed4f
commit 69aa4f7
Showing
10 changed files
with
188 additions
and
37 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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,52 @@ | ||
| ```k | ||
| module RUST-LOOP-EXPRESSIONS | ||
| imports RUST-REPRESENTATION | ||
| syntax IteratorLoopExpression ::= "for1" Pattern "limit" PtrValue BlockExpression | ||
| | "for2" Pattern "limit" PtrValue BlockExpression | ||
| rule for Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in ptrValue(_, intRange(First, Last)) B:BlockExpression => | ||
| { | ||
| .InnerAttributes | ||
| let Patt = ptrValue(null, First); | ||
| (for1 Patt | R limit ptrValue(null, Last) B):IteratorLoopExpression; | ||
| .NonEmptyStatements | ||
| }; | ||
| requires checkIntOfSameType(First, Last) | ||
| rule for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B:BlockExpression => | ||
| if (Patt :: .PathExprSegments):PathExprSegments < Last | ||
| { | ||
| .InnerAttributes B; | ||
| (for2 Patt | .PatternNoTopAlts limit Last B):IteratorLoopExpression; | ||
| .NonEmptyStatements | ||
| }; | ||
| rule for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit ptrValue(_, LastValue) #as Last B:BlockExpression => | ||
| incrementPatt(Patt, LastValue) ~> for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts limit Last B | ||
| rule while (E:ExpressionExceptStructExpression) S:BlockExpression => if E { .InnerAttributes S; while(E)S; .NonEmptyStatements}; | ||
| // Necessary for handling all possible integer types provided in the range expression of for loops | ||
| syntax LetStatement ::= incrementPatt(Identifier, Value) [function] | ||
| rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => | ||
| let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i32(Int2MInt(1:Int))); | ||
| requires checkIntOfType(ComparisonValue, i32) | ||
| rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => | ||
| let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u32(Int2MInt(1:Int))); | ||
| requires checkIntOfType(ComparisonValue, u32) | ||
| rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => | ||
| let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u64(Int2MInt(1:Int))); | ||
| requires checkIntOfType(ComparisonValue, u64) | ||
| rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => | ||
| let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i64(Int2MInt(1:Int))); | ||
| requires checkIntOfType(ComparisonValue, i64) | ||
| rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => | ||
| let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, u128(Int2MInt(1:Int))); | ||
| requires checkIntOfType(ComparisonValue, u128) | ||
| 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,4 @@ | ||
| new LoopExpressions; | ||
| call LoopExpressions.iterator_evaluation; | ||
| return_value; | ||
| check_eq () |
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,4 @@ | ||
| new LoopExpressions; | ||
| call LoopExpressions.while_evaluation; | ||
| return_value; | ||
| check_eq () |
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,4 @@ | ||
| new LoopExpressions; | ||
| call LoopExpressions.iterator_with_variables; | ||
| return_value; | ||
| check_eq () |
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,4 @@ | ||
| new LoopExpressions; | ||
| call LoopExpressions.iterator_with_same_pattern; | ||
| return_value; | ||
| check_eq () |
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,43 @@ | ||
| #![no_std] | ||
|
|
||
| #[allow(unused_imports)] | ||
| use multiversx_sc::imports::*; | ||
|
|
||
| #[multiversx_sc::contract] | ||
| pub trait LoopExpressions { | ||
| #[init] | ||
| fn init(&self) { | ||
| } | ||
|
|
||
| #[upgrade] | ||
| fn upgrade(&self) {} | ||
|
|
||
| fn iterator_evaluation(&self){ | ||
| for i in 1_u64..10_u64 { | ||
| let x = i * 2_u64; | ||
| }; | ||
| } | ||
|
|
||
| fn while_evaluation(&self){ | ||
| while 1_u64 < 1_u64 { | ||
| let x: u64 = 2_u64; | ||
| }; | ||
| } | ||
|
|
||
| fn iterator_with_variables(&self) { | ||
| let y = 20_u64; | ||
| let z = 10_u64; | ||
|
|
||
| for i in z..y { | ||
| let x = i * 2_u64; | ||
| }; | ||
| } | ||
|
|
||
| fn iterator_with_same_pattern(&self) { | ||
| let i = 1_u64; | ||
| for i in i..i+3_u64 { | ||
| let x = i * 2_u64; | ||
| }; | ||
| } | ||
|
|
||
| } |