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