Unary minus unsupported in math expressions

[senier]

Expressions with unary minus (aka. negation) are not excepted by our parser:

>>> from rflx.parser import *
>>> grammar.mathematical_expression().parseString("-X")
...
pyparsing.ParseException: Expected {{"and" | "or"} term | {{{{{"=" | "/="} | "<="} | "<"} | ">="} | ">" | {"in" | "not in"}} term}, found '-'  (at char 0), (line:1, col:1)

Why is it needed? Our simplification produces these kind of expressions:

>>> str(Sub(Variable("X"), Mul(Variable("Y"), Number(8))).simplified())
'X + Y * (-8)'

If we want to be able to parse the result, we need to support unary minus. Another option would be to fix the simplification to avoid these changes.

[treiher]

I would propose to add support for negative numeric literals (e.g., -8). Adding support for unary minus for expressions in general would be a bigger change and I don't see a benefit in that. The problem with the expression shown above is not only the sign, but also the parentheses. Currently, numeric literals in parentheses are interpreted as aggregate (e.g., (8) is parsed as Aggregate(Number(8)).

Option 1: Only support negative numeric literals without parentheses

X + Y * -8.

Con: This interpretation is not consistent to Ada. The need for removing parentheses is uncommon and thus confusing.

Option 2: Change syntax of aggregates with single element

2.1: (0 => -8)

Pro: Similar to Ada.
Con: As we don't have index types in our arrays, using 0 (or any other number) seems arbitrary and could be confusing. On the other hand we could also define 0 as the first index of all our arrays (similar to C).

2.2: (-8,)

Pro: Simple and obvious syntax.
Con: Syntax is contrary to Ada.

[senier]

Option 3: Change syntax of aggregates

<-8> / <1, 2, 3> or {-8} / {1, 2, 3} or [-1] / [1, 2, 3]

Pro: No ambiguities wrt. to parenthesizing
Con: Syntax inconsistent with Ada

[senier]

Option 2.1 is something I always hated about Ada aggregates and I always found it a confusing technicality. I don't think option 1 is favorable either - users will be confused about expressions that look perfectly valid.

Option 2.2 is okayish, but the difference between a single-element aggregate and a parenthesized number is still minimal (which again may confuse users). I'm also not a big fan of the trailing comma. Maybe we should switch to backets like in Python lists? Aggregates are not that common in our specs after all and I don't want to be Ada-compatible at any cost.

@jklmnn @treiher What do you think?

[treiher]

I like the idea of using square brackets. That would be my preferred option. 2.2 would be fine too.

[jklmnn]

Option 2.1 is clear as long as one is used to the Ada syntax, it might be confusing otherwise.

Option 2.2 is something I really dislike as it introduces an error possibility by forgetting a single symbol (especially since the error leads to changing the type of the expression instead of an invalid syntax).

Option 3 with square brackets would be okay for me since this is a common syntax for aggregates and also already discussed here.

[senier]

Option 3 with square brackets would be okay for me since this is a common syntax for aggregates and also already discussed here.

Interesting! Then square brackets it is.

[treiher]

Introducing an expression representation which is incompatible with Ada has some implications. Currently, we just use the same expression classes for representing our specification in Python as for generating Ada code. This will not work anymore, when aggregates have a different syntax. That is why I would decouple both representations by duplicating the existing expression hierarchy into the Ada module. This separation has also the advantage, that it makes clear which expressions need support for additional functionality like simplification, substitution, Z3 proof or typing, and which not (expressions in our specification vs. expressions needed for Ada). Expr will get a method ada_expr which creates a corresponding Ada representation (similar to z3expr).