***( This file is part of the Maude 2 interpreter. Copyright 1997-2006 SRI International, Menlo Park, CA 94025, USA. This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA. ) *** *** Approximation of Maude 1.0 MachineInts. *** Version 2.3. *** *** Note that 0 lives in MachineZero. Also using out of range *** integer constants may cause incorrect results. MACHINE-INT may *** be instanciated using a view that maps $nrBits to any power of *** 2 that is >= 2. *** 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 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 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 fmod MACHINE-INT{X :: BIT-WIDTH} is *** *** Note that operations *** ~_ _&_ _|_ _<_ _<=_ _>_ _=>_ *** are inherited unmodified. *** 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