%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%--------------------------------------------------%
% Copyright (C) 1994-1998,2001-2008,2010, 2012 The University of Melbourne.
% Copyright (C) 2013-2016, 2018-2020 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%--------------------------------------------------%
%
% File: float.m.
% Main author: fjh.
% Stability: medium.
%
% Floating point support.
%
% Floats are double precision, except in .spf grades where they
% are single precision.
%
% Note that implementations which support IEEE floating point
% should ensure that in cases where the only valid answer is a "NaN"
% (the IEEE float representation for "not a number"), the det
% functions here will halt with a runtime error (or throw an exception)
% rather than returning a NaN. Quiet (non-signalling) NaNs have a
% semantics which is not valid in Mercury, since they don't obey the
% axiom "all [X] X = X".
%
% XXX Unfortunately the current Mercury implementation does not
% do that on all platforms, since neither ANSI C nor POSIX provide
% any portable way of ensuring that floating point operations
% whose result is not representable will raise a signal rather
% than returning a NaN. (Maybe C9X will help...?)
% The behaviour is correct on Linux and Digital Unix,
% but not on Solaris, for example.
%
% IEEE floating point also specifies that some functions should
% return different results for +0.0 and -0.0, but that +0.0 and -0.0
% should compare equal. This semantics is not valid in Mercury,
% since it doesn't obey the axiom `all [F, X, Y] X = Y => F(X) = F(Y)'.
% Again, the resolution is that in Mercury, functions which would
% return different results for +0.0 and -0.0 should instead halt
% execution with a run-time error (or throw an exception).
%
% XXX Here too the current Mercury implementation does not
% implement the intended semantics correctly on all platforms.
%
% XXX On machines such as x86 which support extra precision
% for intermediate results, the results may depend on the
% level of optimization, in particular inlining and evaluation
% of constant expressions.
% For example, the goal `1.0/9.0 = std_util.id(1.0)/9.0' may fail.
%
%--------------------------------------------------%
%--------------------------------------------------%

:- module float.
:- interface.

:- import_module pretty_printer.

%--------------------------------------------------%
%
% Arithmetic functions.
%

    % Addition.
    %
:- func (float::in) + (float::in) = (float::uo) is det.

    % Subtraction.
    %
:- func (float::in) - (float::in) = (float::uo) is det.

    % Multiplication.
    %
:- func (float::in) * (float::in) = (float::uo) is det.

    % Division.
    % Throws a `domain_error' exception if the right operand is zero.
    % See the comments at the top of math.m to find out how to disable
    % this check.
    %
:- func (float::in) / (float::in) = (float::uo) is det.

    % unchecked_quotient(X, Y) is the same as X / Y, but the behaviour
    % is undefined if the right operand is zero.
    %
:- func unchecked_quotient(float::in, float::in) = (float::uo) is det.

    % Unary plus.
    %
:- func + (float::in) = (float::uo) is det.

    % Unary minus.
    %
:- func - (float::in) = (float::uo) is det.

%--------------------------------------------------%
%
% Comparison predicates.
%

    % Less than.
    %
:- pred (float::in) < (float::in) is semidet.

    % Less than or equal.
    %
:- pred (float::in) =< (float::in) is semidet.

    % Greater than or equal.
    %
:- pred (float::in) >= (float::in) is semidet.

    % Greater than.
    %
:- pred (float::in) > (float::in) is semidet.

%--------------------------------------------------%
%
% Conversion from integer types.
%

    % Convert an int into float.
    %
    % The behaviour when the int exceeds the range of what can be exactly
    % represented by a float is undefined.
    %
:- func float(int) = float.

    % Convert a signed 8-bit integer into a float.
    % Always succeeds as all signed 8-bit integers have an exact
    % floating-point representation.
    %
:- func from_int8(int8) = float.

    % Convert a signed 16-bit integer into a float.
    % Always succeeds as all signed 16-bit integers have an exact
    % floating-point representation.
    %
:- func from_int16(int16) = float.

    % Convert a signed 32-bit integer into a float.
    % The behaviour when the integer exceeds the range of what can be
    % exactly represented by a float is undefined.
    %
:- func cast_from_int32(int32) = float.

    % Convert a signed 64-bit integer into a float.
    % The behaviour when the integer exceeds the range of what can be
    % exactly represented by a float is undefined.
    %
:- func cast_from_int64(int64) = float.

    % Convert an unsigned 8-bit integer into a float.
    % Always succeeds as all unsigned 8-bit integers have an exact
    % floating-point representation.
    %
