2.4.2 The Machine Integers

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