Machine integers

Versions of Maude prior to 2.0 supported machine integers in place of arbitrary size integers. Initially they were 32-bit in Maude 1.0 but were increased to 64-bit in Maude 1.0.5.

For certain applications, such as specifying programming languages that support machine integers as a built-in data type, it is convenient to have a predefined specification for machine integers. Fortunately, it is straightforward to efficiently emulate machine integers in terms of arbitrary size integers.

First we rename a copy of the regular integers, giving the sorts new names consistent with the new semantics and renaming those operators that either will not be defined on machine integers or else will have new semantics. Note that the operators ~_, _&_, _|_, _<_, _<=_, _>_, and _=>_ are not modified by the renaming.

  fmod RENAMED-INT is
    protecting INT * (sort Zero to MachineZero,
                      sort NzNat to NzMachineNat,
                      sort Nat to MachineNat,
                      sort NzInt to NzMachineInt,
                      sort Int to MachineInt,
                      op s_ : Nat -> NzNat to $succ,
                      op sd : Nat Nat -> Nat to $sd,
                      op -_ : Int -> Int to $neg,
                      op _+_ : Int Int -> Int to $add,
                      op _-_ : Int Int -> Int to $sub,
                      op _*_ : NzInt NzInt -> NzInt to $mult,
                      op _quo_ : Int NzInt -> Int to $quo,
                      op _rem_ : Int NzInt -> Int to $rem,
                      op _^_ : Int Nat -> Int to $pow,
                      op abs : NzInt -> NzNat to $abs,
                      op gcd : NzInt Int -> NzNat to $gcd,
                      op lcm : NzInt NzInt -> NzNat to $lcm,
                      op min : NzInt NzInt -> NzInt to $min,
                      op max : NzInt NzInt -> NzInt to $max,
                      op _xor_ : Int Int -> Int to $xor,
                      op _>>_ : Int Nat -> Int to  $shr,
                      op _<<_ : Int Nat -> Int to $shl,
                      op _divides_ : NzInt Int -> Bool to $divides) .
  endfm

We then give a parameter theory that specifies the number of bits in a machine integer, which must be a power of 2, greater or equal to 2. Notice that this theory is based on the previous module, which is imported in protecting mode. Therefore, $nrBits is a parameter constant ranging over the NzMachineNat sort in the RENAMED-INT module, which is imported with an initial algebra semantics.

  fth BIT-WIDTH is
    protecting RENAMED-INT .
    op $nrBits : -> NzMachineNat .

    var N : NzMachineNat .
    eq $divides(2, $nrBits) = true [nonexec] .
    ceq $divides(2, N) = true 
      if $divides(N, $nrBits) /\ N > 1 [nonexec] .
  endfth

Also provided are two predefined views that set the number of bits value $nrBits respectively to 32 and 64, the two most common sizes.

  view 32-BIT from BIT-WIDTH to RENAMED-INT is
    op $nrBits to term 32 .
  endv

  view 64-BIT from BIT-WIDTH to RENAMED-INT is
    op $nrBits to term 64 .
  endv

The module MACHINE-INT takes a bit width parameter and defines those operations that have a new semantics when applied to machine integers. In many cases this means applying the operation $wrap to the results to correctly simulate the wrap-around effect over an overflow on signed fixed bit width integers by, in effect, extending the sign bit infinitely to the left. In the case of _^_ the meaning of the operation changes to exclusive or (from exponentiation on arbitrary size integers).

  fmod MACHINE-INT{X :: BIT-WIDTH} is

    vars I J : MachineInt .
    var K : NzMachineInt .

    op $mask : -> NzMachineInt [memo] .
    eq $mask = $sub($nrBits, 1) .

    op $sign : -> NzMachineInt [memo] .
    eq $sign = $pow(2, $mask) .

    op maxMachineInt : -> NzMachineInt [memo] .
    eq maxMachineInt = $sub($sign, 1) .

    op minMachineInt : -> NzMachineInt [memo] .
    eq minMachineInt = $neg($sign) .

    op $wrap : MachineInt -> MachineInt .
    eq $wrap(I) = (I & maxMachineInt) | $neg(I & $sign) .

    op _+_ : MachineInt MachineInt -> MachineInt 
        [assoc comm prec 33] .
    eq I + J = $wrap($add(I, J)) .

    op -_ : MachineInt -> MachineInt .
    eq - I = $wrap($neg(I)) .

    op _-_ : MachineInt MachineInt -> MachineInt 
        [prec 33 gather (E e)] .
    eq I - J = $wrap($sub(I, J)) .

    op _*_ : MachineInt MachineInt -> MachineInt 
        [assoc comm prec 31] .
    eq I * J = $wrap($mult(I, J)) .

    op _/_ : MachineInt NzMachineInt -> MachineInt 
        [prec 31 gather (E e)] .
    eq I / K = $wrap($quo(I, K)) .

    op _%_ : MachineInt NzMachineInt -> MachineInt 
        [prec 31 gather (E e)] .
    eq I % K = $rem(I, K) .

    op _^_ : MachineInt MachineInt -> MachineInt 
        [prec 55 gather (E e)] .
    eq I ^ J = $xor(I, J) .

    op _>>_ : MachineInt MachineInt -> MachineInt 
        [prec 35 gather (E e)] .
    eq I >> J = $shr(I, ($mask & J)) .

    op _<<_ : MachineInt MachineInt -> MachineInt 
        [prec 35 gather (E e)] .
    eq I << J = $wrap($shl(I, ($mask & J))) .
  endfm

Notice that using out of range integer constants may cause incorrect results.

We consider now the instantiation with the predefined view 32-BIT, and show the wrap-around effect in several examples.

  fmod MACHINE-INT-TEST is
    protecting MACHINE-INT{32-BIT} .
  endfm

In the first examples, we can see the wrap-around from negative to positive and vice versa:

  Maude> red -2147483648 - 1 .
  result NzMachineNat: 2147483647

  Maude> red 2147483647 + 1 .
  result NzMachineInt: -2147483648

In the following product, the negative case does not wrap-around but the positive case does:

  Maude> red -1073741824 * 2 .
  result NzMachineInt: -2147483648

  Maude> red 1073741824 * 2 .
  result NzMachineInt: -2147483648

Division can only cause a wrap-around in this one case:

  Maude> red -2147483648 / -1 .
  result NzMachineInt: -2147483648

Remainder never wraps around:

  Maude> red -2147483648 % -1 .
  result MachineZero: 0

Finally, we see that the sign bit ``falls off the left end'' in a left shift:

  Maude> red -2147483648 << 1 .
  result MachineZero: 0

The parameterized MACHINE-INT module is an interesting example of Maude's support for what in type theory are called dependent types (see, for example, [55]). These are types like the power type X$^\texttt{[n]}$ or the ARRAY{X,[n]} type depending on a data parameter n, for example a natural number. We can view MACHINE-INT as the Maude analogue of a dependent type definition; however, note that the data parameter is not just any nonzero natural number, but must also satisfy additional axioms, specified in the BIT-WIDTH theory. For two other interesting examples of a Maude parameterized module defining the analogue of a dependent type, see the POWER[n] module in Section 14.3.1 (the exact analogue of the power type X$^\texttt{[n]}$) and the NAT/{N} module of natural numbers modulo N in Section 15.7. Similarly, the TUPLE[n] module in Section 14.3.1 provides a form of dependent type that is not even available in some type theories with dependent types.