This is documentation for ACL2 Version 3.4
Copyright (C) 2008  University of Texas at Austin

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.

Written by:  Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.

PARALLELISM-TUTORIAL    a tutorial on how to use the parallelism library.

In this topic we introduce the ACL2 parallelism primitives using the
example of a doubly-recursive Fibonacci function, whose basic
definition is as follows.  See PARALLELISM for a very
high-level summary of the parallelism capability described here, and
see PARALLELISM-BUILD for how to build an executable image that
supports parallel evaluation.  Here, we assume that such an executable
is being used.

Serial Fibonacci

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (+ (fib (- x 1)) (fib (- x 2))))))

Introducing Pargs

A simple way to introduce parallelism into this function definition is
to wrap the addition expression with a call of pargs, and the arguments
to the addition will be computed in parallel whenever resources are
available.  As a result, we end up with a very similar and thus
intuitive function definition.  Note that we replaced + by binary-+,
since pargs expects a function call, not a macro call.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs (binary-+ (pfib (- x 1))
                                 (pfib (- x 2)))))))

Introducing the Granularity Problem

After you submit the above two versions of the Fibonacci function, test
them with the following forms.

     (time$ (fib 10))
     (time$ (pfib 10))

Now increase the argument by increments of 5 to 10 until you find your
curiosity satisfied or your patience wearing thin.  You can interrupt
evaluation if necessary and return to the ACL2 loop.  You will
immediately notice that you have not increased execution speed, at
least not by much, by introducing parallelism.

First, consider the computation of (pfib 4).  Assuming resources are
available, (pfib 4) will create a thread for computing (pfib 3) and
another thread for (pfib 2).  It is easy to imagine that setting up each
thread takes much longer than the entire computation of (fib 4).

Second, we must realize that if we have two threads available for
computing (fib 10), then the evaluation of (fib 8) will probably
complete before the evaluation of (fib 9).  Once (fib 8) finishes,
parallelism resources will become available for the next recursive call
made on behalf of (fib 9).  If for example that call is (fib 3), we
will waste a lot of cycles just handing work to the thread that does
this relatively small computation.  We need a way to ensure that
parallelism resources are only used on problems of a "large" size.
Ensuring that only "large" problems are spawned is called the
"granularity problem."

In summary: We want to tell ACL2 that it can evaluate the arguments of
pargs in parallel only when the parameter of pfib is greater than some
threshold.  Our tests using OpenMCL have suggested that 27 is a
reasonable threshold.

Explicit Programming for the Granularity Problem

One way to avoid the granularity problem is to duplicate code as
follows.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (if (> x 27) ; the granularity test
                    (pargs (binary-+ (pfib (- x 1))
                                     (pfib (- x 2))))
                  (binary-+ (pfib (- x 1))
                            (pfib (- x 2)))))))

Duplicating code is fundamentally a bad design principle, because it can
double the work for future maintenance.  A "granularity form" is an
expression

     (declare (granularity <form>))

that can allow threads to be spawned (without duplicating code)
whenever the evaluation of <form> results in a non-nil value.  It may
be placed inside any call of a parallelism primitive, in a position
documentated separately for each primitive.  Here is a definition of
pfib using this feature for a call of the parallelism primitive pargs.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (pargs
                 (declare (granularity (> x 27)))
                 (binary-+ (pfib (- x 1))
                           (pfib (- x 2)))))))

Test each version as follows (or substitute your own natural number for
33).

       (time$ (fib 33))
       (time$ (pfib 33))

Another Granularity Issue Related to Thread Limitations

Our implementation of parallelism primitives has the property that once
a thread is assigned a computation, that assignment stays in effect
until the computation is complete.  In particular, if a thread
encounters a parallelism primitive that spawns child threads, the
parent thread stays assigned, waiting until the child computations
complete before it can continue its own computation.  In the meantime,
the parent thread reduces the number of additional threads that Lisp
can provide by 1, rather than being reassigned to do other work.

