machine-int.maude 3.87 KB
Newer Older
Joy Mitra's avatar
Joy Mitra committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
***(

    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