Major Section: PROGRAMMING

Non-characters in the given list are coerced to the character with code 0.

Major Section: PROGRAMMING

For a nonnegative integer `size`

, `(Make-list size)`

is a list of
elements of length `size`

, each of which is initialized to the
`:initial-element`

(which defaults to `nil`

).

`Make-list`

is a macro in ACL2, defined in terms of a tail
recursive function `make-list-ac`

whose guard requires `size`

to
be a nonnegative integer. `Make-list`

is a Common Lisp function.
See any Common Lisp documentation for more information.

Major Section: PROGRAMMING

`(Max x y)`

is the larger of the numbers `x`

and `y`

.

The guard for `max`

requires its arguments to be rational numbers.

`Max`

is a Common Lisp function. See any Common Lisp documentation
for more information.

`eql`

as test
Major Section: PROGRAMMING

`(Member x l)`

equals the longest tail of `l`

that begins with
`x`

, or else `nil`

if no such tail exists.

`(Member x l)`

is provably the same in the ACL2 logic as
`(member-equal x l)`

. It has a stronger guard than `member-equal`

because uses `eql`

to test for whether `x`

is equal to a given
member of `l`

. Its guard requires that `l`

is a true list, and
moreover, either `(eqlablep x)`

or all members of `l`

are
`eqlablep`

. See member-equal and see member-eq.

`Member`

is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot
take keyword arguments (though macros can), the ACL2 functions
`member-equal`

and `member-eq`

are defined to correspond to calls
of the Common Lisp function `member`

whose keyword argument
`:test`

is `equal`

or `eq`

, respectively.

`eq`

as test
Major Section: PROGRAMMING

`(Member-eq x lst)`

equals the longest tail of `lst`

that
begins with `x`

, or else `nil`

if no such tail exists.

`(Member-eq x lst)`

is provably the same in the ACL2 logic as
`(member x lst)`

and `(member-equal x lst)`

, but it has a stronger
guard because it uses `eq`

for a more efficient test for whether
`x`

is equal to a given member of `lst`

. Its guard requires that
`lst`

is a true list, and moreover, either `x`

is a symbol or
`lst`

is a list of symbols. See member-equal and
see member.

Major Section: PROGRAMMING

`(Member-equal x lst)`

equals the longest tail of `lst`

that
begins with `x`

, or else `nil`

if no such tail exists.

`(Member-equal x lst)`

has a guard of `(true-listp lst)`

.
`Member-equal`

has the same functionality as the Common Lisp
function `member`

, except that it uses the `equal`

function to
test whether `x`

is the same as each successive element of `lst`

.
See member and see member-eq.

Major Section: PROGRAMMING

`(Min x y)`

is the smaller of the numbers `x`

and `y`

.

The guard for `min`

requires its arguments to be rational numbers.

`Min`

is a Common Lisp function. See any Common Lisp documentation
for more information.

Major Section: PROGRAMMING

`(Minusp x)`

is true if and only if `x < 0`

.

The guard of `minusp`

requires its argument to be a rational number.

`Minusp`

is a Common Lisp function. See any Common Lisp
documentation for more information.

`floor`

Major Section: PROGRAMMING

ACL2 !>(mod 14 3) 2 ACL2 !>(mod -14 3) 1 ACL2 !>(mod 14 -3) -1 ACL2 !>(mod -14 -3) -2 ACL2 !>(mod -15 -3) 0 ACL2 !>

`(Mod i j)`

is that number `k`

that `(* j (floor i j))`

added to
`k`

equals `i`

.
The guard for `(mod i j)`

requires that `i`

and `j`

are rational
numbers and `j`

is non-zero.

`Mod`

is a Common Lisp function. See any Common Lisp documentation
for more information.

Major Section: PROGRAMMING

`Mv`

is the mechanism provided by ACL2 for returning two or more
values. Logically, `(mv x1 x2 ... xn)`

is the same as
`(list x1 x2 ... xn)`

, a list of the indicated values. However,
ACL2 avoids the cost of building this list structure, with the cost
that `mv`

may only be used in a certain style in definitions: if a
function ever returns using `mv`

