FMT-TO-COMMENT-WINDOW

print to the comment window
Major Section:  PROGRAMMING

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.

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)
Major Section:  PROGRAMMING

See fmt for further explanation.

The tilde-directives are
~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














































































FOURTH

fourth member of the list
Major Section:  PROGRAMMING

See any Common Lisp documentation for details.















































































HARD-ERROR

print an error message and stop execution
Major Section:  PROGRAMMING

(Hard-error ctx str alist) causes evaluation to halt with a short message using the ``context'' ctx. An error message is printed using the string str and alist alist that are of the same kind as expected by fmt. See fmt.

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
Major Section:  PROGRAMMING

(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
Major Section:  PROGRAMMING

(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''
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

(Illegal ctx str alist) causes evaluation to halt with a short message using the ``context'' ctx. An error message is 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).

The difference between illegal and hard-error is that the former has a guard of nil while the latter has a guard ot 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
Major Section:  PROGRAMMING

Completion Axiom:

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

Guard for (imagpart x):

(acl2-numberp x)














































































IMPLIES

logical implication
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

(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
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

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















































































INTEGERP

recognizer for whole numbers
Major Section:  PROGRAMMING

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















































































INTERN

create a new symbol in a given package
Major Section:  PROGRAMMING

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

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-IN-PACKAGE-OF-SYMBOL

create a symbol with a given name
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

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
Major Section:  PROGRAMMING

(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
Major Section:  PROGRAMMING

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))
  (peek-char$ (channel state) boolean)
  (read-byte$ (channel state) (mv byte/nil state))
  (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-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) (fmt (string alist 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.

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. 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
Major Section:  PROGRAMMING

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.

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
Major Section:  PROGRAMMING

(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
Major Section:  PROGRAMMING

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













































































LAST

the last cons (not element) of a list
Major Section:  PROGRAMMING

(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
Major Section:  PROGRAMMING

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.













































































LENGTH

length of a string or proper list
Major Section:  PROGRAMMING

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.













































































LET

binding of lexically scoped (local) variables
Major Section:  PROGRAMMING

Example LET Form:
(let ((x (* x x))
      (y (* 2 x)))
 (list x y))
If the form above is executed in an environment in which x has the value -2, then the result is '(4 -4).

Let expressions bind variables so that their ``local'' values, the values they have when the ``body'' of the let is evaluated, are possibly different than their ``global'' values, the values they have in the context in which the let expression appears. In the let expression above, the local variables bound by the let are x and y. They are locally bound to the values delivered by the two forms (* x x) and (* 2 x), respectively, that appear in the ``bindings'' of the let. The body of the let is (list x y).

Suppose that the let expression above occurs in a context in which x has the value -2. (The global value of y is irrelevant to this example.) For example, one might imagine that the let form above occurs as the body of some function, fn, with the formal parameter x and we are evaluating (fn -2).

To evaluate the let above in a context in which x is -2, we first evaluate the two forms specifying the local values of the variables. Thus, (* x x) is evaluated and produces 4 (because x is -2) and (* 2 x) is evaluated and produces -4 (because x is -2). Then x and y are bound to these values and the body of the let is evaluated. Thus, when the body, (list x y) is evaluated, x is 4 and y is -4. Thus, the body produces '(4 -4).

Note that the binding of y, which is written after the binding of x and which mentions x, nevertheless uses the global value of x, not the new local value. That is, the local variables of the let are bound ``in parallel'' rather than ``sequentially.'' In contrast, if the

Example LET* Form:
(let* ((x (* x x))
       (y (* 2 x)))
 (list x y))
is evaluated when the global value of x is -2, then the result is '(4 8), because the local value of y is computed after x has been bound to 4. Let* binds its local variables ``sequentially.''
General LET Forms:
(let ((var1 term1) ... (varn termn)) body) 
and
(let ((var1 term1) ... (varn termn))
 (declare ...) ... (declare ...)
 body)
where the vari are distinct variables, the termi are terms involving only variables bound in the environment containing the let, and body is a term involving only the vari plus the variables bound in the environment containing the let. Each vari must be used in body or else declared ignored.

A let form is evaluated by first evaluating each of the termi, obtaining for each a vali. Then, each vari is bound to the corresponding vali and body is evaluated.

Actually, let forms are just abbreviations for certain uses of lambda notation. In particular

(let ((var1 term1) ... (varn termn)) (declare ...) body)
is equivalent to
((lambda (var1 ... varn)
   (declare ...)
   body)
 term1 ... termn).
Let* forms are used when it is desired to bind the vari sequentially, i.e., when the local values of preceding varj are to be used in the computation of the local value for vari.
General LET* Forms:
(let* ((var1 term1) ... (varn termn)) body) 
where the vari are variables (not necessarily distinct), the termi are terms involving only variables bound in the environment containing the let* and those varj such that j<i, and body is a term involving only the vari plus the variables bound in the environment containing the let*. Each vari must be used in either some subsequent termj or in body. Note that let* does not permit the inclusion of declare forms.

The above let* is equivalent to

(let ((var1 term1))
 ...
 (let ((varn termn)) body)...)
Thus, the termi are evaluated successively and after each evaluation the corresponding vali is bound to the value of termi.

Each (vari termi) pair in a let or let* form is called a ``binding'' of vari and the vari are called the ``local variables'' of the let or let*. The common use of let and let* is to save the values of certain expressions (the termi) so that they may be referenced several times in the body without suggesting their recomputation.

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













































































LET*

binding of lexically scoped (local) variables
Major Section:  PROGRAMMING

Example LET* Form:
(let* ((x (* x x))
       (y (* 2 x)))
 (list x y))
If the form above is executed in an environment in which x has the value -2, then the result is '(4 8). See let for a discussion of both let and let*, or read on for a briefer discussion.

The difference between let and let* is that the former binds its local variables in parallel while the latter binds them sequentially. Thus, in let*, the term evaluated to produce the local value of one of the locally bound variables is permitted to reference any locally bound variable occurring earlier in the binding list and the value so obtained is the newly computed local value of that variable. See let.

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













































































LIST

build a list
Major Section:  PROGRAMMING

List is the macro for building a list of objects. For example, (list 5 6 7) returns a list of length 3 whose elements are 5, 6, and 7 respectively. Also see list*.

List is defined in Common Lisp. See any Common Lisp documentation for more information.













































































LIST*

build a list
Major Section:  PROGRAMMING

List* is the Common Lisp macro for building a list of objects from given elements and a tail. For example, (list* 5 6 '(7 8 9)) equals the list '(5 6 7 8 9). Also see list.

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













































































LISTP

recognizer for (not necessarily proper) lists
Major Section:  PROGRAMMING

(listp x) is true when x is either a cons pair or is nil.

Listp has no guard, i.e., its guard is t.

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