How can this lack of reassignment affect the user?  Consider, for
example, the application of a recursive function to a long list.
Imagine that this function is written so that the body contains a
recursive call, for example as (pargs (process (car x)) (recur (cdr
x))).  Each such pargs call that spawns child work must wait for its
children, one of which is the work of evaluating (recur (cdr x)), to
complete.  There is an ACL2 limit on how much pending work can be in
the system, limiting the number of pargs calls that can result in
parallel evaluation.  For example, if the ACL2 limit is k and each call
of pargs actually spawns threads for evaluating  its arguments, then
after k cdrs there will be no further parallel evaluation.

Possible solutions may include reworking of algorithms (for example to
be tree-based rather than list-based) or using appropriate granularity
forms.  We hope that future implementations will allow thread
"re-deployment" in order to mitigate this problem.

Introducing Plet

We can use a let binding to compute the recursive calls of fib and then
add the bound variables together, as follows.

     (defun fib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (let ((a (fib (- x 1)))
                      (b (fib (- x 2))))
                  (+ a b)))))

By using the parallelism primitive plet, we can introduce parallelism
much as we did using pargs, with an optional granularity form, as
follows.

     (defun pfib (x)
       (declare (xargs :guard (natp x)))
       (cond ((or (zp x) (<= x 0)) 0)
             ((= x 1) 1)
             (t (plet
                 (declare (granularity (> x 27)))
                 ((a (pfib (- x 1)))
                  (b (pfib (- x 2))))
                 (+ a b)))))

Notice that this time, we were able to use + rather than being forced to
use binary-+.  Unlike pargs, which expects a function call (not a macro
call), plet allows macros at the top level of its body.

Introducing Pand (By Way of a Tree Validation Example)

