This is documentation for ACL2 Version 3.3
Copyright (C) 2007  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.

FMT    formatted printing

ACL2 provides the functions fmt, fmt1, and fms as substitutes for Common
Lisp's format function.  Also see FMT!, see FMT1!, and
see FMS! for versions of these functions that write forms to
files in a manner that allows them to be read, by avoiding using
backslash (\) to break long lines.

All three print a given string under an alist pairing character objects
with values, interpreting certain "tilde-directives" in the string.
Channel must be a character output channel (e.g., *standard-co*).

     General Forms:                                            result
     (fms string alist channel state evisc-tuple)         ; state
     (fmt string alist channel state evisc-tuple)         ; (mv col state)
     (fmt1 string alist column channel state evisc-tuple) ; (mv col state)

Fms and fmt print an initial newline to put channel in column 0; Fmt1
requires the current column as input.  Columns are numbered from 0.
The current column is the column into which the next character will be
printed.  (Thus, the current column number is also the number of
characters printed since the last newline.)  The col returned by fmt
and fmt1 is the current column at the conclusion of the formatting.
Evisc-tuple must be either nil (meaning no abbreviations are used when
objects are printed) or an "evisceration tuple" such as that returned by
(default-evisc-tuple state).

We list the tilde-directives below.  The notation is explained after
the chart.

     ~xx  pretty print vx (maybe after printing a newline)
     ~yx  pretty print vx starting in current column; end with newline
     ~Xxy like ~xx but use vy as the evisceration tuple
     ~Yxy like ~yx but use vy as the evisceration tuple
     ~px  pretty print term (maybe with infix) vx
          (maybe after printing a newline)
     ~qx  pretty print term (maybe with infix) vx
          starting in current column; end with newline
     ~Pxy like ~px but use vy as the evisceration tuple
     ~Qxy like ~qx but use vy as the evisceration tuple
     ~@x  if vx is a string, "str",  recursively format "str"
          if vx is ("str" . a), recursively format "str" under a+
     ~#x~[...~/...~/ ... ~/...~] cases on vx
          ^    ^     ...   ^  if 0<=vx<=k, choose vxth alternative
          0    1     ...   k  if vx is a list of length 1, case 0; else 1
     ~*x  iterator: vx must be of the form
          ("str0" "str1" "str2" "str3" lst . a);
          if lst is initially empty, format "str0" under a+; otherwise,
          bind #\* successively to the elements of lst and then
          recursively format "stri" under a+, where i=1 if there is one
          element left to process, i=2 if there are two left, and i=3
          otherwise.
     ~&x  print elements of vx with ~x, separated by commas and a
          final ``and''
     ~vx  print elements of vx with ~x, separated by commas and a
          final ``or''
     ~nx  if vx is a small positive integer, print it as a word, e.g.,
          seven;
          if vx is a singleton containing a small positive integer, print
            the corresponding ordinal as a word, e.g., seventh
     ~Nx  like ~nx but the word is capitalized, e.g., Seven or Seventh
     ~tx  tab out to column vx; newline first if at or past column vx
     ~cx  vx is (n . w), print integer n right justified in field of
          width w
     ~fx  print object vx flat over as many lines as necessary
     ~Fx  same as ~f, except that subsequent lines are indented to
          start one character to the right of the first character printed
     ~sx  if vx is a symbol, print vx, breaking on hyphens; if vx is a
          string, print the characters in it, breaking on hyphens
     ~    tilde space: print a space
     ~_x  print vx spaces
     ~
          tilde newline: skip following whitespace
     ~%   output a newline
     ~|   output a newline unless already on left margin
     ~~   print a tilde
     ~-   if close to rightmargin, output a hyphen and newline; else
          skip this char

If x is a character, then vx is the value of #\x under the current
alist.  When we say "format str under a+" we mean recursively process
the given string under an alist obtained by appending a to the current
alist.

ACL2's formatting functions print to the indicated channel, keeping
track of which column they are in.  Fmt1 can be used if the caller
knows which column the channel is in (i.e., how many characters have
been printed since the last newline).  Otherwise, fmt or fms must be
used, both of which output a newline so as to establish the column
position at 0.  Unlike Common Lisp's format routine, fmt and its
relatives break the output into lines so as to try to avoid printing
past column 77.  That number is built-into the definitions of ACL2's
formatting functions.  Line breaks are automatically inserted as
necessary in place of spaces and after hyphens in the text being
printed.

The formatting functions scan the string from left to right, printing
each successive character unless it is a tilde (~).  Upon encountering
tildes the formatters take action determined by the character or
characters immediately following the tilde.  The typical
tilde-directive is a group of three successive characters from the
string being printed.  For example, ~x0 is a 3 character
tilde-directive.  The first character in a tilde-directive is always
the tilde character itself.  The next character is called the "command"
character.  The character after that is usually taken as the name of a
"format variable" that is bound in the alist under which the string is
being printed.  Format variables are, by necessity, characters.  The
objects actually printed by a tilde-directive are the objects obtained
by looking up the command's format variables in the alist.  Typical
format variable names are 0, 1, 2, ..., 9, a, b, c, etc., and if a
tilde-directive uses the format variable 0, as in ~x0, then the
character #\0 must be bound in the alist.  Some tilde commands take no
arguments and others take more than one, so some directives are of
length two and others are longer.

