logand requires its arguments to be integers.
Logand is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logand returns their bitwise logical `and'.
The guard for logand requires its arguments to be integers.
Logand is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logandc1 returns the bitwise logical `and' of the second with the
bitwise logical `not' of the first.
The guard for logandc1 requires its arguments to be integers.
Logandc1 is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logandc2 returns the bitwise logical `and' of the first with the
bitwise logical `not' of the second.
The guard for logandc2 requires its arguments to be integers.
Logandc2 is defined in Common Lisp. See any Common Lisp
documentation for more information.
ith bit of an integer
Major Section: PROGRAMMING
For a nonnegative integer i and an integer j, (logbitp i j)
is the value of the ith bit in the two's complement
representation of j.
(Logbitp i j) has a guard that i is a nonnegative integer and
j is an integer.
Logbitp is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Logcount x) is the number of ``on'' bits in the two's complement
representation of x.
(Logcount x) has a guard of (integerp x).
Logcount is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logeqv returns the bitwise logical equivalence of the first with
the second.
The guard for logeqv requires its arguments to be integers.
Logeqv is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logior returns their bitwise logical inclusive or.
The guard for logior requires its arguments to be integers.
Logior is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
lognand returns their bitwise logical `nand'.
The guard for lognand requires its arguments to be integers.
Lognand is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
lognor returns the bitwise logical `nor' of the first with the
second.
The guard for lognor requires its arguments to be integers.
Lognor is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(lognot i) is the two's complement bitwise `not' of the integer i.
Lognot is actually defined by coercing its argument to an integer
(see ifix), negating the result, and then subtracting 1.
The guard for lognot requires its argument to be an integer.
Lognot is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logorc1 returns the bitwise logical inclusive or of the second
with the bitwise logical `not' of the first.
The guard for logorc1 requires its arguments to be integers.
Logorc1 is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logorc2 returns the bitwise logical inclusive or of the first
with the bitwise logical `not' of the second.
The guard for logorc2 requires its arguments to be integers.
Logorc2 is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers x and y are viewed in their two's complement
representation, (logtest x y) is true if and only if there is
some position for which both x and y have a `1' bit in that
position.
The guard for logtest requires its arguments to be integers.
Logtest is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
When integers are viewed in their two's complement representation,
logxor returns the bitwise logical exclusive or of the first with
the second.
The guard for logxor requires its arguments to be integers.
Logxor is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Lower-case-p x) is true if and only if x is a lower case
character, i.e., a member of the list #A, #B, ..., #Z.
The guard for lower-case-p requires its argument to be a character.
Lower-case-p is a Common Lisp function. See any Common Lisp
documentation for more information.
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 (real,
in ACL2(r)) 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 (real,
in ACL2(r)) 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 (real, in
ACL2(r)) 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
(real, in ACL2(r)) 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)) ; body
The 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 ignored. 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 ignored
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 conses and whose
leaves are non-conses. 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 nth 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, see realfix, and see fix for
analogous functions that coerce to an integer, a rational number, a
real, 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 nth 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 consing
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 (real, in
ACL2(r)) 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 either lst is a
string, or else lst is a true list such that 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 list seq, if in fact item is
an element of seq. Otherwise (position-eq 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) when lst is a
true list, 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, which unlike position-eq have
guards that allow the second argument to be a string.
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)))
Major Section: PROGRAMMING
See hard-error and see illegal for examples of functions
to call in the first argument of prog2$.
Semantically, (Prog2$ x y) equals y; the value of x is ignored.
However, x is first evaluated for side effect. Since the ACL2
programming language is applicative, there can be no logical impact
of evaluating x. However, x may involve a call of a function such
as hard-error or illegal, which can cause so-called ``hard errors.''
Here is a simple, contrived example using hard-error. The intention
is to check at run-time that the input is appropriate before calling
function bar.
(defun foo-a (x)
(declare (xargs :guard (consp x)))
(prog2$
(or (good-car-p (car x))
(hard-error 'foo-a
"Bad value for x: ~p0"
(list (cons #\0 x))))
(bar x)))
The following similar function uses illegal instead of hard-error.
Since illegal has a guard of nil, guard verification would
guarantee that the call of illegal below will never be made (at
least when guard checking is on; see set-guard-checking).
(defun foo-b (x)
(declare (xargs :guard (and (consp x) (good-car-p (car x)))))
(prog2$
(or (good-car-p (car x))
(illegal 'foo-b
"Bad value for x: ~p0"
(list (cons #\0 x))))
(bar x)))
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.