(either directly, or by calling
another function that returns multiple values), then this function
must always return the same number of multiple values.

For more explanation of the multiple value mechanism, see mv-let.

ACL2 does not support the Common Lisp construct `values`

, whose
logical meaning seems difficult to characterize. `Mv`

is the ACL2
analogue of that construct.

Major Section: PROGRAMMING

Example Form: (mv-let (x y z) ; local variables (mv 1 2 3) ; multi-valued expression (declare (ignore y)) ; optional declarations (cons x z)) ; bodyThe form above binds the three ``local variables,''

`x`

, `y`

, and `z`

,
to the three results returned by the multi-valued expression and
then evaluates the body. The result is `'(1 . 3)`

. The second local,
`y`

, is declared `ignore`

d. The multi-valued expression can be any ACL2
expression that returns `k`

results, where `k`

is the number of local
variables listed. Often however it is simply the application of a
`k`

-valued function. `Mv-let`

is the standard way to invoke a
multi-valued function when the caller must manipulate the vector of
results returned.

General Form: (mv-let (var1 ... vark) term body) or (mv-let (var1 ... vark) term (declare ...) ... (declare ...) body)where the

`vari`

are distinct variables, `term`

is a term that returns
`k`

results and mentions only variables bound in the environment
containing the `mv-let`

expression, and `body`

is a term mentioning only
the `vari`

and variables bound in the environment containing the
`mv-let`

. Each `vari`

must occur in `body`

unless it is declared `ignore`

d
in one of the optional `declare`

forms, unless this requirement is
turned off; see set-ignore-ok. The value of the `mv-let`

term is
the result of evaluating `body`

in an environment in which the `vari`

are bound, in order, to the `k`

results obtained by evaluating
`term`

in the environment containing the `mv-let`

.
Here is an extended example that illustrates both the definition of
a multi-valued function and the use of `mv-let`

to call it. Consider
a simple binary tree whose interior nodes are `cons`

es and whose
leaves are non-`cons`

es. Suppose we often need to know the number, `n`

,
of interior nodes of such a tree; the list, `syms`

, of symbols that
occur as leaves; and the list, `ints`

, of integers that occur as
leaves. (Observe that there may be leaves that are neither symbols
nor integers.) Using a multi-valued function we can collect all
three results in one pass.

Here is the first of two definitions of the desired function. This definition is ``primitive recursive'' in that it has only one argument and that argument is reduced in size on every recursion.

(defun count-and-collect (x)This use of multiple values to ``do several things at once'' is very common in ACL2. However, the function above is inefficient because it appends; We return three results, (mv n syms ints) as described above.

(cond ((atom x)

; X is a leaf. Thus, there are 0 interior nodes, and depending on ; whether x is a symbol, an integer, or something else, we return ; the list containing x in as the appropriate result.

(cond ((symbolp x) (mv 0 (list x) nil)) ((integerp x)(mv 0 nil (list x))) (t (mv 0 nil nil)))) (t

; X is an interior node. First we process the car, binding n1, syms1, and ; ints1 to the answers.

(mv-let (n1 syms1 ints1) (count-and-collect (car x))

; Next we process the cdr, binding n2, syms2, and ints2.

(mv-let (n2 syms2 ints2) (count-and-collect (car x))

; Finally, we compute the answer for x from those obtained for its car ; and cdr, remembering to increment the node count by one for x itself.

(mv (1+ (+ n1 n2)) (append syms1 syms2) (append ints1 ints2)))))))

`syms1`

to `syms2`

and `ints1`

to `ints2`

, copying the
list structures of `syms1`

and `ints1`

in the process. By adding
``accumulators'' to the function, we can make the code more
efficient.
(defun count-and-collect1 (x n syms ints) (cond ((atom x) (cond ((symbolp x) (mv n (cons x syms) ints)) ((integerp x) (mv n syms (cons x ints))) (t (mv n syms ints)))) (t (mv-let (n2 syms2 ints2) (count-and-collect1 (cdr x) (1+ n) syms ints) (count-and-collect1 (car x) n2 syms2 ints2)))))We claim that

`(count-and-collect x)`

