Fgl-syntactic-checker-binders
Functions for checking syntactic properties of objects, and inferring
the logical properties that they imply
These functions are useful for creating FGL rewrite rules that
prescribe some behavior based on the syntax of the objects passed in. See
binder for background on the FGL binder facility, which these depend on.
Each checker function, when encountered in the FGL interpreter, checks some
syntactic property of its input. Its logical definition reflects what it
checks. For example, (check-integerp ans x) implies (integerp x) in
its logical formulation. Under the FGL interpreter, when invoked as
(binder (check-integerp x-intp x)) where x-intp is an unbound
variable, its meta rule checks whether x can be syntactically determined
to be an integer; if so, it returns T.
Each of these checker functions also has a corresponding macro whose name is
suffixed with ! and simply wraps the function invocation in (binder
...).
Subtopics
- Integer-length-bound
- FGL binder that finds a bound for the integer-length of X if possible.
- Check-int-sign
- FGL binder that checks whether x is syntactically known to be either
positive or negative when fixed to an integer; returns 0 or -1 (the tail of the integer) if it can be
determined and NIL otherwise.
- Check-int-endp
- FGL binder that checks whether X is syntactically a int-endp, i.e.
either 0, -1, or not an integer.
- Check-unsigned-byte-p
- FGL binder that checks whether X is syntactically an unsigned integer of length at most n.
- Check-signed-byte-p
- FGL binder that checks whether X is syntactically a signed integer of length at most n.
- Check-integerp
- FGL binder that checks whether X is syntactically an integer.
- Check-true
- FGL binder that checks whether X is syntactically known true.
- Check-non-integerp
- FGL binder that checks whether X is syntactically a non-integer, i.e. known not to be an integer.
- Check-non-consp
- FGL binder that checks whether X is syntactically a non-cons.
- Check-non-booleanp
- FGL binder that checks whether X is syntactically a non-Boolean.
- Check-booleanp
- FGL binder that checks whether X is syntactically a Boolean.
- Check-natp
- FGL binder that checks whether X is syntactically a natural number.
- Check-equal
- FGL binder that checks whether X and Y are syntactically equal.
- Check-consp
- FGL binder that checks whether X is syntactically cons.
- Check-bitp
- FGL binder that checks whether X is syntactically a bit.
