Major Section: TAU-SYSTEM

General Form: (make-tau-interval doc lo-rel lo hi-rel hi)

An interval is a structure of the form: `(`

*dom* `(`

*lo-rel* `.`

*lo*`)`

`.`

`(`

*hi-rel* `.`

*hi*`))`

. Every tau contains an
interval used to represent the domain, the upper, and the lower bounds of the
objects recognized by the tau.

`make-tau-interval`

constructs well-formed intervals only if its five arguments
satisfy certain restrictions given below. When these restrictions are
violated `make-tau-interval`

can construct objects that are not intervals!
`make-tau-interval`

does not attempt to coerce or adjust its arguments to make
well-formed intervals.

For examples of intervals (and non-intervals!) constructed by
`make-tau-interval`

see `tau-intervalp`

. For examples of what objects are
contained in certain intervals, see `in-tau-intervalp`

.

The components of an interval are as follows:

*dom* (``domain'') -- must be one of four symbols: `INTEGERP`

,
`RATIONALP`

, `ACL2-NUMBERP`

, or `NIL`

denoting no restriction
on the domain.

The two ``relations,'' *lo-rel* and *hi-rel* are Booleans, where `t`

denotes less-than inequality (`<`

) and `nil`

represents
less-than-or-equal inequality (`<=`

). Think of `t`

meaning ``strong''
and `nil`

meaning ``weak'' inequality.

*Lo* and *hi* must be either `nil`

or explicit rational numbers. If
*lo* is `nil`

it denotes negative infinity; if *hi* is `nil`

it
denotes positive infinity. *Lo* must be no greater than *hi*.
*Note*: Even though `ACL2-NUMBERP`

intervals may contain complex
rationals, the *lo* and *hi* bounds must be rational. This is an
arbitrary decision made by the implementors to simplify coding.

Finally, if the *dom* is `INTEGERP`

, then both relations should be weak
and *lo* and *hi* must be integers when they are non-`nil`

.

For *x* to be ``in'' an interval it must be of the type described
by the domain predicate *dom*, *lo* must be smaller than *x* in the
strong or weak sense denoted by *lo-rel*, and *x* must be smaller than
*hi* in the strong or weak sense denoted by *hi-rel*.

The components of an interval may be accessed with the functions
`tau-interval-dom`

, `tau-interval-lo-rel`

, `tau-interval-lo`

,
`tau-interval-hi-rel`

, and `tau-interval-hi`

.