* is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
* is really a macro that expands to calls of the function
binary-*. So for example
(* x y 4 z)represents the same term as
(binary-* x (binary-* y (binary-* 4 z))).
See binary-*.
* is a Common Lisp function. See any Common Lisp documentation
for more information.
*standard-input*
Major Section: PROGRAMMING
The value of the ACL2 constant *standard-ci* is an open character
input channel that is synonymous to Common Lisp's
*standard-input*.
ACL2 character input from *standard-ci* is actually obtained by
reading characters from the stream named by Common Lisp's
*standard-input*. That is, by changing the setting of
*standard-input* in raw Common Lisp you can change the source from
which ACL2 reads on the channel *standard-ci*.
See *standard-co*.
*standard-output*
Major Section: PROGRAMMING
The value of the ACL2 constant *standard-co* is an open character
output channel that is synonymous to Common Lisp's
*standard-output*.
ACL2 character output to *standard-co* will go to the stream named
by Common Lisp's *standard-output*. That is, by changing the
setting of *standard-output* in raw Common Lisp you can change the
actual destination of ACL2 output on the channel named by
*standard-co*. Observe that this happens without changing the
logical value of *standard-co* (which is some channel symbol).
Changing the setting of *standard-output* in raw Common Lisp
essentially just changes the map that relates ACL2 to the physical
world of terminals, files, etc.
To see the value of this observation, consider the following.
Suppose you write an ACL2 function which does character output to
the constant channel *standard-co*. During testing you see that the
output actually goes to your terminal. Can you use the function to
output to a file? Yes, if you are willing to do a little work in
raw Common Lisp: open a stream to the file in question, set
*standard-output* to that stream, call your ACL2 function, and then
close the stream and restore *standard-output* to its nominal value.
Similar observations can be made about the two ACL2 input channels,
*standard-oi* and *standard-ci*, which are analogues of
*standard-input*.
Another reason you might have for wanting to change the actual
streams associated with *standard-oi* and *standard-co* is to drive
the ACL2 top-level loop, ld, on alternative input and output
streams. This end can be accomplished easily within ACL2 by either
calling ld on the desired channels or file names or by resetting the
ACL2 state global variables 'standard-oi and 'standard-co which are
used by ld. See standard-oi and see standard-co.
*standard-input*
Major Section: PROGRAMMING
The value of the ACL2 constant *standard-oi* is an open object input
channel that is synonymous to Common Lisp's *standard-input*.
ACL2 object input from *standard-oi* is actually obtained by reading
from the stream named by Common Lisp's *standard-input*. That is,
by changing the setting of *standard-input* in raw Common Lisp you
can change the source from which ACL2 reads on the channel
*standard-oi*. See *standard-co*.
Major Section: PROGRAMMING
+ is really a macro that expands to calls of the function
binary-+. So for example
(+ x y 4 z)represents the same term as
(binary-+ x (binary-+ y (binary-+ 4 z))).See binary-+.
Major Section: PROGRAMMING
See binary-+ for addition and see unary-- for negation.
Note that - represents subtraction as follows:
(- x y)represents the same term as
(+ x (- y))which is really
(binary-+ x (unary-- y)).Also note that
- represents arithmetic negation as follows:
(- x)expands to
(unary-- x).
Major Section: PROGRAMMING
See binary-* for multiplication and see unary-/ for reciprocal.
Note that / represents division as follows:
(/ x y)represents the same term as
(* x (/ y))which is really
(binary-* x (unary-/ y)).Also note that
/ represents reciprocal as follows:
(/ x)expands to
(unary-/ x).
/ is a Common Lisp macro. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
(/= x y) is logically equivalent to (not (equal x y)).
Unlike equal, /= has a guard requiring both of its arguments
to be numbers. Generally, /= is executed more efficiently than
a combination of not and equal.
For a discussion of the various ways to test against 0, See zero-test-idioms.
/= is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
(1+ x) is the same as (+ 1 x). See +.
1+ is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
(1- x) is the same as (- x 1). See -.
1- is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
Completion Axiom:
(equal (< x y)
(if (and (rationalp x)
(rationalp y))
(< x y)
(let ((x1 (if (acl2-numberp x) x 0))
(y1 (if (acl2-numberp y) y 0)))
(or (< (realpart x1) (realpart y1))
(and (equal (realpart x1) (realpart y1))
(< (imagpart x1) (imagpart y1)))))))
Guard for (< x y):
(and (rationalp x) (rationalp y))Notice that like all arithmetic functions,
< treats non-numeric
inputs as 0.
This function has the usual meaning on the rational numbers, but is
extended to the complex rational numbers using the lexicographic
order: first the real parts are compared, and if they are equal,
then the imaginary parts are compared.
Major Section: PROGRAMMING
<= is a macro, and (<= x y) expands to the same thing as
(not (< y x)). See <.
<= is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
(= x y) is logically equivalent to (equal x y).
Unlike equal, = has a guard requiring both of its arguments
to be numbers. Generally, = is executed more efficiently than
equal.
For a discussion of the various ways to test against 0, See zero-test-idioms.
= is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
> is a macro, and (> x y) expands to the same thing as
(< y x). See <.
> is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
>= is a macro, and (>= x y) expands to the same thing as
(not (< x y)). See <.
>= is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
(Abs x) is -x if x is negative and is x otherwise.
The guard for abs requires its argument to be a rational (real,
in ACL2(r)) number.
Abs is a Common Lisp function. See any Common Lisp documentation
for more information.
From ``Common Lisp the Language'' page 205, we must not allow
complex x as an argument to abs in ACL2, because if we did we
would have to return a number that might be a floating point number
and hence not an ACL2 object.
Major Section: PROGRAMMING
(acl2-numberp x) is true if and only if x is a number, i.e., a
rational or complex rational number.
Major Section: PROGRAMMING
This package imports the standard Common Lisp symbols that ACL2
supports and also a few symbols from package "ACL2" that are
commonly used when interacting with ACL2. You may prefer to select
this as your current package so as to avoid colliding with ACL2
system names.
This package imports the symbols listed in
*common-lisp-symbols-from-main-lisp-package*, which contains
hundreds of CLTL function and macro names including those supported
by ACL2 such as cons, car, and cdr. It also imports the symbols in
*acl2-exports*, which contains a few symbols that are frequently
used while interacting with the ACL2 system, such as implies,
defthm, and rewrite. It imports nothing else.
Thus, names such as alistp, member-equal, and type-set, which are
defined in the "ACL2" package are not present here. If you find
yourself frequently colliding with names that are defined in
"ACL2" you might consider selecting "ACL2-USER" as your current
package (see in-package). If you select "ACL2-USER" as the
current package, you may then simply type member-equal to refer to
acl2-user::member-equal, which you may define as you see fit. Of
course, should you desire to refer to the "ACL2" version of
member-equal, you will have to use the "ACL2::" prefix, e.g.,
acl2::member-equal.
If, while using "ACL2-USER" as the current package, you find that
there are symbols from "ACL2" that you wish we had imported into
it (because they are frequently used in interaction), please bring
those symbols to our attention. For example, should union-theories
and universal-theory be imported? Except for stabilizing on the
``frequently used'' names from "ACL2", we intend never to define a
symbol whose symbol-package-name is "ACL2-USER".
Major Section: PROGRAMMING
(Acons key datum alist) equals the result of consing the pair
(cons key datum) to the front of the association list alist.
(Acons key datum alist) has a guard of (alistp alist).
Acons is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
For a symbol x and a true list lst, (add-to-set-eq x lst)
is the result of consing x on to the front of lst, unless
x is already a member of lst, in which case it equals lst.
(add-to-set-eq x lst) has a guard that lst is a true list and
moreover, either x is a symbol or lst is a list of symbols.
Major Section: PROGRAMMING
(alistp x) is true if and only if x is a list of cons pairs.
(alistp x) has a guard of t.
Major Section: PROGRAMMING
(Alpha-char-p x) is true if and only if x is a alphabetic
character, i.e., one of the characters #a, #b, ..., #z, #A, #B,
..., #Z.
The guard for alpha-char-p requires its argument to be a character.
Alpha-char-p is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
And is the macro for conjunctions. And takes any number of
arguments. And returns nil if one of the arguments is nil,
but otherwise returns the last argument. If there are no arguments,
and returns t.
And is a Common Lisp macro. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
Append, which takes two or more arguments, expects all the
arguments except perhaps the last to be true (null-terminated)
lists. It returns the result of concatenating all the elements of
all the given lists into a single list. Actually, in ACL2 append
is a macro that expands into calls of the binary function
binary-append.
Append is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(ash i c) is the result of taking the two's complement
representation of the integer i and shifting it by c bits,
padding with c 0 bits if c is positive, and dropping (abs c)
bits if c is negative.
The guard for ash requires that its arguments are integers.
Ash is a Common Lisp function. See any Common Lisp documentation
for more information.
eql as test
Major Section: PROGRAMMING
(Assoc x alist) is the first member of alist whose car
is x, or nil if no such member exists.
(Assoc x alist) is provably the same in the ACL2 logic as
(assoc-equal x alist). It has a stronger guard than
assoc-equal because it uses eql to test whether x is equal
to the car of a given member of alist. Its guard
requires that alist is an alistp, and moreover, either
(eqlablep x) or all cars of members of alist are
eqlablep. See assoc-equal and see assoc-eq.
Assoc 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
assoc-equal and assoc-eq are defined to correspond to calls
of the Common Lisp function assoc whose keyword argument
:test is equal or eq, respectively.
eq as test
Major Section: PROGRAMMING
(Assoc-eq x alist) is the first member of alist whose car
is x, or nil if no such member exists.
(Assoc-eq x alist) is provably the same in the ACL2 logic as
(assoc x alist) and (assoc-equal x alist), but it has a
stronger guard because it uses eq for a more efficient test for
whether x is equal to a given key of alist. Its guard
requires that alist is an association list (see alistp), and
moreover, either x is a symbol or all keys of alist are
symbols, i.e., alist is a symbol-alistp.
Major Section: PROGRAMMING
(Assoc-equal x alist) is the first member of alist whose car
is x, or nil if no such member exists.
(Assoc-equal x alist) has a guard of (alistp alist), and
returns the first member of alist whose car is x, or nil if
no such member exists. Thus, assoc-equal has the same
functionality as the Common Lisp function assoc, except that it
uses the equal function to test whether x is the same as each
successive `key' of alist. See assoc and see assoc-eq.
keyword-value-listp
Major Section: PROGRAMMING
If l is a list of even length of the form (k1 a1 k2 a2 ... kn an),
where each ki is a keyword, then (assoc-keyword key l) is the
first tail of l starting with key if key is some ki, and is
nil otherwise.
The guard for (assoc-keyword key l) is (keyword-value-listp l).
Major Section: PROGRAMMING
(Assoc-string-equal x alist) is similar to assoc-equal.
However, for string x and alist alist, the comparison of x
with successive keys in alist is done using string-equal
rather than equal.
The guard for assoc-string-equal requires that x is a string
and alist is an alist.
Major Section: PROGRAMMING
(atom x) is true if and only if x is an atom, i.e., not a
cons pair.
Atom has a guard of t, and is a Common Lisp function. See any
Common Lisp documentation for more information.
Major Section: PROGRAMMING
The predicate atom-listp tests whether its argument is a
true-listp of atoms, i.e., of non-conses.
Major Section: PROGRAMMING
Completion Axiom:
(equal (binary-* x y)
(if (acl2-numberp x)
(if (acl2-numberp y)
(binary-* x y)
0)
0))
Guard for (binary-* x y):
(and (acl2-numberp x) (acl2-numberp y))Notice that like all arithmetic functions,
binary-* treats
non-numeric inputs as 0.
Calls of the macro * expand to calls of binary-*;
see *.
Major Section: PROGRAMMING
Completion Axiom:
(equal (binary-+ x y)
(if (acl2-numberp x)
(if (acl2-numberp y)
(binary-+ x y)
x)
(if (acl2-numberp y)
y
0)))
Guard for (binary-+ x y):
(and (acl2-numberp x) (acl2-numberp y))Notice that like all arithmetic functions,
binary-+ treats
non-numeric inputs as 0.
Calls of the macro + expand to calls of binary-+;
see +.
Major Section: PROGRAMMING
This binary function implements append, which is a macro in ACL2.
See append
The guard for binary-append requires the first argument to be a
true-listp.
Major Section: PROGRAMMING
(Booleanp x) is t if x is t or nil, and is nil otherwise.
See generalized-booleans for a discussion of a potential
soundness problem for ACL2 related to the question: Which Common
Lisp functions are known to return Boolean values?
Major Section: PROGRAMMING
(Butlast l n) is the list obtained by removing the last n
elements from the true list l. The following is a theorem
(though it takes some effort, including lemmas, to get ACL2 to prove
it).
(implies (and (integerp n)
(<= 0 n)
(true-listp l))
(equal (length (butlast l n))
(if (< n (length l))
(- (length l) n)
0)))
For related functions, see take and see nthcdr.
The guard for (butlast l n) requires that n is a nonnegative
integer and lst is a true list.
Butlast is a Common Lisp function. See any Common Lisp
documentation for more information. Note: In Common Lisp the
second argument of butlast is optional, but in ACL2 it is
required.
car of the caaar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the caadr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the caar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cadar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the caddr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cadr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the car
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cdaar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cdadr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cdar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cddar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cdddr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cddr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
car of the cdr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
nil
Major Section: PROGRAMMING
Completion Axiom:
(equal (car x)
(cond
((consp x)
(car x))
(t nil)))
(or (consp x) (equal x nil))Notice that in the ACL2 logic,
car returns nil for every atom.
eql
Major Section: PROGRAMMING
Example Form: (case typ ((:character foo) (open file-name :direction :output)) (bar (open-for-bar file-name)) (otherwise (my-error "Illegal.")))is the same as
(cond ((member typ '(:character foo))
(open file-name :direction :output))
((eql typ 'bar)
(open-for-bar file-name))
(t (my-error "Illegal.")))
which in turn is the same as
(if (member typ '(:character foo))
(open file-name :direction :output)
(if (eql typ 'bar)
(open-for-bar file-name)
(my-error "Illegal.")))
General Forms:
(case expr
(x1 val-1)
...
(xk val-k)
(otherwise val-k+1))
(case expr
(x1 val-1)
...
(xk val-k)
(t val-k+1))
where each xi is either eqlablep or a true list of eqlablep
objects.
Case is defined in Common Lisp. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
General Form: (case-match x (pat1 dcl1 body1) ... (patk dclk bodyk))where
x is a variable symbol, the pati are structural patterns
as described below, the dcli are optional declare forms and
the bodyi are terms. Return the value(s) of the bodyi
corresponding to the first pati matching x, or nil if none
matches.
Pattern Language:
With the few special exceptions described below, matching requires
that the cons structure of x be isomorphic to that of the
pattern, down to the atoms in the pattern. Non-symbol atoms in the
pattern match only themselves. Symbols in the pattern denote
variables which match anything and which are bound by a successful
match to the corresponding substructure of x. Variables that
occur more than once must match the same (EQUAL) structure in
every occurrence.
Exceptions:
& Matches anything and is not bound. Multiple
occurrences of & in a pattern may match different
structures.
nil, t, *sym* These symbols cannot be bound and match only their
global values.
!sym where sym is a symbol that is already bound in the
context of the case-match, matches only the
current binding of sym.
'obj Matches only itself.
Some examples are shown below.
Below we show some sample patterns and examples of things they match and do not match.
pattern matches non-matches
(x y y) (ABC 3 3) (ABC 3 4) ; 3 is not 4
(fn x . rst) (P (A I) B C) (ABC) ; NIL is not (x . rst)
(J (A I)) ; rst matches nil
('fn (g x) 3) (FN (H 4) 3) (GN (G X) 3) ; 'fn matches only itself
(& t & !x) ((A) T (B) (C)) ; provided x is '(C)
Consider the two binary trees that contain three leaves. They might
be described as (x . (y . z)) and ((x . y) . z), where x,
y, and z are atomic. Suppose we wished to recognize those
trees. The following case-match would do:
(case-match tree ((x . (y . z)) (and (atom x) (atom y) (atom z))) (((x . y) . z) (and (atom x) (atom y) (atom z))))Suppose we wished to recognize such trees where all three tips are identical. Suppose further we wish to return the tip if the tree is one of those recognized ones and to return the number
7 otherwise.
(case-match tree ((x . (x . x)) (if (atom x) x 7)) (((x . x) . x) (if (atom x) x 7)) (& 7))Note that
case-match returns nil if no pati matches. Thus if we
must return 7 in that case, we have to add as the final pattern the
&, which always matches anything.
cdr of the caaar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the caadr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the caar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cadar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the caddr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cadr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the car
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cdaar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cdadr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cdar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cddar
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cdddr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cddr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cdr of the cdr
Major Section: PROGRAMMING
See any Common Lisp documentation for details.
cons pair, else nil
Major Section: PROGRAMMING
Completion Axiom:
(equal (cdr x)
(cond
((consp x)
(cdr x))
(t nil)))
(or (consp x) (equal x nil))Notice that in the ACL2 logic,
cdr returns nil for every atom.
Major Section: PROGRAMMING
Example Forms: ACL2 !>(ceiling 14 3) 5 ACL2 !>(ceiling -14 3) -4 ACL2 !>(ceiling 14 -3) -4 ACL2 !>(ceiling -14 -3) 5 ACL2 !>(ceiling -15 -3) 5
(Ceiling i j) is the result of taking the quotient of i and
j and returning the smallest integer that is at least as great as
that quotient. For example, the quotient of -14 by 3 is -4 2/3, and
the smallest integer at least that great is -4.
The guard for (ceiling i j) requires that i and j are
rational (real, in ACL2(r)) numbers and j is non-zero.
Ceiling is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Char s n) is the nth element of s, zero-based. If n is
greater than or equal to the length of s, then char returns
nil.
(Char s n) has a guard that n is a non-negative integer and
s is a stringp.
Char is a Common Lisp function. See any Common Lisp documentation
for more information.
Major Section: PROGRAMMING
Completion Axiom:
(equal (char-code x)
(if (characterp x)
(char-code x)
0))
Guard for (char-code x):
(characterp x)This function maps all non-characters to
0.
Major Section: PROGRAMMING
(Char-downcase x) is equal to #A when x is #a, #B when x is
#b, ..., and #Z when x is #z, and is x for any other character.
The guard for char-downcase requires its argument to be a character.
Char-downcase is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
For characters x and y, (char-equal x y) is true if and only if x
and y are the same except perhaps for their case.
The guard on char-equal requires that its arguments are both
characters.
Char-equal is a Common Lisp function. See any Common Lisp
documentation for more information.
Major Section: PROGRAMMING
(Char-upcase x) is equal to #A when x is #a, #B when x is
#b, ..., and #Z when x is #z, and is x for any other character.
The guard for char-upcase requires its argument to be a character.
Char-upcase is a Common Lisp function. See any Common Lisp
documentation for more information.