True-list-fix
Coerce to a true list
Many functions that process lists follows the true-list-fix
convention: whenever f is given some non-true-listp x
where it expected a list, that is, some x with a non-nil final-cdr, it will act as though it had been given (true-list-fix x)
instead. As a few examples, logically,
- (endp x) ignores the final cdr of x
- (len x) ignores the final cdr of x
- (append x y) ignores the final cdr of x (but not
y)
- (member a x) ignores the final cdr of x
True-list-fix is often useful when writing theorems about how
list-processing functions behave. For example, it allows us to write strong,
hypothesis-free theorems such as:
(equal (character-listp (append x y))
(and (character-listp (true-list-fix x))
(character-listp y)))
Indeed, true-list-fix is the basis for list-equiv, an extremely
common equivalence relation.
Efficiency note. In practice, most lists are nil-terminated. As an
optimization, true-list-fix tries to avoid any consing by first checking
whether its argument is a true-listp, and, in that case, it simply
returns its argument unchanged.
For a logically equivalent utility that returns its argument unchanged
(with no checking) during normal evaluation, see the-true-list.
Function: true-list-fix-exec
(defun true-list-fix-exec (x)
(declare (xargs :guard t))
(if (consp x)
(cons (car x)
(true-list-fix-exec (cdr x)))
nil))
Function: true-list-fix
(defun true-list-fix (x)
(declare (xargs :guard t))
(mbe :logic
(if (consp x)
(cons (car x) (true-list-fix (cdr x)))
nil)
:exec
(if (true-listp x)
x
(true-list-fix-exec x))))