Consider "genetic trees" that contains leaves of DNA elements, in the
sense that each tip is one of the symbols A, G, C, or T.  First we
define the function valid-tip which recognizes whether a tip contains
one of these symbols.

     (defun valid-tip (tip)
       (declare (xargs :guard t))
       (or (eq tip 'A)
           (eq tip 'G)
           (eq tip 'C)
           (eq tip 'T)))

Now we define a function that traverses the tree, checking that every
tip is valid.

     (defun valid-tree-serial (tree)
       (declare (xargs :guard t))
       (if (atom tree)
           (valid-tip tree)
         (and (valid-tree-serial (car tree))
              (valid-tree-serial (cdr tree)))))

We also define a parallel version.

     (defun valid-tree-parallel (tree)
       (declare (xargs :guard t))
       (if (atom tree)
           (valid-tip tree)
         (pand (valid-tree-parallel (car tree))
               (valid-tree-parallel (cdr tree)))))

Before we can time the functions, we need to create test trees.  We have
found that test trees need to be approximately 1 gigabyte before we
clearly see speedup, and we make them asymmetric to demonstrate the
ability of our implementation to adapt to asymmetric data.  We can
create the trees with the execution of the following forms.

     (defun make-valid-binary-tree (x)
       (declare (xargs :mode :program))
       (if (< x 0)
           (cons (cons 'C 'G) (cons 'A 'T))
         (cons (make-valid-binary-tree (- x 2)) ; 2 to make asymmetric
               (make-valid-binary-tree (- x 1)))))

     (defconst *valid-tree* (make-valid-binary-tree 30)) ; takes awhile
     (defconst *invalid-tree* (cons *valid-tree* nil)) ; nil is invalid tip

We can time our functions with the forms:

     (time$ (valid-tree-serial *valid-tree*))
     (time$ (valid-tree-parallel *valid-tree*))

Unfortunately, the serial version runs faster than the parallelism
version; however, there is more to this story.

Demonstrating Early Termination with an Invalid Tree

Now observe this magic:

     (time$ (valid-tree-serial   *invalid-tree*))
     (time$ (valid-tree-parallel *invalid-tree*))

The serial version took awhile, while the parallel version finished
almost immediately.  The test for validation was split into testing the
car and the cdr of the *invalid-tree* root, and since the cdr was equal
to nil, its test returned immediately.  This immediate return quickly
interrupted the computation associated with the car, and returned the
result.

Granularity with Pand

We can also define a parallel version with a granularity form:

     (defun valid-tree-parallel (tree depth)
       (declare (xargs :guard (natp depth)))
       (if (atom tree)
           (valid-tip tree)
         (pand
          (declare (granularity (< depth 5)))
          (valid-tree-parallel (car tree) (1+ depth))
          (valid-tree-parallel (cdr tree) (1+ depth)))))

We can test this form by executing our previous forms.  You will
probably find some speedup on a machine with several cores available,
but more speedup can likely be obtained with an expensive test on the
leaves in place of valid-tip.

     (time$ (valid-tree-serial   *valid-tree*))
     (time$ (valid-tree-parallel *valid-tree* 0))

Introducing Por

Por can be used in the same way as pand, but with early termination
occurring when an argument evaluates to a non-nil value, in which case
the value returned is t.  Finally, por also supports the use of a
granularity form.

PARGS    parallel evaluation of arguments in a function call

     Example Forms:
     (pargs (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))

     (pargs (declare (granularity (> x 35)))
            (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))

     General Form:
     (pargs (declare (granularity expr)) ; optional granularity declaration
            (f arg1 ... argN))

where N >= 0 and each argi and expr are arbitrary terms.  Logically,
pargs is just the identity macro, in the sense that the above forms can
logically be replaced by (f arg1 ... argN).  However, this pargs form
may parallelize the evaluation of arguments arg1 through argN before
applying function f to those results.  If the above granularity
declaration is present, then its expression (expr above) is first
evaluated, and if the result is nil, then such parallelism is avoided.
Even if parallelism is not thus avoided, parallelism may be limited by
available resources.

Since macros can change expressions in unexpected ways, it is illegal
to call pargs on a form that is a macro call.  To parallelize
computation of arguments to a macro, see PLET.

See PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.

PLET    parallel version of let

     Example Forms:
     (plet ((a (fibonacci (- x 1)))
            (b (fibonacci (- x 2))))
           (+ a b))

     (plet (declare (granularity (> x 35)))
           ((a (fibonacci (- x 1)))
            (b (fibonacci (- x 2))))
           (+ a b))

     General Form:
     (plet (declare (granularity expr)) ; optional granularity declaration
           ((var1 val1)
            ...
            (varN valN))
           (declare ...) ... (declare ...) ; optional declarations
           body)

The syntax of plet is identical to the syntax of let, except that plet
permits an optional granularity declaration in the first argument
position; see GRANULARITY.  In the logic a call of plet
macroexpands to the corresponding call of let, where the granularity
declaration (if any) is dropped.

Plet cause the evaluation of each vali above to be done in parallel
before processing the body.  If the above granularity declaration is
present, then its expression (expr above) is first evaluated, and if the
result is nil, then such parallelism is avoided.  Even if parallelism is
not thus avoided, parallelism may be limited by available resources.

See PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.

POR    parallel, Boolean version of or

     Example Forms:
     (por (subsetp-equal x y)
          (subsetp-equal y x))

     (por (declare
           (granularity
            (and (> (length x) 500)
                 (> (length y) 500))))
           (subsetp-equal x y)
           (subsetp-equal y x))

     General Form:
     (por (declare (granularity expr)) ; optional granularity declaration
          arg1 ... argN)

where N >= 0 and each argi and expr are arbitrary terms.

Por evaluates its arguments in parallel.  It returns a Boolean result:
t if any argument evaluates to non-nil, else nil.  Note that while or
returns the first non-nil value from evaluating its arguments
left-to-right (if any such value is not nil) por always returns a
Boolean result, in support of efficiency (see EARLY-TERMINATION)
in light of the nondeterministic order in which argument values are
returned.

Another difference between por and or is that for a call of por, even
if the an argument's value is not nil, a subsequent argument may be
evaluated.  See PAND for a discussion of the analogous property
of pand.  In particular, guards generated from calls of por may not
assume for an argument that the preceding arguments evaluated to nil.

See PARALLELISM-TUTORIAL for another example.  Also see
PARALLELISM-AT-THE-TOP-LEVEL for restrictions on evaluating
parallelism primitives from within the ACL2 top-level loop.  Finally
see EARLY-TERMINATION to read how por can offer more efficiency
than or by avoiding evaluation of some of its arguments.

SET-PARALLEL-EVALUATION    enabling or disabling parallel evaluation

See PARALLEL and see PARALLELISM-TUTORIAL for an
introduction to parallel evaluation in ACL2 using parallelism
primitives pand, por, plet, and pargs.

     General Forms:
     (set-parallel-evaluation nil) ; default for images not built for parallelism
     (set-parallel-evaluation t)   ; default for images built for parallelism
     (set-parallel-evaluation :bogus-parallelism-ok)

Set-parallel-evaluation takes an argument that specifies the enabling or
disabling of parallel evaluation.  However, calls of parallelism
primitives made explicitly in the ACL2 top-level loop, as opposed to
inside function bodies, will never cause parallel evaluation; see
PARALLELISM-AT-THE-TOP-LEVEL.  Parallel evaluation is determined by
the value of the argument to set-parallel-evaluation, as follows.

Value t:
All parallelism primitives used in bodies of function definitions are
given the opportunity to execute in parallel.  However, the use of
parallelism primitives directly in the ACL2 top-level loop causes an
error.

Value :bogus-parallelism-ok:
Parallel evaluation is enabled, as for value t.  However, the use of
parallelism primitives directly in the ACL2 top-level loop does not
cause an error, but rather, simply results in serial evaluation for
these primitives.

Value nil:
All parallelism primitives will degrade to their serial equivalents,
include their calls made directly in the ACL2 top-level loop, which
does not cause an error.

PROGRAMMING    built-in ACL2 functions

The built-in ACL2 functions that one typically uses in writing programs
are listed below.  See their individual documentations.  We do not
bother to document some of the more obscure functions provided by ACL2
that do not correspond to functions of Common Lisp.

Related topics other than immediate subtopics:

See any documentation for Common Lisp for more details on many of these
functions.

*    multiplication macro

* 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-CI*    an ACL2 character-based analogue of CLTL's *standard-input*

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-CO*    the ACL2 analogue of CLTL's *standard-output*

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-OI*    an ACL2 object-based analogue of CLTL's *standard-input*

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*.

+    addition macro

+ 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-+.

-    macro for subtraction and negation

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).

/    macro for division and reciprocal

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.

/=    test inequality of two numbers

(/= 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.

1+    increment by 1

(1+ x) is the same as (+ 1 x).  See +.

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

1-    decrement by 1

(1- x) is the same as (- x 1).  See -.

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

<    less-than

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.

<=    less-than-or-equal test

<= 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.

=    test equality of two numbers

(= 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.

>    greater-than test

> 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.

>=    greater-than-or-equal test

>= 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.

ABS    the absolute value of a real number

(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.

ACL2-NUMBERP    recognizer for numbers

(acl2-numberp x) is true if and only if x is a number, i.e., a rational
or complex rational number.

ACL2-USER    a package the ACL2 user may prefer

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".

ACONS    constructor for association lists

(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.

ADD-TO-SET-EQ    add a symbol to a list

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.

ADD-TO-SET-EQL    add an object to a list

For an object x and a true list lst, (add-to-set-eql 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-eql x lst) has a guard that lst is a true list and
moreover, either x is eqlablep or lst is an eqlable-listp.

ADD-TO-SET-EQUAL    add an object to a list

For an object x and a true list lst, (add-to-set-equal 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-equal x lst) has a guard that lst is a true list.

ALISTP    recognizer for association lists

(alistp x) is true if and only if x is a list of cons pairs.

(alistp x) has a guard of t.

ALLOCATE-FIXNUM-RANGE    set aside fixnums in GCL

(Allocate-fixnum-range fixnum-lo fixnum-hi) causes Gnu Common Lisp
(GCL) to create a persistent table for the integers between fixnum-lo
and fixnum-hi (both bounds inclusive). This table is referenced first
when any integer is boxed and the existing box in the table is used if
the integer is in bounds.  This can speed up GCL considerably by
avoiding wasteful fixnum boxing.  Here, fixnum-lo and fixnum-hi should
be fixnums, more specifically of type (signed-byte 30), with fixnum-lo
<= fixnum-hi.

When this function is executed in a Lisp implementation other than GCL,
it has no side effect.  This function always returns nil.

ALPHA-CHAR-P    recognizer for alphabetic characters

(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.