:- func from_uint8(uint8) =  float.

    % Convert an unsigned 16-bit integer into a float.
    % Always succeeds as all unsigned 16-bit integers have an exact
    % floating-point representation.
    %
:- func from_uint16(uint16) = float.

    % Convert an unsigned 32-bit integer into a float.
    % The behaviour when the integer exceeds the range of what can be
    % exactly represented by a float is undefined.
    %
:- func cast_from_uint32(uint32) = float.

    % Convert an unsigned 64-bit integer into a float.
    % The behaviour when the integer exceeds the range of what can be
    % exactly represented by a float is undefined.
    %
:- func cast_from_uint64(uint64) = float.

%--------------------------------------------------%
%
% Conversion to int.
%

    % ceiling_to_int(X) returns the smallest integer not less than X.
    %
:- func ceiling_to_int(float) = int.

    % floor_to_int(X) returns the largest integer not greater than X.
    %
:- func floor_to_int(float) = int.

    % round_to_int(X) returns the integer closest to X.
    % If X has a fractional value of 0.5, it is rounded up.
    %
:- func round_to_int(float) = int.

    % truncate_to_int(X) returns the integer closest to X such that
    % |truncate_to_int(X)| =< |X|.
    %
:- func truncate_to_int(float) = int.

%--------------------------------------------------%
%
% Miscellaneous functions.
%

    % Absolute value.
    %
:- func abs(float) = float.

    % Maximum.
    %
:- func max(float, float) = float.

    % Minimum.
    %
:- func min(float, float) = float.

    % pow(Base, Exponent) returns Base raised to the power Exponent.
    % Fewer domain restrictions than math.pow: works for negative Base,
    % and pow(B, 0) = 1.0 for all B, even B=0.0.
    % Only pow(0, <negative>) throws a `domain_error' exception.
    %
:- func pow(float, int) = float.

    % Compute a non-negative integer hash value for a float.
    %
:- func hash(float) = int.
:- pred hash(float::in, int::out) is det.

%--------------------------------------------------%
%
% Classification.
%

    % True iff the argument is of infinite magnitude.
    %
:- pred is_infinite(float::in) is semidet.

    % Synonym for the above.
    %
:- pred is_inf(float::in) is semidet.

    % True iff the argument is not-a-number (NaN).
    %
:- pred is_nan(float::in) is semidet.

    % True iff the argument is of infinite magnitude or not-a-number (NaN).
    %
:- pred is_nan_or_infinite(float::in) is semidet.

    % Synonym for the above.
    %
:- pred is_nan_or_inf(float::in) is semidet.

    % True iff the argument is not of infinite magnitude and is not a
    % not-a-number (NaN) value.
    %
:- pred is_finite(float::in) is semidet.

    % True iff the argument is of zero magnitude.
    %
:- pred is_zero(float::in) is semidet.

%--------------------------------------------------%
%
% System constants.
%

    % Maximum finite floating-point number.
    %
    % max = (1 - radix ** mantissa_digits) * radix ** max_exponent
    %
:- func max = float.

    % Minimum normalised positive floating-point number.
    %
    % min = radix ** (min_exponent - 1)
    %
:- func min = float.

    % Positive infinity.
    %
:- func infinity = float.

    % Smallest number x such that 1.0 + x \= 1.0.
    % This represents the largest relative spacing of two consecutive floating
    % point numbers.
    %
    % epsilon = radix ** (1 - mantissa_digits)
    %
:- func epsilon = float.

    % Radix of the floating-point representation.
    % In the literature, this is sometimes referred to as `b'.
    %
:- func radix = int.

    % The number of base-radix digits in the mantissa.
    % In the literature, this is sometimes referred to as `p' or `t'.
    %
:- func mantissa_digits = int.

    % Minimum negative integer such that:
    %   radix ** (min_exponent - 1)
    % is a normalised floating-point number. In the literature,
    % this is sometimes referred to as `e_min'.
    %
:- func min_exponent = int.

    % Maximum integer such that:
    %   radix ** (max_exponent - 1)
    % is a normalised floating-point number.
    % In the literature, this is sometimes referred to as `e_max'.
    %
:- func max_exponent = int.

%--------------------------------------------------%

    % Convert a float to a pretty_printer.doc for formatting.
    %
:- func float_to_doc(float) = doc.

%--------------------------------------------------%
%--------------------------------------------------%