Réels

TYPE real
  INHERIT field{real}
  INHERIT total_order{real}
  INHERIT exponenetials{real}
  INHERIT trigonometry{real}

  MESSAGE rational_to_real(r1: rational)
    -- Type conversion operation for mixed-mode arithmetic.
    REPLY(r2: real)
    WHERE rational_to_real(zero) = zero,
      rational_to_real(one) = one,
      ALL(x y: rational ::
          rational_to_real(x - y) =
          rational_to_real(x) - rational_to_real(y) ),
      ALL(x y: rational SUCH THAT y ~= zero ::
          rational_to_real(x / y) =
          rational_to_real(x) / rational_to_real(y) )

  MESSAGE integer_to_real(i: integer)
    -- Type conversion operation for mixed-mode arithmetic.
    REPLY(r: real)
    WHERE r = rational_to_real(integer_to_rational@rational(i))

  MESSAGE nat_to_real(n: nat)
    -- Type conversion operation for mixed-mode arithmetic.
    REPLY(r: real)
    WHERE r = rational_to_real(nat_to_rational@rational(n))

  MESSAGE is_rational(r: real)
    REPLY(b: boolean)
    WHERE SOME(i: integer :: r = rational_to_real(i))

  MESSAGE is_integer(r: real)
    REPLY(b: boolean)
    WHERE SOME(i: integer :: r = integer_to_real(i))

  MESSAGE is_nat(r: real)
    REPLY(b: boolean)
    WHERE SOME(n: nat :: r = nat_to_real(n))

  MESSAGE zero -- Literal 0.0 = zero.
    REPLY(r: real)

  MESSAGE one -- Literal 1.0 = one.
    REPLY(r: real)

  MESSAGE pi REPLY(i: real)
    WHERE pi = MINIMUM(r: real SUCH THAT r > zero & sin(r) = zero :: r)

  MESSAGE e REPLY(i: real)
    WHERE e = exp(one)

  MESSAGE "-"(r1: real) REPLY(r2: real)
    WHERE r2 = zero - r1

  MESSAGE abs(r1: real) REPLY(r2: real)
    WHERE r2 = IF r1 >= zero THEN r1 ELSE -r1 FI

  MESSAGE "+"(r1 r2: real) REPLY(r3: real)

  MESSAGE "-"(r1 r2: real) REPLY(r3: real)
    WHERE r1 = r2 + r3

  MESSAGE "*"(r1 r2: real) REPLY(r3: real)

  MESSAGE "/"(r1 r2: real)
    WHEN r2 ~= zero REPLY(r3: real)
      WHERE r1 = r2 * r3
    OTHERWISE REPLY EXCEPTION divide_by_zero

  MESSAGE "MOD"(r1 r2: real)
    -- r1 MOD r2 is also written r1 \\ r2.
    WHEN r2 ~= zero REPLY(r: real)
      WHERE SOME(q: real :: r1 = q * r2 + r &
                            abs(r2) > r >= zero &
                            is_integer(q) )
    OTHERWISE REPLY EXCEPTION divide_by_zero

  MESSAGE "^"(r1 r2: real)
    WHEN (r1 = zero & r2 <= zero) | (r1 < zero & ~is_integer(r2))
      REPLY EXCEPTION undefined_expt
    OTHERWISE REPLY(r3: real)
      WHERE ALL(r: real :: r ^ 1.0 = r),
        ALL(r: real SUCH THAT r > zero :: zero ^ r = zero),
        ALL(r x y: real SUCH THAT
            r > zero | r < zero & is_integer(x) &
              is_integer(y) ::
            r ^ (x + y) = (r ^ x) * (r ^ y) )

  MESSAGE equal(r1 r2: real) REPLY(b: boolean)

  MESSAGE "<"(r1 r2: real) REPLY(b: boolean)
    WHERE ALL(x y: rational ::
              rational_to_real(x) < rational_to_real(y) <=>
              x < y ),
      ALL(x y z: real :: x + y < x + z <=> y < z),
      ALL(x y z: real SUCH THAT x > zero ::
          x * y < x * z <=> y < z ),
      ALL(x y z: real SUCH THAT x < zero ::
          x * y < x * z <=> y > z )
END