Type constraints for right-hand operand of shift operators #1158
Description
The following program:
input relation X(x: bit<16>, y: bit<16>)
output relation Y(x: bit<16>, y: bit<16>, z: bit<16>)
Y(x, y, x << y) :- X(x, y).
yields the following compiler error that I don't expect (with release v1.2.3 and earlier releases):
error: /home/blp/nerpa/nerpa/ofp4/test.dl:3.6-3.7: Unsatisfiable bit-width constraint '16 = 0' in
expected type: bit<16>
actual type: bit<32>
in
expression 'y'
Y(x, y, x << y) :- X(x, y).
^
I can fix it by casting y to u32 in the shift expression, like this:
Y(x, y, x << (y as u32)) :- X(x, y).
I would prefer that << (and presumably >>) accept any integer type as its right-hand operand.