[m-rev.] for review: define <<u and >>u

[Peter Wang]

On Tue, 06 Dec 2022 18:55:10 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 
> On Tue, 6 Dec 2022 17:44:28 +1100, Peter Wang <novalazy at gmail.com> wrote:
> 
> > On Tue, 06 Dec 2022 16:53:33 +1100 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> > > 
> > > As for const_prop, I have just done the required updates.
> > > I found the existing code strange, in that uint_emu.m reduces
> > > the unchecked shift ops to the checked ones,
> > > which I think is the right thing to do, while int_emu.m does not.
> > > And unchecked_{left,right}_shift in int_enu.m check their arguments
> > > using code that is (a) different from the checks in {left,right}_shift
> > > in int_emu.m, but (b) similar to the checks in {left,right}_shift in
> > > uint_emu.m.
> > > 
> > > Peter, you wrote the original int_emu.m. Do you remember the
> > > reason for (a)?
> > 
> > The additional checks in int_emu.unchecked_{left,right}_shift
> > are to ensure that they only succeed when the behaviour of
> > int.unchecked_{left,right}_shift is defined.
> 
> I didn't mean to imply that the checks in unchecked_{left,right}_shift
> should be changed. I think they are fine as they are, but those same
> checks should also be done by their checked versions. This is what is done
> in uint_emu.m.
> 
> And if the implementations of the emulations of checked and unchecked
> shifts are the same, then one can be deleted, and calls to the deleted
> predicate redirected to the other, which should then be renamed
> to avoid giving a misleading impression of specificity.

I see. It's because int_emu still implements the old behaviour of
int.(<<) and int.(>>) operations, which would succeed (not throw an
exception) for a shift amount outside the range range [0, bits_per_int).

If you merged the predicates and renamed it to
checked_or_unchecked_left_shift or something, that would be okay.
I would keep them as separate predicates. My original intention
was that each predicate in int_emu emulates the corresponding operation
in int.m.

Peter