Abstraction: xreal
Version: 1
Date: 5 November, 2002
Author: Mike O'Donnell

Depends: ratintvl version >= 1

Values in the xreal abstraction are exact real numbers. Each xreal x
determines a method for producing an arbitrarily small ratintvl
contain x.

Types
-----

xreal       exact real numbers

xrealcomp   tokens indicating the result of a comparison of xreals

Constructors
------------

lt_xrealcomp is the token indicating that one xreal is less than another.

in_xrealcomp is the token indicating that two xreals are
    indistinguishable at a particular precision.

gt_xrealcomp is the token indicating that one xreal is greater than another.

Type conversions in
-------------------

(rational->xreal r) returns an xreal numerically equal to the rational r.

    If r is not a rational, report an error.

Predicates
----------

(xreal? expr) returns #t if expr is an xreal, #f otherwise.

    xreal? requires an otherwise unneccesary tag in the representation
    of an xreal, so we may decide to skip it.

(member_xreal_ratintvl? xr ri) returns #t if the xreal xr is a member
    of the ratintvl ri, #f otherwise.

    If ri = [xr,xr], the procedure computes infinitely.

    If ri is a single point, the procedure may optionally report a
    warning.

(xrealcomp? expr) returns #t if expr is an xrealcomp, #f otherwise.

(lt_xrealcomp? xrc) returns #t if xrc is lt_xrealcomp, #f otherwise.

    If xrc is not an xrealcomp, report an error.

(in_xrealcomp? xrc) returns #t if xrc is in_xrealcomp, #f otherwise.

    If xrc is not an xrealcomp, report an error.

(gt_xrealcomp? xrc) returns #t if xrc is gt_xrealcomp, #f otherwise.

    If xrc is not an xrealcomp, report an error.

Comparisons
-----------

(comporder_xreal xr1 xr2 prec) returns nondeterministically one of

        lt_xrealcomp if xr1 < xr2
        in_xrealcomp if |xr1 - xr2| < prec
        gt_xrealcomp if xr1 > xr2

    If xr1 = xr2 and prec = 0, then the procedure computes infinitely.

    Usually, an implementation should prefer ltxreal_comp or
    gtxreal_comp when possible at the same cost as inxreal_comp.

    If prec < 0, report an error.

Operations
----------

(add_xreal xr1 xr2) returns the sum of two xreals xr1+xr2 as an xreal.

(sub_xreal xr1 xr2) returns the difference of two xreals xr1-xr2 as an xreal.

(mult_xreal xr1 xr2) returns the product of of two xreals xr1*xr2 as an xreal.

(div_xreal xr1 xr2) returns the ratio of two xreals xr1/xr2 as an xreal.

(power_xreal xr1 n) returns an xreal to an integer power xr1^n as an xreal.

(exp_xreal xr) returns the exponential function of an xreal e^xr.

(ln_xreal xr) returns the natural logarithm of an xreal ln(xr).

(expt_xreal xr1 xr2) returns an xreal to an xreal power xr1^xr2 as an xreal.

Type conversions out
--------------------

(abs_xreal->ratintvl xr a) returns a ratintvl of absolute tolerance (width)
    at most (rational) a containing the xreal xr.

(rel_xreal->ratintvl xr r) returns a ratintvl of relative tolerance at
    most (rational) r containing the xreal xr.

    If xr = 0. 

    rel_xreal->ratintvl is much harder than abs_xreal->ratintvl, so we
    may decide to skip it.

(simplest_xreal->rational ri a) returns the simplest rational r
    such that |r - ri| < a, where a is a rational absolute tolerance.

    simplest_xreal->rational is a bit hard, so we may decide to skip
    it.

Diagnostic utilities
--------------------

(abs_xreal->ratintvllist xr alist) returns a list of ratintvls with
    absolute tolerances in the (rational) list alist containing the
    xreal xr. Normally, if

        alist = (a1 ... an)

   then the returned value is

        ((abs_xreal->ratintvl xr a1) ... (abs_xreal->ratintvl xr an))

    Normally, the values in alist are strictly decreasing, and the
    ratintvls in the returned list are strictly contained in one
    another. But correct implementations may deviate from these norms
    depending on need.

String representations
----------------------

(decimal_sn_xreal->string ri prec) returns a string representing the
    xreal ri in scientific notation with (integer) prec >= 0
    significant digits.

    If prec < 0, report an error.

(decimal_xreal->string ri prec) returns a string representing the

    xreal ri in normal decimal notation with (integer) prec digits to
    the right of the decimal point. If prec < 0, provide |prec|
    insignificant trailing 0s to the left of the decimal point.

(std_rtintvllist->string rilist) returns a character string displaying the
    intervals in the list rilist of ratintvls. std_rtintvllist->string
    is particularly intended to be used with abs_xreal->ratintvllist
    for diagnostic purposes. We may experiment with the most useful
    form of display.