shiftL package:sbv

A definition of shiftLeft that can deal with variable length shifts. (Note that the `shiftL` method from the Bits class requires an Int shift amount.) Unfortunately, this'll generate rather clumsy C code due to the use of tables etc., so we uninterpret it for code generation purposes using the cgUninterpret function.

Generalization of shiftL, when the shift-amount is symbolic. Since Haskell's shiftL only takes an Int as the shift amount, it cannot be used when we have a symbolic amount to shift with.

Generalization of svShl, where the shift-amount is symbolic.

Test function that uses shiftLeft defined above. When used as a normal Haskell function or in verification the definition is fully used, i.e., no uninterpretation happens. To wit, we have:

>>> tstShiftLeft 3 4 5
224 :: SWord32

>>> prove $ \x y -> tstShiftLeft x y 0 .== x + y
Q.E.D.