returns the same triple of
results as `(count-and-collect1 x 0 nil nil)`

. The reader is urged to
study this claim until convinced that it is true and that the latter
method of computing the results is more efficient. One might try
proving the theorem
(defthm count-and-collect-theorem (equal (count-and-collect1 x 0 nil nil) (count-and-collect x))).Hint: the inductive proof requires attacking a more general theorem.

ACL2 does not support the Common Lisp construct
`multiple-value-bind`

, whose logical meaning seems difficult to
characterize. `Mv-let`

is the ACL2 analogue of that construct.

Major Section: PROGRAMMING

`(Mv-nth n l)`

is the `n`

th element of `l`

, zero-based. If `n`

is
greater than or equal to the length of `l`

, then `mv-nth`

returns
`nil`

.

`(Mv-nth n l)`

has a guard that `n`

is a non-negative integer and
`l`

is a `true-listp`

.

`Mv-nth`

is equivalent to the Common Lisp function `nth`

, but is used by
ACL2 to access the nth value returned by a multiply valued expression. For
an example of the use of `mv-nth`

, try

ACL2 !>:trans1 (mv-let (erp val state) (read-object ch state) (value (list erp val)))

Major Section: PROGRAMMING

`Nfix`

simply returns any natural number argument unchanged,
returning `0`

on an argument that is not a natural number. Also
see ifix, see rfix, and see fix for analogous
functions that coerce to an integer, a rational number, and a
number, respectively.

`Nfix`

has a guard of `t`

.

Major Section: PROGRAMMING

See any Common Lisp documentation for details.

`eql`

for equality)
Major Section: PROGRAMMING

`(no-duplicatesp l)`

is true if and only if no member of `l`

occurs twice in `l`

.

`(no-duplicatesp l)`

has a guard of `(eqlable-listp l)`

.
Membership is tested using `member`

, hence using `eql`

as
the test.

`equal`

for equality)
Major Section: PROGRAMMING

`(no-duplicatesp-equal l)`

is true if and only if no member of `l`

occurs twice in `l`

.

`(no-duplicatesp-equal l)`

has a guard of `(true-listp l)`

.
Membership is tested using `member-equal`

, hence using `equal`

as
the test.

Major Section: PROGRAMMING

Example Forms: (nonnegative-integer-quotient 14 3) ; equals 4 (nonnegative-integer-quotient 15 3) ; equals 5

`(nonnegative-integer-quotient i j)`

returns the integer quotient
of the integers `i`

and (non-zero) `j`

, i.e., the largest `k`

such that `(* j k)`

is less than or equal to `i`

. Also
see floor, see ceiling and see truncate, which are
derived from this function and apply to rational numbers.
The guard of `(nonnegative-integer-quotient i j)`

requires that
`i`

is a nonnegative integer and `j`

is a positive integer.

Major Section: PROGRAMMING

`Iff`

is the ACL2 negation function. The negation of `nil`

is `t`

and
the negation of anything else is `nil`

.

`Not`

is a Common Lisp function. See any Common Lisp documentation
for more information.

Major Section: PROGRAMMING

`(Nth n l)`

is the `n`

th element of `l`

, zero-based. If `n`

is
greater than or equal to the length of `l`

, then `nth`

returns `nil`

.

`(Nth n l)`

has a guard that `n`

is a non-negative integer and
`l`

is a `true-listp`

.

`Nth`

is a Common Lisp function. See any Common Lisp documentation
for more information.

Major Section: PROGRAMMING

`(Nthcdr n l)`

removes the first `n`

elements from the list `l`

.

The following is a theorem.

(implies (and (integerp n) (<= 0 n) (true-listp l)) (equal (length (nthcdr n l)) (if (<= n (length l)) (- (length l) n) 0)))For related functions, see take and see butlast.

The guard of `(nthcdr n l)`

requires that `n`

is a nonnegative
integer and `l`

is a true list.

`Nthcdr`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`Null`

is the function that checks whether its argument is `nil`

.
For recursive definitions it is often preferable to test for the end
of a list using `endp`

instead of `null`

; see endp.

`Null`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

Completion Axiom:

