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