Allow using normal division operator for integer division

[viper-admin]

Created by @marcoeilers on 2017-06-28 13:36
Last updated on 2017-11-27 14:28

Silver currently interprets "/" as a division resulting in a permission, and "" as integer division. Since "/" is the normal division operator people know from other languages, it would be preferable if it could also be used for integer division. The type checker can figure out which one is meant from the expected type of the expression.

However, in some expressions, the type is ambiguous (e.g. (1/2) * (2/1), this could either be equal to a full permission or to zero). In these cases, the user needs to be able to reliably get the result they want. The type checker should therefore default to a perm-expression if both options are valid, and the user can simply use the old "" operator in these cases (which we might want to keep anyway for backwards compatibility).

[viper-admin]

@mschwerhoff commented on 2017-11-26 15:25

@marcoeilers Is this issue still valid as-is? I thought you had worked on this during some hackathon.

[viper-admin]

@mschwerhoff on 2017-11-26 17:51:

• changed component from (none) to Parser

[viper-admin]

@marcoeilers commented on 2017-11-27 11:04

No, I have implemented this as described above.
What's left is that I wanted to check, at some point, if the case where the type is ambiguous and we default to Perm actually occurs in code that we have (e.g. in the test suite).

[viper-admin]

@alexanderjsummers commented on 2017-11-27 12:01

By the way, I think the error messages still display the old symbol (maybe the pretty-printer still needs updating)

[viper-admin]

@marcoeilers commented on 2017-11-27 14:28

The problem with that is that as long as there may be ambiguous situations, printing integer division as "/" might mean that we print a program with a different meaning than the original (because the original might actually contain "", which is still allowed and the only way to enforce integer division in potentially ambiguous places).