(equal (numerator x) (if (rationalp x) (numerator x) 0))

Guard for `(numerator x)`

:

(rationalp x)

Major Section: PROGRAMMING

`(oddp x)`

is true if and only if `x`

is odd, i.e., not even in
the sense of `evenp`

.

The guard for `oddp`

requires its argument to be an integer.

`Oddp`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`Or`

is the macro for disjunctions. `Or`

takes any number of
arguments and returns the first that is non-`nil`

, or `nil`

if
there is no non-`nil`

element.

`Or`

is a Common Lisp macro. See any Common Lisp documentation
for more information.

`pairlis$`

Major Section: PROGRAMMING

The Common Lisp language allows its `pairlis`

function to construct
an alist in any order! So we have to define our own version:
See pairlis$.

Major Section: PROGRAMMING

The Common Lisp language allows its `pairlis`

function to construct
an alist in any order! So we have to define our own version,
`pairlis$`

. It returns the list of pairs obtained by `cons`

ing
together successive respective members of the given lists.

The guard for `pairlis$`

requires that its arguments are true lists.

Major Section: PROGRAMMING

`(Plusp x)`

is true if and only if `x > 0`

.

The guard of `plusp`

requires its argument to be a rational number.

`Plusp`

is a Common Lisp function. See any Common Lisp
documentation for more information.

`eql`

as test
Major Section: PROGRAMMING

`(Position item seq)`

is the least index (zero-based) of the
element `item`

in the string or list `seq`

, if in fact `item`

is
an element of `seq`

. Otherwise `(position item seq)`

is `nil`

.

`(Position item lst)`

is provably the same in the ACL2 logic as
`(position-equal item lst)`

. It has a stronger guard than
`position-equal`

because uses `eql`

to test equality of `item`

with members of `lst`

. Its guard requires that `lst`

is a true
list, and moreover, either `(eqlablep item)`

or all members of
`lst`

are `eqlablep`

. See position-equal and
see position-eq.

`Position`

is a Common Lisp function. See any Common Lisp
documentation for more information. Since ACL2 functions cannot
take keyword arguments (though macros can), the ACL2 functions
`position-equal`

and `position-eq`

are defined to correspond to
calls of the Common Lisp function `position`

whose keyword argument
`:test`

is `equal`

or `eq`

, respectively.

`eq`

as test
Major Section: PROGRAMMING

`(Position-eq item seq)`

is the least index (zero-based) of the
element `item`

in the string or list `seq`

, if in fact `item`

is
an element of `seq`

. Otherwise `(position item seq)`

is `nil`

.

`(Position-eq item lst)`

is provably the same in the ACL2 logic as
`(position item lst)`

and `(position-equal item lst)`

, but it has
a stronger guard because it uses `eq`

for a more efficient test for
whether `item`

is equal to a given member of `lst`

. Its guard
requires that `lst`

is a true list, and moreover, either `item`

is
a symbol or `lst`

is a list of symbols. See position-equal
and see position.

Major Section: PROGRAMMING

`(Position item seq)`

is the least index (zero-based) of the
element `item`

in the string or list `seq`

, if in fact `item`

is
an element of `seq`

. Otherwise `(position item seq)`

is `nil`

.

`(Position-equal item lst)`

has a guard of `(true-listp lst)`

.
`Position-equal`

has the same functionality as the Common Lisp
function `position`

, except that it uses the `equal`

function to
test whether `item`

is the same as each successive element of
`lst`

. See position and see position-eq.

Major Section: PROGRAMMING

