make a tau interval
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.