Major Section: TAU-SYSTEM

General Form: (tau-intervalp x)

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 and the upper and lower bounds of the
objects recognized by the tau.

Restrictions on the components of an interval are as follows. For an
interpretation of the meaning of the components, see `in-tau-intervalp`

or
`make-tau-interval`

.

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

,
`RATIONALP`

, `ACL2-NUMBERP`

, or `NIL`

.

The two ``relations,'' *lo-rel* and *hi-rel*, must be Booleans.

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

or explicit rational numbers.
*Lo* must be no greater than *hi* (where `nil`

s represent negative or
positive infinity for *lo* and *hi* respectively.

Finally, if the *dom* is `INTEGERP`

, then both relations must `nil`

and *lo* and *hi* must be integers when they are non-`nil`

.

Recall that `make-tau-interval`

constructs intervals. The intervals it
constructs are well-formed only if the arguments to `make-tau-interval`

satisfy
the rules above; `make-tau-interval`

does not coerce or adjust its
arguments in any way. Thus, it can be (mis-)used to create non-intervals.
Here are examples of `tau-intervalp`

using `make-tau-interval`

.

; integers: 0 <= x <= 10: (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10)) = t ; integers: 0 <= x (i.e., the natural numbers): (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil nil)) = t ; violations of domain rules: (tau-intervalp (make-tau-interval 'INTEGERP t 0 t 10)) = nil (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10/11)) = nil ; violation of rule that bounds must be rational if non-nil: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t #c(3 5))) = nil ; violation of rule that lo <= hi: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t -10)) = nil ; rationals: 0 < x <= 22/7: (tau-intervalp (make-tau-interval 'RATIONALP t 0 nil 22/7)) = t ; numbers: -10 < x < 10: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t -10 t 10)) = t ; any: -10 < x < 10: (tau-intervalp (make-tau-interval nil t -10 t 10)) = t : any: (tau-intervalp (make-tau-interval nil nil nil nil nil)) = tNote that the second-to-last interval, with domain

`nil`

contains all
non-numbers as well as numbers strictly between -10 and 10. The reason is
that the interval contains `0`

and all non-numbers are coerced to `0`

by
the inequality functions.Note that the last interval contains all ACL2 objects. It is called the ``universal interval.''