It should be noted that this use of characters in the string to denote
arguments is another break from Common Lisp's format routine.  In
Common Lisp, the directives refer implicitly to the "next item to be
printed."  But in ACL2 the directives name each item explicitly with
our format variables.

The following text contains examples that can be evaluated.  To make
this process easier, we use a macro which is defined as part of ACL2
just for this documentation.  The macro is named fmx and it takes up to
eleven arguments, the first of which is a format string, str, and the
others of which are taken as the values of format variables.  The
variables used are #\0 through #\9.  The macro constructs an
appropriate alist, a, and then evaluates (fmt str a *standard-co* state
nil).

Thus,

     (fmx "Here is v0, ~x0, and here is v1, ~x1."
          (cons 'value 0)
          (cons 'value 1))

is just an abbreviation for

     (fmt "Here is v0, ~x0, and here is v1, ~x1."
          (list (cons #\0 (cons 'value 0))
                (cons #\1 (cons 'value 1)))
          *standard-co*
          state
          nil)

which returns (mv 53 state) after printing the line

        Here is v0, (VALUE . 0), and here is v1, (VALUE . 1).

We now devote special attention to three of the tilde-directives whose
use is non-obvious.

_The Case Statement_

~#x is essentially a "case statement" in the language of fmt.  The
proper form of the statement is

     ~#x~[case-0~/case-1~/ ... ~/case-k~],

where each of the case-i is a format string.  In the most common use,
the variable x has an integer value, vx, between 0 and k, inclusive.
The effect of formatting the directive is to format case-vx.

For example

     (fmx "Go ~#0~[North~/East~/South~/West~].~%" 1)

will print "Go East." followed by a newline and will return

(mv 0 state), while if you change the 1 above to 3 (the maximum legal
value), it will print "Go West."

In order to make it easier to print such phrases as "there are seven
cases" requiring agreement between subject and verb based on the number
of elements of a list, the case statement allows its variable to take a
list as its value and selects case-0 if the list has length 1 and
case-1 otherwise.

     (let ((cases '(a b c)))
       (fmx "There ~#0~[is ~n1 case~/are ~n1 cases~]."
            cases
            (length cases)))

will print "There are three cases." but if you change the

'(a b c) above simply to '(a) it will print "There is one case." and if
you change it to nil it will print "There are zero cases."

_Indirection_

Roughly speaking, ~@ will act as though the value of its argument is a
format string and splice it into the current string at the current
position.  It is often used when the phrase to be printed must be
computed.  For example,

     (let ((ev 'DEFUN))
      (fmx "~x0 is an event~@1."
           'foo
           (if (member-eq ev '(defun defstub encapsulate))
               " that may introduce a function symbol"
               "")))

will print "foo is an event that may introduce a function symbol," but
if the value of ev is changed from 'defun to 'defthm, it prints "foo is
an event."  The ~@ directive "splices" in the computed phrase (which
might be empty).  Of course, this particular example could be done with
the case statement

     ~#1~[~/ that may introduce a function symbol~]

where the value of #\1 is appropriately computed to be 0 or 1.

If the argument to ~@ is a pair, it is taken to be a format string
consed onto an alist, i.e., ("str" . a), and the alist, a, is used to
extend the current one before "str" is recursively processed.  This
feature of fmt can be used to pass around "phrases" that contain
computed contextual information in a.  The most typical use is as
"error messages."  For example, suppose you are writing a function
which does not have access to state and so cannot print an error
message.  It may nevertheless be necessary for it to signal an error to
its caller, say by returning two results, the first of which is
interpreted as an error message if non-nil.  Our convention is to use a
~@ pair to represent such messages.  For example, the error value might
be produced by the code:

     (cons
       "Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
       (list (cons #\0 (current-instruction st))
             (cons #\1 (i-stack st))))

If the current-instruction and i-stack (whatever they are) are '(popi
3) and '(a b) when the cons above is evaluated, then it produces

     '("Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
       (#\0 POPI 3)
       (#\1 A B))

and if this pair is made the value of the fmt variable 0, then ~@0 will
print

        Error:  The instruction (POPI 3) is illegal when the stack is (A B).

For example, evaluate

     (let
      ((pair
       '("Error:  The instruction ~x0 is illegal when the stack is ~x1.~%"
         (#\0 POPI 3)
         (#\1 A B))))
      (fmx "~@0" pair)).

Thus, even though the function that produced the "error" could not
print it, it could specify exactly what error message and data are to
be printed.

This example raises another issue.  Sometimes it is desirable to break
lines in your format strings so as to make your source code more
attractive.  That is the purpose of the tilde-newline directive.  The
following code produces exactly the same output as described above.

     (let ((pair '("Error:  The instruction ~x0 ~
                   is illegal when the stack is ~
                   ~x1.~%"
                   (#\0 POPI 3)
                   (#\1 A B))))
      (fmx "~@0" pair)).

Finally, observe that when ~@0 extends the current alist, alist, with
the one, a, in its argument, the bindings from a are added to the front
of alist, overriding the current values of any shared variables.  This
ensures that the variable values seen by the recursively processed
string, "str", are those from a, but if "str" uses variables not bound
in a, their values are as specified in the original alist.
Intuitively, variables bound in a are local to the processing of ("str"
. a) but "str" may use "global variables."  The example above
illustrates this because when the ~@0 is processed, #\0 is bound to the
error message pair.  But when the ~x0 in the error string is processed,
#\0 is bound to the illegal instruction.

_Iteration_

The ~* directive is used to process each element of a list.  For
example,

     (let ((lst '(a b c d e f g h))) ; a true-list whose elements we exhibit
      (fmx "~*0"
           `("Whoa!"          ; what to print if there's nothing to print
             "~x*!"           ; how to print the last element
             "~x* and "       ; how to print the 2nd to last element
             "~x*, "          ; how to print all other elements
             ,lst)))          ; the list of elements to print

will print "A, B, C, D, E, F, G and H!".  Try this example with other
true list values of lst, such as '(a b), '(a), and nil.  The
tilde-directives ~&0 and ~v0, which take a true list argument and
display its elements separated by commas and a final "and" or "or," are
implemented in terms of the more general ~*.

The ~* directive allows the 5-tuple to specify in its final cdr an
alist with which to extend the current one before processing the
individual elements.

We often use ~* to print a series of phrases, separated by suitable
punctuation, whitespace and noise words.  In such use, the ~* handles
the separation of the phrases and each phrase is generally printed by
~@.

Here is a complex example.  In the let*, below, we bind phrases to a
list of ~@ pairs and then we create a ~* 5-tuple to print out the
conjunction of the phrases with a parenthetical "finally!" if the
series is longer than 3.

     (let* ((phrases
             (list (list "simplifying with the replacement rules ~&0"
                         (cons #\0 '(rewrite-rule1
                                     rewrite-rule2
                                     rewrite-rule3)))
                   (list "destructor elimination using ~x0"
                         (cons #\0 'elim-rule))
                   (list "generalizing the terms ~&0"
                         (cons #\0 '((rev x) (app u v))))
                   (list "inducting on ~x0"
                         (cons #\0 'I))))
            (5-tuple
             (list
              "magic"                            ; no phrases
              "~@*"                              ; last phrase
              "~@*, and~#f~[~/ (finally!)~] "    ; second to last phrase
              "~@*, "                            ; other phrases
              phrases                            ; the phrases themselves
              (cons #\f
                    (if (>(length phrases) 3) 1 0))))) ;print ``finally''?
       (fmx "We did it by ~*0." 5-tuple))

This let* prints

        We did it by simplifying with the replacement rules REWRITE-RULE1,
        REWRITE-RULE2 and REWRITE-RULE3, destructor elimination using ELIM-
        RULE, generalizing the terms (REV X) and (APP U V), and (finally!)
        inducting on I.

You might wish to try evaluating the let* after removing elements of
phrases.

Most of the output produced by ACL2 is produced via fmt statements.
Thus, inspection of the source code will yield many examples.  A
complicated example is the code that explains the simplifier's work.
See :pc simplify-clause-msg1.  An ad hoc example is provided by the
function fmt-doc-example, which takes two arguments: an arbitrary true
list and state.  To see how fmt-doc-example works, :pe fmt-doc-example.

     (fmt-doc-example '(a b c d e f g h i j k l m n o p) state)

will produce the output

        Here is a true list:  (A B C D E F G H I J K L M N O P).  It has 16
        elements, the third of which is C.

        We could print each element in square brackets:
        ([A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N],
        [almost there: O], [the end: P]).  And if we wished to itemize them
        into column 15 we could do it like this
        0123456789012345
            0 (zeroth) A
            1 (first)  B
            2 (second) C
            3 (third)  D
            4 (fourth) E
            5 (fifth)  F
            6 (sixth)  G
            7 (seventh)
                       H
            8 (eighth) I
            9 (ninth)  J
           10 (tenth)  K
           11 (eleventh)
                       L
           12 (twelfth)
                       M
           13 (thirteenth)
                       N
           14 (14th)   O
           15 (15th)   P
        End of example.

and return (mv 15 state).

Finally, we should remind the reader that fmt and its subfunctions,
most importantly fmt0, are written entirely in ACL2.  We make this
comment for two reasons.  First, it illustrates the fact that quite low
level code can be efficiently written in the language.  Second, it
means that as a last resort for documentation purposes you can read the
source code without changing languages.

FMT!    :(str alist co-channel state evisc) => state

This function is nearly identical to fmt; see FMT.  The only
difference is that fmt may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fmt! instead if you want to be able to read
the forms back in.

FMT-TO-COMMENT-WINDOW    print to the comment window

See CW for an introduction to the comment window and the usual
way to print it.

Function fmt-to-comment-window is identical to fmt1 (see FMT),
except that the channel is in essence *standard-co* and the ACL2 state
is neither an input nor an output.  An analogous function,
fmt-to-comment-window!, prints with fmt! instead of fmt, in order to
avoid insertion of backslash (\) characters for margins; also see
CW!.

     General Form:
     (fmt-to-comment-window fmt-string alist col evisc-tuple)

where these arguments are as desribed for fmt1; see FMT.

FMT1    :(str alist col co-channel state evisc) => (mv col state)

See FMT for further explanation, including documentation of the
tilde-directives.

FMT1!    :(str alist col channel state evisc) => (mv col state)

This function is nearly identical to fmt1; see FMT1.  The only
difference is that fmt1 may insert backslash (\) characters when forced
to print past the right margin in order to make the output a bit
clearer in that case.  Use fmt1! instead if you want to be able to read
the forms back in.

FOURTH    fourth member of the list

See any Common Lisp documentation for details.

GETENV$    read an environment variable

(Getenv$ str state), where str is a string, reads the value of
environment variable str, returning nil if none is found or if the read
fails.  The formal story is that getenv$ reads its value from the
oracle field of the ACL2 state.  The return value is thus a triple of
the form (mv erp val state), where erp will always be nil in practice,
val is the value that has been read, and state is the new state, which
is obtained by popping val from the top of the state's oracle.

     Example:
     (getenv$ "PWD") ==> (mv nil "/u/joe/work" state)

Also see SETENV$.

HARD-ERROR    print an error message and stop execution

(Hard-error ctx str alist) causes evaluation to halt with a short
message using the "context" ctx.  An error message is first printed
using the string str and alist alist that are of the same kind as
expected by fmt.  See FMT.  Also see ER for a macro
that provides a unified way of signaling errors.

Hard-error has a guard of t.  Also see ILLEGAL for a similar
capability which however has a guard of nil that supports static
checking using guard verification, rather than using dynamic (run-time)
checking.   This distinction is illustrated elsewhere: see
PROG2$ for examples.

Semantically, hard-error ignores its arguments and always returns nil.
But if a call (hard-error ctx str alist) is encountered during
evaluation, then the string str is printed using the association list
alist (as in fmt), after which evaluation halts immediately.  Here is a
trivial, contrived example.

     ACL2 !>(cons 3 (hard-error 'my-context
                                 "Printing 4: ~n0"
                                 (list (cons #\0 4))))

     HARD ACL2 ERROR in MY-CONTEXT:  Printing 4: four

     ACL2 Error in TOP-LEVEL:  Evaluation aborted.

     ACL2 !>

IDENTITY    the identity function

(Identity x) equals x; what else can we say?

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

IF    if-then-else function

(if x y z) is equal to y if x is any value other than nil, and is equal
to z if x is nil.

Only one of y, z is evaluated when (if x y z) is evaluated.

If has a guard of t.

If is part of Common Lisp.  See any Common Lisp documentation for more
information.

IFF    logical ``if and only if''

Iff is the ACL2 biconditional, "if and only if".  (iff P Q) means that
either P and Q are both false (i.e., nil) or both true (i.e., not nil).

IFIX    coerce to an integer

Ifix simply returns any integer argument unchanged, returning 0 on a
non-integer argument.  Also see NFIX, see RFIX, see
REALFIX and see FIX for analogous functions that coerce
to a natural number, a rational number, a real, and a number,
respectively.

Ifix has a guard of t.

ILLEGAL    print an error message and stop execution

(Illegal ctx str alist) causes evaluation to halt with a short message
using the "context" ctx.  An error message is first printed using the
string str and alist alist that are of the same kind as expected by
fmt.  See FMT, and see PROG2$ for an example of how to
use a related function, hard-error (see HARD-ERROR).  Also see
ER for a macro that provides a unified way of signaling errors.

The difference between illegal and hard-error is that the former has a
guard of nil while the latter has a guard of t.  Thus, you may want to
use illegal rather than hard-error when you intend to do guard
verification at some point, and you expect the guard to guarantee that
the illegal call is never executed.  See PROG2$ for an example.

IMAGPART    imaginary part of a complex number

Completion Axiom:

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

Guard for (imagpart x):

     (acl2-numberp x)

IMPLIES    logical implication

Implies is the ACL2 implication function.  (implies P Q) means that
either P is false (i.e., nil) or Q is true (i.e., not nil).

IMPROPER-CONSP    recognizer for improper (non-null-terminated) non-empty lists

Improper-consp is the function that checks whether its argument is a
non-empty list that ends in other than nil.  See PROPER-CONSP
and also see TRUE-LISTP.

INT=    test equality of two integers

(int= x y) is logically equivalent to (equal x y).

Unlike equal, int= requires its arguments to be numbers (or else causes
a guard violation; see GUARD).  Generally, int= is executed
more efficiently than equal or = on integers.

INTEGER-LENGTH    number of bits in two's complement integer representation

For non-negative integers, (integer-length i) is the minimum number of
bits needed to represent the integer.  Any integer can be represented
as a signed two's complement field with a minimum of (+ (integer-length
i) 1) bits.

The guard for integer-length requires its argument to be an integer.
Integer-length is defined in Common Lisp.  See any Common Lisp
documentation for more information.

INTEGER-LISTP    recognizer for a true list of integers

The predicate integer-listp tests whether its argument is a true list
of integers.

INTEGERP    recognizer for whole numbers

(integerp x) is true if and only if x is an integer.

INTERN    create a new symbol in a given package

(intern symbol-name symbol-package-name) returns a symbol with the
given symbol-name and the given symbol-package-name.  We restrict
Common Lisp's intern so that the second argument is either the symbol
*main-lisp-package-name*, the value of that constant, or is one of
"ACL2", "ACL2-INPUT-CHANNEL", "ACL2-OUTPUT-CHANNEL", or "KEYWORD".  To
avoid that restriction, see INTERN$.

In ACL2 intern is actually implemented as a macro that expands to a
call of a similar function whose second argument is a symbol.  Invoke
:pe intern to see the definition, or see
INTERN-IN-PACKAGE-OF-SYMBOL.

To see why is intern so restricted consider (intern "X" "P").  In
particular, is it a symbol and if so, what is its symbol-package-name?
One is tempted to say "yes, it is a symbol in the package "P"."  But if
package "P" has not yet been defined, that would be premature because
the imports to the package are unknown.  For example, if "P" were
introduced with

     (defpkg "P" '(LISP::X))

then in Common Lisp (symbol-package-name (intern "X" "P")) returns
"LISP".

The obvious restriction on intern is that its second argument be the
name of a package known to ACL2.  We cannot express such a restriction
(except, for example, by limiting it to those packages known at some
fixed time, as we do).  Instead, we provide intern-in-package-of-symbol
which requires a "witness symbol" for the package instead of the
package.  The witness symbol is any symbol (expressible in ACL2) and
uniquely specifies a package necessarily known to ACL2.

INTERN$    create a new symbol in a given package

Intern$ is a macro that behaves the same as the macro intern, except
for weakening the restriction to a fixed set of package names so that
any package name other than "" is legal.  See INTERN.  Note
that if you evaluate a call (intern$ x y) for which there is no package
with name y that is known to ACL2, you will get an error.

(Intern$ x y) expands to:

     (intern-in-package-of-symbol x (pkg-witness y))

See INTERN-IN-PACKAGE-OF-SYMBOL and see PKG-WITNESS.

INTERN-IN-PACKAGE-OF-SYMBOL    create a symbol with a given name

Completion Axiom:

     (equal (intern-in-package-of-symbol x y)
            (if (and (stringp x)
                     (symbolp y))
                (intern-in-package-of-symbol x y)
              nil))

Guard for (intern-in-package-of-symbol x y):

     (and (stringp x) (symbolp y))

Intuitively, (intern-in-package-of-symbol x y) creates a symbol with
symbol-name x interned in the package containing y.  More precisely,
suppose x is a string, y is a symbol with symbol-package-name pkg and
that the defpkg event creating pkg had the list of symbols imports as
the value of its second argument.  Then (intern-in-package-of-symbol x
y) returns a symbol, ans, the symbol-name of ans is x, and the
symbol-package-name of ans is pkg, unless x is the symbol-name of some
member of imports with symbol-package-name ipkg, in which case the
symbol-package-name of ans is ipkg.  Because defpkg requires that there
be no duplications among the symbol-names of the imports,
intern-in-package-of-symbol is uniquely defined.

For example, suppose "MY-PKG" was created by

     (defpkg "MY-PKG" '(ACL2::ABC LISP::CAR)).

Let w be 'my-pkg::witness.  Observe that

     (symbolp w) is t                     ; w is a symbol
     (symbol-name w) is "WITNESS"         ; w's name is "WITNESS"
     (symbol-package-name w) is "MY-PKG"  ; w is in the package "MY-PKG"

The construction of w illustrates one way to obtain a symbol in a given
package:  write it down as a constant using the double-colon notation.

But another way to obtain a symbol in a given package is to create it
with intern-in-package-of-symbol.

     (intern-in-package-of-symbol "XYZ" w) is MY-PKG::XYZ

     (intern-in-package-of-symbol "ABC" w) is ACL2::ABC

     (intern-in-package-of-symbol "CAR" w) is LISP::CAR

     (intern-in-package-of-symbol "car" w) is MY-PKG::|car|

INTERSECTP-EQ    test whether two lists of symbols intersect

See INTERSECTP-EQUAL, which is logically the same function.

(Intersectp-eq x y) has a guard that x and y are lists of symbols.

INTERSECTP-EQUAL    test whether two lists intersect

(Intersectp-equal x y) returns t if x and y have a member in common,
else it returns nil.  Also see INTERSECTP-EQ, which is
logically the same but can be more efficient since it uses eq instead
of equal to look for members common to the two given lists.

(Intersectp-equal x y) has a guard that x and y are true lists.

IO    input/output facilities in ACL2

     Example:
     (mv-let
       (channel state)
       (open-input-channel "foo.lisp" :object state)
       (mv-let (eofp obj state)
               (read-object channel state)
               (.
                 .
                  (let ((state (close-input-channel channel state)))
                        (mv final-ans state))..)))

Also see FILE-READING-EXAMPLE.

ACL2 supports input and output facilities equivalent to a subset of
those found in Common Lisp.  ACL2 does not support random access files
or bidirectional streams.  In Common Lisp, input and output are to or
from objects of type stream.  In ACL2, input and output are to or from
objects called "channels," which are actually symbols.  Although a
channel is a symbol, one may think of it intuitively as corresponding
to a Common Lisp stream.  Channels are in one of two ACL2 packages,
"ACL2-INPUT-CHANNEL" and "ACL2-OUTPUT-CHANNEL".  When one "opens" a
file one gets back a channel whose symbol-name is the file name passed
to "open," postfixed with -n, where n is a counter that is incremented
every time an open or close occurs.

There are three channels which are open from the beginning and which
cannot be closed:

       acl2-input-channel::standard-character-input-0
       acl2-input-channel::standard-object-input-0
       acl2-input-channel::standard-character-output-0

All three of these are really Common Lisp's *standard-input* or
*standard-output*, appropriately.

For convenience, three global variables are bound to these rather
tedious channel names:

       *standard-ci*
       *standard-oi*
       *standard-co*

Common Lisp permits one to open a stream for several different kinds of
io, e.g. character or byte.  ACL2 permits an additional type called
"object".  In ACL2 an "io-type" is a keyword, either :character, :byte,
or :object.  When one opens a file, one specifies a type, which
determines the kind of io operations that can be done on the channel
returned.  The types :character and :byte are familiar.  Type :object
is an abstraction not found in Common Lisp.  An :object file is a file
of Lisp objects.  One uses read-object to read from :object files and
print-object$ to print to :object files.  (The reading and printing are
really done with the Common Lisp read and print functions.)

File-names are strings.  ACL2 does not support the Common Lisp type
pathname.

Here are the names, formals and output descriptions of the ACL2 io
functions.

     Input Functions:
       (open-input-channel (file-name io-type state) (mv channel state))
       (open-input-channel-p (channel io-type state) boolean)
       (close-input-channel (channel state) state)
       (read-char$ (channel state) (mv char/nil state)) ; nil for EOF
       (peek-char$ (channel state) boolean)
       (read-byte$ (channel state) (mv byte/nil state)) ; nil for EOF
       (read-object (channel state) (mv eof-read-flg obj-read state))

     Output Functions:
       (open-output-channel  (file-name io-type state) (mv channel state))
       (open-output-channel! (file-name io-type state) (mv channel state))
       (open-output-channel-p (channel io-type state) boolean)
       (close-output-channel (channel state) state)
       (princ$ (obj channel state) state)
       (write-byte$ (byte channel state) state)
       (print-object$ (obj channel state) state)
       (fms  (string alist channel state evisc-tuple) state)
       (fms! (string alist channel state evisc-tuple) state)
       (fmt  (string alist channel state evisc-tuple) (mv col state))
       (fmt! (string alist channel state evisc-tuple) (mv col state))
       (fmt1 (string alist col channel state evisc-tuple) (mv col state))
       (fmt1! (string alist col channel state evisc-tuple) (mv col state))
       (cw (string arg0 arg1 ... argn) nil)

The "formatting" functions are particularly useful; see FMT and
see CW.  In particular, cw prints to a "comment window" and
does not involve the ACL2 state, so many may find it easier to use than
fmt and its variants.  The functions fms!, fmt!, and fmt1! are the same
as their respective functions without the "!," except that the "!"
functions are guaranteed to print forms that can be read back in (at a
slight readability cost).

When one enters ACL2 with (lp), input and output are taken from
*standard-oi* to *standard-co*.  Because these are synonyms for
*standard-input* and *standard-output*, one can drive ACL2 io off of
arbitrary Common Lisp streams, bound to *standard-input* and
*standard-output* before entry to ACL2.

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  See
SET-ACL2-PRINT-CASE for how to get ACL2 to print symbols in lower
case.

By default, numbers are printed in radix 10 (base 10).See
SET-ACL2-PRINT-BASE for how to get ACL2 to print numbers in radix 2,
8, or 16.

Comment for advanced users: Function open-output-channel! is identical
as a function to open-output-channel, except that the former may be
called even during make-event expansion and clause-processor hints, but
requires that there is an active trust tag (see DEFTTAG).

Finally, we note that the distributed book books/misc/file-io.lisp
contains useful file io functions whose definitions illustrate some of
the features described above.

OPEN-OUTPUT-CHANNEL!    when trust tags are needed to open output channels

The book below illustrates the soundness loophole plugged in ACL2
Version_3.2 related to file writes during book certification.

     ; The following example is adapted (with only very slight changes)
     ; from one written by Peter Dillinger.  It illustrates the prohibition
     ; against writing files enforced by with-output-channel during book
     ; certification (more specifically, during make-event expansion).

     ; This book certifies in ACL2 Version_3.1 before the fix discussed in the
     ; paragraph on with-writes-okp in :DOC NOTE-3-2.  The fix was actually made
     ; to ACL2 function open-output-channel.

     ; After the fix, in order for certification to succeed one needs to do
     ; two things.  First, in raw lisp:
     ;   (push :after-writes-okp-fix *features*)
     ; Second, certify with this command:
     ;   (certify-book "writes-okp" 0 nil :ttags (:writes-okp))

     (in-package "ACL2")

     (local
      (defun write-objects-to-channel (obj-lst chan state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (true-listp obj-lst)))
        (if (consp obj-lst)
            (pprogn (print-object$ (car obj-lst) chan state)
                    (write-objects-to-channel (cdr obj-lst) chan state)
                    state)
          state)))

     #+after-writes-okp-fix
     (defttag :writes-okp)

     (local
      (defun write-objects-to-file (obj-lst filename state)
        (declare (xargs :mode :program
                        :stobjs state
                        :guard (and (stringp filename)
                                    (true-listp obj-lst))))
        (mv-let (chan state)
                #-after-writes-okp-fix
                (open-output-channel filename :object state)
                #+after-writes-okp-fix
                (open-output-channel! filename :object state)
                (if chan
                    (pprogn (write-objects-to-channel obj-lst chan state)
                            (close-output-channel chan state)
                            (value :done))
                  (er soft 'write-object-to-file
                      "Could not open for writing: ~x0"
                      filename)))))

     (local
      (defconst *nil.lisp*
        '((in-package "ACL2")
          (defthm bad nil :rule-classes nil))))

     (local
      (defconst *nil.cert*
        '((IN-PACKAGE "ACL2")
          "ACL2 Version 3.1"
          :BEGIN-PORTCULLIS-CMDS
          :END-PORTCULLIS-CMDS
          NIL
          (("/home/peterd/test/nil.lisp" "nil" "nil"
            ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 134094174))
          62589544
          )))

     (local
      (make-event (er-progn
                   (write-objects-to-file *nil.lisp* "nil.lisp" state)
                   (write-objects-to-file *nil.cert* "nil.cert" state)
                   (value '(value-triple :invisible)))))

     (local (include-book
             "nil" :load-compiled-file nil))

     (defthm bad nil :rule-classes nil)

PRINC$    print a string

Use princ$ to print a string, without the surrounding double-quotes.
Princ$ returns state.

     Examples:
     ACL2 !>(princ$ "Howdy ho" (standard-co state) state)
     Howdy ho<state>
     ACL2 !>(pprogn (princ$ "Howdy ho" (standard-co state) state)
                    (newline (standard-co state) state))
     Howdy ho
     <state>
     ACL2 !>

See FMT for more sophisticated printing routines, and see
IO for general information about input and output.

SET-ACL2-PRINT-BASE    control radix in which number are printed

By default, integers and ratios are printed in base 10.  ACL2 also
supports printing in radix 2, 8, or 16 by calling set-acl2-print-base
with the desired radix (base).

       :set-acl2-print-base 10   ; Default printing
       (set-acl2-print-base 10)  ; Same as above
       :set-acl2-print-base 16   ; Print integers and ratios in hex, e.g., #x3A
       (set-acl2-print-base 16)  ; Same as above

Note: ACL2 events and some other top-level commands (for example, thm,
verify, and history commands such as :pe and :pbt) set the print base
to 10 during their evaluation.  So set-acl2-print-base has no effect
while these forms are being processed.

SET-ACL2-PRINT-CASE    control whether symbols are printed in upper case or in lower case

By default, symbols are printed in upper case when vertical bars are
not required, as specified by Common Lisp.  As with Common Lisp, ACL2
supports printing in a "downcase" mode, where symbols are printed in
lower case.  Many printing functions (some details below) print
characters in lower case for a symbol when the ACL2 state global
variable print-case has value :downcase and vertical bars are not
necessary for printing that symbol.  (Thus, this state global functions
in complete analogy to the Common Lisp global *print-case*.)  The value
print-case is returned by (acl2-print-case), and may be set using the
macro set-acl2-print-case (which returns state), as follows.

       :set-acl2-print-case :upcase    ; Default printing
       (set-acl2-print-case :upcase)   ; Same as above
       :set-acl2-print-case :downcase  ; Print symbols in lower case when
                                       ;   vertical bars are not required
       (set-acl2-print-case :downcase) ; Same as above

The ACL2 user can expect that the :downcase setting will have an effect
for formatted output (see FMT and see FMS) when the
directives are ~p, ~P, ~q, or ~Q, for built-in functions princ$ and
prin1$, and the ppr family of functions, and _not_ for built-in
function print-object$.  For other printing functions, the effect of
:downcase is unspecified.

IRRELEVANT-FORMALS    formals that are used but only insignificantly

Let fn be a function of n arguments.  Let x be the ith formal of fn.
We say x is "irrelevant in fn" if x is not involved in either the guard
or the measure for fn, x is used in the body, but the value of (fn
a1...ai...an) is independent of ai.

The easiest way to define a function with an irrelevant formal is
simply not to use the formal in the body of the function.  Such formals
are said to be "ignored" by Common Lisp and a special declaration is
provided to allow ignored formals.  ACL2 makes a distinction between
ignored and irrelevant formals.  Note however that if a variable is
declared ignored or ignorable, then it will not be reported as
irrelevant.

An example of an irrelevant formal is x in the definition of fact below.

     (defun fact (i x)
       (declare (xargs :guard (and (integerp i) (<= 0 i))))
       (if (zerop i) 0 (* i (fact (1- i) (cons i x))))).

Observe that x is only used in recursive calls of fact; it never "gets
out" into the result.  ACL2 can detect some irrelevant formals by a
closure analysis on how the formals are used.  For example, if the ith
formal is only used in the ith argument position of recursive calls,
then it is irrelevant.  This is how x is used above.

It is possible for a formal to appear only in recursive calls but still
be relevant.  For example, x is *not* irrelevant below, even though it
only appears in the recursive call.

     (defun fn (i x) (if (zerop i) 0 (fn x (1- i))))

The key observation above is that while x only appears in a recursive
call, it appears in an argument position, namely i's, that is relevant.
(The function above can be admitted with a :guard requiring both
arguments to be nonnegative integers and the :measure (+ i x).)

Establishing that a formal is irrelevant, in the sense defined above,
can be an arbitrarily hard problem because it requires theorem proving.
For example, is x irrelevant below?

     (defun test (i j k x) (if (p i j k) x 0))

Note that the value of (test i j k x) is independent of x -- thus
making x irrelevant -- precisely if (p i j k) is a theorem.  ACL2's
syntactic analysis of a definition does not guarantee to notice all
irrelevant formals.

We regard the presence of irrelevant formals as an indication that
something is wrong with the definition.  We cause an error on such
definitions and suggest that you recode the definition so as to
eliminate the irrelevant formals.  If you must have an irrelevant
formal, one way to "trick" ACL2 into accepting the definition, without
slowing down the execution of your function, is to use the formal in an
irrelevant way in the guard.  For example, to admit fact, above, with
its irrelevant x one might use

     (defun fact (i x)
       (declare (xargs :guard (and (integerp i) (<= 0 i) (equal x x))))
       (if (zerop i) 0 (* i (fact (1- i) (cons i x)))))

For those who really want to turn off this feature, we have provided a
way to use the acl2-defaults-table for this purpose; see
SET-IRRELEVANT-FORMALS-OK.

If you need to introduce a function with an irrelevant formal, please
explain to the authors why this should be allowed.

KEYWORD-VALUE-LISTP    recognizer for true lists whose even-position elements are keywords

(keyword-value-listp l) is true if and only if l is a list of even
length of the form (k1 a1 k2 a2 ... kn an), where each ki is a keyword.

KEYWORDP    recognizer for keywords

(Keywordp x) is true if and only if x is a keyword, i.e., a symbol in
the "KEYWORD" package.  Such symbols are typically printed using a
colon (:) followed by the symbol-name of the symbol.

Keywordp has a guard of t.

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

KWOTE    quote an arbitrary object

For any object x, (kwote x) returns the two-element list whose elements
are the symbol quote and the given x, respectively.  The guard of
(kwote x) is t.

KWOTE-LST    quote an arbitrary true list of objects

The function kwote-lst applies the function kwote to each element of a
given list.  The guard of (kwote-lst lst) is (true-listp lst).

LAST    the last cons (not element) of a list

(Last l) is the last cons of a list.  Here are examples.

     ACL2 !>(last '(a b . c))
     (B . C)
     ACL2 !>(last '(a b c))
     (C)

(Last l) has a guard of (listp l); thus, l need not be a true-listp.

Last is a Common Lisp function.  See any Common Lisp documentation for
more information.  Unlike Common Lisp, we do not allow an optional
second argument for last.

LEN    length of a list

Len returns the length of a list.

A Common Lisp function that is appropriate for both strings and proper
lists is length; see LENGTH.  The guard for len is t.

(Low-level implementation note.  ACL2 provides a highly-optimized
implementation of len, which is tail-recursive and fixnum-aware, that
differs from its simple ACL2 definition.)

LENGTH    length of a string or proper list

Length is the function for determining the length of a sequence.  In
ACL2, the argument is required to be either a true-listp or a string.

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