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.
