The machine integers are defined below. The constants in this module represent the C++ data type int, as elements of a sort MachineInt, with a subsort NzMachineInt of nonzero machine integers. The first two operator declarations illustrate the way of linking the built-in integer constants to the sorts MachineInt and NzMachineInt. The other operations declared in the module represent their C++ counterparts with the same notation; their meaning is indicated in the associated comments. The division and remainder operations produce an unreduced error term if their second argument is zero. The machine integers provide a fast arithmetic data type for general purpose programming and for metalevel hooks into the rewriting engine.
fmod MACHINE-INT is sorts MachineInt NzMachineInt . subsort NzMachineInt < MachineInt . op <MachineInts> : -> NzMachineInt [special ( ... )] . op <MachineInts> : -> MachineInt [special ( ... )] . op -_ : MachineInt -> MachineInt [prec 15 special ( ... )] . *** minus op -_ : NzMachineInt -> NzMachineInt [prec 15 special ( ... )] . *** minus op ~_ : MachineInt -> MachineInt [prec 15 special ( ... )] . *** bitwise complement op _+_ : MachineInt MachineInt -> MachineInt [prec 33 gather (E e) special ( ... )] . *** addition op _-_ : MachineInt MachineInt -> MachineInt [prec 33 gather (E e) special ( ... )] . *** difference op _*_ : MachineInt MachineInt -> MachineInt [prec 31 gather (E e) special ( ... )] . *** multiplication op _*_ : NzMachineInt NzMachineInt -> NzMachineInt [prec 31 gather (E e) special ( ... )] . *** multiplication op _/_ : MachineInt NzMachineInt -> MachineInt [prec 31 gather (E e) special ( ... )] . *** division op _%_ : MachineInt NzMachineInt -> MachineInt [prec 31 gather (E e) special ( ... )] . *** remainder op _&_ : MachineInt MachineInt -> MachineInt [prec 53 gather (E e) special ( ... )] . *** bitwise and op _|_ : MachineInt MachineInt -> MachineInt [prec 57 gather (E e) special ( ... )] . *** bitwise or op _|_ : NzMachineInt NzMachineInt -> NzMachineInt [prec 57 gather (E e) special ( ... )] . *** bitwise or op _^_ : MachineInt MachineInt -> MachineInt [prec 55 gather (E e) special ( ... )] . *** bitwise xor op _>>_ : MachineInt MachineInt -> MachineInt [prec 35 gather (E e) special ( ... )] . *** left shift op _<<_ : MachineInt MachineInt -> MachineInt [prec 35 gather (E e) special ( ... )] . *** right shift op _<_ : MachineInt MachineInt -> Bool [prec 37 special ( ... )] . *** less than op _<=_ : MachineInt MachineInt -> Bool [prec 37 special ( ... )] . *** less or equal than op _>_ : MachineInt MachineInt -> Bool [prec 37 special ( ... )] . *** greater than op _>=_ : MachineInt MachineInt -> Bool [prec 37 special ( ... )] . *** greater or equal than endfm