Example Form: (pprogn (cond ((or (equal (car l) #\) (equal (car l) slash-char)) (princ$ #\ channel state)) (t state)) (princ$ (car l) channel state) (mv (cdr l) state))The convention for

`pprogn`

usage is to give it a non-empty
sequence of forms, each of which (except possibly for the last)
returns state (see state) as its only value. The state returned by
each but the last is passed on to the next. The value or values of
the last form are returned as the value of the `pprogn`

.If you are using single-threaded objects you may wish to define an analogue of this function for your own stobj.

General Form:

(PPROGN form1 form2 ... formk result-form)This general form is equivalent, via macro expansion, to:

(LET ((STATE form1)) (LET ((STATE form2)) ... (LET ((STATE formk)) result-form)))

`er-progn`

Major Section: PROGRAMMING

ACL2 does not allow the use of `progn`

in definitions. Instead, a
function `er-progn`

can be used for sequencing state-oriented
operations; see er-progn and see state. If you are using single-threaded
objects (see stobj) you may wish to define a version `progn`

that
cascades the object through successive changes. Our `pprogn`

is the
`state`

analogue of such a macro.

`Progn`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

`Proofs-co`

is an `ld`

special (see ld). The accessor is
`(proofs-co state)`

and the updater is `(set-proofs-co val state)`

.
`Proofs-co`

must be an open character output channel. It is to this
channel that `defun`

, `defthm`

, and the other event commands print their
commentary.

``Proofs-co'' stands for ``proofs character output.'' The initial
value of `proofs-co`

is the same as the value of `*standard-co*`

(see *standard-co*).

Major Section: PROGRAMMING

`Proper-consp`

is the function that checks whether its argument is
a non-empty list that ends in `nil`

. Also see true-listp.

Major Section: PROGRAMMING

`(Put-assoc-eq name val alist)`

returns an alist that is the same
as the list `alist`

, except that the first pair in `alist`

with a
`car`

of `name`

is replaced by `(cons name val)`

, if there is
one. If there is no such pair, then `(cons name val)`

is added at
the end. Note that the order of the keys occurring in `alist`

is
unchanged (though a new key may be added).

The guard of `(put-assoc-eq name val alist)`

requires that `alist`

is an `alistp`

, and moreover, either `name`

is a symbol or
`alist`

is a `symbol-alistp`

.

Major Section: PROGRAMMING

`(Put-assoc-equal name val alist)`

returns an alist that is the same
as the list `alist`

, except that the first pair in `alist`

with a
`car`

of `name`

is replaced by `(cons name val)`

, if there is
one. If there is no such pair, then `(cons name val)`

is added at
the end.

The guard of `(put-assoc-equal name val alist)`

requires that `alist`

is an `alistp`

.

`eql`

as test
Major Section: PROGRAMMING

`(Rassoc x alist)`

is similar to `(assoc x alist)`

, the difference
being that it looks for the first pair in the given alist whose
`cdr`

, rather than `car`

, is `eql`

to `x`

. See assoc.

The guard of `rassoc`

requires its second argument to be an alist,
and in addition, that either its first argument is `eqlablep`

or
else all second components of pairs belonging to the second argument
are `eqlablep`

. See eqlablep.

`Rassoc`

is a Common Lisp function. See any Common Lisp
documentation for more information.

Major Section: PROGRAMMING

The predicate `rational-listp`

tests whether its argument is a true
list of rational numbers.

Major Section: PROGRAMMING

`(rationalp x)`

is true if and only if `x`

is an rational
number.

Major Section: PROGRAMMING

Completion Axiom:

(equal (realpart x) (if (acl2-numberp x) (realpart x) 0))

Guard for `(realpart x)`

:

(acl2-numberp x)

Major Section: PROGRAMMING

ACL2 does not in general allow the redefinition of functions because
logical inconsistency can result: previously stored theorems can be
rendered invalid if the axioms defining the functions involved are
changed. However, to permit prototyping of both `:`

`program`

and
`:`

`logic`

mode systems, ACL2 permits redefinition if the user has
accepted logical responsibility for the consequences by setting
`ld-redefinition-action`

to an appropriate non-`nil`

value. The
refusal of ACL2 to support the unrestricted redefinition of
`:`

`program`

mode functions may appear somewhat capricious. After
all, what are the logical consequences of changing a definition if
no axioms are involved?

Three important points should be made before we discuss redefinition further.

The first is that ACL2 does support redefinition (of both
`:`

`program`

and `:`

`logic`

functions) when
`ld-redefinition-action`

is non-`nil`

.

The second is that a ``redefinition'' that does not change the mode,
formals or body of a function is considered redundant and is
permitted even when `ld-redefinition-action`

is `nil`

. We
recognize and permit redundant definitions because it is not
uncommon for two distinct books to share identical function
definitions. When determining whether the body of a function is
changed by a proposed redefinition, we actually compare the
untranslated versions of the two bodies. See term. For
example, redundancy is not recognized if the old body is `(list a b)`

and the new body is `(cons a (cons b nil))`

. We use the
untranslated bodies because of the difficulty of translating the new
body in the presence of the old syntactic information, given the
possibility that the redefinition might attempt to change the
signature of the function, i.e., the number of formals, the
number of results, or the position of single-threaded objects in either.

The third important point is that a ``redefinition'' that preserves
the formals and body but changes the mode from `:`

`program`

to
`:`

`logic`

is permitted even when `ld-redefinition-action`

is
`nil`

. That is what `verify-termination`

does.

This note addresses the temptation to allow redefiniton of
`:`

`program`

functions in situations other than the three
described above. Therefore, suppose `ld-redefinition-action`

is
`nil`

and consider the cases.

Case 1. Suppose the new definition attempts to change the formals
or more generally the signature of the function. Accepting
such a redefinition would render ill-formed other `:`

`program`

functions which call the redefined function. Subsequent attempts to
evaluate those callers could arbitrarily damage the Common Lisp
image. Thus, redefinition of `:`

`program`

functions under these
circumstances requires the user's active approval, as would be
sought with `ld-redefinition-action`

`'(:query . :overwrite)`

.

Case 2. Suppose the new definition attempts to change the body
(even though it preserves the signature). At one time we
believed this was acceptable and ACL2 supported the quiet
redefinition of `:`

`program`

mode functions in this circumstance.
However, because such functions can be used in macros and redundancy
checking is based on untranslated bodies, this turns out to be
unsound! It is therefore now prohibited. We illustrate such an
unsoundness below. Let `foo-thm1.lisp`

be a book with the
following contents.

(in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 't 'nil)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm1 (iff (foo x) x) :rule-classes nil)Note that the macro form

`(p x)`

translates to `(if x t nil)`

.
The `:`

`program`

function `p1`

is used to generate this
translation. The function `foo`

is defined so that `(foo x)`

is
`(p x)`

and a theorem about `foo`

is proved, namely, that `(foo x)`

is true iff `x`

is true.
Now let `foo-thm2.lisp`

be a book with the following contents.

(in-package "ACL2") (defun p1 (x) (declare (xargs :mode :program)) (list 'if x 'nil 't)) (defmacro p (x) (p1 x)) (defun foo (x) (p x)) (defthm foo-thm2 (iff (foo x) (not x)) :rule-classes nil)In this book, the

`:`

`program`

function `p1`

is defined so that
`(p x)`

means just the negation of what it meant in the first book,
namely, `(if x nil t)`

. The function `foo`

is defined identically
-- more precisely, the `foo`

is identical
in the two books, but because of the difference between the two
versions of the the `:`

`program`

function `p1`

the axioms
defining the two `foo`

s are different. In the second book we prove
the theorem that `(foo x)`

is true iff `x`

is nil.
Now consider what would happen if the signature-preserving
redefinition of `:`

`program`

functions were permitted and these
two books were included. When the second book is included the
redefinition of `p1`

would be permitted since the signature is
preserved and `p1`

is just a `:`

`program`

. But then when the
redefinition of `foo`

is processed it would be considered redundant
and thus be permitted. The result would be a logic in which it was
possible to prove that `(foo x)`

is equivalent to both `x`

and
`(not x)`

. In particular, the following sequence leads to a proof
of nil:

(include-book "foo-thm1") (include-book "foo-thm2") (thm nil :hints (("Goal" :use (foo-thm1 foo-thm2))))

It might be possible to loosen the restrictions on the redefinition
of `:`

`program`

functions by allowing signature-preserving
redefinition of `:`

`program`

functions not involved in macro
definitions. Alternatively, we could implement definition
redundancy checking based on the translated bodies of functions
(though that is quite problematic). Barring those two changes, we
believe it is necessary simply to impose the same restrictions on
the redefinition of `:`

`program`

mode functions as we do on
`:`

`logic`

mode functions.