Entiers

TYPE integer
  INHERIT number{integer}
  INHERIT total_order{integer}
    -- Generated by {zero, succ, pred}.

  MESSAGE nat_to_integer(n: nat)
    -- Type conversion operation for mixed-mode arithmetic.
    REPLY(i: integer)
    WHERE nat_to_integer(zero) = zero,
      ALL(n: nat ::
          nat_to_integer(succ(n)) = succ(nat_to_integer(n)) )

  MESSAGE is_nat(i: integer) REPLY(b: boolean)
    WHERE SOME(n: nat :: i = nat_to_integer(n))

  MESSAGE zero -- Literal 0 = zero.
    REPLY(i: integer)

  MESSAGE one -- Literal 1 = one.
    REPLY(i: integer) WHERE i = succ(zero)

  MESSAGE succ(i1: integer)
    -- Literal 2 = succ(1), literal 3 = succ(2), ...
    REPLY(i2: integer)

  MESSAGE pred(i1: integer)
    -- Literal -1 = pred(0), literal -2 = pred(-1), ...
    REPLY(i2: integer)

  MESSAGE "-"(i1: integer) REPLY(i2: integer)
    WHERE ALL(i: integer :: -i = 0 - i)

  MESSAGE abs(i1: integer) REPLY(i2: integer)
    WHERE i2 = IF i1 >= 0 THEN i1 ELSE -i1 FI

  MESSAGE "+"(i1 i2: integer) REPLY(i3: integer)
    WHERE ALL(i j: integer :: i + succ(j) = succ(i + j)),
      ALL(i j: integer :: i + pred(j) = pred(i + j))

  MESSAGE "-"(i1 i2: integer) REPLY(i3: integer)
    WHERE i1 = i2 + i3

  MESSAGE "*"(i1 i2: integer) REPLY(i3: integer)
    WHERE ALL(i j: integer :: i * succ(j) = (i * j) + i),
      ALL(i j: integer :: i * pred(j) = (i * j) - i)

  MESSAGE "/"(i1 i2: integer) 
    WHEN i2 ~= zero REPLY(q: integer)
      WHERE SOME(r: integer ::
                 i1 = q * i2 + r & abs(i2) > r >= 0 )
    OTHERWISE REPLY EXCEPTION divide_by_zero

  MESSAGE "MOD"(i1 i2: integer)
    -- i1 MOD i2 is also written i1 \\ i2.
    WHEN i2 ~= zero REPLY(r: integer)
      WHERE SOME(q: integer ::
                 i1 = q * i2 + r & abs(i2) > r >= 0 )
    OTHERWISE REPLY EXCEPTION divide_by_zero

  MESSAGE "^"(i: integer, n: nat) 
    WHEN i ~= 0 | n ~= 0 REPLY(j: integer)
      WHERE ALL(i: integer SUCH THAT i ~= 0 ::
                i ^ 0 = 1 & 0 ^ i = 0 ),
        ALL(i: integer, n: nat :: i ^ succ(n) = (i ^ n) * i)
    OTHERWISE REPLY EXCEPTION undefined_expt

  MESSAGE equal(i1 i2: integer) REPLY(b: boolean)
    WHERE ALL(i: integer :: succ(pred(i)) = i = pred(succ(i)))

  MESSAGE "<"(i1 i2: integer) REPLY(b: boolean)
    WHERE ALL(i: integer :: pred(i) < i < succ(i))
END