For and While Loops

[ACassimiro]

Introducing functional loops to our rust lite semantics.

[virgil-serbanuta]

Remove spaces?

[virgil-serbanuta]

Hmmm... This is interesting...

Right now, we have defined addition only between ints of the same kind, and I think that Rust does not allow adding ints of different types, e.g. 12u64 + 1u32 does not compile. Now, this probably works for our examples, but it's not correct, so here are some suggestions:

• Add a TODO saying that this is wrong and it should be fixed.
• define and use a function intOfSameType(1, Last) (Last should be a value when this rule is being applied, so it should have a concrete int type)

[virgil-serbanuta]

Looks good, but I left some suggestions for improvements.

[virgil-serbanuta]

I think that this should be intRange(Value, Value), the pointer part does not help here.

[virgil-serbanuta]

Remove the TODO since you just added this to the syntax.

[virgil-serbanuta]

My previous suggestion was something a bit different, but, if you want to implement it this way, I think this should be something like:

syntax Bool ::= checkIntOfType(Value, Type)  [function, total]
rule checkIntOfType(u32(_), u32) => true
...

(you may need to import RUST-REPRESENTATION)

Then you would use it like this:

syntax LetStatement ::= incrementPatt(Identifier, Value)

rule incrementPatt(Patt:Identifier, ComparisonValue:Value) => 
            let Patt = (Patt :: .PathExprSegments):PathExprSegments + ptrValue(null, i32(Int2MInt(1:Int)));
        requires checkIntOfType(ComparisonValue, i32)
...

and like this:

    rule for Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in ptrValue(_, intRange(First, Last)) #as Range B:BlockExpression => 
            {
                .InnerAttributes
                let Patt = First;
                (for1 Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in Range B:BlockExpression):IteratorLoopExpression; 
                .NonEmptyStatements
            };
        requires checkIntOfSameType(First, Last)
    rule for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in ptrValue(_, intRange(_First, Last)) #as Range B:BlockExpression => 
                if (Patt :: .PathExprSegments):PathExprSegments < Last { .InnerAttributes B; (for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in Range B):IteratorLoopExpression;  .NonEmptyStatements};
            
    rule for2 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in ptrValue(_, intRange(_First, ptrValue(_, Last))) B:BlockExpression => 
            incrementPatt(Patt, Last)
            ~> for1 Patt:Identifier:PatternNoTopAlt | .PatternNoTopAlts in Range B

Note that:

1. This removes the need for using ptrValue(...) in a lot of places
2. Changing the start of the range was not needed since it was not actually used in for1 or for2

Because of 2, this means that you can probably write simpler code:

    syntax IteratorLoopExpression ::=  "for1" Pattern "limit" PtrValue BlockExpression
                                    | "for2" Pattern "limit" PtrValue BlockExpression

    rule for Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts in ptrValue(_, intRange(First, Last)) => 
            {
                .InnerAttributes
                let Patt = First;
                (for1 Patt:Identifier:PatternNoTopAlt | R:PatternNoTopAlts limit Last B:BlockExpression):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:Identifier:PatternNoTopAlt | .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

[virgil-serbanuta]

I would split this into multiple lines.

Also, you can probably inline the "for2" rule below if you want.

[ACassimiro]

Addresses #18.